Quelle  Fermat3.thy

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

section ‹Fermat's last theorem, case $n=3$›

theory Fermat3
imports Quad_Form
begin

context
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.$$›

(* TODO: this lemma is also used in Fermat4 with a slightly different generalization to ints.
Maybe it should be generalized to factorial rings and moved to another theory. *)
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)  dvd_power[of n p] gcd_nat.trans by blast
    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
    moreover have "0 < b" "0 < a" using h2 dvd_0_right gr0I True by fastforce+
    then have "0 < c" "1 < p" using p(1) 1(3) nat_0_less_mult_iff [of a b] n0 prime_gt_Suc_0_nat
      by simp_all
    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_odd_power_divisors:
  assumes "odd n" and "(a::int) * b = c ^ n" and "coprime a b"
  shows "∃k. a = k^n" 
proof -
  from assms have "∣a∣ * ∣b∣ = ∣c∣ ^ n"
    by (simp add: abs_mult [symmetric] power_abs)
  then have "nat ∣a∣ * nat ∣b∣ = nat ∣c∣ ^ n"
    by (simp add: nat_mult_distrib [of "∣a∣" "∣b∣", symmetric] nat_power_eq)
  moreover have "coprime (nat ∣a∣) (nat ∣b∣)" using assms(3) gcd_int_def by fastforce
  ultimately have "∃ k. nat ∣a∣ = k^n"
    using nat_relprime_power_divisors[of n "nat ∣a∣" "nat ∣b∣" "nat ∣c∣"] assms(1) by blast
  then obtain k' where k': "nat ∣a∣ = k'^n" by blast
  moreover define k where "k = int k'"
  ultimately have k: "∣a∣ = k^n" using int_nat_eq[of "∣a∣"] of_nat_power[of k' n] by force
  { assume "a ≠ k^n"
    with k have "a = -(k^n)" by arith
    hence "a = (-k)^n" using assms(1) power_minus_odd by simp }
  thus ?thesis by blast
qed

private lemma factor_sum_cubes: "(x::int)^3 + y^3 = (x+y)*(x^2 - x*y + y^2)"
  by (simp add: eval_nat_numeral field_simps)

private lemma two_not_abs_cube: "∣x^3∣ = (2::int) ==> False"
proof -
  assume "∣x^3∣ = 2"
  hence x32: "∣x∣^3 = 2" by (simp add: power_abs)
  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 $coprime v w$ and $x$ even, by constructing a solution with a smaller $|x^3|$.›

private lemma no_rewritten_fermat3: 
  "¬ (∃ v w. v^3+w^3 = x^3 ∧ v*w*x ≠ 0 ∧ even (x::int) ∧ coprime v w)"
proof (induct x rule: infinite_descent0_measure[where V="λx. nat∣x^3∣"])
  case (0 x) hence "x^3 = 0" by arith
  hence "x=0" by auto
  thus ?case by auto
next
  case (smaller x)
  then obtain v w where vwx: 
    "v^3+w^3=x^3 ∧ v*w*x ≠ 0 ∧ even x ∧ coprime v w" (is "?P v w x")
    by auto
  then have "coprime v w"
    by simp
  have "∃ α β γ. ?P α β γ ∧ nat∣γ^3∣ < nat∣x^3∣"
  proof -
    ― ‹obtain coprime $p$ and $q$ such that $v = p+q$ and $w = p-q$›
    have vwOdd: "odd v ∧ odd w"
    proof (rule ccontr, case_tac "odd v", simp_all)
      assume ve: "even v"
      hence "even (v^3)" by simp
      moreover from vwx have "even (x^3)" by simp
      ultimately have "even (x^3-v^3)" by simp
      moreover from vwx have "x^3-v^3 = w^3" by simp
      ultimately have "even (w^3)" by simp
      hence "even w" by simp
      with ve have "2 dvd v ∧ 2 dvd w" by auto
      hence "2 dvd gcd v w" by simp
      with vwx show False by simp
    next
      assume "odd v" and "even w"
      hence "odd (v^3)" and "even (w^3)" 
        by auto
      hence "odd (w^3 + v^3)" by simp
      with vwx have "odd (x^3)" by (simp add: add.commute)
      hence "odd x" by simp
      with vwx show False by auto
    qed
    hence "even (v+w) ∧ even (v-w)" by simp
    then obtain p q where pq: "v+w = 2*p ∧ v-w = 2*q"
      using evenE[of "v+w"] evenE[of "v-w"] by meson
    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: eval_nat_numeral field_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 = "gcd (2 * p) (p² + 3 * q²)"
    have g1: "?g ≥ 1" 
    proof (rule ccontr)
      assume "¬ ?g ≥ 1"
      then have "?g < 0 ∨ ?g = 0" unfolding not_le by arith
      moreover have "?g ≥ 0" by simp
      ultimately have "?g = 0" by arith
      hence "p = 0" by simp
      with vwpq vwx ‹0 < nat∣x^3∣› show False by auto
    qed
    have gOdd: "odd ?g"
    proof (rule ccontr)
      assume "¬ odd ?g"
      hence"2 dvd p^2+3*q^2" by simp
      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
      also have "… = (p+q)*(p-q)" by (simp add: power2_eq_square algebra_simps)
      finally have "v*w = 2*(k - 2*q^2)" using vw by presburger
      hence "even (v*w)" by auto
      hence "even (v) ∨ even (w)" by simp
      with vwOdd show False by simp
    qed
    then have even_odd_p_q: "even p ∧ odd q ∨ odd p ∧ even q"
      by auto
    ― ‹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)
        assume "¬ ¬ 3 dvd ?g" hence "3 dvd 2*p" by simp
        hence "(3::int) dvd 2 ∨ 3 dvd p"
          using prime_dvd_multD[of 3] by (fastforce simp add: prime_dvd_mult_iff)
        with p3 show False by arith
      qed
      from ‹coprime v w› have pq_relprime: "coprime p q"
      proof (rule coprime_imp_coprime)
        fix c
        assume "c dvd p" and "c dvd q"
        then have "c dvd p + q" and "c dvd p - q"
          by simp_all
        with vw show "c dvd v" and "c dvd w"
          by simp_all
      qed
      from ‹coprime p q› have "coprime p (q²)"
        by simp
      then have factors_relprime: "coprime (2 * p) (p² + 3 * q²)" 
      proof (rule coprime_imp_coprime)
        fix c
        assume g2p: "c dvd 2 * p" and gpq: "c dvd p² + 3 * q²"
        have "coprime 2 c"
          using g2p gpq even_odd_p_q dvd_trans [of 2 c "p² + 3 * q²"]
          by auto
        with g2p show "c dvd p"
          by (simp add: coprime_dvd_mult_left_iff ac_simps)
        then have "c dvd p²"
          by (simp add: power2_eq_square)
        with gpq have "c dvd 3 * q²"
          by (simp add: dvd_add_right_iff)
        moreover have "coprime 3 c"
          using ‹c dvd p› p3 dvd_trans [of 3 c p]
          by (auto intro: prime_imp_coprime)
        ultimately show "c dvd q²"
          by (simp add: coprime_dvd_mult_right_iff ac_simps)
      qed
      moreover from vwx vwpq have pqx: "(2*p)*(p^2 + 3*q^2) = x^3" by auto
      ultimately have "∃ c. 2*p = c^3" by (simp add: int_relprime_odd_power_divisors)
      then obtain c where c: "c^3 = 2*p" by auto
      from pqx factors_relprime have "coprime (p^2 + 3*q^2) (2*p)"
        and "(p^2 + 3*q^2)*(2*p) = x^3" by (auto simp add: ac_simps)
      hence "∃ d. p^2 + 3*q^2 = d^3" by (simp add: int_relprime_odd_power_divisors)
      then obtain d where d: "p^2 + 3*q^2 = d^3" by auto
      have "odd d"
      proof (rule ccontr)
        assume "¬ odd d"
        hence "even (d^3)" by simp
        hence "2 dvd d^3" by simp
        moreover have "2 dvd 2*p" by (rule dvd_triv_left)
        ultimately have "2 dvd gcd (2*p) (d^3)" by simp
        with d factors_relprime show False by simp
      qed
      with d pq_relprime have "coprime p q ∧ p^2 + 3*q^2 = d^3 ∧ odd d"
        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: eval_nat_numeral field_simps)
      with c have abc: "(2*a)*(a+3*b)*(a- 3*b) = c^3" by auto
      from pq_relprime ab have ab_relprime: "coprime a b"
        by (auto intro: coprime_imp_coprime)
      then have ab1: "coprime (2 * a) (a + 3 * b)"
      proof (rule coprime_imp_coprime)
        fix h
        assume h2a: "h dvd 2 * a" and hab: "h dvd a + 3 * b"
        have "coprime 2 h"
          using ab even_odd_p_q hab dvd_trans [of 2 h "a + 3 * b"]
          by auto
        with h2a show "h dvd a"
          by (simp add: coprime_dvd_mult_left_iff ac_simps)
        with hab have "h dvd 3 * b" and "¬ 3 dvd h"
          using dvd_trans [of 3 h a] ab ‹¬ 3 dvd p›
          by (auto simp add: dvd_add_right_iff)
        moreover have "coprime 3 h"
          using ‹¬ 3 dvd h› by (auto intro: prime_imp_coprime)
        ultimately show "h dvd b"
          by (simp add: coprime_dvd_mult_left_iff ac_simps)
      qed
      then have [simp]: "even b ⟷ odd a"
        and ab3: "coprime a (a + 3 * b)"
        by simp_all
      from ‹coprime a b› have ab4: "coprime a (a - 3 * b)"
      proof (rule coprime_imp_coprime)
        fix h
        assume h2a: "h dvd a" and hab: "h dvd a - 3 * b"
        then show "h dvd a"
          by simp
        with hab have "h dvd 3 * b" and "¬ 3 dvd h"
          using dvd_trans [of 3 h a] ab ‹¬ 3 dvd p› dvd_add_right_iff [of h a "- 3 * b"]
          by auto
        moreover have "coprime 3 h"
          using ‹¬ 3 dvd h› by (auto intro: prime_imp_coprime)
        ultimately show "h dvd b"
          by (simp add: coprime_dvd_mult_left_iff ac_simps)
      qed
      from ab1 have ab2: "coprime (a + 3 * b) (a - 3 * b)"
        by (rule coprime_imp_coprime)
          (use dvd_add [of _ "a + 3 * b" "a - 3 * b"] in simp_all)
      have "∃k l m. 2 * a = k ^ 3 ∧ a + 3 * b = l ^ 3 ∧ a - 3 * b = m ^ 3"
        using ab2 ab3 ab4 abc
          int_relprime_odd_power_divisors [of 3 "2 * a" "(a + 3 * b) * (a - 3 * b)" c]
          int_relprime_odd_power_divisors [of 3 "(a + 3 * b)" "2 * a * (a - 3 * b)" c]
          int_relprime_odd_power_divisors [of 3 "(a - 3 * b)" "2 * a * (a + 3 * b)" c]
        by auto (auto simp add: ac_simps)
      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 "even γ"
      proof -
        have "even (2*a)" by simp
        with albega have "even (γ^3)" by simp
        thus ?thesis by simp
      qed
      moreover have "coprime α β"
      using ab2 proof (rule coprime_imp_coprime)
        fix h
        assume ha: "h dvd α" and hb: "h dvd β"
        then have "h dvd α * α^2 ∧ h dvd β * β^2" by simp
        then have "h dvd α^Suc 2 ∧ h dvd β^Suc 2" by (auto simp only: power_Suc)
        with albega show "h dvd a - 3 * b" "h dvd a + 3 * b" by auto 
      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 ‹0 < nat∣x^3∣› 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 arith
          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
              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 pq_relprime have "∣p∣ = 1" by simp
            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 ‹0 < nat∣x^3∣› 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 dvd_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 dvd_mult)
      ultimately have g3: "3 dvd ?g" by simp
      from ‹coprime v w› have qr_relprime: "coprime q r" 
      proof (rule coprime_imp_coprime)
        fix h
        assume hq: "h dvd q" "h dvd r"
        with r have "h dvd p" by simp
        with hq have "h dvd p + q" "h dvd p - q"
          by simp_all
        with vw show "h dvd v" "h dvd w"
          by simp_all
      qed
      have factors_relprime: "coprime (18*r) (q^2 + 3*r^2)"
      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: "prime h ∧ h dvd k"
            using prime_divisor_exists[of k] by auto
          with k have hg: "3*h dvd ?g" by (auto simp add: mult_dvd_mono)
          hence "3*h dvd p^2 + 3*q^2" and hp: "3*h dvd 2*p" by auto
          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 (auto dest: prime_dvd_multD)
          moreover have "¬ h dvd 2" 
          proof (rule ccontr, simp)
            assume "h dvd 2" 
            with h have "h=2" using zdvd_not_zless[of 2 h] by (auto simp: prime_int_iff)
            with hg have "2*3 dvd ?g" by auto
            hence "2 dvd ?g" by (rule dvd_mult_left)
            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: right_diff_distrib)
          hence "h dvd q^2" by simp
          with h have "h dvd q" using prime_dvd_multD[of h q q]
            by (simp add: power2_eq_square)
          with hr have "h dvd gcd q r" by simp
          with h qr_relprime show False by (unfold prime_def, auto)
        qed
        with k r have "3 = gcd (2*(3*r)) ((3*r)^2 + 3*q^2)" by auto
        also have "… = gcd (3*(2*r)) (3*(3*r^2 + q^2))" 
          by (simp add: power_mult_distrib)
        also have "… = 3 * gcd (2*r) (3*r^2 + q^2)" using gcd_mult_distrib_int[of 3] by auto
        finally have "coprime (2*r) (3*r^2 + q^2)"
          by (auto dest: gcd_eq_1_imp_coprime)
        moreover have "coprime 9 (3*r^2 + q^2)"
        using ‹coprime v w› proof (rule coprime_imp_coprime)
          fix h :: int
          assume "¬ is_unit h"
          assume h9: "h dvd 9" and hrq: "h dvd 3 * r² + q²"
          have "prime (3::int)"
            by simp
          moreover from ‹h dvd 9› have "h dvd 3²"
            by simp
          ultimately obtain k where "normalize h = 3 ^ k"
            by (rule divides_primepow)
          with ‹¬ is_unit h› have "0 < k"
            by simp
          with ‹normalize h = 3 ^ k› have "∣h∣ = 3 * 3 ^ (k - 1)"
            by (cases k) simp_all
          then have "3 dvd ∣h∣" ..
          then have "3 dvd h"
            by simp
          then have "3 dvd 3 * r² + q²"
            using hrq by (rule dvd_trans)
          then have "3 dvd q²"
            by presburger
          then have "3 dvd q"
            using prime_dvd_power_int [of 3 q 2] by auto
          with p3 have "3 dvd p + q" and "3 dvd p - q"
            by simp_all
          with vw have "3 dvd v" and "3 dvd w"
            by simp_all
          with ‹coprime v w› have "is_unit (3::int)"
            by (rule coprime_common_divisor)
          then show "h dvd v" and "h dvd w"
            by simp_all
        qed
        ultimately have "coprime (2 * r * 9) (3 * r² + q²)"
          by (simp only: coprime_mult_left_iff)
        then show ?thesis
          by (simp add: ac_simps)
      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
      ultimately have "∃ c. 18*r = c^3" 
        by (simp add: int_relprime_odd_power_divisors)
      then obtain c1 where c1: "c1^3 = 3*(6*r)" by auto
      hence "3 dvd c1^3" and "prime (3::int)" by auto
      hence "3 dvd c1" using prime_dvd_power[of 3] by fastforce
      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 "coprime (q^2 + 3*r^2) (18*r)"
        and "(q^2 + 3*r^2)*(18*r) = x^3" by (auto simp add: ac_simps)
      hence "∃ d. q^2 + 3*r^2 = d^3" 
        by (simp add: int_relprime_odd_power_divisors)
      then obtain d where d: "q^2 + 3*r^2 = d^3" by auto
      have "odd d"
      proof (rule ccontr)
        assume "¬ odd d"
        hence "2 dvd d^3" by simp
        moreover have "2 dvd 2*(9*r)" by (rule dvd_triv_left)
        ultimately have "2 dvd gcd (2*(9*r)) (d^3)" by simp
        with d factors_relprime show False by auto
      qed
      with d qr_relprime have "coprime q r ∧ q^2 + 3*r^2 = d^3 ∧ odd d" 
        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: eval_nat_numeral field_simps)
      with c have abc: "(2*b)*(a+b)*(a-b) = c^3" by auto
      from qr_relprime ab have ab_relprime: "coprime a b"
        by (auto intro: coprime_imp_coprime)
      then have ab1: "coprime (2*b) (a+b)"
      proof (rule coprime_imp_coprime)
        fix h
        assume h2b: "h dvd 2*b" and hab: "h dvd a+b"
        have "odd h"
        proof
          assume "even h"
          then have "even (a + b)"
            using hab by (rule dvd_trans)
          then have "even (a+3*b)"
            by simp
          with ab have "even q" "even r"
            by auto
          then show False
            using coprime_common_divisor_int qr_relprime by fastforce
        qed
        with h2b show "h dvd b" 
          using coprime_dvd_mult_right_iff [of h 2 b] by simp
        with hab show "h dvd a"
          using dvd_diff [of h "a + b" b] by simp
      qed
      from ab1 have ab2: "coprime (a+b) (a-b)"
      proof (rule coprime_imp_coprime)
        fix h
        assume hab1: "h dvd a+b" and hab2: "h dvd a-b"
        then show "h dvd 2*b" using dvd_diff[of h "a+b" "a-b"] by fastforce
      qed
      from ab1 have ab3: "coprime (a-b) (2*b)"
      proof (rule coprime_imp_coprime)
        fix h
        assume hab: "h dvd a-b" and h2b: "h dvd 2*b"
        have "a-b+2*b = a+b" by simp
        then show "h dvd a+b" using hab h2b dvd_add [of h "a-b" "2*b"] by presburger
      qed
      then have [simp]: "even b ⟷ odd a"
        by simp
      have "∃ k l m. 2*b = k^3 ∧ a+b = l^3 ∧ a-b = m^3"
        using abc ab1 ab2 ab3
          int_relprime_odd_power_divisors [of 3 "2 * b" "(a + b) * (a - b)" c]
          int_relprime_odd_power_divisors [of 3 "a + b" "(2 * b) * (a - b)" c]
          int_relprime_odd_power_divisors [of 3 "a - b" "(2 * b) * (a + b)" c]
        by simp (simp add: ac_simps, simp add: algebra_simps)
      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 a1 have a2: "α^3 = b-a" by auto
      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 "even γ"
      proof -
        have "even (2*b)" by simp
        with a1 have "even (γ^3)" by simp
        thus ?thesis by simp
      qed
      moreover have "coprime α β"
      using ab2 proof (rule coprime_imp_coprime)
        fix h
        assume ha: "h dvd α" and hb: "h dvd β"
        then have "h dvd α * α^2" and "h dvd β * β^2" by simp_all
        then have "h dvd α^Suc 2" and "h dvd β^Suc 2" by (auto simp only: power_Suc)
        with a1 a2 have "h dvd b - a" and "h dvd a + b" by auto 
        then show "h dvd a + b" and "h dvd a - b"
          by (simp_all add: dvd_diff_commute)
      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 ‹0 < nat∣x^3∣› 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 ‹0 < nat∣x^3∣› 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 ?case by auto
qed

text ‹The theorem. Puts equation in requested shape.›  

theorem fermat_3:
  assumes ass: "(x::int)^3 + y^3 = z^3"
  shows "x*y*z=0"
proof (rule ccontr)
  let ?g = "gcd 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 ∧ coprime a b"
    using gcd_coprime_exists[of x y] by (auto simp: mult.commute)
  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
    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 distrib_left)
    qed
    have cgz: "?c * ?g = z"
    proof - 
      from zgab have "?g^3 dvd z^3" by simp
      hence "?g dvd z" by simp
      thus ?thesis by (simp only: ac_simps dvd_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›
  from ab have "coprime (a ^ 3) (b ^ 3)"
    by simp
  have "∃ u v w. u^3 + v^3 = w^3 ∧ u*v*w≠(0::int) ∧ even w ∧ coprime u v"
  proof -
    let "?Q u v w" = "u^3 + v^3 = w^3 ∧ u*v*w≠(0::int) ∧ even w ∧ coprime u v"
    have "even a ∨ even b ∨ even ?c"
    proof (rule ccontr)
      assume "¬(even a ∨ even b ∨ even ?c)"
      hence aodd: "odd a" and "odd b ∧ odd ?c" by auto
      hence "even (?c^3 - b^3)" by simp
      moreover from abc have "?c^3-b^3 = a^3" by simp
      ultimately have "even (a^3)" by auto
      hence "even (a)" by simp
      with aodd show False by simp
    qed
    moreover
    { assume "even (a)"
      then obtain u v w where uvwabc: "u = -b ∧ v = ?c ∧ w = a ∧ even w" 
        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
        also with abc and uvwabc have "… = w^3" by auto
        finally show ?thesis by simp
      qed
      moreover have "coprime u v"
      using ‹coprime (a ^ 3) (b ^ 3)› proof (rule coprime_imp_coprime)
        fix h
        assume hu: "h dvd u" and "h dvd v"
        with uvwabc have "h dvd ?c*?c^2" by (simp only: dvd_mult2)
        with abc have "h dvd a^3+b^3" using power_Suc[of ?c 2] by simp
        moreover from hu uvwabc have hb3: "h dvd b*b^2" by simp
        ultimately have "h dvd a^3+b^3-b^3"
          using power_Suc [of b 2] dvd_diff [of h "a ^ 3 + b ^ 3" "b ^ 3"] by simp
        with hb3 show "h dvd a^3" "h dvd b^3" using power_Suc[of b 2] by auto
      qed
      ultimately have "?Q u v w" using ‹even a› by simp
      hence ?thesis by auto }
    moreover 
    { assume "even b"
      then obtain u v w where uvwabc: "u = -a ∧ v = ?c ∧ w = b ∧ even w" 
        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
        also with abc and uvwabc have "… = w^3" by auto
        finally show ?thesis by simp
      qed
      moreover have "coprime u v"
      using ‹coprime (a ^ 3) (b ^ 3)› proof (rule coprime_imp_coprime)
        fix h
        assume hu: "h dvd u" and "h dvd v"
        with uvwabc have "h dvd ?c*?c^2" by (simp only: dvd_mult2)
        with abc have "h dvd a^3+b^3" using power_Suc[of ?c 2] by simp
        moreover from hu uvwabc have hb3: "h dvd a*a^2" by simp
        ultimately have "h dvd a^3+b^3-a^3"
          using power_Suc [of a 2] dvd_diff [of h "a ^ 3 + b ^ 3" "a ^ 3"] by simp
        with hb3 show "h dvd a^3" and "h dvd b^3" using power_Suc[of a 2] by auto
      qed
      ultimately have "?Q u v w" using ‹even b› by simp
      hence ?thesis by auto }
    moreover 
    { assume "even ?c"
      then obtain u v w where uvwabc: "u = a ∧ v = b ∧ w = ?c ∧ even w"
        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::int) ∧ even w ∧ coprime u v"
    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: ac_simps 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 fermat_3)
  thus ?thesis by auto
qed

end

end