English
If a^n + 1 is prime with a > 1 and n ≠ 0, then n is a power of two.
Русский
Если a^n + 1 простое, при a > 1 и n ≠ 0, то n является степенью двойки.
LaTeX
$$If\\( a>1, n\\neq 0, (a^n+1)\\text{ prime} \\Rightarrow \\exists m, n=2^m$$
Lean4
/-- Prime `a ^ n + 1` implies `n` is a power of two (**Fermat primes**). -/
theorem pow_of_pow_add_prime {a n : ℕ} (ha : 1 < a) (hn : n ≠ 0) (hP : (a ^ n + 1).Prime) : ∃ m : ℕ, n = 2 ^ m :=
by
obtain ⟨k, m, hm, rfl⟩ := exists_eq_two_pow_mul_odd hn
rw [pow_mul] at hP
use k
replace ha : 1 < a ^ 2 ^ k := one_lt_pow (pow_ne_zero k two_ne_zero) ha
let h := hm.nat_add_dvd_pow_add_pow (a ^ 2 ^ k) 1
rw [one_pow, hP.dvd_iff_eq (Nat.lt_add_right 1 ha).ne', add_left_inj, pow_eq_self_iff ha] at h
rw [h, mul_one]
