English
If p is a prime, and p divides a and p divides b, and a^n + b^n + c^n = 0 for integers a,b,c, then p divides c (provided n ≠ 0).
Русский
Пусть p — простое число, и p делит a и p делит b, а также a^n + b^n + c^n = 0 для целых a,b,c; тогда p делит c (при n ≠ 0).
LaTeX
$$$\\forall n\\in\\mathbb{N},\\forall p\\in\\mathbb{Z},\\text{Prime}(p) \\rightarrow \\forall a,b,c\\in\\mathbb{Z},\\ p|a \\land p|b \\land a^n + b^n + c^n = 0 \\Rightarrow p|c \\; (n \\neq 0)$$$
Lean4
theorem dvd_c_of_prime_of_dvd_a_of_dvd_b_of_FLT {n : ℕ} {p : ℤ} (hp : Prime p) {a b c : ℤ} (hpa : p ∣ a) (hpb : p ∣ b)
(HF : a ^ n + b ^ n + c ^ n = 0) : p ∣ c :=
by
rcases eq_or_ne n 0 with rfl | hn
· simp at HF
refine hp.dvd_of_dvd_pow (n := n) (dvd_neg.1 ?_)
rw [add_eq_zero_iff_eq_neg] at HF
exact HF.symm ▸ dvd_add (dvd_pow hpa hn) (dvd_pow hpb hn)
