Theory Fermat4

(*  Title:      Fermat4.thy
    Author:     Roelof Oosterhuis
                2007  Rijksuniversiteit Groningen
*)

header {* Pythagorean triples and Fermat's last theorem, case $n=4$ *}

theory Fermat4
  imports InfDesc IntNatAux Parity
begin

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.$$ *}

lemma even_eq_two_dvd: "even (r::nat) = (2 dvd r)"
  apply safe
  apply (simp only: even_nat_equiv_def2, arith)
  apply (auto simp add: even_def dvd_eq_mod_eq_0)
done

lemma nat_power2_add: "((a::nat)+b)^2 = a^2 + b^2 + 2*a*b"
proof -
  have "(a+b)^2 = (a+b)*(a+b)" by (rule power2_eq_square)
  also have "… = a^2 + 2*(a*b) + b^2" 
    by (simp only: add_mult_distrib add_mult_distrib2 mult_commute power2_eq_square)
  finally show ?thesis by simp
qed
(* 
NB: this lemma is quite slow, maybe use more steps *)
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
  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

lemma nat_power_le_imp_le_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 ≥ 0" and "a^Suc m ≤ b^Suc m" and "b ≥ 0" by auto
  thus ?thesis by (rule_tac n="m" in power_le_imp_le_base)
qed
  
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}$) *}

theorem nat_euclid_pyth_triples:
  assumes abc: "a^2 + b^2 = c^2" and ab_relprime: "gcd(a,b)=1" and aodd: "odd a"
  shows "∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ c = p^2 + q^2 ∧ gcd(p,q)=1"
proof -
  have two0: "(2::nat) ≠ 0" by simp
  from abc have a2cb: "a^2 = c^2 - b^2" by arith
  -- "factor $a^2$ in coprime factors $(c-b)$ and $(c+b)$; hence both are squares"
  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 auto
    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: "gcd(b,c) = 1"
  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 only: gcd_power_distrib)
    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)" by simp
    with a2cb have "?g^2 dvd a^2" by (simp only: gcd_dvd2)
    hence "?g dvd a ∧ ?g dvd b" by (simp add: nat_power_dvd_mono gcd_dvd1)
    hence "?g dvd gcd(a,b)" by (simp only: gcd_greatest)
    with ab_relprime show ?thesis by auto
  qed
  have p2: "prime 2" by (rule two_is_prime)
  have factors_odd: "odd (c-b) ∧ odd (c+b)"
  proof (auto simp only: ccontr)
    assume "even (c-b)" hence "2 dvd c-b" by (simp only: even_eq_two_dvd)
    with a2factor have "2 dvd a^2" by (simp only: dvd_mult2)
    with p2 have "2 dvd a" by (rule prime_dvd_power)
    hence "even a" by (simp only: even_eq_two_dvd)
    with aodd show False by simp
  next
    assume "even (c+b)" hence "2 dvd c+b" by (simp only: even_eq_two_dvd)
    with a2factor have "2 dvd a^2" by (simp only: dvd_mult)
    with p2 have "2 dvd a" by (rule prime_dvd_power)
    hence "even a" by (simp only: even_eq_two_dvd)
    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: "gcd(c-b,c+b) =1"
  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)" by simp
    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_distrib2)
    with bc_relprime have "?g dvd 2" by simp
    with p2 have g1or2: "?g = 2 ∨ ?g = 1" by (unfold prime_def, auto)
    thus ?thesis
    proof (auto)
      assume "?g = 2" hence "2 dvd ?g" by simp
      hence "2 dvd c-b" by (simp add: gcd_dvd1)
      with factors_odd show False by (simp add: even_eq_two_dvd)
    qed
  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 gcd_commute)
  then obtain s where s: "c+b = s^2" by auto
  -- "now $p := (s+r)/2$ and $q := (s-r)/2$ is our solution"
  have rs_odd: "odd r ∧ odd s"
  proof (auto dest: ccontr)
    assume "even r" hence "2 dvd r" by (simp only: even_eq_two_dvd )
    with r have  "2 dvd (c-b)" by (simp only: power2_eq_square dvd_mult)
    hence "even (c-b)" by (simp only: even_eq_two_dvd)
    with factors_odd show False by simp
  next
    assume "even s" hence "2 dvd s" by (simp only: even_eq_two_dvd)
    with s have "2 dvd (c+b)" by (simp only: power2_eq_square dvd_mult)
    hence "even (c+b)" by (simp only: even_eq_two_dvd)
    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 auto
  qed
  hence "2 dvd m" by (simp only: even_eq_two_dvd)
  then obtain q where "m = 2*q" by (auto simp add: dvd_def)
  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 (simp add: nat_power2_add)
    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 (simp add: nat_power2_add)
    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: nat_power2_add)
    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: nat_power2_add power_mult_distrib mult_ac)
    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 "gcd(p,q)=1"
  proof -
    let ?k = "gcd(p,q)"
    have "?k dvd p ∧ ?k dvd q" by (simp add: gcd_dvd1 gcd_dvd2)
    with b and a have "?k dvd a ∧ ?k dvd b" 
      by (simp add: dvd_mult power2_eq_square dvd_diff)
    hence "?k dvd gcd(a,b)" by (simp only: gcd_greatest)
    with ab_relprime show ?thesis by auto
  qed
  ultimately show ?thesis by auto
qed

text {* Now for the case of integers. Based on \textit{nat-euclid-pyth-triples}. *}
  
corollary int_euclid_pyth_triples: "[| zgcd(a,b) = 1; a ∈ zOdd; a^2 + b^2 = c^2 |]
  ==> ∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ ¦c¦ = p^2 + q^2 ∧ zgcd(p,q)=1"
proof -
  assume ab_rel: "zgcd(a,b) = 1" and aodd: "a ∈ zOdd" 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 add: zero_le_power2)
  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 (auto simp add: power2_eq_square abs_power2_distrib)
  hence "nat(¦a¦^2) + nat(¦b¦^2) = nat(¦c¦^2)"
    by (simp add: abs_power2_distrib)
  hence new_abc: "?a^2 + ?b^2 = ?c^2"
    by (simp add: nat_mult_distrib power2_eq_square nat_add_distrib)
  moreover from ab_rel have new_ab_rel: "gcd(?a,?b)=1" by (simp add: zgcd_def)
  moreover have new_a_odd: "odd ?a" 
  proof -
    from aodd obtain k where k: "a = 2*k+1" by (unfold zOdd_def, auto)
    show ?thesis
    proof (cases)
      assume apos: "a ≥ 0" with k have "k≥0" by auto
      with k and apos have "?a = 2*(nat k)+1" by arith
      thus ?thesis by simp
    next
      assume "¬ a≥0" hence aneg: "a<0" by simp
      with k have k2: "2*(-1-k)≥ 0" by simp
      have aux2: "(2::int) ≥ 0" by simp
      have aux1: "(1::int) ≥ 0" by simp
      from k and aneg have "¦a¦ = 2*(-1-k) + 1" by simp
      with k2 aux1 have "?a = nat (2*(-1-k)) + nat 1"
        by (simp only: nat_add_distrib)
      with aux2 have "?a = (nat 2)*nat(-1-k) + nat 1"
        by (simp only: nat_mult_distrib)
      thus ?thesis by simp
    qed
  qed
  ultimately have 
    "∃ p q. ?a = p^2-q^2 ∧ ?b = 2*p*q ∧ ?c = p^2 + q^2 ∧ gcd(p,q) =1" 
    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 ∧ gcd(m,n) =1" by auto
  have "n^2 ≤ m^2"
  proof (rule ccontr)
    assume "¬ n^2 ≤ m^2" hence "n^2 > m^2" by simp 
    with mn have "?a = 0" by simp
    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 (auto simp only: int_nat_abs_eq_abs zdiff_int)
  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 int_mult)
  from mn have mn_rel: "zgcd(int m,int n)=1" by (simp add: zgcd_def)
  show "∃ p q. a = p^2 - q^2 ∧ b = 2*p*q ∧ ¦c¦ = p^2 + q^2 ∧ zgcd(p,q)=1" 
    (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: zgcd_commute)
      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: zgcd_commute mult_ac)
      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\,\gcd(a,b)=1\,\land\,abc\ne 0\,\land\,a~{\rm odd}.$$ *}

lemma smaller_fermat4:
  assumes abc: "a^4+b^4=c^2" and abc0: "a*b*c ≠ 0" and aodd: "a ∈ zOdd" 
    and ab_relprime: "zgcd(a,b)=1"
  shows 
  "∃ p q r. (p^4+q^4=r^2 ∧ p*q*r ≠ 0 ∧ p ∈ zOdd ∧ zgcd(p,q) = 1 ∧ r^2 < c^2)"
proof - 
  -- "put equation in shape of a pythagorean triple and obtain $u$ and $v$"
  from ab_relprime have a2b2relprime: "zgcd(a^2,b^2) = 1" 
    by (simp only: zgcd_1_power_distrib)
  moreover from aodd have "a^2 ∈ zOdd" by (simp only: power_preserves_odd)
  moreover from abc have "(a^2)^2 + (b^2)^2 = c^2" by (simp only: quartic_square_square)
  ultimately obtain u and v where uvabc: 
    "a^2 = u^2-v^2 ∧ b^2 = 2*u*v ∧ ¦c¦ = u^2 + v^2 ∧ zgcd(u,v)=1" 
    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: "zgcd(a,v) = 1" 
  proof -
    from uvabc have "zgcd(v,a^2) dvd zgcd(b^2,a^2)" by (simp only: zgcd_zdvd_zgcd_zmult)
    with a2b2relprime have "zgcd(a^2,v) dvd (1::int)" by (simp only: zgcd_commute)
    moreover have "zgcd(a,v) dvd zgcd(a^2,v)" 
      by (simp only: zgcd_zdvd_zgcd_zmult power2_eq_square)
    ultimately have "zgcd(a,v) dvd 1" by (rule_tac m="zgcd(a,v)" in zdvd_trans)
    hence "¦zgcd(a,v)¦= 1" by auto
    thus ?thesis by (simp add: zgcd_geq_zero)
  qed
  -- "make again a pythagorean triple and obtain $k$ and $l$"
  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: "zgcd(k,l)=1" 
    by (frule_tac a="a" in int_euclid_pyth_triples, auto)
  --"prove $b=2m$ and $kl(k^2 + l^2) = m^2$, for coprime $k$, $l$ and $k^2+l^2$"
  from uvabc have "b^2 ∈ zEven" by (unfold zEven_def, auto)
  hence "b ∈ zEven" by (simp only: power_preserves_even)
  then obtain m where bm: "b = 2*m" by (auto simp only: zEven_def)
  have "¦k¦*¦l¦*¦k^2+l^2¦ = m^2"
  proof -  
    from bm have "4*m^2 = b^2" by (simp only: power2_eq_square mult_ac)
    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 "zgcd(¦k¦,¦l¦)=1" by (unfold zgcd_def, auto)
  moreover have "zgcd(¦l¦,¦k^2+l^2¦)=1"
  proof -
    from kl_rel have "zgcd(k*k,l)=1" by (simp only: zgcd_zgcd_zmult)
    hence "zgcd(k*k+l*l,l)=1" by simp
    hence "zgcd(l,k^2+l^2)=1" by (simp only: power2_eq_square zgcd_commute)
    thus ?thesis by (unfold zgcd_def, auto)
  qed
  moreover have "zgcd(¦k^2+l^2¦,¦k¦)=1"
  proof -
    from kl_rel have "zgcd(l,k)=1" by (simp only: zgcd_commute)
    hence "zgcd(l*l,k)=1" by (simp only: zgcd_zgcd_zmult)
    hence "zgcd(l*l+k*k,k)=1" by simp
    hence "zgcd(k^2+l^2,k)=1" by (simp only: add_ac power2_eq_square)
    thus ?thesis by (unfold zgcd_def, auto)
  qed
  ultimately have 
    "∃ x y z. ¦¦k¦¦ = x^2 ∧ ¦¦l¦¦ = y^2 ∧ ¦¦k^2+l^2¦¦ = z^2"
    by (rule int_triple_relprime_power_divisors)
  then obtain α β γ where albega: 
    "¦k¦ = α^2 ∧ ¦l¦ = β^2 ∧ ¦k^2+l^2¦ = γ^2" 
    by auto
  -- "show this is a new solution"
  have "k^2 = α^4"
  proof -
    from albega have "¦k¦^2 = (α^2)^2" by simp
    thus ?thesis by (simp add: quartic_square_square abs_power2_distrib)
  qed
  moreover have "l^2 = β^4"
  proof -
    from albega have "¦l¦^2 = (β^2)^2" by simp
    thus ?thesis by (simp add: quartic_square_square abs_power2_distrib)
  qed
  moreover have gamma2: "k^2 + l^2 = γ^2"
  proof -
    have "k^2 ≥ 0 ∧ l^2 ≥ 0" by (simp add: zero_le_power2)
    with albega show ?thesis by auto
  qed
  ultimately have newabc: "α^4 + β^4 = γ^2" by auto 
  from uv0 klavu albega have albega0: "α * β * γ  ≠ 0" by auto
  -- "show the coprimality"
  have alphabeta_relprime: "zgcd(α,β) = 1"
  proof (rule classical)
    let ?g = "zgcd(α,β)"
    assume gnot1: "?g ≠ 1"
    have "?g > 1"
    proof -
      have "?g ≠ 0"
      proof
        assume "?g=0"
        hence "nat ¦α¦=0" by (unfold zgcd_def, auto simp add: gcd_zero)
        hence "α=0" by arith
        with albega0 show False by simp
      qed
      hence "?g>0" by (auto simp only: zgcd_geq_zero less_int_def)
      with gnot1 show ?thesis by simp
    qed
    moreover have "?g dvd zgcd(k,l)"
    proof -
      have "?g dvd α ∧ ?g dvd β" by auto
      with albega have "?g dvd ¦k¦ ∧ ?g dvd ¦l¦" 
        by (simp add: zdvd_zmult power2_eq_square zmult_commute)  
      hence "?g dvd k ∧ ?g dvd l" by (simp add: zdvd_abs2)
      thus ?thesis by (simp add: zgcd_greatest_iff)
    qed
    ultimately have "zgcd(k,l) ≠ 1" by auto
    with kl_rel show ?thesis by auto
  qed
  -- "choose $p$ and $q$ in the right way"
  have "∃ p q. p^4 + q^4 = γ^2 ∧ p*q*γ ≠ 0 ∧ p ∈ zOdd ∧ zgcd(p,q)=1"
  proof -
    have "α ∈ zOdd ∨ β ∈ zOdd"      
    proof (rule ccontr)
      assume "¬ (α ∈ zOdd ∨ β ∈ zOdd)" 
      hence "α ∈ zEven ∧ β ∈ zEven" by (auto simp add: not_odd_impl_even)
      then have "2 dvd α ∧ 2 dvd β" by (auto simp add: zEven_def)
      then have "2 dvd zgcd(α,β)" by (simp add: zgcd_greatest_iff)
      with alphabeta_relprime show False by auto
    qed
    moreover
    { assume "α ∈ zOdd"
      with newabc albega0 alphabeta_relprime obtain p q where 
        "p=α ∧ q=β ∧ p^4 + q^4 = γ^2 ∧ p*q*γ  ≠ 0 ∧ p ∈ zOdd ∧ zgcd(p,q)=1" 
        by auto
      hence ?thesis by auto }
    moreover
    { assume "β ∈ zOdd"
      with newabc albega0 alphabeta_relprime obtain p q where 
        "q=α ∧ p=β ∧ p^4 + q^4 = γ^2 ∧ p*q*γ  ≠ 0 ∧ p ∈ zOdd ∧ zgcd(p,q)=1" 
        by (auto simp add: add_ac zgcd_commute)
      hence ?thesis by auto }
    ultimately show ?thesis by auto
  qed
  -- "show the solution is smaller"
  moreover have "γ^2 < c^2"
  proof -
    from gamma2 klavu have "γ^2 ≤ ¦u¦" by simp
    also have "… ≤ ¦u¦^2" by (rule power2_ge_self)
    also have "… ≤ u^2" by (simp add: abs_power2_distrib)
    also have "… < u^2 + v^2" 
    proof -
      from uv0 have v2non0: "0 ≠ v^2" 
        by (auto simp add: power2_eq_square zero_le_power2)
      have "0 ≤ v^2" by (rule zero_le_power2)
      with v2non0 have "0 < v^2" by (auto simp add: less_int_def)
      thus ?thesis by auto
    qed
    also with uvabc have "… ≤ ¦c¦" by auto
    also have "… ≤ ¦c¦^2" by (rule power2_ge_self)
    also have "… ≤ c^2" by (simp add: abs_power2_distrib)
    finally show ?thesis by simp
  qed
  ultimately show ?thesis by auto
qed

text {* Show that no solution exists, by infinite descent of $c^2$. *}

lemma no_rewritten_fermat4:
  fixes c::int
  shows "¬ (∃ a b. (a^4 + b^4 = c^2 ∧ a*b*c ≠ 0 ∧ a ∈ zOdd ∧ zgcd(a,b)=1))" 
  (is "?Q c")
proof (rule_tac x="c" and V = "λc. nat(c^2)" in val_infinite_descent)
  fix x
  assume x2zero: "nat(x^2)=0"
  have "x^2 ≥ 0" by (rule zero_le_power2)
  with x2zero have "int(nat(x^2)) = 0" by auto
  hence "x = 0" by auto
  thus "?Q x" by auto
next
  fix x
  assume x2pos: "0<nat(x^2)" and "¬ ?Q x"
  then obtain a b where "a^4 + b^4 = x^2" and "a*b*x ≠ 0" 
    and "a ∈ zOdd" and "zgcd(a,b)=1" by auto
  hence "∃ p q r. (p^4+q^4=r^2 ∧ p*q*r ≠ 0 ∧ p ∈ zOdd 
    ∧ zgcd(p,q)=1 ∧ 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 ∧ p ∈ zOdd 
    ∧ zgcd(p,q)=1 ∧ 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 (simp only: zless_int)
  with pqr show "∃ y. nat(y^2) < nat(x^2) ∧ ¬ ?Q y" by auto
qed

text {* The theorem. Puts equation in requested shape. *}

theorem fermat4:
  assumes ass: "(x::int)^4 + y^4 = z^4"
  shows "x*y*z=0"
proof (rule ccontr)
  let ?g = "zgcd(x,y)"
  let ?c = "(z div ?g)^2"
  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: "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 zadd_zmult_distrib2)
    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 only: zpower_zdvd_mono)
      hence "(z div ?g)*?g = z" by (simp only: mult_ac zdvd_mult_div_cancel)
      with ab show ?thesis by (auto simp only: power2_eq_square mult_ac)
    qed
    with xyz0 have c0: "?c≠0" by (auto simp add: power2_eq_square)
    from xyz0 have g0: "?g≠0" by (simp add: zgcd_def gcd_zero)
    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 (simp only: quartic_square_square power_mult_distrib)
        also with cgz have "… = (z^2)^2" by simp
        also have "… = z^4" by (rule quartic_square_square)
        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
  -- "choose the parity right"
  have "∃ p q. p^4 + q^4 = ?c^2 ∧ p*q*?c≠0 ∧ p ∈ zOdd ∧ zgcd(p,q)=1"
  proof -
    have "a ∈ zOdd ∨ b ∈ zOdd"
    proof (rule ccontr)
      assume "¬(a ∈ zOdd ∨ b ∈ zOdd)"
      hence "a ∈ zEven ∧ b ∈ zEven" by (auto simp add: not_odd_impl_even)
      hence "2 dvd a ∧ 2 dvd b" by (auto simp add: zEven_def)
      hence "2 dvd zgcd(a,b)" by (simp add: zgcd_greatest_iff)
      with ab show False by auto
    qed
    moreover
    { assume "a ∈ zOdd"
      then obtain p q where "p = a" and "q = b" and "p ∈ zOdd" by simp
      with ab abc have ?thesis by auto }
    moreover 
    { assume "b ∈ zOdd"
      then obtain p q where "p = b" and "q = a" and "p ∈ zOdd" by simp    
      with ab abc have 
        "p^4 + q^4 = ?c^2 ∧ p*q*?c≠0 ∧ p ∈ zOdd ∧ zgcd(p,q)=1" 
        by (auto simp add: zgcd_commute zmult_commute)
      hence ?thesis by auto }
    ultimately show ?thesis by auto
  qed
  -- "show contradiction using the earlier result"
  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: mult_ac 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 fermat4)
  thus ?thesis by auto
qed

end