English
If c ≠ 0 and gcd(a,b)=1 then a^3+b^3 ≠ c^3 for the three mutual divisibility scenarios of 3 and the prime divisibility conditions.
Русский
Если c ≠ 0 и gcd(a,b)=1, то при трёх сценариях делимости 3 и простого деления a^3+b^3 не равно c^3.
LaTeX
$$$\forall a,b,c \in \mathbb{Z}, c\neq 0, \gcd(a,b)=1 \Rightarrow a^3+b^3\neq c^3$ под соответствующими условиями разбиения по 3.$$
Lean4
/-- To prove Fermat's Last Theorem for `n = 3`, it is enough to show that for all `a`, `b`, `c`
in `ℤ` such that `c ≠ 0`, `¬ 3 ∣ a`, `¬ 3 ∣ b`, `a` and `b` are coprime and `3 ∣ c`, we have
`a ^ 3 + b ^ 3 ≠ c ^ 3`.
-/
theorem fermatLastTheoremThree_of_three_dvd_only_c
(H : ∀ a b c : ℤ, c ≠ 0 → ¬3 ∣ a → ¬3 ∣ b → 3 ∣ c → IsCoprime a b → a ^ 3 + b ^ 3 ≠ c ^ 3) :
FermatLastTheoremFor 3 := by
rw [fermatLastTheoremFor_iff_int]
refine fermatLastTheoremWith_of_fermatLastTheoremWith_coprime (fun a b c ha hb hc Hgcd hF ↦ ?_)
by_cases h1 : 3 ∣ a * b * c
swap
· exact fermatLastTheoremThree_case_1 h1 hF
rw [(prime_three).dvd_mul, (prime_three).dvd_mul] at h1
rw [← sub_eq_zero, sub_eq_add_neg, ← (show Odd 3 by decide).neg_pow] at hF
rcases h1 with (h3a | h3b) | h3c
· refine fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 ha h3a ?_ H hF
simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← abs_eq_normalize, abs_neg]
· rw [add_comm (a ^ 3)] at hF
refine fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 hb h3b ?_ H hF
simp only [← Hgcd, insert_comm, gcd_insert, gcd_singleton, id_eq, ← abs_eq_normalize, abs_neg]
· rw [add_comm _ ((-c) ^ 3), ← add_assoc] at hF
refine fermatLastTheoremThree_of_dvd_a_of_gcd_eq_one_of_case2 (neg_ne_zero.2 hc) (by simp [h3c]) ?_ H hF
rw [Finset.insert_comm (-c), Finset.pair_comm (-c) b]
simp only [← Hgcd, gcd_insert, gcd_singleton, id_eq, ← abs_eq_normalize, abs_neg]
