English
Same recurrence for Fermat numbers holds in natural numbers with the Nat interpretation.
Русский
Та же рекуррентность для чисел Ферма сохраняется в естественных числах.
LaTeX
$$$\\mathrm{fermatNumber}(n+2) = (\\mathrm{fermatNumber}(n+1))^2 - 2 \\cdot (\\mathrm{fermatNumber}(n) - 1)^2$$$
Lean4
/-- Prime factors of `a ^ (2 ^ n) + 1` are of form `k * 2 ^ (n + 1) + 1`. -/
theorem pow_pow_add_primeFactors_one_lt {a n p : ℕ} (hp : p.Prime) (hp2 : p ≠ 2) (hpdvd : p ∣ a ^ (2 ^ n) + 1) :
∃ k, p = k * 2 ^ (n + 1) + 1 :=
by
have : Fact (2 < p) := Fact.mk (lt_of_le_of_ne hp.two_le hp2.symm)
have : Fact p.Prime := Fact.mk hp
have ha1 : (a : ZMod p) ^ (2 ^ n) = -1 := by
rw [eq_neg_iff_add_eq_zero]
exact_mod_cast (natCast_eq_zero_iff (a ^ (2 ^ n) + 1) p).mpr hpdvd
have ha0 : (a : ZMod p) ≠ 0 := by
intro h
rw [h, zero_pow (pow_ne_zero n two_ne_zero), zero_eq_neg] at ha1
exact one_ne_zero ha1
have ha : orderOf (a : ZMod p) = 2 ^ (n + 1) :=
by
apply orderOf_eq_prime_pow
· rw [ha1]
exact neg_one_ne_one
· rw [pow_succ, pow_mul, ha1, neg_one_sq]
simpa [ha, dvd_def, Nat.sub_eq_iff_eq_add hp.one_le, mul_comm] using orderOf_dvd_card_sub_one ha0
