Theory Fermat4
section ‹Pythagorean triples and Fermat's last theorem, case $n=4$›
theory Fermat4
imports "HOL-Computational_Algebra.Primes"
begin
context
begin
private lemma nat_relprime_power_divisors:
assumes n0: "0 < n" and abc: "(a::nat)*b = c^n" and relprime: "coprime a b"
shows "∃ k. a = k^n"
using assms proof (induct c arbitrary: a b rule: nat_less_induct)
case (1 c)
show ?case
proof (cases "a > 1")
case False
hence "a = 0 ∨ a = 1" by linarith
thus ?thesis using n0 power_one zero_power by (simp only: eq_sym_conv) blast
next
case True
then obtain p where p: "prime p" "p dvd a" using prime_factor_nat[of a] by blast
hence h1: "p dvd (c^n)" using 1(3) dvd_mult2[of p a b] by presburger
hence "(p^n) dvd (c^n)"
using p(1) prime_dvd_power_nat[of p c n] dvd_power_same[of p c n] by blast
moreover have h2: "¬ p dvd b"
using p ‹coprime a b› coprime_common_divisor_nat [of a b p] by auto
hence "¬ (p^n) dvd b" using n0 p(1)
by (auto intro: dvd_trans dvd_power[of n p])
ultimately have "(p^n) dvd a"
using "1.prems" p(1) prime_elem_divprod_pow [of p a b n] by simp
then obtain a' c' where ac: "a = p^n * a'" "c = p * c'"
using h1 dvdE[of "p^n" a] dvdE[of p c] prime_dvd_power_nat[of p c n] p(1) by meson
hence "p^n * (a' * b) = p^n * c'^n" using 1(3)
by (simp add: power_mult_distrib semiring_normalization_rules(18))
hence "a' * b = c'^n" using p(1) by auto
moreover have "coprime a' b" using 1(4) ac(1)
by (simp add: ac_simps)
moreover have "0 < b" "0 < a" using h2 dvd_0_right gr0I True by fastforce+
then have "0 < c" "1 < p"
using p ‹a * b = c ^ n› n0 nat_0_less_mult_iff [of a b] n0
by (auto simp add: prime_gt_Suc_0_nat)
hence "c' < c" using ac(2) by simp
ultimately obtain k where "a' = k^n" using 1(1) n0 by presburger
hence "a = (p*k)^n" using ac(1) by (simp add: power_mult_distrib)
thus ?thesis by blast
qed
qed
private lemma int_relprime_power_divisors:
assumes "0 < n" and "0 ≤ a" and "0 ≤ b" and "(a::int) * b = c ^ n" and "coprime a b"
shows "∃k. a = k^n"
proof (cases "a = 0")
case False
from ‹0 ≤ a› ‹0 ≤ b› ‹a * b = c ^ n›[symmetric] have "0 ≤ c ^ n"
by simp
hence "c^n = ¦c¦^n" using power_even_abs[of n c] zero_le_power_eq[of c n] by linarith
hence "a * b = ¦c¦^n" using assms(4) by presburger
hence "nat a * nat b = (nat ¦c¦)^n" using nat_mult_distrib[of "a" "b"] assms(2)
by (simp add: nat_power_eq)
moreover have "0 ≤ b" using assms mult_less_0_iff[of a b] False by auto
with ‹0 ≤ a› ‹coprime a b› have "coprime (nat a) (nat b)"
using coprime_nat_abs_left_iff [of a "nat b"] by simp
ultimately have "∃ k. nat a = k^n"
using nat_relprime_power_divisors[of n "nat a" "nat b" "nat ¦c¦"] assms(1) by blast
thus ?thesis using assms(2) int_nat_eq[of "a"] by fastforce
qed (simp add: zero_power[of n] assms(1))
text ‹Proof of Fermat's last theorem for the case $n=4$: $$\forall x,y,z:~x^4 + y^4 = z^4 \Longrightarrow xyz=0.$$›
private lemma nat_power2_diff: "a ≥ (b::nat) ⟹ (a-b)^2 = a^2 + b^2 - 2*a*b"
proof -
assume a_ge_b: "a ≥ b"
hence a2_ge_b2: "a^2 ≥ b^2" by (simp only: power_mono)
from a_ge_b have ab_ge_b2: "a*b ≥ b^2" by (simp add: power2_eq_square)
have "b*(a-b) + (a-b)^2 = a*(a-b)" by (simp add: power2_eq_square diff_mult_distrib)
also have "… = a*b + a^2 + (b^2 - b^2) - 2*a*b"
by (simp add: diff_mult_distrib2 power2_eq_square)
also with a2_ge_b2 have "… = a*b + (a^2 - b^2) + b^2 - 2*a*b"
by (simp add: power2_eq_square)
also with ab_ge_b2 have "… = (a*b - b^2) + a^2 + b^2 - 2*a*b" by auto
also have "… = b*(a-b) + a^2 + b^2 - 2*a*b"
by (simp only: diff_mult_distrib2 power2_eq_square mult.commute)
finally show ?thesis by arith
qed
private lemma nat_power_le_imp_le_base: "⟦ n ≠ 0; a^n ≤ b^n ⟧ ⟹ (a::nat) ≤ b"
by simp
private lemma nat_power_inject_base: "⟦ n ≠ 0; a^n = b^n ⟧ ⟹ (a::nat) = b"
proof -
assume "n ≠ 0" and ab: "a^n = b^n"
then obtain m where "n = Suc m" by (frule_tac n="n" in not0_implies_Suc, auto)
with ab have "a^Suc m = b^Suc m" and "a ≥ 0" and "b ≥ 0" by auto
thus ?thesis by (rule power_inject_base)
qed
subsection ‹Parametrisation of Pythagorean triples (over $\mathbb{N}$ and $\mathbb{Z}$)›
private theorem nat_euclid_pyth_triples:
assumes abc: "(a::nat)^2 + b^2 = c^2" and ab_relprime: "coprime a b" and aodd: "odd a"
shows "∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ c = p^2 + q^2 ∧ coprime p q"
proof -
have two0: "(2::nat) ≠ 0" by simp
from abc have a2cb: "a^2 = c^2 - b^2" by arith
have a2factor: "a^2 = (c-b)*(c+b)"
proof -
have "c*b - c*b = 0" by simp
with a2cb have "a^2 = c*c + c*b - c*b - b*b" by (simp add: power2_eq_square)
also have "… = c*(c+b) - b*(c+b)"
by (simp add: add_mult_distrib2 add_mult_distrib mult.commute)
finally show ?thesis by (simp only: diff_mult_distrib)
qed
have a_nonzero: "a ≠ 0"
proof (rule ccontr)
assume "¬ a ≠ 0" hence "a = 0" by simp
with aodd have "odd (0::nat)" by simp
thus False by simp
qed
have b_less_c: "b < c"
proof -
from abc have "b^2 ≤ c^2" by linarith
with two0 have "b ≤ c" by (rule_tac n="2" in nat_power_le_imp_le_base)
moreover have"b ≠ c"
proof
assume "b=c" with a2cb have "a^2 = 0" by simp
with a_nonzero show False by (simp add: power2_eq_square)
qed
ultimately show ?thesis by auto
qed
hence b2_le_c2: "b^2 ≤ c^2" by (simp add: power_mono)
have bc_relprime: "coprime b c"
proof -
from b2_le_c2 have cancelb2: "c^2-b^2+b^2 = c^2" by auto
let ?g = "gcd b c"
have "?g^2 = gcd (b^2) (c^2)" by simp
with cancelb2 have "?g^2 = gcd (b^2) (c^2-b^2+b^2)" by simp
hence "?g^2 = gcd (b^2) (c^2-b^2)" using gcd_add2[of "b^2" "c^2 - b^2"]
by (simp add: algebra_simps del: gcd_add1)
with a2cb have "?g^2 dvd a^2" by (simp only: gcd_dvd2)
hence "?g dvd a ∧ ?g dvd b" by simp
hence "?g dvd gcd a b" by (simp only: gcd_greatest)
with ab_relprime show ?thesis
by (simp add: ac_simps gcd_eq_1_imp_coprime)
qed
have p2: "prime (2::nat)" by simp
have factors_odd: "odd (c-b) ∧ odd (c+b)"
proof (auto simp only: ccontr)
assume "even (c-b)"
with a2factor have "2 dvd a^2" by (simp only: dvd_mult2)
with p2 have "2 dvd a" by auto
with aodd show False by simp
next
assume "even (c+b)"
with a2factor have "2 dvd a^2" by (simp only: dvd_mult)
with p2 have "2 dvd a" by auto
with aodd show False by simp
qed
have cb1: "c-b + (c+b) = 2*c"
proof -
have "c-b + (c+b) = ((c-b)+b)+c" by simp
also with b_less_c have "… = (c+b-b)+c" by (simp only: diff_add_assoc2)
also have "… = c+c" by simp
finally show ?thesis by simp
qed
have cb2: "2*b + (c-b) = c+b"
proof -
have "2*b + (c-b) = b+b + (c - b)" by auto
also have "… = b + ((c-b)+b)" by simp
also with b_less_c have " … = b + (c+b-b)" by (simp only: diff_add_assoc2)
finally show ?thesis by simp
qed
have factors_relprime: "coprime (c-b) (c+b)"
proof -
let ?g = "gcd (c-b) (c+b)"
have cb1: "c-b + (c+b) = 2*c"
proof -
have "c-b + (c+b) = ((c-b)+b)+c" by simp
also with b_less_c have "… = (c+b-b)+c" by (simp only: diff_add_assoc2)
also have "… = c+c" by simp
finally show ?thesis by simp
qed
have "?g = gcd (c-b + (c+b)) (c+b)" by simp
with cb1 have "?g = gcd (2*c) (c+b)" by (rule_tac a="c-b + (c+b)" in back_subst)
hence g2c: "?g dvd 2*c" by (simp only: gcd_dvd1)
have "gcd (c-b) (2*b + (c-b)) = gcd (c-b) (2*b)"
using gcd_add2[of "c - b" "2*b + (c - b)"] by (simp add: algebra_simps)
with cb2 have "?g = gcd (c-b) (2*b)" by (rule_tac a="2*b + (c-b)" in back_subst)
hence g2b: "?g dvd 2*b" by (simp only: gcd_dvd2)
with g2c have "?g dvd 2 * gcd b c" by (simp only: gcd_greatest gcd_mult_distrib_nat)
with bc_relprime have "?g dvd 2" by simp
moreover have "?g ≠ 0"
using b_less_c by auto
ultimately have "1 ≤ ?g" "?g ≤ 2"
by (simp_all add: dvd_imp_le)
then have g1or2: "?g = 2 ∨ ?g = 1"
by arith
moreover have "?g ≠ 2"
proof
assume "?g = 2"
moreover have "?g dvd c - b"
by simp
ultimately show False
using factors_odd by simp
qed
ultimately show ?thesis
by (auto intro: gcd_eq_1_imp_coprime)
qed
from a2factor have "(c-b)*(c+b) = a^2" and "(2::nat) >1" by auto
with factors_relprime have "∃ k. c-b = k^2"
by (simp only: nat_relprime_power_divisors)
then obtain r where r: "c-b = r^2" by auto
from a2factor have "(c+b)*(c-b) = a^2" and "(2::nat) >1" by auto
with factors_relprime have "∃ k. c+b = k^2"
by (simp only: nat_relprime_power_divisors ac_simps)
then obtain s where s: "c+b = s^2" by auto
have rs_odd: "odd r ∧ odd s"
proof (auto dest: ccontr)
assume "even r" hence "2 dvd r"by presburger
with r have "2 dvd (c-b)" by (simp only: power2_eq_square dvd_mult)
with factors_odd show False by auto
next
assume "even s" hence "2 dvd s" by presburger
with s have "2 dvd (c+b)" by (simp only: power2_eq_square dvd_mult)
with factors_odd show False by auto
qed
obtain m where m: "m = s-r" by simp
from r s have "r^2 ≤ s^2" by arith
with two0 have "r ≤ s" by (rule_tac n="2" in nat_power_le_imp_le_base)
with m have m2: "s = r + m" by simp
have "even m"
proof (rule ccontr)
assume "odd m" with rs_odd and m2 show False by presburger
qed
then obtain q where "m = 2*q" ..
with m2 have q: "s = r + 2*q" by simp
obtain p where p: "p = r+q" by simp
have c: "c = p^2 + q^2"
proof -
from cb1 and r and s have "2*c = r^2 + s^2" by simp
also with q have "… = 2*r^2+(2*q)^2+2*r*(2*q)" by algebra
also have "… = 2*r^2+2^2*q^2+2*2*q*r" by (simp add: power_mult_distrib)
also have "… = 2*(r^2+2*q*r+q^2)+2*q^2" by (simp add: power2_eq_square)
also with p have "… = 2*p^2+2*q^2" by algebra
finally show ?thesis by auto
qed
moreover have b: "b = 2*p*q"
proof -
from cb2 and r and s have "2*b = s^2 - r^2" by arith
also with q have "… = (2*q)^2 + 2*r*(2*q)" by (simp add: power2_sum)
also with p have "… = 4*q*p" by (simp add: power2_eq_square add_mult_distrib2)
finally show ?thesis by auto
qed
moreover have a: "a = p^2 - q^2"
proof -
from p have "p≥q" by simp
hence p2_ge_q2: "p^2 ≥ q^2" by (simp only: power_mono)
from a2cb and b and c have "a^2 = (p^2 + q^2)^2 - (2*p*q)^2" by simp
also have "… = (p^2)^2 + (q^2)^2 - 2*(p^2)*(q^2)"
by (auto simp add: power2_sum power_mult_distrib ac_simps)
also with p2_ge_q2 have "… = (p^2 - q^2)^2" by (simp only: nat_power2_diff)
finally have "a^2 = (p^2 - q^2)^2" by simp
with two0 show ?thesis by (rule_tac n="2" in nat_power_inject_base)
qed
moreover have "coprime p q"
proof -
let ?k = "gcd p q"
have "?k dvd p ∧ ?k dvd q" by simp
with b and a have "?k dvd a ∧ ?k dvd b"
by (simp add: power2_eq_square)
hence "?k dvd gcd a b" by (simp only: gcd_greatest)
with ab_relprime show ?thesis
by (auto intro: gcd_eq_1_imp_coprime)
qed
ultimately show ?thesis by auto
qed
text ‹Now for the case of integers. Based on \textit{nat-euclid-pyth-triples}.›
private corollary int_euclid_pyth_triples: "⟦ coprime (a::int) b; odd a; a^2 + b^2 = c^2 ⟧
⟹ ∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ ¦c¦ = p^2 + q^2 ∧ coprime p q"
proof -
assume ab_rel: "coprime a b" and aodd: "odd a" and abc: "a^2 + b^2 = c^2"
let ?a = "nat¦a¦"
let ?b = "nat¦b¦"
let ?c = "nat¦c¦"
have ab2_pos: "a^2 ≥ 0 ∧ b^2 ≥ 0" by simp
hence "nat(a^2) + nat(b^2) = nat(a^2 + b^2)" by (simp only: nat_add_distrib)
with abc have "nat(a^2) + nat(b^2) = nat(c^2)" by presburger
hence "nat(¦a¦^2) + nat(¦b¦^2) = nat(¦c¦^2)" by simp
hence new_abc: "?a^2 + ?b^2 = ?c^2"
by (simp only: nat_mult_distrib power2_eq_square nat_add_distrib)
moreover from ab_rel have new_ab_rel: "coprime ?a ?b"
by (simp add: gcd_int_def)
moreover have new_a_odd: "odd ?a" using aodd
by simp
ultimately have
"∃ p q. ?a = p^2-q^2 ∧ ?b = 2*p*q ∧ ?c = p^2 + q^2 ∧ coprime p q"
by (rule_tac a="?a" and b = "?b" and c="?c" in nat_euclid_pyth_triples)
then obtain m and n where mn:
"?a = m^2-n^2 ∧ ?b = 2*m*n ∧ ?c = m^2 + n^2 ∧ coprime m n" by auto
have "n^2 ≤ m^2"
proof (rule ccontr)
assume "¬ n^2 ≤ m^2"
with mn have "?a = 0" by auto
with new_a_odd show False by simp
qed
moreover from mn have "int ?a = int(m^2 - n^2)" and "int ?b = int(2*m*n)"
and "int ?c = int(m^2 + n^2)" by auto
ultimately have "¦a¦ = int(m^2) - int(n^2)" and "¦b¦ = int(2*m*n)"
and "¦c¦ = int(m^2) + int(n^2)" by (simp add: of_nat_diff)+
hence absabc: "¦a¦ = (int m)^2 - (int n)^2 ∧ ¦b¦ = 2*(int m)*int n
∧ ¦c¦ = (int m)^2 + (int n)^2" by (simp add: power2_eq_square)
from mn have mn_rel: "coprime (int m) (int n)"
by (simp add: gcd_int_def)
show "∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ ¦c¦ = p^2 + q^2 ∧ coprime p q"
(is "∃ p q. ?Q p q")
proof (cases)
assume apos: "a ≥ 0" then obtain p where p: "p = int m" by simp
hence "∃ q. ?Q p q"
proof (cases)
assume bpos: "b ≥ 0" then obtain q where "q = int n" by simp
with p apos bpos absabc mn_rel have "?Q p q" by simp
thus ?thesis by (rule exI)
next
assume "¬ b≥0" hence bneg: "b<0" by simp
then obtain q where "q = - int n" by simp
with p apos bneg absabc mn_rel have "?Q p q" by simp
thus ?thesis by (rule exI)
qed
thus ?thesis by (simp only: exI)
next
assume "¬ a≥0" hence aneg: "a<0" by simp
then obtain p where p: "p = int n" by simp
hence "∃ q. ?Q p q"
proof (cases)
assume bpos: "b ≥ 0" then obtain q where "q = int m" by simp
with p aneg bpos absabc mn_rel have "?Q p q"
by (simp add: ac_simps)
thus ?thesis by (rule exI)
next
assume "¬ b≥0" hence bneg: "b<0" by simp
then obtain q where "q = - int m" by simp
with p aneg bneg absabc mn_rel have "?Q p q"
by (simp add: ac_simps)
thus ?thesis by (rule exI)
qed
thus ?thesis by (simp only: exI)
qed
qed
subsection ‹Fermat's last theorem, case $n=4$›
text ‹Core of the proof. Constructs a smaller solution over $\mathbb{Z}$ of $$a^4+b^4=c^2\,\land\,coprime\,a\,b\,\land\,abc\ne 0\,\land\,a~{\rm odd}.$$›
private lemma smaller_fermat4:
assumes abc: "(a::int)^4+b^4=c^2" and abc0: "a*b*c ≠ 0" and aodd: "odd a"
and ab_relprime: "coprime a b"
shows
"∃ p q r. (p^4+q^4=r^2 ∧ p*q*r ≠ 0 ∧ odd p ∧ coprime p q ∧ r^2 < c^2)"
proof -
from ab_relprime have a2b2relprime: "coprime (a^2) (b^2)"
by simp
moreover from aodd have "odd (a^2)" by presburger
moreover from abc have "(a^2)^2 + (b^2)^2 = c^2" by simp
ultimately obtain u and v where uvabc:
"a^2 = u^2-v^2 ∧ b^2 = 2*u*v ∧ ¦c¦ = u^2 + v^2 ∧ coprime u v"
by (frule_tac a="a^2" in int_euclid_pyth_triples, auto)
with abc0 have uv0: "u≠0 ∧ v≠0" by auto
have av_relprime: "coprime a v"
proof -
have "gcd a v dvd gcd (a^2) v" by (simp add: power2_eq_square)
moreover from uvabc have "gcd v (a^2) dvd gcd (b^2) (a^2)"
by simp
with a2b2relprime have "gcd (a^2) v dvd (1::int)"
by (simp add: ac_simps)
ultimately have "gcd a v dvd 1"
by (rule dvd_trans)
then show ?thesis
by (simp add: gcd_eq_1_imp_coprime)
qed
from uvabc have "a^2 + v^2 = u^2" by simp
with av_relprime and aodd obtain k l where
klavu: "a = k^2-l^2 ∧ v = 2*k*l ∧ ¦u¦ = k^2+l^2" and kl_rel: "coprime k l"
by (frule_tac a="a" in int_euclid_pyth_triples, auto)
from uvabc have "even (b^2)" by simp
hence "even b" by simp
then obtain m where bm: "b = 2*m" using evenE by blast
have "¦k¦*¦l¦*¦k^2+l^2¦ = m^2"
proof -
from bm have "4*m^2 = b^2" by (simp only: power2_eq_square ac_simps)
also have "… = ¦b^2¦" by simp
also with uvabc have "… = 2*¦v¦*¦¦u¦¦" by (simp add: abs_mult)
also with klavu have "… = 2*¦2*k*l¦*¦k^2+l^2¦" by simp
also have "… = 4*¦k¦*¦l¦*¦k^2+l^2¦" by (auto simp add: abs_mult)
finally show ?thesis by simp
qed
moreover have "(2::nat) > 1" by auto
moreover from kl_rel have "coprime ¦k¦ ¦l¦" by simp
moreover have "coprime ¦l¦ (¦k^2+l^2¦)"
proof -
from kl_rel have "coprime (k*k) l"
by simp
hence "coprime (k*k+l*l) l" using gcd_add_mult [of l l "k*k"]
by (simp add: ac_simps gcd_eq_1_imp_coprime)
hence "coprime l (k^2+l^2)"
by (simp add: power2_eq_square ac_simps)
thus ?thesis by simp
qed
moreover have "coprime ¦k^2+l^2¦ ¦k¦"
proof -
from kl_rel have "coprime l k"
by (simp add: ac_simps)
hence "coprime (l*l) k"
by simp
hence "coprime (l*l+k*k) k" using gcd_add_mult[of k k "l*l"]
by (simp add: ac_simps gcd_eq_1_imp_coprime)
hence "coprime (k^2+l^2) k"
by (simp add: power2_eq_square ac_simps)
thus ?thesis by simp
qed
ultimately have "∃ x y z. ¦k¦ = x^2 ∧ ¦l¦ = y^2 ∧ ¦k^2+l^2¦ = z^2"
using int_relprime_power_divisors[of 2 "¦k¦" "¦l¦ * ¦k⇧2 + l⇧2¦" m]
int_relprime_power_divisors[of 2 "¦l¦" "¦k¦ * ¦k⇧2 + l⇧2¦" m]
int_relprime_power_divisors[of 2 "¦k⇧2 + l⇧2¦" "¦k¦*¦l¦" m]
by (simp_all add: ac_simps)
then obtain α β γ where albega:
"¦k¦ = α^2 ∧ ¦l¦ = β^2 ∧ ¦k^2+l^2¦ = γ^2"
by auto
have "k^2 = α^4"
proof -
from albega have "¦k¦^2 = (α^2)^2" by simp
thus ?thesis by simp
qed
moreover have "l^2 = β^4"
proof -
from albega have "¦l¦^2 = (β^2)^2" by simp
thus ?thesis by simp
qed
moreover have gamma2: "k^2 + l^2 = γ^2"
proof -
have "k^2 ≥ 0 ∧ l^2 ≥ 0" by simp
with albega show ?thesis by auto
qed
ultimately have newabc: "α^4 + β^4 = γ^2" by auto
from uv0 klavu albega have albega0: "α * β * γ ≠ 0" by auto
have alphabeta_relprime: "coprime α β"
proof (rule classical)
let ?g = "gcd α β"
assume "¬ coprime α β"
then have gnot1: "?g ≠ 1"
by (auto intro: gcd_eq_1_imp_coprime)
have "?g > 1"
proof -
have "?g ≠ 0"
proof
assume "?g=0"
hence "nat ¦α¦=0" by simp
hence "α=0" by arith
with albega0 show False by simp
qed
hence "?g>0" by auto
with gnot1 show ?thesis by linarith
qed
moreover have "?g dvd gcd k l"
proof -
have "?g dvd α ∧ ?g dvd β" by auto
with albega have "?g dvd ¦k¦ ∧ ?g dvd ¦l¦"
by (simp add: power2_eq_square mult.commute)
hence "?g dvd k ∧ ?g dvd l" by simp
thus ?thesis by simp
qed
ultimately have "gcd k l ≠ 1" by fastforce
with kl_rel show ?thesis by auto
qed
have "∃ p q. p^4 + q^4 = γ^2 ∧ p*q*γ ≠ 0 ∧ odd p ∧ coprime p q"
proof -
have "odd α ∨ odd β"
proof (rule ccontr)
assume "¬ (odd α ∨ odd β)"
hence "even α ∧ even β" by simp
then have "2 dvd α ∧ 2 dvd β" by simp
then have "2 dvd gcd α β" by simp
with alphabeta_relprime show False by auto
qed
moreover
{ assume "odd α"
with newabc albega0 alphabeta_relprime obtain p q where
"p=α ∧ q=β ∧ p^4 + q^4 = γ^2 ∧ p*q*γ ≠ 0 ∧ odd p ∧ coprime p q"
by auto
hence ?thesis by auto }
moreover
{ assume "odd β"
with newabc albega0 alphabeta_relprime obtain p q where
"q=α ∧ p=β ∧ p^4 + q^4 = γ^2 ∧ p*q*γ ≠ 0 ∧ odd p ∧ coprime p q"
by (auto simp add: ac_simps)
hence ?thesis by auto }
ultimately show ?thesis by auto
qed
moreover have "γ^2 < c^2"
proof -
from gamma2 klavu have "γ^2 ≤ ¦u¦" by simp
also have h1: "… ≤ ¦u¦^2" using self_le_power[of "¦u¦" 2] uv0 by auto
also have h2: "… ≤ u^2" by simp
also have h3: "… < u^2 + v^2"
proof -
from uv0 have v2non0: "0 ≠ v^2"
by simp
have "0 ≤ v^2" by (rule zero_le_power2)
with v2non0 have "0 < v^2" by (auto simp add: less_le)
thus ?thesis by auto
qed
also with uvabc have "… ≤ ¦c¦" by auto
also have "… ≤ ¦c¦^2" using self_le_power[of "¦c¦" 2] h1 h2 h3 uvabc by linarith
also have "… ≤ c^2" by simp
finally show ?thesis by simp
qed
ultimately show ?thesis by auto
qed
text ‹Show that no solution exists, by infinite descent of $c^2$.›
private lemma no_rewritten_fermat4:
"¬ (∃ (a::int) b. (a^4 + b^4 = c^2 ∧ a*b*c ≠ 0 ∧ odd a ∧ coprime a b))"
proof (induct c rule: infinite_descent0_measure[where V="λc. nat(c^2)"])
case (0 x)
have "x^2 ≥ 0" by (rule zero_le_power2)
with 0 have "int(nat(x^2)) = 0" by auto
hence "x = 0" by auto
thus ?case by auto
next
case (smaller x)
then obtain a b where "a^4 + b^4 = x^2" and "a*b*x ≠ 0"
and "odd a" and "coprime a b" by auto
hence "∃ p q r. (p^4+q^4=r^2 ∧ p*q*r ≠ 0 ∧ odd p
∧ coprime p q ∧ r^2 < x^2)" by (rule smaller_fermat4)
then obtain p q r where pqr: "p^4 + q^4 = r^2 ∧ p*q*r ≠ 0 ∧ odd p
∧ coprime p q ∧ r^2 < x^2" by auto
have "r^2 ≥ 0" and "x^2 ≥ 0" by (auto simp only: zero_le_power2)
hence "int(nat(r^2)) = r^2 ∧ int(nat(x^2)) = x^2" by auto
with pqr have "int(nat(r^2)) < int(nat(x^2))" by auto
hence "nat(r^2) < nat(x^2)" by presburger
with pqr show ?case by auto
qed
text ‹The theorem. Puts equation in requested shape.›
theorem fermat_4:
assumes ass: "(x::int)^4 + y^4 = z^4"
shows "x*y*z=0"
proof (rule ccontr)
let ?g = "gcd x y"
let ?c = "(z div ?g)^2"
assume xyz0: "x*y*z ≠ 0"
hence "x ≠ 0 ∨ y ≠ 0" by simp
then obtain a b where ab: "x = ?g*a ∧ y = ?g*b ∧ coprime a b"
using gcd_coprime_exists[of x y] by (auto simp: mult.commute)
moreover have abc: "a^4 + b^4 = ?c^2 ∧ a*b*?c ≠ 0"
proof -
have zgab: "z^4 = ?g^4 * (a^4+b^4)"
proof -
from ab ass have "z^4 = (?g*a)^4+(?g*b)^4" by simp
thus ?thesis by (simp only: power_mult_distrib distrib_left)
qed
have cgz: "z^2 = ?c * ?g^2"
proof -
from zgab have "?g^4 dvd z^4" by simp
hence "?g dvd z" by simp
hence "(z div ?g)*?g = z" by (simp only: ac_simps dvd_mult_div_cancel)
with ab show ?thesis by (auto simp only: power2_eq_square ac_simps)
qed
with xyz0 have c0: "?c≠0" by (auto simp add: power2_eq_square)
from xyz0 have g0: "?g≠0" by simp
have "a^4 + b^4 = ?c^2"
proof -
have "?c^2 * ?g^4 = (a^4+b^4)*?g^4"
proof -
have "?c^2 * ?g^4 = (?c*?g^2)^2" by algebra
also with cgz have "… = (z^2)^2" by simp
also have "… = z^4" by algebra
also with zgab have "… = ?g^4*(a^4+b^4)" by simp
finally show ?thesis by simp
qed
with g0 show ?thesis by auto
qed
moreover from ab xyz0 c0 have "a*b*?c≠0" by auto
ultimately show ?thesis by simp
qed
have "∃ p q. p^4 + q^4 = ?c^2 ∧ p*q*?c≠0 ∧ odd p ∧ coprime p q"
proof -
have "odd a ∨ odd b"
proof (rule ccontr)
assume "¬(odd a ∨ odd b)"
hence "2 dvd a ∧ 2 dvd b" by simp
hence "2 dvd gcd a b" by simp
with ab show False by auto
qed
moreover
{ assume "odd a"
then obtain p q where "p = a" and "q = b" and "odd p" by simp
with ab abc have ?thesis by auto }
moreover
{ assume "odd b"
then obtain p q where "p = b" and "q = a" and "odd p" by simp
with ab abc have
"p^4 + q^4 = ?c^2 ∧ p*q*?c≠0 ∧ odd p ∧ coprime p q"
by (simp add: ac_simps)
hence ?thesis by auto }
ultimately show ?thesis by auto
qed
thus False by (auto simp only: no_rewritten_fermat4)
qed
corollary fermat_mult4:
assumes xyz: "(x::int)^n + y^n = z^n" and n: "4 dvd n"
shows "x*y*z=0"
proof -
from n obtain m where "n = m*4" by (auto simp only: ac_simps dvd_def)
with xyz have "(x^m)^4 + (y^m)^4 = (z^m)^4" by (simp only: power_mult)
hence "(x^m)*(y^m)*(z^m) = 0" by (rule fermat_4)
thus ?thesis by auto
qed
end
end