[GOAL]
⊢ I * I = ↑(-1)
[PROOFSTEP]
simp
[GOAL]
x y : ℤ
⊢ ↑toComplex { re := x, im := y } = ↑x + ↑y * I
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x : ℤ[i]
⊢ ↑toComplex x = { re := ↑x.re, im := ↑x.im }
[PROOFSTEP]
apply Complex.ext
[GOAL]
case a
x : ℤ[i]
⊢ (↑toComplex x).re = { re := ↑x.re, im := ↑x.im }.re
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
case a
x : ℤ[i]
⊢ (↑toComplex x).im = { re := ↑x.re, im := ↑x.im }.im
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x : ℤ[i]
⊢ ↑x.re = (↑toComplex x).re
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x : ℤ[i]
⊢ ↑x.im = (↑toComplex x).im
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x y : ℤ
⊢ (↑toComplex { re := x, im := y }).re = ↑x
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x y : ℤ
⊢ (↑toComplex { re := x, im := y }).im = ↑y
[PROOFSTEP]
simp [toComplex_def]
[GOAL]
x : ℤ[i]
⊢ ↑toComplex (star x) = ↑(starRingEnd ((fun x => ℂ) x)) (↑toComplex x)
[PROOFSTEP]
rw [toComplex_def₂, toComplex_def₂]
[GOAL]
x : ℤ[i]
⊢ { re := ↑(star x).re, im := ↑(star x).im } = ↑(starRingEnd ((fun x => ℂ) x)) { re := ↑x.re, im := ↑x.im }
[PROOFSTEP]
exact congr_arg₂ _ rfl (Int.cast_neg _)
[GOAL]
x y : ℤ[i]
⊢ ↑toComplex x = ↑toComplex y ↔ x = y
[PROOFSTEP]
cases x
[GOAL]
case mk
y : ℤ[i]
re✝ im✝ : ℤ
⊢ ↑toComplex { re := re✝, im := im✝ } = ↑toComplex y ↔ { re := re✝, im := im✝ } = y
[PROOFSTEP]
cases y
[GOAL]
case mk.mk
re✝¹ im✝¹ re✝ im✝ : ℤ
⊢ ↑toComplex { re := re✝¹, im := im✝¹ } = ↑toComplex { re := re✝, im := im✝ } ↔
    { re := re✝¹, im := im✝¹ } = { re := re✝, im := im✝ }
[PROOFSTEP]
simp [toComplex_def₂]
[GOAL]
x : ℤ[i]
⊢ ↑toComplex x = 0 ↔ x = 0
[PROOFSTEP]
rw [← toComplex_zero, toComplex_inj]
[GOAL]
x : ℤ[i]
⊢ ↑(norm x) = ↑normSq (↑toComplex x)
[PROOFSTEP]
rw [Zsqrtd.norm, normSq]
[GOAL]
x : ℤ[i]
⊢ ↑(x.re * x.re - -1 * x.im * x.im) =
    ↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
          map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
      (↑toComplex x)
[PROOFSTEP]
simp
[GOAL]
x : ℤ[i]
⊢ ↑(norm x) = ↑(↑normSq (↑toComplex x))
[PROOFSTEP]
cases x
[GOAL]
case mk
re✝ im✝ : ℤ
⊢ ↑(norm { re := re✝, im := im✝ }) = ↑(↑normSq (↑toComplex { re := re✝, im := im✝ }))
[PROOFSTEP]
rw [Zsqrtd.norm, normSq]
[GOAL]
case mk
re✝ im✝ : ℤ
⊢ ↑({ re := re✝, im := im✝ }.re * { re := re✝, im := im✝ }.re -
        -1 * { re := re✝, im := im✝ }.im * { re := re✝, im := im✝ }.im) =
    ↑(↑{ toZeroHom := { toFun := fun z => z.re * z.re + z.im * z.im, map_zero' := normSq.proof_1 },
            map_one' := normSq.proof_2, map_mul' := normSq.proof_3 }
        (↑toComplex { re := re✝, im := im✝ }))
[PROOFSTEP]
simp
[GOAL]
x : ℤ[i]
⊢ -1 ≤ 0
[PROOFSTEP]
norm_num
[GOAL]
x : ℤ[i]
⊢ norm x = 0 ↔ x = 0
[PROOFSTEP]
rw [← @Int.cast_inj ℝ _ _ _]
[GOAL]
x : ℤ[i]
⊢ ↑(norm x) = ↑0 ↔ x = 0
[PROOFSTEP]
simp
[GOAL]
x : ℤ[i]
⊢ 0 < norm x ↔ x ≠ 0
[PROOFSTEP]
rw [lt_iff_le_and_ne, Ne.def, eq_comm, norm_eq_zero]
[GOAL]
x : ℤ[i]
⊢ 0 ≤ norm x ∧ ¬x = 0 ↔ x ≠ 0
[PROOFSTEP]
simp [norm_nonneg]
[GOAL]
α : Type u_1
inst✝ : Ring α
x : ℤ[i]
⊢ ↑(Int.natAbs (norm x)) = ↑(norm x)
[PROOFSTEP]
rw [← Int.cast_ofNat, abs_coe_nat_norm]
[GOAL]
x : ℤ[i]
⊢ Int.ofNat (Int.natAbs (norm x)) = Int.ofNat (Int.natAbs x.re * Int.natAbs x.re + Int.natAbs x.im * Int.natAbs x.im)
[PROOFSTEP]
simp
[GOAL]
x : ℤ[i]
⊢ norm x = x.re * x.re + x.im * x.im
[PROOFSTEP]
simp [Zsqrtd.norm]
[GOAL]
x y : ℤ[i]
⊢ { re := round (↑(x * star y).re * (↑(norm y))⁻¹), im := round (↑(x * star y).im * (↑(norm y))⁻¹) } =
    { re := round (↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }
[PROOFSTEP]
simp [div_eq_mul_inv]
[GOAL]
x y : ℤ[i]
⊢ (↑toComplex (x / y)).re = ↑(round (↑toComplex x / ↑toComplex y).re)
[PROOFSTEP]
rw [div_def, ← @Rat.round_cast ℝ _ _]
[GOAL]
x y : ℤ[i]
⊢ (↑toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round (↑(x * star y).im / ↑(norm y)) }).re =
    ↑(round (↑toComplex x / ↑toComplex y).re)
[PROOFSTEP]
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
[GOAL]
x y : ℤ[i]
⊢ (↑toComplex (x / y)).im = ↑(round (↑toComplex x / ↑toComplex y).im)
[PROOFSTEP]
rw [div_def, ← @Rat.round_cast ℝ _ _, ← @Rat.round_cast ℝ _ _]
[GOAL]
x y : ℤ[i]
⊢ (↑toComplex { re := round ↑(↑(x * star y).re / ↑(norm y)), im := round ↑(↑(x * star y).im / ↑(norm y)) }).im =
    ↑(round (↑toComplex x / ↑toComplex y).im)
[PROOFSTEP]
simp [-Rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
[GOAL]
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ ↑normSq x ≤ ↑normSq y
[PROOFSTEP]
rw [normSq_apply, normSq_apply, ← _root_.abs_mul_self, _root_.abs_mul, ← _root_.abs_mul_self y.re, _root_.abs_mul y.re,
  ← _root_.abs_mul_self x.im, _root_.abs_mul x.im, ← _root_.abs_mul_self y.im, _root_.abs_mul y.im]
[GOAL]
x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ |x.re| * |x.re| + |x.im| * |x.im| ≤ |y.re| * |y.re| + |y.im| * |y.im|
[PROOFSTEP]
exact add_le_add (mul_self_le_mul_self (abs_nonneg _) hre) (mul_self_le_mul_self (abs_nonneg _) him)
[GOAL]
x y : ℤ[i]
⊢ ↑toComplex x / ↑toComplex y - ↑toComplex (x / y) =
    ↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
      (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I
[PROOFSTEP]
apply Complex.ext
[GOAL]
case a
x y : ℤ[i]
⊢ (↑toComplex x / ↑toComplex y - ↑toComplex (x / y)).re =
    (↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
        (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I).re
[PROOFSTEP]
simp
[GOAL]
case a
x y : ℤ[i]
⊢ (↑toComplex x / ↑toComplex y - ↑toComplex (x / y)).im =
    (↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
        (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I).im
[PROOFSTEP]
simp
[GOAL]
x y : ℤ[i]
⊢ ↑normSq
      (↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
        (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I) ≤
    ↑normSq (1 / 2 + 1 / 2 * I)
[PROOFSTEP]
have : |(2⁻¹ : ℝ)| = 2⁻¹ := abs_of_nonneg (by norm_num)
[GOAL]
x y : ℤ[i]
⊢ 0 ≤ 2⁻¹
[PROOFSTEP]
norm_num
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ ↑normSq
      (↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
        (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I) ≤
    ↑normSq (1 / 2 + 1 / 2 * I)
[PROOFSTEP]
exact
  normSq_le_normSq_of_re_le_of_im_le
    (by rw [toComplex_div_re]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).re)
    (by rw [toComplex_div_im]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).im)
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
          (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|
[PROOFSTEP]
rw [toComplex_div_re]
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(↑toComplex x / ↑toComplex y).re - ↑↑(round (↑toComplex x / ↑toComplex y).re) +
          (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|
[PROOFSTEP]
simp [normSq, this]
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑toComplex x / ↑toComplex y).re - ↑(round (↑toComplex x / ↑toComplex y).re)| ≤ 2⁻¹
[PROOFSTEP]
simpa using abs_sub_round (x / y : ℂ).re
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
          (↑(↑toComplex x / ↑toComplex y).im - ↑(↑toComplex (x / y)).im) * I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|
[PROOFSTEP]
rw [toComplex_div_im]
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(↑toComplex x / ↑toComplex y).re - ↑(↑toComplex (x / y)).re +
          (↑(↑toComplex x / ↑toComplex y).im - ↑↑(round (↑toComplex x / ↑toComplex y).im)) * I).im| ≤
    |(1 / 2 + 1 / 2 * I).im|
[PROOFSTEP]
simp [normSq, this]
[GOAL]
x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑toComplex x / ↑toComplex y).im - ↑(round (↑toComplex x / ↑toComplex y).im)| ≤ 2⁻¹
[PROOFSTEP]
simpa using abs_sub_round (x / y : ℂ).im
[GOAL]
x y : ℤ[i]
⊢ ↑normSq (1 / 2 + 1 / 2 * I) < 1
[PROOFSTEP]
simp [normSq]
[GOAL]
x y : ℤ[i]
⊢ 2⁻¹ * 2⁻¹ + 2⁻¹ * 2⁻¹ < 1
[PROOFSTEP]
norm_num
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑toComplex y ≠ 0
[PROOFSTEP]
rwa [Ne.def, ← toComplex_zero, toComplex_inj]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
this : ↑toComplex y ≠ 0
⊢ ↑(norm (x % y)) = ↑normSq (↑toComplex x - ↑toComplex y * ↑toComplex (x / y))
[PROOFSTEP]
simp [mod_def]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
this : ↑toComplex y ≠ 0
⊢ ↑normSq (↑toComplex x - ↑toComplex y * ↑toComplex (x / y)) =
    ↑normSq (↑toComplex y) * ↑normSq (↑toComplex x / ↑toComplex y - ↑toComplex (x / y))
[PROOFSTEP]
rw [← normSq_mul, mul_sub, mul_div_cancel' _ this]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
this : ↑toComplex y ≠ 0
⊢ ↑normSq (↑toComplex y) * 1 = ↑(norm y)
[PROOFSTEP]
simp
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑(Int.natAbs (norm (x % y))) < ↑(Int.natAbs (norm y))
[PROOFSTEP]
simp [-Int.ofNat_lt, norm_mod_lt x hy]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ Int.natAbs (norm x) ≤ Int.natAbs (norm (x * y))
[PROOFSTEP]
rw [Zsqrtd.norm_mul, Int.natAbs_mul]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ Int.natAbs (norm x) ≤ Int.natAbs (norm x) * Int.natAbs (norm y)
[PROOFSTEP]
exact
  le_mul_of_one_le_right (Nat.zero_le _)
    (Int.ofNat_le.1
      (by
        rw [abs_coe_nat_norm]
        exact Int.add_one_le_of_lt (norm_pos.2 hy)))
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ ↑(Int.natAbs (norm y))
[PROOFSTEP]
rw [abs_coe_nat_norm]
[GOAL]
x y : ℤ[i]
hy : y ≠ 0
⊢ ↑1 ≤ norm y
[PROOFSTEP]
exact Int.add_one_le_of_lt (norm_pos.2 hy)
[GOAL]
⊢ 0 ≠ 1
[PROOFSTEP]
decide
[GOAL]
src✝¹ : CommRing ℤ[i] := instCommRing
src✝ : Nontrivial ℤ[i] := instNontrivial
⊢ ∀ (a : ℤ[i]), (fun x x_1 => x / x_1) a 0 = 0
[PROOFSTEP]
simp [div_def]
[GOAL]
src✝¹ : CommRing ℤ[i] := instCommRing
src✝ : Nontrivial ℤ[i] := instNontrivial
⊢ { re := 0, im := 0 } = 0
[PROOFSTEP]
rfl
[GOAL]
src✝¹ : CommRing ℤ[i] := instCommRing
src✝ : Nontrivial ℤ[i] := instNontrivial
x✝¹ x✝ : ℤ[i]
⊢ x✝ * (fun x x_1 => x / x_1) x✝¹ x✝ + (fun x x_1 => x % x_1) x✝¹ x✝ = x✝¹
[PROOFSTEP]
simp [mod_def]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬Int.natAbs (norm ↑p) = 1
[PROOFSTEP]
rw [norm_nat_cast, Int.natAbs_mul, mul_eq_one]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
⊢ ¬(Int.natAbs ↑p = 1 ∧ Int.natAbs ↑p = 1)
[PROOFSTEP]
exact fun h => (ne_of_lt hp.1.one_lt).symm h.1
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
⊢ ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
[PROOFSTEP]
simpa only [true_and, not_false_iff, exists_prop, irreducible_iff, hpu, not_forall, not_or] using hpi
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ Int.natAbs (norm a) * Int.natAbs (norm b) = p ^ 2
[PROOFSTEP]
rw [← Int.coe_nat_inj', Int.coe_nat_pow, sq, ← @norm_nat_cast (-1), hpab]
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
⊢ ↑(Int.natAbs (norm a) * Int.natAbs (norm b)) = norm (a * b)
[PROOFSTEP]
simp
[GOAL]
p : ℕ
hp : Fact (Nat.Prime p)
hpi : ¬Irreducible ↑p
hpu : ¬IsUnit ↑p
hab : ∃ a b, ↑p = a * b ∧ ¬IsUnit a ∧ ¬IsUnit b
a b : ℤ[i]
hpab : ↑p = a * b
hau : ¬IsUnit a
hbu : ¬IsUnit b
hnap : Int.natAbs (norm a) = p
⊢ Int.natAbs a.re ^ 2 + Int.natAbs a.im ^ 2 = p
[PROOFSTEP]
simpa [natAbs_norm_eq, sq] using hnap
