English
Any two distinct Fermat numbers are coprime: for m ≠ n, gcd(F_m, F_n) = 1.
Русский
Любые два различных числа Ферматом взаимно просты: для m ≠ n их наибольший общий делитель равен 1.
LaTeX
$$Coprime\\( \\mathrm{fermatNumber}(m) , \\mathrm{fermatNumber}(n) \\)$$
Lean4
/-- **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 coprime_fermatNumber_fermatNumber {m n : ℕ} (hmn : m ≠ n) : Coprime (fermatNumber m) (fermatNumber n) :=
by
wlog hmn' : m < n
· simpa only [coprime_comm] using this hmn.symm (by cutsat)
let d := (fermatNumber m).gcd (fermatNumber n)
have h_n : d ∣ fermatNumber n := gcd_dvd_right ..
have h_m : d ∣ 2 :=
(Nat.dvd_add_right <| (gcd_dvd_left _ _).trans <| dvd_prod_of_mem _ <| mem_range.mpr hmn').mp <|
fermatNumber_eq_prod_add_two _ ▸ h_n
refine ((dvd_prime prime_two).mp h_m).resolve_right fun h_two ↦ ?_
exact (odd_fermatNumber _).not_two_dvd_nat (h_two ▸ h_n)
