English
If gcd(a,b,c) = 1 and a^n + b^n + c^n = 0, then a and b are coprime.
Русский
Если gcd(a,b,c)=1 и a^n + b^n + c^n = 0, то a и b coprime.
LaTeX
$$$\\forall n\\in\\mathbb{N},\\forall a,b,c\\in\\mathbb{Z},\\ gcd(a,b,c)=1 \\land a^n + b^n + c^n = 0 \\Rightarrow \\gcd(a,b)=1$$$
Lean4
theorem isCoprime_of_gcd_eq_one_of_FLT {n : ℕ} {a b c : ℤ} (Hgcd : Finset.gcd { a, b, c } id = 1)
(HF : a ^ n + b ^ n + c ^ n = 0) : IsCoprime a b :=
by
rcases eq_or_ne n 0 with rfl | hn
· simp only [pow_zero, Int.reduceAdd, OfNat.ofNat_ne_zero] at HF
refine isCoprime_of_prime_dvd ?_ <| (fun p hp hpa hpb ↦ hp.not_dvd_one ?_)
· rintro ⟨rfl, rfl⟩
simp only [ne_eq, hn, not_false_eq_true, zero_pow, add_zero, zero_add, pow_eq_zero_iff] at HF
simp only [HF, Finset.mem_singleton, Finset.insert_eq_of_mem, Finset.gcd_singleton, id_eq, map_zero,
zero_ne_one] at Hgcd
· rw [← Hgcd]
refine Finset.dvd_gcd_iff.mpr fun x hx ↦ ?_
simp only [Finset.mem_insert, Finset.mem_singleton] at hx
rcases hx with hx | hx | hx <;>
simp only [id_eq, hx, hpa, hpb, dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT hp hpa hpb HF]
