English
Prime divisors p of a^{2^n}+1 with p ≠ 2 have the form p = k·2^{n+1}+1.
Русский
Простые делители p числа a^{2^n}+1 (p ≠ 2) имеют вид p = k·2^{n+1}+1.
LaTeX
$$If\\( p \\text{ is prime}, p \\neq 2, p \\mid a^{2^n} + 1 \\Rightarrow \\exists k, p = k \\cdot 2^{n+1} + 1$$
Lean4
theorem fermat_primeFactors_one_lt (n p : ℕ) (hn : 1 < n) (hp : p.Prime) (hpdvd : p ∣ fermatNumber n) :
∃ k, p = k * 2 ^ (n + 2) + 1 := by
have : Fact p.Prime := Fact.mk hp
have hp2 : p ≠ 2 := by exact ((even_pow.mpr ⟨even_two, pow_ne_zero n two_ne_zero⟩).add_one).ne_two_of_dvd_nat hpdvd
have hp8 : p % 8 = 1 := by
obtain ⟨k, rfl⟩ := pow_pow_add_primeFactors_one_lt hp hp2 hpdvd
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le' hn
rw [add_assoc, pow_add, ← mul_assoc, ← mod_add_mod, mul_mod]
simp
obtain ⟨a, ha⟩ := (exists_sq_eq_two_iff hp2).mpr (Or.inl hp8)
suffices h : p ∣ a.val ^ (2 ^ (n + 1)) + 1 by exact pow_pow_add_primeFactors_one_lt hp hp2 h
rw [fermatNumber] at hpdvd
rw [← natCast_eq_zero_iff, Nat.cast_add _ 1, Nat.cast_one, Nat.cast_pow] at hpdvd ⊢
rwa [natCast_val, ZMod.cast_id, pow_succ', pow_mul, sq, ← ha]
-- TODO: move to NumberTheory.Mersenne, once we have that.
