Theory FLT_Sufficient_Conditions

(* Author: Benoît Ballenghien, Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF *)

(*<*)
theory FLT_Sufficient_Conditions
  imports SG_Preliminaries Fermat3_4.Fermat4
begin
  (*>*)



section ‹Sufficient Conditions for FLT›

text ‹Recall that FLT stands for ``Fermat's Last Theorem''.
      FLT states that there is no nontrivial integer solutions to the equation
      \<^term>‹(x :: int) ^ n + y ^ n = z ^ n› for any natural number \<^term>‹(2 :: int) < n›.
      as soon as the natural number ‹n› is greater than \<^term>‹2 :: nat›.
      More formally: \<^term>‹(2 :: nat) < n ⟹ ∄x y z :: int. x ^ n + y ^ n = z ^ n›.
      We give here some sufficient conditions.›

subsection ‹Coprimality›

text ‹We first notice that it is sufficient to prove FLT for integers
      ‹x›, ‹y› and ‹z› that are (setwise) \<^const>‹coprime›.›

lemma (in semiring_Gcd) FLT_setwise_coprime_reduction :
  assumes ‹x ^ n + y ^ n = z ^ n› ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0›
  defines ‹d ≡ Gcd {x, y, z}›
  shows ‹(x div d) ^ n + (y div d) ^ n = (z div d) ^ n› ‹x div d ≠ 0›
    ‹y div d ≠ 0› ‹z div d ≠ 0› ‹Gcd {x div d, y div d, z div d} = 1›
proof -
  have ‹d dvd x› ‹d dvd y› ‹d dvd z› by (unfold d_def, rule Gcd_dvd; simp)+
  thus ‹x div d ≠ 0› ‹y div d ≠ 0› ‹z div d ≠ 0›
    by (simp_all add: ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0› dvd_div_eq_0_iff)

  have ‹{x div d, y div d, z div d} = (λn. n div d) ` {x, y, z}› by blast
  thus ‹Gcd {x div d, y div d, z div d} = 1›
    by (metis GCD_div_Gcd_is_one ‹x div d ≠ 0› d_def div_by_0)

  from  ‹x ^ n + y ^ n = z ^ n› show ‹(x div d) ^ n + (y div d) ^ n = (z div d) ^ n›
    by (metis ‹d dvd x› ‹d dvd y› ‹d dvd z› div_add div_power dvd_power_same)
qed

corollary (in semiring_Gcd) FLT_for_coprime_is_sufficient : 
  ‹∄x y z. x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ Gcd {x, y, z} = 1 ∧ x ^ n + y ^ n = z ^ n ⟹
   ∄x y z. x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ x ^ n + y ^ n = z ^ n›
  by (metis (no_types) FLT_setwise_coprime_reduction)

― ‹These very generic lemmas are of course working for integers.›
lemma ‹OFCLASS(int, semiring_Gcd_class)› by intro_classes



text ‹This version involving congruences will be useful later.›

lemma FLT_setwise_coprime_reduction_mod_version :
  fixes x y z :: int
  assumes ‹x ^ n + y ^ n = z ^ n› ‹[x ≠ 0] (mod m)› ‹[y ≠ 0] (mod m)› ‹[z ≠ 0] (mod m)›
  defines ‹d ≡ Gcd {x, y, z}›
  shows ‹(x div d) ^ n + (y div d) ^ n = (z div d) ^ n› ‹[x div d ≠ 0] (mod m)›
    ‹[y div d ≠ 0] (mod m)› ‹[z div d ≠ 0] (mod m)› ‹Gcd {x div d, y div d, z div d} = 1›
proof -
  have ‹d dvd x› ‹d dvd y› ‹d dvd z› by (unfold d_def, rule Gcd_dvd; simp)+
  show ‹[x div d ≠ 0] (mod m)›
    by (metis ‹d dvd x› assms(2) cong_0_iff dvd_mult dvd_mult_div_cancel)
  show ‹[y div d ≠ 0] (mod m)›
    by (metis ‹d dvd y› assms(3) cong_0_iff dvd_mult dvd_mult_div_cancel)
  show ‹[z div d ≠ 0] (mod m)›
    by (metis ‹d dvd z› assms(4) cong_0_iff dvd_mult dvd_mult_div_cancel)

  have ‹{x div d, y div d, z div d} = (λn. n div d) ` {x, y, z}› by blast
  thus ‹Gcd {x div d, y div d, z div d} = 1›
    by (metis GCD_div_Gcd_is_one ‹[x div d ≠ 0] (mod m)› cong_refl d_def div_by_0)

  from  ‹x ^ n + y ^ n = z ^ n› show ‹(x div d) ^ n + (y div d) ^ n = (z div d) ^ n›
    by (metis ‹d dvd x› ‹d dvd y› ‹d dvd z› div_plus_div_distrib_dvd_right div_power dvd_power_same)
qed



text ‹Actually, it is sufficient to prove FLT for integers
      ‹x›, ‹y› and ‹z› that are pairwise \<^const>‹coprime››

lemma (in semiring_Gcd) FLT_setwise_coprime_imp_pairwise_coprime :
  ‹coprime x y› if ‹n ≠ 0› ‹x ^ n + y ^ n = z ^ n› ‹Gcd {x, y, z} = 1›
proof (rule ccontr)
  assume ‹¬ coprime x y›
  with is_unit_gcd obtain d where ‹¬ is_unit d› ‹d dvd x› ‹d dvd y› by blast
  from ‹d dvd x› ‹d dvd y› have ‹d ^ n dvd x ^ n› ‹d ^ n dvd y ^ n›
    by (simp_all add: dvd_power_same)
  moreover from calculation ‹x ^ n + y ^ n = z ^ n› have ‹d ^ n dvd z ^ n›
    by (metis dvd_add_right_iff)
  moreover from ‹Gcd {x, y, z} = 1› have ‹Gcd {x ^ n, y ^ n, z ^ n} = 1›
    by (simp add: gcd_exp_weak)
  ultimately have ‹is_unit (d ^ n)› by (metis Gcd_2 Gcd_insert gcd_greatest)
  with ‹¬ is_unit d› show False by (metis is_unit_power_iff ‹n ≠ 0›)
qed



subsection ‹Odd prime Exponents›

text ‹From \<^session>‹Fermat3_4›, FLT is already proven for \<^term>‹n = (4 :: nat)›.
      Using this, we can prove that it is sufficient to
      prove FLT for \<^const>‹odd› \<^const>‹prime› exponents.›

lemma (in semiring_1_no_zero_divisors) FLT_exponent_reduction :
  assumes ‹x ^ n + y ^ n = z ^ n› ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0› ‹p dvd n›
  shows ‹(x ^ (n div p)) ^ p + (y ^ (n div p)) ^ p = (z ^ (n div p)) ^ p›
    ‹x ^ (n div p) ≠ 0› ‹y ^ (n div p) ≠ 0› ‹z ^ (n div p) ≠ 0›
proof -
  from power_not_zero[OF ‹x ≠ 0›] show ‹x ^ (n div p) ≠ 0› .
  from power_not_zero[OF ‹y ≠ 0›] show ‹y ^ (n div p) ≠ 0› .
  from power_not_zero[OF ‹z ≠ 0›] show ‹z ^ (n div p) ≠ 0› .

  from ‹p dvd n› have * : ‹n = (n div p) * p› by simp
  from ‹x ^ n + y ^ n = z ^ n›
  show ‹(x ^ (n div p)) ^ p + (y ^ (n div p)) ^ p = (z ^ (n div p)) ^ p›
    by (subst (asm) (1 2 3) "*") (simp add: power_mult)
qed

lemma ‹OFCLASS(int, semiring_1_no_zero_divisors_class)› by intro_classes



lemma odd_prime_or_four_factorE :
  fixes n :: nat assumes ‹2 < n›
  obtains p where ‹p dvd n› ‹odd p› ‹prime p› | ‹4 dvd n›
proof -
  assume hyp1 : ‹p dvd n ⟹ odd p ⟹ prime p ⟹ thesis› for p
  assume hyp2 : ‹4 dvd n ⟹ thesis›

  show thesis
  proof (cases ‹∃p. p dvd n ∧ odd p ∧ prime p›)
    from hyp1 show ‹∃p. p dvd n ∧ odd p ∧ prime p ⟹ thesis› by blast
  next
    assume ‹∄p. p dvd n ∧ odd p ∧ prime p›
    hence ‹p ∈ prime_factors n ⟹ p = 2› for p
      by (metis in_prime_factors_iff primes_dvd_imp_eq two_is_prime_nat)
    then obtain k where ‹prime_factorization n = replicate_mset k 2›
      by (metis set_mset_subset_singletonD singletonI subsetI)
    hence ‹n = 2 ^ k› by (subst prod_mset_prime_factorization_nat[symmetric])
        (use assms in simp_all)
    with ‹2 < n› have ‹1 < k› by (metis nat_power_less_imp_less pos2 power_one_right)
    with ‹n = 2 ^ k› have ‹4 dvd n›
      by (metis Suc_leI dvd_power_iff_le numeral_Bit0_eq_double
          power.simps(2) power_one_right verit_comp_simplify1(2))
    with hyp2 show thesis by blast
  qed
qed



text ‹Finally, proving FLT for odd prime exponents is sufficient.›

corollary FLT_for_odd_prime_exponents_is_sufficient : 
  ‹∄x y z :: int. x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ x ^ n + y ^ n = z ^ n› if ‹2 < n›
  and odd_prime_FLT :
  ‹⋀p. odd p ⟹ prime p ⟹
        ∄x y z :: int.  x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ x ^ p + y ^ p = z ^ p›
proof (rule ccontr)
  assume ‹¬ (∄x y z :: int. x ≠ 0 ∧ y ≠ 0 ∧ z ≠ 0 ∧ x ^ n + y ^ n = z ^ n)›
  then obtain x y z :: int
    where ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0› ‹x ^ n + y ^ n = z ^ n› by blast
  from odd_prime_or_four_factorE ‹2 < n›
  consider p where ‹p dvd n› ‹odd p› ‹prime p› | ‹4 dvd n› by blast
  thus False
  proof cases
    fix p assume ‹p dvd n› ‹odd p› ‹prime p›
    from FLT_exponent_reduction [OF ‹x ^ n + y ^ n = z ^ n› ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0› ‹p dvd n›]
      odd_prime_FLT[OF ‹odd p› ‹prime p›]
    show False by blast
  next
    assume ‹4 dvd n›
    from fermat_mult4[OF ‹x ^ n + y ^ n = z ^ n› ‹4 dvd n›] ‹x ≠ 0› ‹y ≠ 0› ‹z ≠ 0›
    show False by (metis mult_eq_0_iff)
  qed
qed



(*<*)
end
  (*>*)