English
If p is a natural prime and p is Gaussian-prime (Prime in ℤ[i]), then p ≡ 3 mod 4.
Русский
Если p — простое натуральное число и p — простое в ℤ[i], то p ≡ 3 (mod 4).
LaTeX
$$$ p \mod 4 = 3 $$$
Lean4
theorem mod_four_eq_three_of_nat_prime_of_prime (p : ℕ) [hp : Fact p.Prime] (hpi : Prime (p : ℤ[i])) : p % 4 = 3 :=
hp.1.eq_two_or_odd.elim
(fun hp2 => by
have := hpi.irreducible.isUnit_or_isUnit (a := ⟨1, 1⟩) (b := ⟨1, -1⟩)
simp [hp2, Zsqrtd.ext_iff, ← norm_eq_one_iff, norm_def] at this)
fun hp1 =>
by_contradiction fun hp3 : p % 4 ≠ 3 =>
by
let ⟨k, hk⟩ := (ZMod.exists_sq_eq_neg_one_iff (p := p)).2 hp3
obtain ⟨k, k_lt_p, rfl⟩ : ∃ (k' : ℕ) (_ : k' < p), (k' : ZMod p) = k := by
exact ⟨k.val, k.val_lt, ZMod.natCast_zmod_val k⟩
have hpk : p ∣ k ^ 2 + 1 := by
rw [pow_two, ← CharP.cast_eq_zero_iff (ZMod p) p, Nat.cast_add, Nat.cast_mul, Nat.cast_one, ← hk,
neg_add_cancel]
have hkmul : (k ^ 2 + 1 : ℤ[i]) = ⟨k, 1⟩ * ⟨k, -1⟩ := by ext <;> simp [sq]
have hkltp : 1 + k * k < p * p :=
calc
1 + k * k ≤ k + k * k := by
apply add_le_add_right
exact (Nat.pos_of_ne_zero fun (hk0 : k = 0) => by clear_aux_decl; simp_all)
_ = k * (k + 1) := by simp [add_comm, mul_add]
_ < p * p := mul_lt_mul k_lt_p k_lt_p (Nat.succ_pos _) (Nat.zero_le _)
have hpk₁ : ¬(p : ℤ[i]) ∣ ⟨k, -1⟩ := fun ⟨x, hx⟩ =>
lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
calc
(norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, -1⟩).natAbs := by rw [hx]
_ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
_ ≤ (norm (p * x : ℤ[i])).natAbs :=
norm_le_norm_mul_left _ fun hx0 =>
show (-1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
have hpk₂ : ¬(p : ℤ[i]) ∣ ⟨k, 1⟩ := fun ⟨x, hx⟩ =>
lt_irrefl (p * x : ℤ[i]).norm.natAbs <|
calc
(norm (p * x : ℤ[i])).natAbs = (Zsqrtd.norm ⟨k, 1⟩).natAbs := by rw [hx]
_ < (norm (p : ℤ[i])).natAbs := by simpa [add_comm, Zsqrtd.norm] using hkltp
_ ≤ (norm (p * x : ℤ[i])).natAbs :=
norm_le_norm_mul_left _ fun hx0 =>
show (1 : ℤ) ≠ 0 by decide <| by simpa [hx0] using congr_arg Zsqrtd.im hx
obtain ⟨y, hy⟩ := hpk
have := hpi.2.2 ⟨k, 1⟩ ⟨k, -1⟩ ⟨y, by rw [← hkmul, ← Nat.cast_mul p, ← hy]; simp⟩
tauto
