English
Fermat's Last Theorem for exponent 3 holds in the integer setting when one excludes divisibility by 3 and uses a coprimality structure; a classical reduction shows a^3+b^3 ≠ c^3 when 3 ∤ abc under coprimality conditions.
Русский
Применимо к n=3: если 3 не делит abc и a,b,c взаимно простые, то a^3+b^3 не равно c^3.
LaTeX
$$$a,b,c\in \mathbb{Z},\; 3
mid abc,\; \gcd(a,b)=1,\; a^3+b^3\neq c^3$$$
Lean4
/-- If `a b c : ℤ` are such that `¬ 3 ∣ a * b * c`, then `a ^ 3 + b ^ 3 ≠ c ^ 3`. -/
theorem fermatLastTheoremThree_case_1 {a b c : ℤ} (hdvd : ¬3 ∣ a * b * c) : a ^ 3 + b ^ 3 ≠ c ^ 3 :=
by
simp_rw [Int.prime_three.dvd_mul, not_or] at hdvd
apply mt (congrArg (Int.cast : ℤ → ZMod 9))
simp_rw [Int.cast_add, Int.cast_pow]
rcases cube_of_not_dvd hdvd.1.1 with ha | ha <;> rcases cube_of_not_dvd hdvd.1.2 with hb | hb <;>
rcases cube_of_not_dvd hdvd.2 with hc | hc <;>
rw [ha, hb, hc] <;>
decide
