Fermat numbers

The Fermat numbers are a sequence of natural numbers defined as Nat.fermatNumber n = 2^(2^n) + 1, for all natural numbers n.

Main theorems

• Nat.coprime_fermatNumber_fermatNumber: two distinct Fermat numbers are coprime.
• Nat.pepin_primality: For 0 < n, Fermat number Fₙ is prime if 3 ^ (2 ^ (2 ^ n - 1)) = -1 mod Fₙ
• fermat_primeFactors_one_lt: For 1 < n, Prime factors the Fermat number Fₙ are of form k * 2 ^ (n + 2) + 1.

def Nat.fermatNumber (n : ℕ) : ℕ

Fermat numbers: the n-th Fermat number is defined as 2^(2^n) + 1.

@[simp]

theorem Nat.fermatNumber_zero : fermatNumber 0 = 3

@[simp]

theorem Nat.fermatNumber_one : fermatNumber 1 = 5

@[simp]

theorem Nat.fermatNumber_two : fermatNumber 2 = 17

theorem Nat.fermatNumber_strictMono : StrictMono fermatNumber

theorem Nat.fermatNumber_mono : Monotone fermatNumber

theorem Nat.fermatNumber_injective : Function.Injective fermatNumber

theorem Nat.three_le_fermatNumber (n : ℕ) : 3 ≤ n.fermatNumber

theorem Nat.two_lt_fermatNumber (n : ℕ) : 2 < n.fermatNumber

theorem Nat.fermatNumber_ne_one (n : ℕ) : n.fermatNumber ≠ 1

theorem Nat.odd_fermatNumber (n : ℕ) : Odd n.fermatNumber

theorem Nat.prod_fermatNumber (n : ℕ) : ∏ k ∈ Finset.range n, k.fermatNumber = n.fermatNumber - 2

theorem Nat.fermatNumber_eq_prod_add_two (n : ℕ) : n.fermatNumber = ∏ k ∈ Finset.range n, k.fermatNumber + 2

theorem Nat.fermatNumber_succ (n : ℕ) : (n + 1).fermatNumber = (n.fermatNumber - 1) ^ 2 + 1

theorem Nat.two_mul_fermatNumber_sub_one_sq_le_fermatNumber_sq (n : ℕ) : 2 * (n.fermatNumber - 1) ^ 2 ≤ (n + 1).fermatNumber ^ 2

theorem Nat.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) : (n + 2).fermatNumber = (n + 1).fermatNumber ^ 2 - 2 * (n.fermatNumber - 1) ^ 2

theorem Int.fermatNumber_eq_fermatNumber_sq_sub_two_mul_fermatNumber_sub_one_sq (n : ℕ) : ↑(n + 2).fermatNumber = ↑(n + 1).fermatNumber ^ 2 - 2 * (↑n.fermatNumber - 1) ^ 2

theorem Nat.coprime_fermatNumber_fermatNumber {m n : ℕ} (hmn : m ≠ n) : m.fermatNumber.Coprime n.fermatNumber

Goldbach's theorem : no two distinct Fermat numbers share a common factor greater than one.

From a letter to Euler, see page 37 in [juskevic2022].

theorem Nat.pairwise_coprime_fermatNumber : Pairwise fun (m n : ℕ) => m.fermatNumber.Coprime n.fermatNumber

theorem Nat.pow_of_pow_add_prime {a n : ℕ} (ha : 1 < a) (hn : n ≠ 0) (hP : Prime (a ^ n + 1)) : ∃ (m : ℕ), n = 2 ^ m

Prime a ^ n + 1 implies n is a power of two (Fermat primes).

theorem Nat.pepin_primality (n : ℕ) (h : 3 ^ 2 ^ (2 ^ n - 1) = -1) : Prime n.fermatNumber

Fₙ = 2^(2^n)+1 is prime if 3^(2^(2^n-1)) = -1 mod Fₙ (Pépin's test).

theorem Nat.pepin_primality' (n : ℕ) (h : 3 ^ ((n.fermatNumber - 1) / 2) = -1) : Prime n.fermatNumber

Fₙ = 2^(2^n)+1 is prime if 3^((Fₙ - 1)/2) = -1 mod Fₙ (Pépin's test).

theorem Nat.pow_pow_add_primeFactors_one_lt {a n p : ℕ} (hp : Prime p) (hp2 : p ≠ 2) (hpdvd : p ∣ a ^ 2 ^ n + 1) : ∃ (k : ℕ), p = k * 2 ^ (n + 1) + 1

Prime factors of a ^ (2 ^ n) + 1 are of form k * 2 ^ (n + 1) + 1.

theorem Nat.fermat_primeFactors_one_lt (n p : ℕ) (hn : 1 < n) (hp : Prime p) (hpdvd : p ∣ n.fermatNumber) : ∃ (k : ℕ), p = k * 2 ^ (n + 2) + 1

Primality of Mersenne numbers Mₙ = a ^ n - 1

theorem Nat.prime_of_pow_sub_one_prime {a n : ℕ} (hn1 : n ≠ 1) (hP : Prime (a ^ n - 1)) : a = 2 ∧ Prime n

Prime a ^ n - 1 implies a = 2 and prime n.