English
If a^n − 1 is prime with n ≠ 1, then a = 2 and n is prime.
Русский
Если a^n − 1 простое и n ≠ 1, то a = 2 и n простое.
LaTeX
$${a,n} : n ≠ 1 ∧ (a^n - 1) \\,\\text{prime} ⇒ a = 2 ∧ n \\,\\text{prime}$$
Lean4
/-- Prime `a ^ n - 1` implies `a = 2` and prime `n`. -/
theorem prime_of_pow_sub_one_prime {a n : ℕ} (hn1 : n ≠ 1) (hP : (a ^ n - 1).Prime) : a = 2 ∧ n.Prime :=
by
have han1 : 1 < a ^ n := tsub_pos_iff_lt.mp hP.pos
have hn0 : n ≠ 0 := fun h ↦ (h ▸ han1).ne' rfl
have ha1 : 1 < a := (Nat.one_lt_pow_iff hn0).mp han1
have ha0 : 0 < a := one_pos.trans ha1
have ha2 : a = 2 := by
contrapose! hn1
let h := Nat.sub_dvd_pow_sub_pow a 1 n
rw [one_pow, hP.dvd_iff_eq (mt (Nat.sub_eq_iff_eq_add ha1.le).mp hn1), eq_comm] at h
exact (pow_eq_self_iff ha1).mp (Nat.sub_one_cancel ha0 (pow_pos ha0 n) h).symm
subst ha2
refine ⟨rfl, Nat.prime_def.mpr ⟨(two_le_iff n).mpr ⟨hn0, hn1⟩, fun d hdn ↦ ?_⟩⟩
have hinj : ∀ x y, 2 ^ x - 1 = 2 ^ y - 1 → x = y := fun x y h ↦
Nat.pow_right_injective le_rfl (sub_one_cancel (pow_pos ha0 x) (pow_pos ha0 y) h)
let h := Nat.sub_dvd_pow_sub_pow (2 ^ d) 1 (n / d)
rw [one_pow, ← pow_mul, Nat.mul_div_cancel' hdn] at h
exact (hP.eq_one_or_self_of_dvd (2 ^ d - 1) h).imp (hinj d 1) (hinj d n)
