(* Title: Fermat3.thy
Author: Roelof Oosterhuis
2007 Rijksuniversiteit Groningen
*)
header {* Fermat's last theorem, case $n=3$ *}
theory Fermat3
imports QuadForm
begin
text {* Proof of Fermat's last theorem for the case $n=3$: $$\forall x,y,z:~x^3 + y^3 = z^3 \Longrightarrow xyz=0.$$ *}
lemma factor_sum_cubes: "(x::int)^3 + y^3 = (x+y)*(x^2 - x*y + y^2)"
by (simp add: nat_number ring_simps)
lemma two_not_abs_cube: "¦x^3¦ = (2::int) ==> False"
proof -
assume "¦x^3¦ = 2"
hence x32: "¦x¦^3 = 2" by (simp only: abs_power3_distrib)
have "¦x¦ ≥ 0" by simp
moreover
{ assume "¦x¦ = 0 ∨ ¦x¦ = 1 ∨ ¦x¦ = 2"
with x32 have False by (auto simp add: power_0_left) }
moreover
{ assume "¦x¦ > 2"
moreover have "(0::int) ≤ 2" and "(0::nat) < 3" by auto
ultimately have "¦x¦^3 > 2^3" by (simp only: power_strict_mono)
with x32 have False by simp }
ultimately show False by arith
qed
text {* Shows there exists no solution $v^3+w^3 = x^3$ with $vwx\ne 0$ and $\gcd(v,w)=1$ and $x$ even, by constructing a solution with a smaller $|x^3|$. *}
lemma no_rewritten_fermat3:
"¬ (∃ v w. v^3+w^3 = x^3 ∧ v*w*x ≠ 0 ∧ x ∈ zEven ∧ zgcd(v,w)=1)" (is "?Q x")
proof (rule_tac x="x" and V="λx. nat¦x^3¦" in val_infinite_descent)
fix x
assume "nat¦x^3¦ = 0" hence "x^3 = 0" by arith
hence "x=0" by auto
thus "?Q x" by auto
next
fix x
assume x3pos: "0 < nat¦x^3¦" and "¬ ?Q x"
then obtain v w where vwx:
"v^3+w^3=x^3 ∧ v*w*x ≠ 0 ∧ x ∈ zEven ∧ zgcd(v,w)=1" (is "?P v w x")
by auto
have "∃ α β γ. ?P α β γ ∧ nat¦γ^3¦ < nat¦x^3¦"
proof -
-- "obtain coprime $p$ and $q$ such that $v = p+q$ and $w = p-q$"
have vwOdd: "v ∈ zOdd ∧ w ∈ zOdd"
proof (rule ccontr, case_tac "v ∈ zOdd", simp_all)
assume "v ∉ zOdd" hence ve: "v ∈ zEven" by (rule not_odd_impl_even)
hence "v^3 ∈ zEven" by (simp only: power_preserves_even)
moreover from vwx have "x^3 ∈ zEven" by (simp only: power_preserves_even)
ultimately have "(x^3-v^3) ∈ zEven" by (simp only: even_minus_even)
moreover from vwx have "x^3-v^3 = w^3" by simp
ultimately have "w^3 ∈ zEven" by simp
hence "w ∈ zEven" by (simp only: power_preserves_even)
with ve have "2 dvd v ∧ 2 dvd w" by (auto simp add: zEven_def)
hence "2 dvd zgcd(v,w)" by (simp add: zgcd_greatest_iff)
with vwx show False by simp
next
assume vo: "v ∈ zOdd" and "w ∉ zOdd"
hence "w ∈ zEven" by (simp add: not_odd_impl_even)
with vo have "v^3 ∈ zOdd" and "w^3 ∈ zEven"
by (auto simp only: power_preserves_even power_preserves_odd)
hence "w^3 + v^3 ∈ zOdd" by (simp only: even_plus_odd)
with vwx have "x^3 ∈ zOdd" by (simp add: zadd_commute)
hence "x ∈ zOdd" by (simp only: power_preserves_odd)
with vwx show False by (auto simp add: odd_iff_not_even)
qed
hence "v+w ∈ zEven ∧ v-w ∈ zEven" by (simp add: odd_minus_odd odd_plus_odd)
then obtain p q where pq: "v+w = 2*p ∧ v-w = 2*q"
by (auto simp add: zEven_def)
hence vw: "v = p+q ∧ w = p-q" by auto
-- "show that $x^3 = (2p)(p^2 + 3q^2)$ and that these factors are"
-- "either coprime (first case), or have $3$ as g.c.d. (second case)"
have vwpq: "v^3 + w^3 = (2*p)*(p^2 + 3*q^2)"
proof -
have "2*(v^3 + w^3) = 2*(v+w)*(v^2 - v*w + w^2)"
by (simp only: factor_sum_cubes)
also from pq have "… = 4*p*(v^2 - v*w + w^2)" by auto
also have "… = p*((v+w)^2 + 3*(v-w)^2)"
by (simp add: nat_number ring_simps)
also with pq have "… = p*((2*p)^2 + 3*(2*q)^2)" by simp
also have "… = 2*(2*p)*(p^2+3*q^2)" by (simp add: power_mult_distrib)
finally show ?thesis by simp
qed
let ?g = "zgcd(2*p, p^2+3*q^2)"
have g1: "?g ≥ 1"
proof (rule ccontr)
assume "¬ ?g ≥ 1" hence "?g < 0 ∨ ?g = 0" by auto
moreover have "?g ≥ 0" by (rule zgcd_geq_zero)
ultimately have "?g = 0" by simp
hence "nat¦2*p¦ = 0" by (unfold zgcd_def, simp add: gcd_zero)
hence "p = 0" by arith
with vwpq vwx x3pos show False by auto
qed
have gOdd: "¬ 2 dvd ?g"
proof (rule ccontr, simp)
assume "2 dvd ?g"
hence"2 dvd p^2+3*q^2" by (simp only: zgcd_greatest_iff)
then obtain k where k: "p^2 + 3*q^2 = 2*k" by (auto simp add: dvd_def)
hence "2*(k - 2*q^2) = p^2-q^2" by auto
with vw have "v*w = 2*(k - 2*q^2)" by (simp add: zspecial_product)
hence "v*w ∈ zEven" by (auto simp only: zEven_def)
hence "v ∈ zEven ∨ w ∈ zEven" by (simp add: even_product)
with vwOdd show False by (auto simp add: odd_iff_not_even)
qed
-- "first case: $p$ is not a multiple of $3$; hence $2p$ and $p^2+3q^2$"
-- "are coprime; hence both are cubes"
{ assume p3: "¬ 3 dvd p"
have g3: "¬ 3 dvd ?g"
proof (rule ccontr, simp)
assume "3 dvd ?g" hence "3 dvd 2*p" by (simp add: zgcd_greatest_iff)
hence "(3::int) dvd 2 ∨ 3 dvd p"
by (auto simp only: zprime_3 zprime_zdvd_zmult_general)
with p3 show False by arith
qed
have pq_relprime: "zgcd(p,q)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and zp: "z dvd p" and zq: "z dvd q"
hence "z dvd p+q ∧ z dvd p-q" by (auto simp only: zdvd_zadd zdvd_zdiff)
with vw have "z dvd v ∧ z dvd w" by simp
with z vwx show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have factors_relprime: "?g = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and z2p: "z dvd 2*p" and zpq: "z dvd p^2+3*q^2"
hence zg: "z dvd ?g" by (simp add: zgcd_greatest_iff)
with gOdd have "z ≠ 2" by auto
with z have zg2: "z > 2" by (auto simp add: zprime_def)
from z z2p have "z dvd 2 ∨ z dvd p" by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "z dvd 2"
hence "z ≤ 2" by (auto simp add: zdvd_imp_le)
with zg2 have False by simp }
ultimately have zp: "z dvd p" by auto
hence "z dvd p^2" by (auto simp add: power2_eq_square zdvd_zmult2)
with zpq have "z dvd p^2+3*q^2-p^2" by (simp only: zdvd_zdiff)
hence "z dvd 3*q^2" by auto
with z have "z dvd 3 ∨ z dvd q^2" by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "z dvd 3"
hence "z ≤ 3" by (auto simp add: zdvd_imp_le)
with zg2 have "z = 3" by auto
with zg g3 have False by auto }
ultimately have "z dvd q^2" by auto
with z have "z dvd q" by (rule zprime_zdvd_power)
with zp z pq_relprime show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
moreover from vwx vwpq have pqx: "(2*p)*(p^2 + 3*q^2) = x^3" by auto
moreover have triv3: "3 = nat 3 ∧ nat 3 > 1 ∧ 3 ∈ zOdd"
by (unfold zOdd_def, auto)
ultimately have "∃ c. 2*p = c^3"
by (simp only: int_relprime_odd_power_divisors)
then obtain c where c: "c^3 = 2*p" by auto
from pqx factors_relprime have "zgcd(p^2 + 3*q^2, 2*p) = 1"
and "(p^2 + 3*q^2)*(2*p) = x^3" by (auto simp add: zgcd_commute mult_ac)
with triv3 have "∃ d. p^2 + 3*q^2 = d^3"
by (simp only: int_relprime_odd_power_divisors)
then obtain d where d: "p^2 + 3*q^2 = d^3" by auto
have "d ∈ zOdd"
proof (rule ccontr)
assume "d ∉ zOdd" hence "d ∈ zEven" by (rule not_odd_impl_even)
hence "d^3 ∈ zEven" by (simp only: power_preserves_even)
hence "2 dvd d^3" by (simp add: zEven_def dvd_def)
moreover have "2 dvd 2*p" by (rule zdvd_triv_left)
ultimately have "2 dvd zgcd(2*p, d^3)" by (simp add: zgcd_greatest_iff)
with d factors_relprime show False by auto
qed
with d pq_relprime have "zgcd(p,q)=1 ∧ p^2 + 3*q^2 = d^3 ∧ d ∈ zOdd"
by simp
hence "is_cube_form p q" by (rule qf3_cube_impl_cube_form)
then obtain a b where "p = a^3 - 9*a*b^2 ∧ q = 3*a^2*b - 3*b^3"
by (unfold is_cube_form_def, auto)
hence ab: "p = a*(a+3*b)*(a- 3*b) ∧ q = b*(a+b)*(a-b)*3"
by (simp add: nat_number ring_simps)
with c have abc: "(2*a)*(a+3*b)*(a- 3*b) = c^3" by auto
have ab_relprime: "zgcd(a,b)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and za: "z dvd a" and zb: "z dvd b"
with ab have "z dvd p ∧ z dvd q" by (simp add: zdvd_zmult2)
with z pq_relprime show
False by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have ab1: "zgcd(2*a, a+3*b) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and "z dvd 2*a" and zab: "z dvd a+3*b"
hence "z dvd 2 ∨ z dvd a" by (simp add: zprime_zdvd_zmult)
moreover have zn2: "¬ z dvd 2"
proof (rule ccontr, simp)
assume z2: "z dvd 2"
hence "z ≤ 2" by (simp only: zdvd_imp_le)
with z have "z = 2" by (unfold zprime_def, auto)
with zab have ab2: "2 dvd a+3*b" by simp
moreover have "2 dvd 2*b" by (rule zdvd_triv_left)
ultimately have "2 dvd a+3*b- 2*b" by (rule zdvd_zdiff)
hence "2 dvd a+b" by arith
hence "2 dvd (a+b)*((a-b)*b*3)" by (rule zdvd_zmult2)
with ab have qEven: "2 dvd q" by (simp only: mult_ac)
from ab2 have "2 dvd (a+3*b)*((a- 3*b)*a)" by (rule zdvd_zmult2)
with ab have "2 dvd p" by (simp only: mult_ac)
with qEven have "2 dvd zgcd(p,q)" by (simp add: zgcd_greatest_iff)
with pq_relprime show False by auto
qed
ultimately have za: "z dvd a" by auto
with zab have "z dvd a+3*b-a" by (simp only: zdvd_zdiff)
hence "z dvd 3*b" by simp
with z have "z dvd 3 ∨ z dvd b" by (simp only: zprime_zdvd_zmult_general)
moreover
{ assume "z dvd 3"
with z have "z ≤ 3" by (auto simp add: zdvd_imp_le)
moreover from zn2 have "z≠2" by auto
moreover from z have "z > 1" by (simp add: zprime_def)
ultimately have "z=3" by auto
with za have "3 dvd a" by simp
with ab have "3 dvd p" by (auto simp add: zdvd_zmult2)
with p3 have False by auto }
ultimately have "z dvd b" by auto
with za z ab_relprime show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have ab2: "zgcd(a+3*b, a- 3*b) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and zab1: "z dvd a+3*b" and zab2: "z dvd a- 3*b"
hence "z dvd (a+3*b)+(a- 3*b)" by (simp only: zdvd_zadd)
hence "z dvd 2*a" by simp
with zab1 z ab1 show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have "zgcd(a- 3*b, 2*a) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and z2a: "z dvd 2*a" and zab: "z dvd a- 3*b"
hence "z dvd 2*a-(a- 3*b)" by (simp only: zdvd_zdiff)
moreover have "2*a-(a- 3*b) = a+3*b" by simp
ultimately have "z dvd a+3*b" by simp
with z2a z ab1 show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
with abc ab1 ab2 triv3 have "∃ k l m. 2*a=k^3 ∧ a+3*b=l^3 ∧ a- 3*b=m^3"
by (simp only: int_triple_relprime_odd_power_divisors)
then obtain α β γ where albega:
"2*a = γ^3 ∧ a - 3*b = α^3 ∧ a+3*b = β^3" by auto
-- "show this is a (smaller) solution"
hence "α^3 + β^3 = γ^3" by auto
moreover have "α*β*γ ≠ 0"
proof (rule ccontr, safe)
assume "α * β * γ = 0"
with albega ab have "p=0" by (auto simp add: power_0_left)
with vwpq vwx show False by auto
qed
moreover have "γ ∈ zEven"
proof -
have "2*a ∈ zEven" by (simp add: zEven_def)
with albega have "γ^3 ∈ zEven" by simp
thus ?thesis by (simp only: power_preserves_even)
qed
moreover have "zgcd(α, β)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and za: "z dvd α" and zb: "z dvd β"
hence "z dvd α * α^2 ∧ z dvd β * β^2" by (simp add: zdvd_zmult2)
hence "z dvd α^Suc 2 ∧ z dvd β^Suc 2" by (auto simp only: power_Suc)
with albega have "z dvd a- 3*b ∧ z dvd a+3*b" by auto
with ab2 z show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
moreover have "nat¦γ^3¦ < nat¦x^3¦"
proof -
let ?A = "p^2 + 3*q^2"
from vwx vwpq have "x^3 = 2*p*?A" by auto
also with ab have "… = 2*a*((a+3*b)*(a- 3*b)*?A)" by auto
also with albega have "… = γ^3 *((a+3*b)*(a- 3*b)*?A)" by auto
finally have eq: "¦x^3¦ = ¦γ^3¦ * ¦(a+3*b)*(a- 3*b)*?A¦"
by (auto simp add: abs_mult)
with x3pos have "¦(a+3*b)*(a- 3*b)*?A¦ > 0" by auto
hence eqpos: "¦(a+3*b)*(a- 3*b)¦ > 0" by auto
moreover have Ag1: "¦?A¦ > 1"
proof -
have Aqf3: "is_qfN ?A 3" by (auto simp add: is_qfN_def)
moreover have triv3b: "(3::int) ≥ 1" by simp
ultimately have "?A ≥ 0" by (simp only: qfN_pos)
hence "?A > 1 ∨ ?A = 0 ∨ ?A =1" by auto
moreover
{ assume "?A = 0" with triv3b have "p = 0 ∧ q = 0" by (rule qfN_zero)
with vwpq vwx have False by auto }
moreover
{ assume A1: "?A = 1"
have "q=0"
proof (rule ccontr)
assume "q ≠ 0"
hence "q^2 > 0" by (simp add: zero_less_power2)
hence "3*q^2 > 1" by arith
moreover have "p^2 ≥ 0" by (rule zero_le_power2)
ultimately have "?A > 1" by arith
with A1 show False by simp
qed
with A1 have p21: "p^2 = 1" by simp
hence "¦p¦ = 1" by (rule power2_eq1_iff)
with vwpq vwx A1 have "¦x^3¦ = 2" by auto
hence False by (rule two_not_abs_cube) }
ultimately show ?thesis by auto
qed
ultimately have
"¦(a+3*b)*(a- 3*b)¦*1 < ¦(a+3*b)*(a- 3*b)¦*¦?A¦"
by (simp only: zmult_zless_mono2)
with eqpos have "¦(a+3*b)*(a- 3*b)¦*¦?A¦ > 1" by arith
hence "¦(a+3*b)*(a- 3*b)*?A¦ > 1" by (auto simp add: abs_mult)
moreover have "¦γ^3¦ > 0"
proof -
from eq have "¦γ^3¦ = 0 ==> ¦x^3¦=0" by auto
with x3pos show ?thesis by auto
qed
ultimately have "¦γ^3¦ * 1 < ¦γ^3¦ * ¦(a+3*b)*(a- 3*b)*?A¦"
by (rule zmult_zless_mono2)
with eq have "¦x^3¦ > ¦γ^3¦" by auto
thus ?thesis by arith
qed
ultimately have ?thesis by auto }
moreover
-- "second case: $p = 3r$ and hence $x^3 = (18r)(q^2+3r^2)$ and these"
-- "factors are coprime; hence both are cubes"
{ assume p3: "3 dvd p"
then obtain r where r: "p = 3*r" by (auto simp add: dvd_def)
moreover have "3 dvd 3*(3*r^2 + q^2)" by (rule zdvd_triv_left)
ultimately have pq3: "3 dvd p^2+3*q^2" by (simp add: power_mult_distrib)
moreover from p3 have "3 dvd 2*p" by (rule zdvd_zmult)
ultimately have g3: "3 dvd ?g" by (simp add: zgcd_greatest_iff)
have qr_relprime: "zgcd(q,r) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and zq: "z dvd q" and "z dvd r"
with r have "z dvd p" by (simp add: zdvd_zmult)
with zq have "z dvd p+q ∧ z dvd p-q" by (simp add: zdvd_zadd zdvd_zdiff)
with vw have "z dvd zgcd(v, w)" by (simp add: zgcd_greatest_iff)
with vwx z show False by (auto simp add: zprime_def)
qed
have factors_relprime: "zgcd(18*r, q^2 + 3*r^2) = 1"
proof -
from g3 obtain k where k: "?g = 3*k" by (auto simp add: dvd_def)
have "k = 1"
proof (rule ccontr)
assume "k ≠ 1"
with g1 k have "k > 1" by auto
then obtain h where h: "zprime h ∧ h dvd k"
by (frule_tac a="k" in zprime_factor_exists, blast)
with k have hg: "3*h dvd ?g" by (auto simp add: zdvd_zmult_mono)
hence "3*h dvd p^2 + 3*q^2" and hp: "3*h dvd 2*p"
by (auto simp only: zgcd_greatest_iff)
then obtain s where s: "p^2 + 3*q^2 = (3*h)*s"
by (auto simp add: dvd_def)
with r have rqh: "3*r^2+q^2 = h*s" by (simp add: power_mult_distrib)
from hp r have "3*h dvd 3*(2*r)" by simp
moreover have "(3::int) ≠ 0" by simp
ultimately have "h dvd 2*r" by (rule zdvd_mult_cancel)
with h have "h dvd 2 ∨ h dvd r" by (simp only: zprime_zdvd_zmult_general)
moreover have "¬ h dvd 2"
proof (rule ccontr, simp)
assume "h dvd 2"
with h have "h=2" by (auto simp add: zdvd_not_zless zprime_def)
with hg have "2*3 dvd ?g" by auto
hence "2 dvd ?g" by (rule zdvd_zmultD2)
with gOdd show False by simp
qed
ultimately have hr: "h dvd r" by simp
then obtain t where "r = h*t" by (auto simp add: dvd_def)
hence t: "r^2 = h*(h*t^2)" by (auto simp add: power2_eq_square)
with rqh have "h*s = h*(3*h*t^2) + q^2" by simp
hence "q^2 = h*(s - 3*h*t^2)" by (simp add: zdiff_zmult_distrib2)
hence "h dvd q^2" by simp
with h have "h dvd q" by (auto dest: zprime_zdvd_power)
with hr have "h dvd zgcd(q,r)" by (simp add: zgcd_greatest_iff)
with h qr_relprime show False by (unfold zprime_def, auto)
qed
with k r have "3 = zgcd(2*(3*r), (3*r)^2 + 3*q^2)" by auto
also have "… = zgcd(3*(2*r), 3*(3*r^2 + q^2))"
by (simp add: power_mult_distrib)
also have "… = 3 * zgcd(2*r, 3*r^2 + q^2)"
by (simp only: zgcd_zmult_distrib2)
finally have "zgcd(2*r, 3*r^2 + q^2) = 1" by auto
moreover have "zgcd(3*3, 3*r^2 + q^2) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix h::int assume "h dvd 3*3" and h: "zprime h" and hrq: "h dvd 3*r^2 + q^2"
hence "h dvd 3 ∨ h dvd 3" by (simp only: zprime_zdvd_zmult_general)
hence h3: "h dvd 3" by simp
have "h ≤ 3"
proof (rule ccontr)
assume "¬ h ≤ 3" hence "h > 3" by simp
with h3 show False by (auto simp add: zdvd_not_zless)
qed
with h have "h = 2 ∨ h = 3" by (unfold zprime_def, auto)
with h h3 have "h = 3 ∨ (2::int) dvd 3" by auto
hence "h=3" by arith
with hrq obtain s where "3*r^2+q^2 = 3*s" by (auto simp add: dvd_def)
hence "q^2 = 3*(s- r^2)" by auto
hence "3 dvd q^2" and "zprime 3" by (auto simp only: zdvd_triv_left zprime_3)
hence "3 dvd q" by (rule_tac p="3" in zprime_zdvd_power)
with p3 have "3 dvd p+q ∧ 3 dvd p-q" by (simp add: zdvd_zdiff zdvd_zadd)
with vw have "3 dvd zgcd(v,w)" by (simp add: zgcd_greatest_iff)
with vwx show False by auto
qed
ultimately have "zgcd((3*3)*(2*r), 3*r^2 + q^2) = 1"
by (simp only: zgcd_zmult_cancel)
thus ?thesis by (auto simp add: mult_ac add_ac)
qed
moreover have rqx: "(18*r)*(q^2 + 3*r^2) = x^3"
proof -
from vwx vwpq have "x^3 = 2*p*(p^2 + 3*q^2)" by auto
also with r have "… = 2*(3*r)*(9*r^2 + 3*q^2)"
by (auto simp add: power2_eq_square)
finally show ?thesis by auto
qed
moreover have triv3: "3 = nat 3 ∧ nat 3 > 1 ∧ 3 ∈ zOdd"
by (unfold zOdd_def, auto)
ultimately have "∃ c. 18*r = c^3"
by (simp only: int_relprime_odd_power_divisors)
then obtain c1 where c1: "c1^3 = 3*(6*r)" by auto
hence "3 dvd c1^3" and "zprime 3" by (auto simp only: zdvd_triv_left zprime_3)
hence "3 dvd c1" by (rule_tac p="3" in zprime_zdvd_power)
with c1 obtain c where c: "3*c^3 = 2*r"
by (auto simp add: power_mult_distrib dvd_def)
from rqx factors_relprime have "zgcd(q^2 + 3*r^2, 18*r) = 1"
and "(q^2 + 3*r^2)*(18*r) = x^3" by (auto simp add: zgcd_commute mult_ac)
with triv3 have "∃ d. q^2 + 3*r^2 = d^3"
by (simp only: int_relprime_odd_power_divisors)
then obtain d where d: "q^2 + 3*r^2 = d^3" by auto
have "d ∈ zOdd"
proof (rule ccontr)
assume "d ∉ zOdd" hence "d ∈ zEven" by (rule not_odd_impl_even)
hence "d^3 ∈ zEven" by (simp only: power_preserves_even)
hence "2 dvd d^3" by (simp add: zEven_def dvd_def)
moreover have "2 dvd 2*(9*r)" by (rule zdvd_triv_left)
ultimately have "2 dvd zgcd(2*(9*r), d^3)" by (simp add: zgcd_greatest_iff)
with d factors_relprime show False by auto
qed
with d qr_relprime have "zgcd(q,r)=1 ∧ q^2 + 3*r^2 = d^3 ∧ d ∈ zOdd"
by simp
hence "is_cube_form q r" by (rule qf3_cube_impl_cube_form)
then obtain a b where "q = a^3 - 9*a*b^2 ∧ r = 3*a^2*b - 3*b^3"
by (unfold is_cube_form_def, auto)
hence ab: "q = a*(a+3*b)*(a- 3*b) ∧ r = b*(a+b)*(a-b)*3"
by (simp add: nat_number ring_simps)
with c have abc: "(2*b)*(a+b)*(a-b) = c^3" by auto
have ab_relprime: "zgcd(a,b)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and za: "z dvd a" and zb: "z dvd b"
with ab have "z dvd q ∧ z dvd r" by (simp add: zdvd_zmult2)
with z qr_relprime show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have ab1: "zgcd(2*b, a+b) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and "z dvd 2*b" and zab: "z dvd a+b"
hence "z dvd 2 ∨ z dvd b" by (simp add: zprime_zdvd_zmult)
moreover
{ assume z2: "z dvd 2"
hence "z ≤ 2" by (simp only: zdvd_imp_le)
with z have "z = 2" by (unfold zprime_def, auto)
with zab have ab2: "2 dvd a+b" by simp
moreover have "2 dvd 2*b" by (rule zdvd_triv_left)
ultimately have "2 dvd a+b+2*b" by (rule zdvd_zadd)
hence "2 dvd a+3*b" by arith
hence "2 dvd (a+3*b)*((a- 3*b)*a)" by (rule zdvd_zmult2)
with ab have qEven: "2 dvd q" by (simp only: mult_ac)
from ab2 have "2 dvd (a+b)*((a-b)*3*b)" by (rule zdvd_zmult2)
with ab have "2 dvd r" by (simp only: mult_ac)
with qEven have "2 dvd zgcd(q,r)" by (simp add: zgcd_greatest_iff)
with qr_relprime have False by auto }
moreover
{ assume zb: "z dvd b"
with zab have "z dvd a+b-b" by (simp only: zdvd_zdiff)
hence "z dvd a" by simp
with zb ab_relprime z have False
by (auto simp add: zgcd1_iff_no_common_primedivisor) }
ultimately show False by auto
qed
have ab2: "zgcd(a+b, a-b) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and zab1: "z dvd a+b" and zab2: "z dvd a-b"
hence "z dvd (a+b)-(a-b)" by (simp only: zdvd_zdiff)
hence "z dvd 2*b" by simp
with zab1 z ab1 show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
have "zgcd(a-b, 2*b) = 1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and z2b: "z dvd 2*b" and zab: "z dvd a-b"
hence "z dvd a-b+2*b" by (simp only: zdvd_zadd)
moreover have "a-b+2*b = a+b" by simp
ultimately have "z dvd a+b" by simp
with z2b z ab1 show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
with abc ab1 ab2 triv3 have "∃ k l m. 2*b = k^3 ∧ a+b = l^3 ∧ a-b = m^3"
by (simp only: int_triple_relprime_odd_power_divisors)
then obtain α1 β γ where a1: "2*b = γ^3 ∧ a-b = α1^3 ∧ a+b = β^3"
by auto
then obtain α where "α = -α1" by auto
-- "show this is a (smaller) solution"
with triv3 a1 have a2: "α^3 = b-a" by (auto simp only: neg_odd_power)
with a1 have "α^3 + β^3 = γ^3" by auto
moreover have "α*β*γ ≠ 0"
proof (rule ccontr, safe)
assume "α * β * γ = 0"
with a1 a2 ab have "r=0" by (auto simp add: power_0_left)
with r vwpq vwx show False by auto
qed
moreover have "γ ∈ zEven"
proof -
have "2*b ∈ zEven" by (simp add: zEven_def)
with a1 have "γ^3 ∈ zEven" by simp
thus ?thesis by (simp only: power_preserves_even)
qed
moreover have "zgcd(α, β)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix z assume z: "zprime z" and za: "z dvd α" and zb: "z dvd β"
hence "z dvd α * α^2 ∧ z dvd β * β^2" by (simp add: zdvd_zmult2)
hence "z dvd α^Suc 2 ∧ z dvd β^Suc 2" by (auto simp only: power_Suc)
with a1 a2 have "z dvd b-a ∧ z dvd a+b" by auto
hence "z dvd -(b-a) ∧ z dvd a+b" by (auto simp only: zdvd_zminus_iff)
with ab2 z show False
by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
moreover have "nat¦γ^3¦ < nat¦x^3¦"
proof -
let ?A = "p^2 + 3*q^2"
from vwx vwpq have "x^3 = 2*p*?A" by auto
also with r have "… = 6*r*?A" by auto
also with ab have "… = 2*b*(9*(a+b)*(a-b)*?A)" by auto
also with a1 have "… = γ^3 *(9*(a+b)*(a-b)*?A)" by auto
finally have eq: "¦x^3¦ = ¦γ^3¦ * ¦9*(a+b)*(a-b)*?A¦"
by (auto simp add: abs_mult)
with x3pos have "¦9*(a+b)*(a-b)*?A¦ > 0" by auto
hence "¦(a+b)*(a-b)*?A¦ ≥ 1" by arith
hence "¦9*(a+b)*(a-b)*?A¦ > 1" by arith
moreover have "¦γ^3¦ > 0"
proof -
from eq have "¦γ^3¦ = 0 ==> ¦x^3¦=0" by auto
with x3pos show ?thesis by auto
qed
ultimately have "¦γ^3¦ * 1 < ¦γ^3¦ * ¦9*(a+b)*(a-b)*?A¦"
by (rule zmult_zless_mono2)
with eq have "¦x^3¦ > ¦γ^3¦" by auto
thus ?thesis by arith
qed
ultimately have ?thesis by auto }
ultimately show ?thesis by auto
qed
thus "∃ y. nat¦y^3¦ < nat¦x^3¦ ∧ ¬ ?Q y" by auto
qed
text {* The theorem. Puts equation in requested shape. *}
theorem fermat3:
assumes ass: "(x::int)^3 + y^3 = z^3"
shows "x*y*z=0"
proof (rule ccontr)
let ?g = "zgcd(x,y)"
let ?c = "z div ?g"
assume xyz0: "x*y*z≠0"
-- "divide out the g.c.d."
hence "x ≠ 0 ∨ y ≠ 0" by simp
then obtain a b where ab: "x = ?g*a ∧ y = ?g*b ∧ zgcd(a,b)=1"
by (frule_tac a="x" in make_zrelprime, auto)
moreover have abc: "?c*?g = z ∧ a^3 + b^3 = ?c^3 ∧ a*b*?c ≠ 0"
proof -
from xyz0 have g0: "?g≠0" by (simp add: zgcd_def gcd_zero)
have zgab: "z^3 = ?g^3 * (a^3+b^3)"
proof -
from ab and ass have "z^3 = (?g*a)^3+(?g*b)^3" by simp
thus ?thesis by (simp only: power_mult_distrib zadd_zmult_distrib2)
qed
have cgz: "?c * ?g = z"
proof -
from zgab have "?g^3 dvd z^3" by simp
hence "?g dvd z" by (simp only: zpower_zdvd_mono)
thus ?thesis by (simp only: mult_ac zdvd_mult_div_cancel)
qed
moreover have "a^3 + b^3 = ?c^3"
proof -
have "?c^3 * ?g^3 = (a^3+b^3)*?g^3"
proof -
have "?c^3 * ?g^3 = (?c*?g)^3" by (simp only: power_mult_distrib)
also with cgz have "… = z^3" by simp
also with zgab have "… = ?g^3*(a^3+b^3)" by simp
finally show ?thesis by simp
qed
with g0 show ?thesis by auto
qed
moreover from ab and xyz0 and cgz have "a*b*?c≠0" by auto
ultimately show ?thesis by simp
qed
-- "make both sides even"
have "∃ u v w. u^3 + v^3 = w^3 ∧ u*v*w≠0 ∧ w ∈ zEven ∧ zgcd(u,v)=1"
proof -
let "?Q u v w" = "u^3 + v^3 = w^3 ∧ u*v*w≠0 ∧ w ∈ zEven ∧ zgcd(u,v)=1"
have "a ∈ zEven ∨ b ∈ zEven ∨ ?c ∈ zEven"
proof (rule ccontr)
assume "¬(a ∈ zEven ∨ b ∈ zEven ∨ ?c ∈ zEven)"
hence aodd: "a ∈ zOdd" and "b ∈ zOdd ∧ ?c ∈ zOdd"
by (auto simp add: odd_iff_not_even)
hence "?c^3 - b^3 ∈ zEven" by (simp only: power_preserves_odd odd_minus_odd)
moreover from abc have "?c^3-b^3 = a^3" by simp
ultimately have "a^3 ∈ zEven" by auto
hence "a ∈ zEven" by (simp only: power_preserves_even)
with aodd show False by (simp add: odd_iff_not_even)
qed
moreover
{ assume "a ∈ zEven"
then obtain u v w where uvwabc: "u = -b ∧ v = ?c ∧ w = a ∧ w ∈ zEven"
by auto
moreover with abc have "u*v*w≠0" by auto
moreover have uvw: "u^3+v^3=w^3"
proof -
from uvwabc have "u^3 + v^3 = (-1*b)^3 + ?c^3" by simp
also have "… = (-1)^3*b^3 + ?c^3" by (simp only: power_mult_distrib)
also have "… = - (b^3) + ?c^3" by (auto simp add: neg_one_odd_power)
also with abc and uvwabc have "… = w^3" by auto
finally show ?thesis by simp
qed
moreover have "zgcd(u,v)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix h::int assume hu: "h dvd u" and "h dvd v" and h: "zprime h"
with uvwabc have "h dvd ?c*?c^2" by (simp only: zdvd_zmult2)
with abc have "h dvd a^3+b^3" by (simp only: cube_square)
moreover from hu uvwabc have "h dvd b*b^2" by (simp add: zdvd_zmult2)
ultimately have "h dvd a^3+b^3-b^3" by (simp only: cube_square zdvd_zdiff)
with h hu uvwabc have "h dvd a ∧ h dvd b" by (auto dest: zprime_zdvd_power)
with h ab show False by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
ultimately have "?Q u v w" by simp
hence ?thesis by auto }
moreover
{ assume "b ∈ zEven"
then obtain u v w where uvwabc: "u = -a ∧ v = ?c ∧ w = b ∧ w ∈ zEven"
by auto
moreover with abc have "u*v*w≠0" by auto
moreover have uvw: "u^3+v^3=w^3"
proof -
from uvwabc have "u^3 + v^3 = (-1*a)^3 + ?c^3" by simp
also have "… = (-1)^3*a^3 + ?c^3" by (simp only: power_mult_distrib)
also have "… = - (a^3) + ?c^3" by (auto simp add: neg_one_odd_power)
also with abc and uvwabc have "… = w^3" by auto
finally show ?thesis by simp
qed
moreover have "zgcd(u,v)=1"
proof (simp only: zgcd1_iff_no_common_primedivisor, clarify)
fix h::int assume hu: "h dvd u" and "h dvd v" and h: "zprime h"
with uvwabc have "h dvd ?c*?c^2" by (simp only: zdvd_zmult2)
with abc have "h dvd a^3+b^3" by (simp only: cube_square)
moreover from hu uvwabc have "h dvd a*a^2" by (simp add: zdvd_zmult2)
ultimately have "h dvd a^3+b^3-a^3" by (simp only: cube_square zdvd_zdiff)
with h hu uvwabc have "h dvd a ∧ h dvd b" by (auto dest: zprime_zdvd_power)
with h ab show False by (auto simp add: zgcd1_iff_no_common_primedivisor)
qed
ultimately have "?Q u v w" by simp
hence ?thesis by auto }
moreover
{ assume "?c ∈ zEven"
then obtain u v w where uvwabc: "u = a ∧ v = b ∧ w = ?c ∧ w ∈ zEven"
by auto
with abc ab have ?thesis by auto }
ultimately show ?thesis by auto
qed
hence "∃ w. ∃ u v. u^3 + v^3 = w^3 ∧ u*v*w ≠ 0 ∧ w ∈ zEven ∧ zgcd(u,v)=1"
by auto
-- "show contradiction using the earlier result"
thus False by (auto simp only: no_rewritten_fermat3)
qed
corollary fermat_mult3:
assumes xyz: "(x::int)^n + y^n = z^n" and n: "3 dvd n"
shows "x*y*z=0"
proof -
from n obtain m where "n = m*3" by (auto simp only: mult_ac dvd_def)
with xyz have "(x^m)^3 + (y^m)^3 = (z^m)^3" by (simp only: power_mult)
hence "(x^m)*(y^m)*(z^m) = 0" by (rule fermat3)
thus ?thesis by auto
qed
end
lemma factor_sum_cubes:
x ^ 3 + y ^ 3 = (x + y) * (x ^ 2 - x * y + y ^ 2)
lemma two_not_abs_cube:
¦x ^ 3¦ = 2 ==> False
lemma no_rewritten_fermat3:
¬ (∃v w. v ^ 3 + w ^ 3 = x ^ 3 ∧ v * w * x ≠ 0 ∧ x ∈ zEven ∧ zgcd (v, w) = 1)
theorem fermat3:
x ^ 3 + y ^ 3 = z ^ 3 ==> x * y * z = 0
corollary fermat_mult3:
[| x ^ n + y ^ n = z ^ n; 3 dvd n |] ==> x * y * z = 0