diff --git a/FltRegular.lean b/FltRegular.lean index bcfabf45..f9693fa1 100644 --- a/FltRegular.lean +++ b/FltRegular.lean @@ -5,11 +5,6 @@ import FltRegular.CaseII.InductionStep import FltRegular.CaseII.Statement import FltRegular.FLT5 import FltRegular.FltRegular -import FltRegular.FltThree.Edwards -import FltRegular.FltThree.FltThree -import FltRegular.FltThree.OddPrimeOrFour -import FltRegular.FltThree.Primes -import FltRegular.FltThree.Spts import FltRegular.MayAssume.Lemmas import FltRegular.NumberTheory.AuxLemmas import FltRegular.NumberTheory.Cyclotomic.CaseI diff --git a/FltRegular/FltThree/Edwards.lean b/FltRegular/FltThree/Edwards.lean deleted file mode 100644 index bc1f56f5..00000000 --- a/FltRegular/FltThree/Edwards.lean +++ /dev/null @@ -1,540 +0,0 @@ -/- -Copyright (c) 2020 Ruben Van de Velde. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. --/ - -import FltRegular.FltThree.Primes -import FltRegular.FltThree.Spts -import FltRegular.FltThree.OddPrimeOrFour - -theorem OddPrimeOrFour.im_ne_zero {p : ℤ√(-3)} (h : OddPrimeOrFour p.norm.natAbs) - (hcoprime : IsCoprime p.re p.im) : p.im ≠ 0 := - by - intro H - rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two] at h - obtain h | ⟨hp, -⟩ := h - · rw [H, isCoprime_zero_right, Int.isUnit_iff_abs_eq] at hcoprime - rw [← sq_abs, hcoprime] at h - norm_num at h - · rw [Int.natAbs_pow] at hp - exact hp.not_prime_pow le_rfl - -theorem Zsqrt3.isUnit_iff {z : ℤ√(-3)} : IsUnit z ↔ abs z.re = 1 ∧ z.im = 0 := - by - rw [← Zsqrtd.norm_eq_one_iff, ← Int.natCast_inj, Int.ofNat_one, - Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) z)] - refine' ⟨Spts.eq_one, fun h => _⟩ - rw [Zsqrtd.norm_def, h.2, MulZeroClass.mul_zero, sub_zero, ← sq, ← sq_abs, h.1, one_pow] - -theorem Zsqrt3.coe_of_isUnit {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : Units ℤ, z = u := - by - obtain ⟨u, hu⟩ := Zsqrt3.isUnit_iff.mp h - obtain ⟨v, hv⟩ : IsUnit z.re := by rwa [Int.isUnit_iff_abs_eq] - use v - rw [Zsqrtd.ext_iff, hu, ← hv] - simp only [Zsqrtd.intCast_re, and_true_iff, eq_self_iff_true, Zsqrtd.intCast_im] - -theorem Zsqrt3.coe_of_isUnit' {z : ℤ√(-3)} (h : IsUnit z) : ∃ u : ℤ, z = u ∧ abs u = 1 := - by - obtain ⟨u, hu⟩ := Zsqrt3.coe_of_isUnit h - refine' ⟨u, _, _⟩ - · rw [hu] - · exact Int.isUnit_iff_abs_eq.mp u.isUnit - -theorem Zsqrt3.norm_natAbs (a : ℤ√(-3)) : a.norm.natAbs = a.norm := by - rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] - -theorem OddPrimeOrFour.factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) - (hx : OddPrimeOrFour x.natAbs) (hfactor : x ∣ a.norm) : - ∃ c : ℤ√(-3), |x| = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 := - by - obtain hx | ⟨hprime, hodd⟩ := hx - · refine' ⟨⟨1, 1⟩, _, zero_le_one, one_ne_zero⟩ - simp only [Zsqrtd.norm_def, mul_one, sub_neg_eq_add, Int.abs_eq_natAbs, hx] - norm_num - · rw [Int.natAbs_odd] at hodd - obtain ⟨c, hc⟩ := _root_.factors a x hcoprime hodd hfactor - rw [hc] - apply Zsqrtd.exists c - intro H - rw [Zsqrtd.norm_def, H, MulZeroClass.mul_zero, sub_zero, ← pow_two, eq_comm, Int.abs_eq_natAbs] - at hc - rw [Nat.prime_iff_prime_int, ← hc] at hprime - exact not_prime_pow one_lt_two.ne' hprime - -theorem step1a {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) : - Odd a.re ∧ Odd a.im := - by - rw [Int.odd_iff_not_even, Int.odd_iff_not_even] - have : Even a.re ↔ Even a.im := by - have : ¬ Even (3 : ℤ) := by decide - simpa [this, Zsqrtd.norm_def, parity_simps] using heven - apply (iff_iff_and_or_not_and_not.mp this).resolve_left - rw [even_iff_two_dvd, even_iff_two_dvd] - rintro ⟨hre, him⟩ - have := hcoprime.isUnit_of_dvd' hre him - rw [isUnit_iff_dvd_one] at this - norm_num at this - -theorem step1 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) : - ∃ u : ℤ√(-3), a = ⟨1, 1⟩ * u ∨ a = ⟨1, -1⟩ * u := - by - obtain ⟨ha, hb⟩ := step1a hcoprime heven - obtain hdvd | hdvd := Int.four_dvd_add_or_sub_of_odd ha hb - · obtain ⟨v, hv⟩ := hdvd - rw [← eq_sub_iff_add_eq] at hv - use ⟨v - a.im, v⟩ - right - rw [Zsqrtd.ext_iff, hv, Zsqrtd.mul_re, Zsqrtd.mul_im] - dsimp only - constructor <;> ring - · obtain ⟨v, hv⟩ := hdvd - rw [sub_eq_iff_eq_add] at hv - use ⟨a.im + v, -v⟩ - left - rw [Zsqrtd.ext_iff, hv, Zsqrtd.mul_re, Zsqrtd.mul_im] - dsimp only - constructor <;> ring - -theorem step1' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (heven : Even a.norm) : - ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ a.norm = 4 * u.norm := - by - obtain ⟨u', hu'⟩ := step1 hcoprime heven - refine' ⟨u', _, _⟩ - · apply Zsqrtd.coprime_of_dvd_coprime hcoprime - obtain rfl | rfl := hu' <;> apply dvd_mul_left - · cases' hu' with hu' hu' <;> - · rw [hu', Zsqrtd.norm_mul] - congr - -theorem step1'' {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hp : p.norm = 4) (hq : p.im ≠ 0) - (heven : Even a.norm) : - ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ a.norm = 4 * u.norm := - by - obtain ⟨u, h2⟩ := step1 hcoprime heven - set q : ℤ√(-3) := ⟨1, 1⟩ - replace h2 : a = q * u ∨ a = star q * u := h2 - obtain ⟨hp', hq'⟩ := Spts.four hp hq - refine' ⟨p.re * u, _, _, _⟩ - · rw [← Int.isUnit_iff_abs_eq] at hp' - rw [Zsqrtd.smul_re, Zsqrtd.smul_im, isCoprime_mul_unit_left hp'] - apply Zsqrtd.coprime_of_dvd_coprime hcoprime - obtain rfl | rfl := h2 <;> apply dvd_mul_left - · rw [abs_eq <| zero_le_one' ℤ] at hp' hq' - cases hp' with - | inl hp' => - have h4 : p = q ∨ p = star q := by - apply Or.imp _ _ hq' <;> - · intro h5 - simp [Zsqrtd.ext_iff, hp', h5] - simp only [hp', one_mul, Int.cast_one] - cases h4 <;> cases h2 <;> simp [*, or_comm] - | inr hp' => - have h4 : p = -q ∨ p = -star q := by - apply Or.imp _ _ hq'.symm - · intro h5 - simp [Zsqrtd.ext_iff, hp', h5] - · intro h5 - simp [Zsqrtd.ext_iff, hp', h5] - simp only [hp', one_mul, Zsqrtd.norm_neg, Int.cast_one, Int.cast_neg, neg_one_mul] - cases h4 <;> cases h2 <;> simp [*] - · rw [Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← sq, ← sq_abs, hp', one_pow, one_mul] - cases' h2 with h2 h2 <;> - · rw [h2, Zsqrtd.norm_mul] - congr - -theorem step2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm) - (hpprime : Prime p.norm) : - ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ - a.norm = p.norm * u.norm := by - obtain ⟨u', h, h'⟩ := Spts.mul_of_dvd'' hdvd hpprime - refine' ⟨u', _, h, h'⟩ - apply Zsqrtd.coprime_of_dvd_coprime hcoprime - obtain rfl | rfl := h <;> apply dvd_mul_left - -theorem step1_2 {a p : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) (hdvd : p.norm ∣ a.norm) - (hp : OddPrimeOrFour p.norm.natAbs) (hq : p.im ≠ 0) : - ∃ u : ℤ√(-3), IsCoprime u.re u.im ∧ (a = p * u ∨ a = star p * u) ∧ - a.norm = p.norm * u.norm := by - obtain hp | ⟨hpprime, -⟩ := hp - · replace hp : p.norm = 4 := by - rw [← Zsqrt3.norm_natAbs] - norm_cast - rw [hp] at hdvd⊢ - have heven : Even a.norm := - by - apply even_iff_two_dvd.mpr (dvd_trans _ hdvd) - norm_num - exact step1'' hcoprime hp hq heven - · rw [← Int.prime_iff_natAbs_prime] at hpprime - apply step2 hcoprime hdvd hpprime - -theorem OddPrimeOrFour.factors' {a : ℤ√(-3)} (h2 : a.norm ≠ 1) (hcoprime : IsCoprime a.re a.im) : - ∃ u q : ℤ√(-3), - 0 ≤ q.re ∧ - q.im ≠ 0 ∧ OddPrimeOrFour q.norm.natAbs ∧ a = q * u ∧ IsCoprime u.re u.im ∧ u.norm < a.norm := - by - have h2 : 2 < a.norm.natAbs := by - zify - rw [abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] - apply lt_of_le_of_ne _ (Spts.not_two _).symm - rw [← one_mul (2 : ℤ), mul_two, Int.add_one_le_iff] - apply lt_of_le_of_ne _ h2.symm - rw [← Int.sub_one_lt_iff, sub_self] - exact Spts.pos_of_coprime' hcoprime - obtain ⟨p, hpdvd, hp⟩ := OddPrimeOrFour.exists_and_dvd h2 - rw [← Int.ofNat_dvd_left] at hpdvd - obtain ⟨q', hcd, hc, hd⟩ := OddPrimeOrFour.factors a p hcoprime hp hpdvd - rw [Nat.abs_cast, ← Zsqrt3.norm_natAbs, Nat.cast_inj] at hcd - rw [hcd] at hpdvd hp - rw [Int.natAbs_dvd] at hpdvd - obtain ⟨u, huvcoprime, huv, huvdvd⟩ := step1_2 hcoprime hpdvd hp hd - use u - cases' huv with huv huv <;> [(use q'); (use star q')] <;> - simp only [IsCoprime, Zsqrtd.star_re, Zsqrtd.star_im, Ne, neg_eq_zero, Zsqrtd.norm_conj] <;> - use hc, hd, hp, huv, huvcoprime <;> - · rw [huvdvd, lt_mul_iff_one_lt_left (Spts.pos_of_coprime' huvcoprime), ← Zsqrt3.norm_natAbs, - Nat.one_lt_cast] - exact hp.one_lt - -theorem step3 {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : - ∃ f : Multiset (ℤ√(-3)), - (a = f.prod ∨ a = -f.prod) ∧ - ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs := - by - suffices - ∀ n : ℕ, - a.norm.natAbs = n → - ∃ f : Multiset (ℤ√(-3)), - (a = f.prod ∨ a = -f.prod) ∧ - ∀ pq : ℤ√(-3), pq ∈ f → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs - by exact this a.norm.natAbs rfl - intro n hn - induction' n using Nat.strong_induction_on with n ih generalizing a - cases' eq_or_ne a.norm 1 with h h - · use 0 - constructor - · simp only [Multiset.prod_zero, Spts.eq_one' h] - · intro pq hpq - exact absurd hpq (Multiset.not_mem_zero _) - · obtain ⟨U, q, hc, hd, hp, huv, huvcoprime, descent⟩ := OddPrimeOrFour.factors' h hcoprime - replace descent := - Int.natAbs_lt_natAbs_of_nonneg_of_lt (Zsqrtd.norm_nonneg (by norm_num) _) descent - rw [hn] at descent - obtain ⟨g, hgprod, hgfactors⟩ := ih U.norm.natAbs descent huvcoprime rfl - refine' ⟨q ::ₘ g, _, _⟩ - · simp only [huv, Multiset.prod_cons, ← mul_neg] - exact Or.imp (congr_arg _) (congr_arg _) hgprod - · rintro pq hpq - rw [Multiset.mem_cons] at hpq - obtain rfl | ind := hpq - · exact ⟨hc, hd, hp⟩ - · exact hgfactors pq ind - -theorem step4_3 {p p' : ℤ√(-3)} (hcoprime : IsCoprime p.re p.im) (hcoprime' : IsCoprime p'.re p'.im) - (h : OddPrimeOrFour p.norm.natAbs) (heq : p.norm = p'.norm) : - abs p.re = abs p'.re ∧ abs p.im = abs p'.im := - by - have hdvd : p'.norm ∣ p.norm := by rw [heq] - have him : p'.im ≠ 0 := by - apply OddPrimeOrFour.im_ne_zero _ hcoprime' - rwa [← heq] - obtain ⟨u, -, H | H, h1⟩ := step1_2 hcoprime hdvd (by rwa [← heq]) him <;> - · rw [heq] at h1 - have := Int.eq_one_of_mul_eq_self_right (Spts.ne_zero_of_coprime' _ hcoprime') h1.symm - obtain ⟨ha, hb⟩ := Spts.eq_one this - simp only [hb, Zsqrtd.ext_iff, Zsqrtd.mul_re, Zsqrtd.mul_im, add_zero, zero_add, - MulZeroClass.mul_zero] at H - rw [H.1, H.2, abs_mul, abs_mul, ha, mul_one, mul_one] - try rw [zsqrtd.conj_re, zsqrtd.conj_im, abs_neg] - simp - -theorem prod_map_norm {d : ℤ} {s : Multiset (ℤ√d)} : - (s.map Zsqrtd.norm).prod = Zsqrtd.norm s.prod := - Multiset.prod_hom s (Zsqrtd.normMonoidHom : ℤ√d →* ℤ) - -theorem prod_map_natAbs {s : Multiset ℤ} : - (s.map Int.natAbs).prod = Int.natAbs s.prod := - Multiset.prod_hom s <| - ({ toFun := Int.natAbs - map_one' := rfl - map_mul' := fun x y => Int.natAbs_mul x y } : ℤ →* ℕ) - -/-- The multiset of factors. -/ -noncomputable def factorization' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : - Multiset (ℤ√(-3)) := - Classical.choose (step3 hcoprime) - -theorem factorization'_prop {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : - (a = (factorization' hcoprime).prod ∨ a = -(factorization' hcoprime).prod) ∧ - ∀ pq : ℤ√(-3), - pq ∈ factorization' hcoprime → 0 ≤ pq.re ∧ pq.im ≠ 0 ∧ OddPrimeOrFour pq.norm.natAbs := - Classical.choose_spec (step3 hcoprime) - -theorem factorization'.coprime_of_mem {a b : ℤ√(-3)} (h : IsCoprime a.re a.im) - (hmem : b ∈ factorization' h) : IsCoprime b.re b.im := - by - obtain ⟨h1, -⟩ := factorization'_prop h - set f := factorization' h - apply Zsqrtd.coprime_of_dvd_coprime h - apply (Multiset.dvd_prod hmem).trans - cases' h1 with h1 h1 <;> rw [h1] - simp only [dvd_neg] - rfl - -theorem no_conj (s : Multiset (ℤ√(-3))) {p : ℤ√(-3)} (hp : ¬IsUnit p) - (hcoprime : IsCoprime s.prod.re s.prod.im) : ¬(p ∈ s ∧ star p ∈ s) := - by - contrapose! hp - obtain ⟨h1, h2⟩ := hp - by_cases him : p.im = 0 - · obtain ⟨t, rfl⟩ := Multiset.exists_cons_of_mem h1 - rw [Multiset.prod_cons] at hcoprime - simp only [him, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_im, Zsqrtd.mul_re, - MulZeroClass.mul_zero] at hcoprime - rw [Zsqrt3.isUnit_iff] - simp only [him, and_true_iff, eq_self_iff_true] - rw [← Int.isUnit_iff_abs_eq] - apply IsCoprime.isUnit_of_dvd' hcoprime <;> apply dvd_mul_right - · have : star p ≠ p := by - rw [Ne, Zsqrtd.ext_iff] - rintro ⟨-, H⟩ - apply him - apply eq_zero_of_neg_eq - simpa using H - obtain ⟨t1, rfl⟩ := Multiset.exists_cons_of_mem h1 - have : star p ∈ t1 := by - rw [Multiset.mem_cons] at h2 - exact h2.resolve_left this - obtain ⟨t2, rfl⟩ := Multiset.exists_cons_of_mem this - rw [Multiset.prod_cons, Multiset.prod_cons, ← mul_assoc, ← Zsqrtd.norm_eq_mul_conj] at hcoprime - rw [Zsqrtd.isUnit_iff_norm_isUnit] - apply IsCoprime.isUnit_of_dvd' hcoprime <;> - simp only [add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, dvd_mul_right, Zsqrtd.mul_re, - MulZeroClass.mul_zero, Zsqrtd.mul_im, Zsqrtd.intCast_im] - -/-- Associated elements in `ℤ√-3`. -/ -def Associated' (x y : ℤ√(-3)) : Prop := - Associated x y ∨ Associated x (star y) - -@[refl] -theorem Associated'.refl (x : ℤ√(-3)) : Associated' x x := - Or.inl (by rfl) - -theorem associated'_of_abs_eq {x y : ℤ√(-3)} (hre : abs x.re = abs y.re) - (him : abs x.im = abs y.im) : Associated' x y := - by - rw [abs_eq_abs] at hre him - cases' hre with h1 h1 <;> cases' him with h2 h2 <;> - [ - (left; use 1); - (right; use 1); - (right; use -1); - (left; use -1) - ] <;> - simp [Zsqrtd.ext_iff, h1, h2] - -theorem associated'_of_associated_norm {x y : ℤ√(-3)} - (h : Associated (Zsqrtd.norm x) (Zsqrtd.norm y)) (hx : IsCoprime x.re x.im) - (hy : IsCoprime y.re y.im) (h' : OddPrimeOrFour x.norm.natAbs) : Associated' x y := - by - have heq : x.norm = y.norm := - haveI hd : (-3 : ℤ) ≤ 0 := by norm_num - Int.eq_of_associated_of_nonneg h (Zsqrtd.norm_nonneg hd _) (Zsqrtd.norm_nonneg hd _) - obtain ⟨hre, him⟩ := step4_3 hx hy h' heq - exact associated'_of_abs_eq hre him - -theorem factorization'.associated'_of_norm_associated {a b c : ℤ√(-3)} (h : IsCoprime a.re a.im) - (hbmem : b ∈ factorization' h) (hcmem : c ∈ factorization' h) - (hnorm : Associated b.norm c.norm) : Associated' b c := by - apply associated'_of_associated_norm - · exact hnorm - · exact factorization'.coprime_of_mem h hbmem - · exact factorization'.coprime_of_mem h hcmem - · exact ((factorization'_prop h).2 b hbmem).2.2 - -theorem factors_2_even' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : - Even (evenFactorExp a.norm.natAbs) := - by - induction' hn : a.norm.natAbs using Nat.strong_induction_on with n ih generalizing a - by_cases hparity : Even a.norm.natAbs - · obtain ⟨u, huvcoprime, huvprod⟩ := step1' hcoprime (Int.natAbs_even.mp hparity) - have huv := Spts.ne_zero_of_coprime' _ huvcoprime - have h₄ : Int.natAbs 4 = 4 := by norm_num - rw [← hn, huvprod, Int.natAbs_mul, h₄, factors_2_even (by simpa using huv), Nat.even_add] - apply iff_of_true even_two - apply ih _ _ huvcoprime rfl - rw [← hn, huvprod, Int.natAbs_mul, lt_mul_iff_one_lt_left (Int.natAbs_pos.mpr huv)] - norm_num - · convert even_zero (α := ℕ) - simp only [evenFactorExp, Multiset.count_eq_zero, hn] - contrapose! hparity with hfactor - rw [hn, even_iff_two_dvd] - exact UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors hfactor - -theorem factorsOddPrimeOrFour.unique {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) {f : Multiset ℕ} - (hf : ∀ x ∈ f, OddPrimeOrFour x) (hassoc : f.prod = a.norm.natAbs) : - factorsOddPrimeOrFour a.norm.natAbs = f := by - rw [← hassoc] - refine factorsOddPrimeOrFour.unique' hf ?_ ?_ - · rw [hassoc, Int.natAbs_pos] - exact Spts.ne_zero_of_coprime' _ hcoprime - · rw [hassoc] - exact factors_2_even' hcoprime - -theorem eq_or_eq_conj_of_associated_of_re_zero {x A : ℤ√(-3)} (hx : x.re = 0) (h : Associated x A) : - x = A ∨ x = star A := by - obtain ⟨u, hu⟩ := h - obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit - have hA : A.re = 0 := by - simp only [← hu, hv1, hx, add_zero, MulZeroClass.zero_mul, Zsqrtd.mul_re, MulZeroClass.mul_zero, - Zsqrtd.intCast_im] - rw [abs_eq <| zero_le_one' ℤ] at hv2 - cases' hv2 with hv2 hv2 - · left - simpa only [hv1, hv2, mul_one, Int.cast_one] using hu - · right - simp only [hv1, hv2, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu - simp [← hu, hx, Zsqrtd.ext_iff] - -theorem eq_or_eq_conj_iff_associated'_of_nonneg {x A : ℤ√(-3)} (hx : 0 ≤ x.re) (hA : 0 ≤ A.re) : - Associated' x A ↔ x = A ∨ x = star A := by - constructor - · rintro (⟨u, hu⟩ | ⟨u, hu⟩) <;> obtain ⟨v, hv1, hv2⟩ := Zsqrt3.coe_of_isUnit' u.isUnit - -- associated x A - · by_cases hxre : x.re = 0 - · apply eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩ - · rw [hv1] at hu - rw [abs_eq <| zero_le_one' ℤ] at hv2 - cases' hv2 with habsv habsv - · left - rw [← hu, habsv, Int.cast_one, mul_one] - · exfalso - simp only [habsv, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu - apply lt_irrefl (0 : ℤ) - calc - 0 ≤ A.re := hA - _ = -x.re := ?_ - _ < 0 := ?_ - - · simp only [← hu, Zsqrtd.neg_re] - · simp only [neg_neg_iff_pos] - exact lt_of_le_of_ne hx (Ne.symm hxre) - -- associated x A.conj - · by_cases hxre : x.re = 0 - · convert(eq_or_eq_conj_of_associated_of_re_zero hxre ⟨u, hu⟩).symm - rw [star_star] - · rw [hv1] at hu - rw [abs_eq <| zero_le_one' ℤ] at hv2 - cases' hv2 with habsv habsv - · right - rw [← hu, habsv, Int.cast_one, mul_one] - · exfalso - simp only [habsv, mul_one, Int.cast_one, mul_neg, Int.cast_neg] at hu - apply lt_irrefl (0 : ℤ) - calc - 0 ≤ A.re := hA - _ = -x.re := ?_ - _ < 0 := ?_ - - · rw [← star_star A, ← hu] - simp only [Zsqrtd.neg_re, Zsqrtd.star_re] - · simp only [neg_neg_iff_pos] - apply lt_of_le_of_ne hx (Ne.symm hxre) - · rintro (rfl | rfl) - · rfl - · right - rfl - -theorem step5' - -- lemma page 54 - (a : ℤ√(-3)) - (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) : - ∃ g : Multiset (ℤ√(-3)), factorization' hcoprime = 3 • g := by - classical - obtain ⟨h1, h2⟩ := factorization'_prop hcoprime - set f := factorization' hcoprime with hf - apply Multiset.exists_smul_of_dvd_count - intro x hx - convert dvd_mul_right 3 (Multiset.count x.norm.natAbs (factorsOddPrimeOrFour r)) - have : Even (evenFactorExp r) := - by - suffices Even (3 * evenFactorExp r) - by - rw [Nat.even_mul] at this - apply this.resolve_left - decide - rw [← evenFactorExp.pow r 3, hcube] - exact factors_2_even' hcoprime - calc - Multiset.count x f = Multiset.card (Multiset.filter (x = ·) f) := by - rw [Multiset.count, Multiset.countP_eq_card_filter] - _ = Multiset.card (Multiset.filter (fun a : ℤ√(-3) => x.norm.natAbs = a.norm.natAbs) f) := - (congr_arg _ (Multiset.filter_congr fun A HA => ?_)) - _ = Multiset.countP (x.norm.natAbs = ·) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) := - (Multiset.countP_map _ f (x.norm.natAbs = ·)).symm - _ = Multiset.countP (x.norm.natAbs = ·) ((factorsOddPrimeOrFour a.norm.natAbs)) := ?_ - _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour a.norm.natAbs)) := by rw [Multiset.count] - _ = Multiset.count x.norm.natAbs ((factorsOddPrimeOrFour (r ^ 3))) := by rw [hcube] - _ = Multiset.count x.norm.natAbs (3 • _) := by rw [factorsOddPrimeOrFour.pow _ _ this] - _ = 3 * _ := Multiset.count_nsmul x.norm.natAbs _ _ - - swap - show - Multiset.countP (Eq x.norm.natAbs) (Multiset.map (Int.natAbs ∘ Zsqrtd.norm) f) = - Multiset.countP (Eq x.norm.natAbs) ((factorsOddPrimeOrFour a.norm.natAbs)) - congr 1 - · rw [factorsOddPrimeOrFour.unique hcoprime] - · intro x hx - obtain ⟨y, hy, rfl⟩ := Multiset.mem_map.mp hx - exact (h2 y hy).2.2 - · rw [← Multiset.map_map, prod_map_natAbs, prod_map_norm] - cases' h1 with h1 h1 <;> rw [h1] - rw [Zsqrtd.norm_neg] - have h2x := h2 x hx - refine' ⟨fun h => by rw [h], fun h => _⟩ - rw [← Int.associated_iff_natAbs] at h - have hassoc := factorization'.associated'_of_norm_associated hcoprime hx HA h - have eq_or_eq_conj := (eq_or_eq_conj_iff_associated'_of_nonneg h2x.1 (h2 A HA).1).mp hassoc - refine' eq_or_eq_conj.resolve_right fun H => _ - apply no_conj f - · intro HH - apply h2x.2.1 - rw [Zsqrt3.isUnit_iff] at HH - exact HH.2 - · cases' h1 with h1 h1 <;> rw [h1] at hcoprime - · exact hcoprime - · rwa [← IsCoprime.neg_neg_iff, ← Zsqrtd.neg_im, ← Zsqrtd.neg_re] - · refine' ⟨hx, _⟩ - rwa [H, star_star] - -theorem step5 - -- lemma page 54 - (a : ℤ√(-3)) - (r : ℕ) (hcoprime : IsCoprime a.re a.im) (hcube : r ^ 3 = a.norm.natAbs) : ∃ p : ℤ√(-3), a = p ^ 3 := - by - obtain ⟨f, hf⟩ := step5' a r hcoprime hcube - obtain ⟨h1, -⟩ := factorization'_prop hcoprime - cases h1 with - | inl h1 => - use f.prod - rw [h1, hf, Multiset.prod_nsmul] - | inr h1 => - use -f.prod - rw [h1, hf, Multiset.prod_nsmul, Odd.neg_pow] - norm_num; decide - -theorem step6 (a b r : ℤ) (hcoprime : IsCoprime a b) (hcube : r ^ 3 = a ^ 2 + 3 * b ^ 2) : - ∃ p q, a = p ^ 3 - 9 * p * q ^ 2 ∧ b = 3 * p ^ 2 * q - 3 * q ^ 3 := - by - set A : ℤ√(-3) := ⟨a, b⟩ with hA - have hcube' : r.natAbs ^ 3 = A.norm.natAbs := - by - rw [← Int.natAbs_pow] - apply congr_arg - simp only [hcube, Zsqrtd.norm_def, hA] - ring - obtain ⟨p, hp⟩ := step5 A r.natAbs hcoprime hcube' - use p.re, p.im - simp only [Zsqrtd.ext_iff, pow_succ', pow_two, Zsqrtd.mul_re, Zsqrtd.mul_im] at hp - convert hp using 2 <;> simp <;> ring diff --git a/FltRegular/FltThree/FltThree.lean b/FltRegular/FltThree/FltThree.lean deleted file mode 100644 index 49349b73..00000000 --- a/FltRegular/FltThree/FltThree.lean +++ /dev/null @@ -1,696 +0,0 @@ -/- -Copyright (c) 2020 Ruben Van de Velde. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. --/ - -import FltRegular.FltThree.Primes -import FltRegular.FltThree.Edwards -import Mathlib.Data.Int.GCD -import Mathlib.NumberTheory.FLT.Basic -import Mathlib.Tactic.IntervalCases - -/-- solutions to Fermat's last theorem for the exponent `3`. -/ -def FltSolution (n : ℕ) (a b c : ℤ) := - a ≠ 0 ∧ b ≠ 0 ∧ c ≠ 0 ∧ a ^ n + b ^ n = c ^ n - -/-- Coprime solutions to Fermat's last theorem for the exponent `3`. -/ -def FltCoprime (n : ℕ) (a b c : ℤ) := - FltSolution n a b c ∧ IsCoprime a b ∧ IsCoprime a c ∧ IsCoprime b c - -theorem exists_coprime {n : ℕ} (hn : 0 < n) {a b c : ℤ} (ha' : a ≠ 0) (hb' : b ≠ 0) (hc' : c ≠ 0) - (h : a ^ n + b ^ n = c ^ n) : - ∃ a' b' c' : ℤ, - a'.natAbs ≤ a.natAbs ∧ b'.natAbs ≤ b.natAbs ∧ c'.natAbs ≤ c.natAbs ∧ FltCoprime n a' b' c' := - by - set d := Int.gcd a b with hd' - obtain ⟨A, HA⟩ : ↑d ∣ a := @Int.gcd_dvd_left a b - obtain ⟨B, HB⟩ : ↑d ∣ b := @Int.gcd_dvd_right a b - obtain ⟨C, HC⟩ : ↑d ∣ c := - by - rw [← Int.pow_dvd_pow_iff hn.ne', ← h, HA, HB, mul_pow, mul_pow, ← mul_add] - exact dvd_mul_right _ _ - have hdpos : 0 < d := Int.gcd_pos_of_ne_zero_left _ ha' - have hd := Int.natCast_ne_zero_iff_pos.mpr hdpos - have hsoln : A ^ n + B ^ n = C ^ n := - by - apply Int.eq_of_mul_eq_mul_left (pow_ne_zero n hd) - simp only [mul_add, ← mul_pow, ← HA, ← HB, ← HC, h] - have hsoln' : B ^ n + A ^ n = C ^ n := by rwa [add_comm] at hsoln - have hcoprime : IsCoprime A B := - by - rw [← Int.gcd_eq_one_iff_coprime] - apply Nat.eq_of_mul_eq_mul_left hdpos - rw [← Int.natAbs_ofNat d, ← Int.gcd_mul_left, ← HA, ← HB, hd', Int.natAbs_ofNat, mul_one] - have HA' : A.natAbs ≤ a.natAbs := by - rw [HA] - simp only [Int.natAbs_ofNat, Int.natAbs_mul] - exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos) - have HB' : B.natAbs ≤ b.natAbs := by - rw [HB] - simp only [Int.natAbs_ofNat, Int.natAbs_mul] - exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos) - have HC' : C.natAbs ≤ c.natAbs := by - rw [HC] - simp only [Int.natAbs_ofNat, Int.natAbs_mul] - exact le_mul_of_one_le_left' (Nat.succ_le_iff.mpr hdpos) - exact - ⟨A, B, C, HA', HB', HC', - ⟨right_ne_zero_of_mul (by rwa [HA] at ha'), right_ne_zero_of_mul (by rwa [HB] at hb'), - right_ne_zero_of_mul (by rwa [HC] at hc'), hsoln⟩, - hcoprime, coprime_add_self_pow hn hsoln hcoprime, - coprime_add_self_pow hn hsoln' hcoprime.symm⟩ - -theorem descent1a {a b c : ℤ} (h : a ^ 3 + b ^ 3 = c ^ 3) (habcoprime : IsCoprime a b) - (haccoprime : IsCoprime a c) (hbccoprime : IsCoprime b c) : - (Even a ∧ ¬Even b ∧ ¬Even c ∨ ¬Even a ∧ Even b ∧ ¬Even c) ∨ ¬Even a ∧ ¬Even b ∧ Even c := - by - have contra : ∀ {x y : ℤ}, IsCoprime x y → Even x → Even y → False := - by - intro x y hcoprime hx hy - rw [even_iff_two_dvd] at hx hy - have := Int.isUnit_eq_one_or (hcoprime.isUnit_of_dvd' hx hy) - norm_num at this - by_cases haparity : Even a <;> by_cases hbparity : Even b <;> by_cases hcparity : Even c - · exact False.elim (contra habcoprime ‹_› ‹_›) - · exact False.elim (contra habcoprime ‹_› ‹_›) - · exact False.elim (contra haccoprime ‹_› ‹_›) - · tauto - · exact False.elim (contra hbccoprime ‹_› ‹_›) - · tauto - · tauto - · exfalso - apply hcparity - rw [← Int.even_pow' three_ne_zero, ← h] - simp [haparity, hbparity, three_ne_zero, parity_simps] - -theorem flt_not_add_self {a b c : ℤ} (ha : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3) : a ≠ b := - by - rintro rfl - rw [← mul_two] at h - obtain ⟨d, rfl⟩ : a ∣ c := - by - rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← h] - apply dvd_mul_right - apply Int.two_not_cube d - rwa [mul_pow, mul_right_inj' (pow_ne_zero 3 ha), eq_comm] at h - -theorem descent1left {a b c : ℤ} (hapos : a ≠ 0) (h : a ^ 3 + b ^ 3 = c ^ 3) - (hbccoprime : IsCoprime b c) (hb : ¬Even b) (hc : ¬Even c) : - ∃ p q : ℤ, - p ≠ 0 ∧ q ≠ 0 ∧ IsCoprime p q ∧ (Even p ↔ ¬Even q) ∧ 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 := - by - obtain ⟨p, hp⟩ : Even (c - b) := by simp [hb, hc, parity_simps] - obtain ⟨q, hq⟩ : Even (c + b) := by simp [hb, hc, parity_simps] - rw [← two_mul] at hp hq - obtain rfl : p + q = c := by - apply Int.eq_of_mul_eq_mul_left two_ne_zero - rw [mul_add, ← hp, ← hq] - ring - obtain rfl : q - p = b := by - apply Int.eq_of_mul_eq_mul_left two_ne_zero - rw [mul_sub, ← hp, ← hq] - ring - have hpnezero : p ≠ 0 := by - rintro rfl - rw [sub_zero, zero_add, add_left_eq_self] at h - exact hapos (pow_eq_zero h) - have hqnezero : q ≠ 0 := by - rintro rfl - rw [zero_sub, add_zero, Odd.neg_pow (by norm_num; decide), ← sub_eq_add_neg, - sub_eq_iff_eq_add] at h - exact flt_not_add_self hpnezero h.symm rfl - refine' ⟨p, q, hpnezero, hqnezero, _, _, _⟩ - · apply isCoprime_of_dvd _ _ (not_and_of_not_left _ hpnezero) - rintro z hznu - hzp hzq - apply hznu - exact hbccoprime.isUnit_of_dvd' (dvd_sub hzq hzp) (dvd_add hzp hzq) - · constructor <;> intro H <;> simpa [H, parity_simps] using hc - · rw [eq_sub_of_add_eq h] - ring - -theorem descent1 (a b c : ℤ) (h : FltCoprime 3 a b c) : - ∃ p q : ℤ, - p ≠ 0 ∧ - q ≠ 0 ∧ - IsCoprime p q ∧ - (Even p ↔ ¬Even q) ∧ - (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ - 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) := - by - obtain ⟨⟨hapos, hbpos, hcpos, h⟩, habcoprime, haccoprime, hbccoprime⟩ := h - obtain (⟨-, hb, hc⟩ | ⟨ha, hb, hc⟩) | ⟨ha, hb, -⟩ := - descent1a h habcoprime haccoprime hbccoprime - · obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1left hapos h hbccoprime hb hc - exact ⟨p, q, hp, hq, hcoprime, hodd, Or.inl hcube⟩ - · rw [add_comm] at h - obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1left hbpos h haccoprime ha hc - refine' ⟨p, q, hp, hq, hcoprime, hodd, Or.inr <| Or.inl hcube⟩ - · have := descent1left hcpos ?_ habcoprime.neg_left ?_ hb - obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := this - exact ⟨p, q, hp, hq, hcoprime, hodd, Or.inr <| Or.inr hcube⟩ - · rw [← h] - ring - · simp [ha, parity_simps] - -theorem descent11 {a b c d : ℤ} (h : d = a ∨ d = b ∨ d = c) : d ∣ a * b * c := - by - rcases h with (rfl | rfl | rfl) - · exact (dvd_mul_right _ _).mul_right _ - · exact (dvd_mul_left _ _).mul_right _ - · exact dvd_mul_left _ _ - -theorem descent2 (a b c : ℤ) (h : FltCoprime 3 a b c) : - ∃ p q : ℤ, - p ≠ 0 ∧ - q ≠ 0 ∧ - IsCoprime p q ∧ - (Even p ↔ ¬Even q) ∧ - (2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ - 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) ∧ - (2 * p).natAbs < (a ^ 3 * b ^ 3 * c ^ 3).natAbs := - by - obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube⟩ := descent1 a b c h - refine' ⟨p, q, hp, hq, hcoprime, hodd, hcube, _⟩ - obtain ⟨⟨hapos, hbpos, hcpos, -⟩, -⟩ := h - set P : ℤ√(-3) := ⟨p, q⟩ - apply lt_of_lt_of_le (b := (2 * p * P.norm).natAbs) - -- calc - -- (2 * p).natAbs < (2 * p * P.norm).natAbs := ?_ - -- _ ≤ (a ^ 3 * b ^ 3 * c ^ 3).natAbs := ?_ - - · rw [Int.natAbs_mul (2 * p)] - apply lt_mul_of_one_lt_right (Int.natAbs_pos.mpr (mul_ne_zero two_ne_zero hp)) - rw [← Int.ofNat_lt] - rw [Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) P)] - exact Spts.one_lt_of_im_ne_zero ⟨p, q⟩ hq - · apply Nat.le_of_dvd - · rw [pos_iff_ne_zero, Int.natAbs_ne_zero, ← mul_pow, ← mul_pow] - exact pow_ne_zero 3 (mul_ne_zero (mul_ne_zero hapos hbpos) hcpos) - · rw [Int.natAbs_dvd_natAbs] - convert descent11 hcube - rw [Zsqrtd.norm] - ring - - -theorem Nat.cast_three [AddMonoidWithOne R] : ((3 : ℕ) : R) = (3 : R) := rfl - - -theorem gcd1or3 (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : Even p ↔ ¬Even q) : - Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 1 ∨ Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) = 3 := - by - set g := Int.gcd (2 * p) (p ^ 2 + 3 * q ^ 2) with hg' - suffices H : ∃ k, g = 3 ^ k ∧ k < 2 by - obtain ⟨k, hg, hk⟩ := H - interval_cases k - · left - rw [pow_zero] at hg - exact hg - · right - rw [pow_one] at hg - exact hg - have basic : ∀ f, Nat.Prime f → (f : ℤ) ∣ 2 * p → (f : ℤ) ∣ p ^ 2 + 3 * q ^ 2 → f = 3 := - by - intro d hdprime hdleft hdright - by_contra hne3 - rw [← Ne] at hne3 - apply (Nat.prime_iff_prime_int.mp hdprime).not_unit - have hne2 : d ≠ 2 := by - rintro rfl - rw [Nat.cast_two, ← even_iff_two_dvd] at hdright - have : ¬ Even (3 : ℤ) := by decide - simp [this, hparity, two_ne_zero, parity_simps] at hdright - have : 2 < d := lt_of_le_of_ne hdprime.two_le hne2.symm - have : 3 < d := lt_of_le_of_ne this hne3.symm - obtain ⟨P, hP⟩ := hdleft - obtain ⟨Q, hQ⟩ := hdright - obtain ⟨H, hH⟩ : 2 ∣ P := by - have H := dvd_mul_right 2 p - rw [hP] at H - apply (Prime.dvd_or_dvd Int.prime_two H).resolve_left - rw [Int.dvd_natCast] - change ¬2 ∣ d - rw [Nat.prime_dvd_prime_iff_eq Nat.prime_two hdprime] - exact hne2.symm - have hp : p = d * H := by rw [← mul_right_inj' (two_ne_zero' ℤ), hP, hH, mul_left_comm] - apply hcoprime.isUnit_of_dvd' - · rw [hp] - exact dvd_mul_right _ _ - · have h000 : d ∣ 3 * q.natAbs ^ 2 := - by - rw [← Int.natCast_dvd_natCast, Int.ofNat_mul, Int.natCast_pow, Int.natAbs_sq, Nat.cast_three] - use Q - d * H ^ 2 - rw [mul_sub, ← hQ, hp] - ring - cases' (Nat.Prime.dvd_mul hdprime).mp h000 with h000 h000 - · rw [Nat.prime_dvd_prime_iff_eq hdprime Nat.prime_three] at h000 - exact absurd h000 hne3 - · rw [Int.natCast_dvd] - exact Nat.Prime.dvd_of_dvd_pow hdprime h000 - set k := g.factors.length - have hg : g = 3 ^ k := by - apply Nat.eq_prime_pow_of_unique_prime_dvd - · apply ne_of_gt - apply Nat.gcd_pos_of_pos_left - rw [Int.natAbs_mul] - apply mul_pos zero_lt_two - rwa [pos_iff_ne_zero, Int.natAbs_ne_zero] - intro d hdprime hddvdg - rw [← Int.natCast_dvd_natCast] at hddvdg - apply basic _ hdprime <;> apply dvd_trans hddvdg <;> rw [hg'] - exacts[Int.gcd_dvd_left, Int.gcd_dvd_right] - refine' ⟨k, hg, _⟩ - by_contra! H - rw [← pow_mul_pow_sub _ H] at hg - have : ¬IsUnit (3 : ℤ) := by - rw [Int.isUnit_iff_natAbs_eq] - norm_num - apply this - have hdvdp : 3 ∣ p := - by - suffices 3 ∣ 2 * p - by - apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two this - norm_num - have : 3 ∣ (g : ℤ) := by - rw [hg, pow_two, mul_assoc, Int.ofNat_mul] - apply dvd_mul_right - exact dvd_trans this Int.gcd_dvd_left - apply IsCoprime.isUnit_of_dvd' hcoprime hdvdp - · rw [← Int.pow_dvd_pow_iff two_ne_zero] at hdvdp - apply Prime.dvd_of_dvd_pow Int.prime_three - rw [← mul_dvd_mul_iff_left (three_ne_zero' ℤ), ← pow_two, ← dvd_add_right hdvdp] - refine' dvd_trans _ Int.gcd_dvd_right - rw [← hg', hg, Int.ofNat_mul] - apply dvd_mul_right - -theorem obscure' (p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) (hparity : Even p ↔ ¬Even q) - (hcube : ∃ r, p ^ 2 + 3 * q ^ 2 = r ^ 3) : - ∃ a b, - p = a * (a - 3 * b) * (a + 3 * b) ∧ - q = 3 * b * (a - b) * (a + b) ∧ IsCoprime a b ∧ (Even a ↔ ¬Even b) := - by - obtain ⟨u, hu⟩ := hcube - obtain ⟨a, b, hp', hq'⟩ := step6 p q u hcoprime hu.symm - refine' ⟨a, b, _, _, _, _⟩ - · rw [hp'] - ring - · rw [hq'] - ring - · apply isCoprime_of_dvd - · rintro ⟨rfl, rfl⟩ - norm_num at hp' - contradiction - rintro k hknu - hkdvdleft hkdvdright - apply hknu - apply hcoprime.isUnit_of_dvd' - · rw [hp'] - apply dvd_sub - · exact dvd_pow hkdvdleft (by norm_num) - · rw [mul_comm (9 : ℤ), mul_assoc] - exact hkdvdleft.mul_right _ - · rw [hq'] - apply dvd_sub - · exact hkdvdright.mul_left _ - · exact (hkdvdright.pow (by norm_num)).mul_left _ - · - by_cases haparity : Even a <;> by_cases hbparity : Even b <;> [skip; tauto; tauto; skip] <;> - · exfalso - have : Even p := by - rw [hp'] - have : ¬ Even (9 : ℤ) := by decide - simp [this, haparity, hbparity, three_ne_zero, parity_simps] - have : Even q := by - rw [hq'] - simp [haparity, hbparity, three_ne_zero, parity_simps] - tauto - -theorem Int.cube_of_coprime (a b c s : ℤ) (ha : a ≠ 0) (hb : b ≠ 0) (hc : c ≠ 0) - (hcoprimeab : IsCoprime a b) (hcoprimeac : IsCoprime a c) (hcoprimebc : IsCoprime b c) - (hs : a * b * c = s ^ 3) : ∃ A B C, A ≠ 0 ∧ B ≠ 0 ∧ C ≠ 0 ∧ a = A ^ 3 ∧ b = B ^ 3 ∧ c = C ^ 3 := - by - have : Odd 3 := by decide - obtain ⟨⟨AB, HAB⟩, ⟨C, HC⟩⟩ := - Int.eq_pow_of_mul_eq_pow_odd (IsCoprime.mul_left hcoprimeac hcoprimebc) this hs - obtain ⟨⟨A, HA⟩, ⟨B, HB⟩⟩ := Int.eq_pow_of_mul_eq_pow_odd hcoprimeab this HAB - refine' ⟨A, B, C, _, _, _, HA, HB, HC⟩ <;> apply ne_zero_pow three_ne_zero - · rwa [← HA] - · rwa [← HB] - · rwa [← HC] - -theorem Int.gcd1_coprime12 (u v : ℤ) (huvcoprime : IsCoprime u v) (notdvd_2_2 : ¬2 ∣ u - 3 * v) - (not_3_dvd_2 : ¬3 ∣ u - 3 * v) : IsCoprime (2 * u) (u - 3 * v) := - by - apply isCoprime_of_prime_dvd - · rintro ⟨-, h2⟩ - rw [h2] at notdvd_2_2 - norm_num at notdvd_2_2 - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - apply huvcoprime.isUnit_of_dvd' - · exact Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdright Int.prime_two hkdvdleft - · apply Int.dvd_mul_cancel_prime' not_3_dvd_2 hkdvdright Int.prime_three - apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdright Int.prime_two - convert dvd_sub hkdvdleft (hkdvdright.mul_left 2) using 1 - ring - -theorem Int.gcd1_coprime13 (u v : ℤ) (huvcoprime : IsCoprime u v) (this' : ¬Even (u + 3 * v)) - (notdvd_3_3 : ¬3 ∣ u + 3 * v) : IsCoprime (2 * u) (u + 3 * v) := - by - rw [even_iff_two_dvd] at this' - apply isCoprime_of_prime_dvd - · rintro ⟨-, h2⟩ - rw [h2] at this' - norm_num at this' - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - apply huvcoprime.isUnit_of_dvd' - · exact Int.dvd_mul_cancel_prime' this' hkdvdright Int.prime_two hkdvdleft - · apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three - apply Int.dvd_mul_cancel_prime' this' hkdvdright Int.prime_two - convert dvd_sub (hkdvdright.mul_left 2) hkdvdleft using 1 - ring - -theorem Int.gcd1_coprime23 (u v : ℤ) (huvcoprime : IsCoprime u v) (notdvd_2_2 : ¬2 ∣ u - 3 * v) - (notdvd_3_3 : ¬3 ∣ u + 3 * v) : IsCoprime (u - 3 * v) (u + 3 * v) := - by - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - rw [h1] at notdvd_2_2 - norm_num at notdvd_2_2 - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - apply huvcoprime.isUnit_of_dvd' - · apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two - convert dvd_add hkdvdleft hkdvdright using 1 - ring - · apply Int.dvd_mul_cancel_prime' notdvd_3_3 hkdvdright Int.prime_three - apply Int.dvd_mul_cancel_prime' notdvd_2_2 hkdvdleft Int.prime_two - convert dvd_sub hkdvdright hkdvdleft using 1 - ring - -theorem descent_gcd1 (a b c p q : ℤ) (hp : p ≠ 0) (hcoprime : IsCoprime p q) - (hodd : Even p ↔ ¬Even q) - (hcube : - 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ - 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) - (hgcd : IsCoprime (2 * p) (p ^ 2 + 3 * q ^ 2)) : - ∃ a' b' c' : ℤ, - a' ≠ 0 ∧ - b' ≠ 0 ∧ - c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3 := - by - -- 5. - obtain ⟨r, hr⟩ : ∃ r, 2 * p * (p ^ 2 + 3 * q ^ 2) = r ^ 3 := by - rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)] - have : Odd 3 := by decide - obtain ⟨hcubeleft, hcuberight⟩ := Int.eq_pow_of_mul_eq_pow_odd hgcd this hr - -- todo shadowing hq - obtain ⟨u, v, hpfactor, hq, huvcoprime, huvodd⟩ := obscure' p q hp hcoprime hodd hcuberight - have u_ne_zero : u ≠ 0 := by - rintro rfl - rw [MulZeroClass.zero_mul, MulZeroClass.zero_mul] at hpfactor - contradiction - have haaa : 2 * p = 2 * u * (u - 3 * v) * (u + 3 * v) := - by - rw [hpfactor] - ring - have : ¬ Even (3 : ℤ) := by decide - have : ¬Even (u - 3 * v) := by simp [‹¬ Even (3 : ℤ)›, huvodd, parity_simps] - have : ¬Even (u + 3 * v) := by simp [‹¬ Even (3 : ℤ)›, huvodd, parity_simps] - have notdvd_2_2 : ¬2 ∣ u - 3 * v := by - rw [← even_iff_two_dvd] - exact ‹¬Even (u - 3 * v)› - have hddd : ¬3 ∣ p := by - intro H - have : 3 ∣ p ^ 2 + 3 * q ^ 2 := by - apply dvd_add - · rw [pow_two] - exact H.mul_left _ - · apply dvd_mul_right - have : 3 ∣ 2 * p := H.mul_left 2 - have := IsCoprime.isUnit_of_dvd' hgcd ‹_› ‹_› - rw [isUnit_iff_dvd_one] at this - norm_num at this - have not_3_dvd_2 : ¬3 ∣ u - 3 * v := by - intro hd2 - apply hddd - rw [hpfactor] - exact (hd2.mul_left _).mul_right _ - have notdvd_3_3 : ¬3 ∣ u + 3 * v := by - intro hd3 - apply hddd - rw [hpfactor] - exact hd3.mul_left _ - obtain ⟨s, hs⟩ := hcubeleft - obtain ⟨C, A, B, HCpos, HApos, HBpos, HC, HA, HB⟩ : - ∃ X Y Z : ℤ, X ≠ 0 ∧ Y ≠ 0 ∧ Z ≠ 0 ∧ 2 * u = X ^ 3 ∧ u - 3 * v = Y ^ 3 ∧ u + 3 * v = Z ^ 3 := - by - apply Int.cube_of_coprime (2 * u) (u - 3 * v) (u + 3 * v) s - · apply mul_ne_zero two_ne_zero u_ne_zero - · rw [sub_ne_zero] - rintro rfl - simp only [‹¬ Even (3 : ℤ)›, false_or_iff, iff_not_self, parity_simps] at huvodd - · intro H - rw [add_eq_zero_iff_eq_neg] at H - simp [‹¬ Even (3 : ℤ)›, H, parity_simps] at huvodd - · apply Int.gcd1_coprime12 u v <;> assumption - · apply Int.gcd1_coprime13 u v <;> assumption - · apply Int.gcd1_coprime23 u v <;> assumption - · rw [← haaa] - exact hs - refine' ⟨A, B, C, HApos, HBpos, HCpos, _, _⟩ - · rw [mul_comm, ← mul_assoc (C ^ 3), ← HA, ← HB, ← HC, ← haaa] - · rw [← HA, ← HB, ← HC] - ring - -theorem gcd3_coprime {u v : ℤ} (huvcoprime : IsCoprime u v) (huvodd : Even u ↔ ¬Even v) : - IsCoprime (2 * v) (u + v) ∧ IsCoprime (2 * v) (u - v) ∧ IsCoprime (u - v) (u + v) := - by - have haddodd : ¬Even (u + v) := by simp [huvodd, parity_simps] - have hsubodd : ¬Even (u - v) := by simp [huvodd, parity_simps] - have haddcoprime : IsCoprime (u + v) (2 * v) := by - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - rw [h1] at haddodd - norm_num at haddodd - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - have hkdvdright' : k ∣ v := by - rw [even_iff_two_dvd] at haddodd - exact Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two hkdvdright - apply huvcoprime.isUnit_of_dvd' _ hkdvdright' - simpa using dvd_sub hkdvdleft hkdvdright' - have hsubcoprime : IsCoprime (u - v) (2 * v) := by - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - rw [h1] at hsubodd - norm_num at hsubodd - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - have hkdvdright' : k ∣ v := by - rw [even_iff_two_dvd] at hsubodd - exact Int.dvd_mul_cancel_prime' hsubodd hkdvdleft Int.prime_two hkdvdright - apply huvcoprime.isUnit_of_dvd' _ hkdvdright' - rw [← sub_add_cancel u v] - exact dvd_add hkdvdleft hkdvdright' - have haddsubcoprime : IsCoprime (u + v) (u - v) := by - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - rw [h1] at haddodd - norm_num at haddodd - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - rw [even_iff_two_dvd] at haddodd - apply huvcoprime.isUnit_of_dvd' <;> - apply Int.dvd_mul_cancel_prime' haddodd hkdvdleft Int.prime_two - · convert dvd_add hkdvdleft hkdvdright using 1 - ring - · convert dvd_sub hkdvdleft hkdvdright using 1 - ring - exact ⟨haddcoprime.symm, hsubcoprime.symm, haddsubcoprime.symm⟩ - -theorem descent_gcd3_coprime {q s : ℤ} (h3_ndvd_q : ¬3 ∣ q) (hspos : s ≠ 0) - (hcoprime' : IsCoprime s q) (hodd' : Even q ↔ ¬Even s) : - IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2) := - by - have h2ndvd : ¬2 ∣ q ^ 2 + 3 * s ^ 2 := - by - rw [← even_iff_two_dvd] - have : ¬ Even (3 : ℤ) := by decide - simp [this, two_ne_zero, hodd', parity_simps] - have h3ndvd : ¬3 ∣ q ^ 2 + 3 * s ^ 2 := by - intro H - apply h3_ndvd_q - rw [dvd_add_left (dvd_mul_right _ _)] at H - exact Prime.dvd_of_dvd_pow Int.prime_three H - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - rw [mul_eq_zero] at h1 - exact hspos (h1.resolve_left (by norm_num)) - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - have : k ∣ s := by - apply Int.dvd_mul_cancel_prime' h2ndvd hkdvdright Int.prime_two - apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three - apply Int.dvd_mul_cancel_prime' h3ndvd hkdvdright Int.prime_three - convert hkdvdleft using 1 - ring - apply hcoprime'.isUnit_of_dvd' this - apply hkprime.dvd_of_dvd_pow - rw [← dvd_add_left ((this.pow two_ne_zero).mul_left _)] - exact hkdvdright - -theorem descent_gcd3 (a b c p q : ℤ) (hp : p ≠ 0) (hq : q ≠ 0) (hcoprime : IsCoprime p q) - (hodd : Even p ↔ ¬Even q) - (hcube : - 2 * p * (p ^ 2 + 3 * q ^ 2) = a ^ 3 ∨ - 2 * p * (p ^ 2 + 3 * q ^ 2) = b ^ 3 ∨ 2 * p * (p ^ 2 + 3 * q ^ 2) = c ^ 3) - (hgcd : (2 * p).gcd (p ^ 2 + 3 * q ^ 2) = 3) : - ∃ a' b' c' : ℤ, - a' ≠ 0 ∧ - b' ≠ 0 ∧ - c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3 := - by - -- 1. - have h3_dvd_p : 3 ∣ p := - by - apply Int.dvd_mul_cancel_prime' _ dvd_rfl Int.prime_two - · zify at hgcd - rw [← hgcd] - exact Int.gcd_dvd_left - · norm_num - have h3_ndvd_q : ¬3 ∣ q := by - intro H - have := hcoprime.isUnit_of_dvd' h3_dvd_p H - rw [Int.isUnit_iff_natAbs_eq] at this - norm_num at this - -- 2. - obtain ⟨s, rfl⟩ := h3_dvd_p - have hspos : s ≠ 0 := right_ne_zero_of_mul hp - have hps : 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = 3 ^ 2 * 2 * s * (q ^ 2 + 3 * s ^ 2) := by - ring - -- 3. - have hcoprime' : IsCoprime s q := by - apply isCoprime_of_prime_dvd - · rintro ⟨h1, -⟩ - exact hspos h1 - intro k hkprime hkdvdleft hkdvdright - apply hkprime.not_unit - apply hcoprime.isUnit_of_dvd' _ hkdvdright - exact hkdvdleft.mul_left 3 - have hodd' : Even q ↔ ¬Even s := - by - rw [Iff.comm, not_iff_comm, Iff.comm] - have : ¬ Even (3 : ℤ) := by decide - simpa [this, parity_simps] using hodd - have hcoprime'' : IsCoprime (3 ^ 2 * 2 * s) (q ^ 2 + 3 * s ^ 2) := - descent_gcd3_coprime h3_ndvd_q hspos hcoprime' hodd' - -- 4. - obtain ⟨r, hr⟩ : ∃ r, 2 * (3 * s) * ((3 * s) ^ 2 + 3 * q ^ 2) = r ^ 3 := by - rcases hcube with (hcube | hcube | hcube) <;> [(use a); (use b); (use c)] - rw [hps] at hr - have : Odd 3 := by norm_num; decide - obtain ⟨hcubeleft, hcuberight⟩ := Int.eq_pow_of_mul_eq_pow_odd hcoprime'' this hr - -- 5. - -- todo shadows hq hq - obtain ⟨u, v, hq, hs, huvcoprime, huvodd⟩ := obscure' q s hq hcoprime'.symm hodd' hcuberight - have hv : v ≠ 0 := by - rintro rfl - norm_num at hs - contradiction - -- 6. - obtain ⟨haddcoprime, hsubcoprime, haddsubcoprime⟩ := gcd3_coprime huvcoprime huvodd - -- 7. - obtain ⟨e, he⟩ := hcubeleft - have : 3 ∣ e := - by - rw [← Int.pow_dvd_pow_iff (by norm_num : 3 ≠ 0), ← he, hs] - convert dvd_mul_right _ (2 * v * (u - v) * (u + v)) using 1 - norm_num - ring - obtain ⟨t, rfl⟩ := this - have ht : 2 * v * (u - v) * (u + v) = t ^ 3 := - by - have : (3 ^ 3 : ℤ) ≠ 0 := by norm_num - rw [← mul_right_inj' this, ← mul_pow, ← he, hs] - ring - obtain ⟨A, B, C, HApos, HBpos, HCpos, HA, HB, HC⟩ : - ∃ X Y Z : ℤ, X ≠ 0 ∧ Y ≠ 0 ∧ Z ≠ 0 ∧ 2 * v = X ^ 3 ∧ u - v = Y ^ 3 ∧ u + v = Z ^ 3 := - by - apply Int.cube_of_coprime - · exact mul_ne_zero two_ne_zero hv - · intro H - rw [sub_eq_zero] at H - simp [H, parity_simps] at huvodd - · intro H - rw [add_eq_zero_iff_eq_neg] at H - simp [H, parity_simps] at huvodd - · exact hsubcoprime - · exact haddcoprime - · exact haddsubcoprime - · exact ht - refine' ⟨A, B, C, HApos, HBpos, HCpos, _, _⟩ - -- 9. - · rw [← mul_assoc, mul_comm, ← mul_assoc (C ^ 3), ← HA, ← HB, ← HC] - set x := v * (u - v) * (u + v) with hx - calc - ((u + v) * (2 * v) * (u - v)).natAbs = (2 * x).natAbs := - by - rw [hx] - congr 1 - ring - _ = 2 * x.natAbs := by - rw [Int.natAbs_mul 2] - rfl - _ ≤ 3 * x.natAbs := (Nat.mul_le_mul_right _ (by norm_num)) - _ = (3 * x).natAbs := by - rw [Int.natAbs_mul 3] - rfl - _ = s.natAbs := by - rw [hx, hs] - congr 1 - ring - _ ≤ 2 * 3 * s.natAbs := (Nat.le_mul_of_pos_left _ (by norm_num)) - _ = (2 * 3 * s).natAbs := by - rw [Int.natAbs_mul (2 * 3)] - rfl - - · rw [← HA, ← HB, ← HC] - ring - -theorem descent (a b c : ℤ) (h : FltCoprime 3 a b c) : - ∃ a' b' c' : ℤ, - a' ≠ 0 ∧ - b' ≠ 0 ∧ c' ≠ 0 ∧ (a' * b' * c').natAbs < (a * b * c).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3 := - by - -- 3. - have := descent2 a b c h - obtain ⟨p, q, hp, hq, hcoprime, hodd, hcube, haaa⟩ := this - suffices - ∃ a' b' c' : ℤ, - a' ≠ 0 ∧ - b' ≠ 0 ∧ - c' ≠ 0 ∧ (a' ^ 3 * b' ^ 3 * c' ^ 3).natAbs ≤ (2 * p).natAbs ∧ a' ^ 3 + b' ^ 3 = c' ^ 3 - by - obtain ⟨a', b', c', ha', hb', hc', hsmaller, hsolution⟩ := this - refine' ⟨a', b', c', ha', hb', hc', _, hsolution⟩ - rw [← Nat.pow_lt_pow_iff_left three_ne_zero] - convert lt_of_le_of_lt hsmaller haaa <;> simp [mul_pow, Int.natAbs_mul, Int.natAbs_pow] - -- 4. - cases' gcd1or3 p q hp hcoprime hodd with hgcd hgcd - -- 5. - · rw [Int.gcd_eq_one_iff_coprime] at hgcd - apply descent_gcd1 a b c p q hp hcoprime hodd hcube hgcd - · apply descent_gcd3 a b c p q hp hq hcoprime hodd hcube hgcd - -theorem flt_three : FermatLastTheoremWith ℤ 3 := by - intros a b c ha hb hc - induction' h : (a * b * c).natAbs using Nat.strong_induction_on with k' IH generalizing a b c - intro H - obtain ⟨x'', y'', z'', hxle, hyle, hzle, hcoprime⟩ := exists_coprime zero_lt_three ha hb hc H - obtain ⟨x', y', z', hx'pos, hy'pos, hz'pos, hsmaller, hsolution⟩ := descent x'' y'' z'' hcoprime - refine' IH (x' * y' * z').natAbs _ _ _ _ hx'pos hy'pos hz'pos rfl hsolution - apply lt_of_lt_of_le hsmaller - rw [← h] - simp only [Int.natAbs_mul] - exact Nat.mul_le_mul (Nat.mul_le_mul hxle hyle) hzle diff --git a/FltRegular/FltThree/OddPrimeOrFour.lean b/FltRegular/FltThree/OddPrimeOrFour.lean deleted file mode 100644 index e22e32a5..00000000 --- a/FltRegular/FltThree/OddPrimeOrFour.lean +++ /dev/null @@ -1,209 +0,0 @@ -/- -Copyright (c) 2020 Ruben Van de Velde. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. --/ -import Mathlib.RingTheory.UniqueFactorizationDomain -import Mathlib.Algebra.GCDMonoid.Nat -import Mathlib.Data.Nat.Prime.Basic - -/-- Being equal to `4` or odd. -/ -def OddPrimeOrFour (z : ℕ) : Prop := - z = 4 ∨ Nat.Prime z ∧ Odd z - -theorem OddPrimeOrFour.ne_zero {z : ℕ} (h : OddPrimeOrFour z) : z ≠ 0 := - by - obtain rfl | ⟨h, -⟩ := h - · norm_num - · exact h.ne_zero - -theorem OddPrimeOrFour.ne_one {z : ℕ} (h : OddPrimeOrFour z) : z ≠ 1 := - by - obtain rfl | ⟨h, -⟩ := h - · norm_num - · exact h.ne_one - -theorem OddPrimeOrFour.one_lt {z : ℕ} (h : OddPrimeOrFour z) : 1 < z := - by - obtain rfl | ⟨h, -⟩ := h - · norm_num - · exact h.one_lt - -theorem OddPrimeOrFour.not_unit {z : ℕ} (h : OddPrimeOrFour z) : ¬IsUnit z := - by - obtain rfl | ⟨h, -⟩ := h - · rw [isUnit_iff_dvd_one] - norm_num - · exact h.not_unit - -theorem OddPrimeOrFour.exists_and_dvd {n : ℕ} (n2 : 2 < n) : ∃ p, p ∣ n ∧ OddPrimeOrFour p := by - obtain h4 | ⟨p, hpprime, hpdvd, hpodd⟩ := Nat.four_dvd_or_exists_odd_prime_and_dvd_of_two_lt n2 - · exact ⟨4, h4, Or.inl rfl⟩ - · exact ⟨p, hpdvd, Or.inr ⟨hpprime, hpodd⟩⟩ - -theorem eq_of_dvd {a p : ℕ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (h : p ∣ a) : - p = a := - by - obtain rfl | ⟨ap, aodd⟩ := ha <;> obtain rfl | ⟨pp, podd⟩ := hp - · rfl - · exfalso - have h0 : (4 : ℕ) = 2 ^ 2 := by norm_num - rw [h0] at h - refine' Nat.even_iff_not_odd.mp _ podd - rw [even_iff_two_dvd] - refine pp.dvd_symm Nat.prime_two (pp.dvd_of_dvd_pow h) - · exfalso - rw [Nat.odd_iff_not_even] at aodd - refine' aodd _ - rw [even_iff_two_dvd] - refine' dvd_trans _ h - norm_num - · rwa [Nat.prime_dvd_prime_iff_eq pp ap] at h - -theorem dvd_or_dvd {a p x : ℕ} (ha : OddPrimeOrFour a) (hp : OddPrimeOrFour p) (hdvd : p ∣ a * x) : - p ∣ a ∨ p ∣ x := by - obtain rfl | ⟨pp, -⟩ := hp - · obtain rfl | ⟨ap, aodd⟩ := ha - · exact Or.inl dvd_rfl - · right - have : (4 : ℕ) = 2 ^ 2 := by norm_num - rw [this] at hdvd⊢ - apply Nat.prime_two.prime.pow_dvd_of_dvd_mul_left _ _ hdvd - rwa [← even_iff_two_dvd, ← Nat.odd_iff_not_even] - · exact pp.dvd_mul.mp hdvd - -theorem mem_of_dvd_prod {p : ℕ} (hp : OddPrimeOrFour p) {s : Multiset ℕ} - (hs : ∀ r ∈ s, OddPrimeOrFour r) (hdvd : p ∣ s.prod) : p ∈ s := - by - induction' s using Multiset.induction_on with a s ih hs - · simp [hp.ne_one] at hdvd - · rw [Multiset.prod_cons] at hdvd - have := hs a (Multiset.mem_cons_self _ _) - obtain h | h := dvd_or_dvd this hp hdvd - · rw [eq_of_dvd this hp h] - exact Multiset.mem_cons_self _ _ - · have := ih (fun r hr => hs _ (Multiset.mem_cons_of_mem hr)) h - exact Multiset.mem_cons_of_mem this - -theorem factors_unique_prod' : - ∀ {f g : Multiset ℕ}, - (∀ x ∈ f, OddPrimeOrFour x) → - (∀ x ∈ g, OddPrimeOrFour x) → - f.prod = g.prod → f = g := - by - intro f - induction' f using Multiset.induction_on with p f ih - · rintro g - hg h - rw [Multiset.prod_zero] at h - symm - apply Multiset.eq_zero_of_forall_not_mem - intro x hx - apply (hg x hx).not_unit - rw [isUnit_iff_dvd_one] - exact dvd_trans (Multiset.dvd_prod hx) h.symm.dvd - · intro g hf hg hfg - have hp := hf p (Multiset.mem_cons_self _ _) - have hdvd : p ∣ g.prod := - by - rw [← hfg, Multiset.prod_cons] - exact dvd_mul_right _ _ - have hbg := mem_of_dvd_prod hp hg hdvd - rw [← Multiset.cons_erase hbg] - congr - apply ih _ _ _ - · exact fun q hq => hf _ (Multiset.mem_cons_of_mem hq) - · exact fun q hq => hg q (Multiset.mem_of_mem_erase hq) - · apply mul_left_cancel₀ hp.ne_zero - rwa [Multiset.prod_erase hbg, ← Multiset.prod_cons] - -/-- The odd factors. -/ -noncomputable def oddFactors (x : ℕ) := - Multiset.filter Odd (UniqueFactorizationMonoid.normalizedFactors x) - -theorem oddFactors.zero : oddFactors 0 = 0 := by - simp [oddFactors] - -theorem oddFactors.pow (z : ℕ) (n : ℕ) : oddFactors (z ^ n) = n • oddFactors z := - by - simp only [oddFactors] - rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.filter_nsmul] - -/-- The exponent of `2` in the factorization. -/ -noncomputable def evenFactorExp (x : ℕ) := - Multiset.count 2 (UniqueFactorizationMonoid.normalizedFactors x) - -theorem evenFactorExp.pow (z : ℕ) (n : ℕ) : evenFactorExp (z ^ n) = n * evenFactorExp z := - by - simp only [evenFactorExp] - rw [UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul] - -theorem even_and_odd_factors'' (x : ℕ) : - UniqueFactorizationMonoid.normalizedFactors x = - (UniqueFactorizationMonoid.normalizedFactors x).filter (Eq 2) + oddFactors x := - by - by_cases hx : x = 0 - · - rw [hx, UniqueFactorizationMonoid.normalizedFactors_zero, oddFactors.zero, Multiset.filter_zero, - add_zero] - simp [evenFactorExp, oddFactors] - rw [Multiset.filter_add_filter] - convert (add_zero - (Multiset.filter (fun a => 2 = a ∨ Odd a) (UniqueFactorizationMonoid.normalizedFactors x))).symm - · symm - rw [Multiset.filter_eq_self] - intro a ha - rw [eq_comm] - have hprime : Prime a := UniqueFactorizationMonoid.prime_of_normalized_factor a ha - exact hprime.nat_prime.eq_two_or_odd' - · rw [Multiset.filter_eq_nil] - rintro a ha ⟨rfl, hodd⟩ - norm_num at hodd - -theorem even_and_odd_factors' (x : ℕ) : - UniqueFactorizationMonoid.normalizedFactors x = - Multiset.replicate (evenFactorExp x) 2 + oddFactors x := - by - convert even_and_odd_factors'' x - simp [evenFactorExp, ← Multiset.filter_eq] - -theorem factors_2_even {z : ℕ} (hz : z ≠ 0) : evenFactorExp (4 * z) = 2 + evenFactorExp z := - by - have h₀ : (4 : ℕ) ≠ 0 := four_ne_zero - have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num - simp [evenFactorExp] - rw [UniqueFactorizationMonoid.normalizedFactors_mul h₀ hz, Multiset.count_add, ← h₁, - UniqueFactorizationMonoid.normalizedFactors_pow, Multiset.count_nsmul, - UniqueFactorizationMonoid.normalizedFactors_irreducible Nat.prime_two, - normalize_eq, Multiset.count_singleton_self, mul_one] - --- most useful with (hz : even (even_factor_exp z)) -/-- Odd factors or `4`. -/ -noncomputable def factorsOddPrimeOrFour (z : ℕ) : Multiset ℕ := - Multiset.replicate (evenFactorExp z / 2) 4 + oddFactors z - -theorem factorsOddPrimeOrFour.prod' {a : ℕ} (ha : 0 < a) (heven : Even (evenFactorExp a)) : - (factorsOddPrimeOrFour a).prod = a := - by - have h₁ : (2 : ℕ) ^ 2 = 4 := by norm_num - have := UniqueFactorizationMonoid.normalizedFactors_prod ha.ne' - rw [associated_eq_eq] at this - conv_rhs => rw [←this] - obtain ⟨m, hm⟩ := even_iff_two_dvd.mp heven - rw [even_and_odd_factors' _, Multiset.prod_add, factorsOddPrimeOrFour, Multiset.prod_add, hm, - Nat.mul_div_right _ zero_lt_two, Multiset.prod_replicate, Multiset.prod_replicate, pow_mul, h₁] - -theorem factorsOddPrimeOrFour.unique' {f : Multiset ℕ} (hf : ∀ x ∈ f, OddPrimeOrFour x) - (ha : 0 < f.prod) (heven : Even (evenFactorExp f.prod)) : - factorsOddPrimeOrFour f.prod = f:= - by - refine factors_unique_prod' ?_ hf (factorsOddPrimeOrFour.prod' ha heven) - intro x hx - simp only [factorsOddPrimeOrFour, Multiset.mem_add] at hx - apply Or.imp _ _ hx - · exact Multiset.eq_of_mem_replicate - · simp only [oddFactors, Multiset.mem_filter] - exact And.imp_left <| Prime.nat_prime ∘ (UniqueFactorizationMonoid.prime_of_normalized_factor _) - -theorem factorsOddPrimeOrFour.pow (z : ℕ) (n : ℕ) (hz : Even (evenFactorExp z)) : - factorsOddPrimeOrFour (z ^ n) = n • factorsOddPrimeOrFour z := by - simp only [factorsOddPrimeOrFour, nsmul_add, Multiset.nsmul_replicate, evenFactorExp.pow, - Nat.mul_div_assoc _ (even_iff_two_dvd.mp hz), oddFactors.pow] diff --git a/FltRegular/FltThree/Primes.lean b/FltRegular/FltThree/Primes.lean deleted file mode 100644 index 3362b853..00000000 --- a/FltRegular/FltThree/Primes.lean +++ /dev/null @@ -1,74 +0,0 @@ -/- -Copyright (c) 2020 Ruben Van de Velde. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. --/ -import Mathlib.RingTheory.PrincipalIdealDomain -import Mathlib.Algebra.EuclideanDomain.Int - -section - -variable {R : Type _} [CommRing R] {x y z : R} - -theorem coprime_add_self_pow {n : ℕ} (hn : 0 < n) (hsoln : x ^ n + y ^ n = z ^ n) - (hxx : IsCoprime x y) : IsCoprime x z := by - have := IsCoprime.mul_add_left_right (hxx.pow (n := n) (m := n)) 1 - rwa [mul_one, hsoln, IsCoprime.pow_iff hn hn] at this - -end - --- Edwards p49 introduction -theorem Int.factor_div (a x : ℤ) (hodd : Odd x) : - ∃ m c : ℤ, c + m * x = a ∧ 2 * c.natAbs < x.natAbs := - by - have h0' : x ≠ 0 := by - rintro rfl - contradiction - set c := a % x with hc - by_cases H : 2 * c.natAbs < x.natAbs - · exact ⟨a / x, c, Int.emod_add_ediv' a x, H⟩ - · push_neg at H - refine' ⟨(a + abs x) / x, c - abs x, _, _⟩ - · have := self_dvd_abs x - rw [Int.add_ediv_of_dvd_right this, add_mul, Int.ediv_mul_cancel this, sub_add_add_cancel, hc, - Int.emod_add_ediv'] - · rw [← Int.ofNat_lt] - replace H := Int.ofNat_le_ofNat_of_le H - have ofNat_two : ((2 : Nat) : Int) = 2 := rfl - rw [Int.ofNat_mul, ofNat_two] at H ⊢ - have hcnonneg := Int.emod_nonneg a h0' - have := Int.emod_lt a h0' - rw [Int.natAbs_of_nonneg hcnonneg] at H - rw [← Int.natAbs_neg, neg_sub, Int.natAbs_of_nonneg (sub_nonneg_of_le this.le), mul_sub, - sub_lt_iff_lt_add, two_mul, Int.abs_eq_natAbs, add_lt_add_iff_left] - apply lt_of_le_of_ne H - contrapose! hodd with heqtwomul - rw [← Int.even_iff_not_odd, ← Int.natAbs_even, ← Int.even_coe_nat, even_iff_two_dvd] - exact ⟨_, heqtwomul⟩ - -theorem two_not_cube (r : ℕ) : r ^ 3 ≠ 2 :=by - apply Monotone.ne_of_lt_of_lt_nat (Nat.pow_left_strictMono three_ne_zero).monotone 1 <;> norm_num - -nonrec theorem Int.two_not_cube (r : ℤ) : r ^ 3 ≠ 2 :=by - intro H - apply two_not_cube r.natAbs - rw [← Int.natAbs_pow, H] - norm_num - --- todo square neg_square and neg_pow_bit0 -section - -variable {R : Type _} [CommRing R] [IsDomain R] [IsPrincipalIdealRing R] [GCDMonoid R] - -theorem Irreducible.coprime_of_not_dvd_of_dvd {p k m : R} (hp : Irreducible p) (hdvd1 : ¬p ∣ m) - (hdvd2 : k ∣ m) : IsCoprime p k := - (Irreducible.coprime_iff_not_dvd hp).mpr fun hdvd1' => hdvd1 (hdvd1'.trans hdvd2) - -theorem Irreducible.dvd_of_dvd_mul_left {p k m n : R} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) - (hp : Irreducible p) (h : k ∣ p * n) : k ∣ n := - (hp.coprime_of_not_dvd_of_dvd hdvd1 hdvd2).symm.dvd_of_dvd_mul_left h - -end - -theorem Int.dvd_mul_cancel_prime' {p k m n : ℤ} (hdvd1 : ¬p ∣ m) (hdvd2 : k ∣ m) (hp : Prime p) - (h : k ∣ p * n) : k ∣ n := - Irreducible.dvd_of_dvd_mul_left hdvd1 hdvd2 hp.irreducible h diff --git a/FltRegular/FltThree/Spts.lean b/FltRegular/FltThree/Spts.lean deleted file mode 100644 index 499dc7b9..00000000 --- a/FltRegular/FltThree/Spts.lean +++ /dev/null @@ -1,408 +0,0 @@ -/- -Copyright (c) 2020 Ruben Van de Velde. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. --/ -import Mathlib.Data.Int.Order.Units -import Mathlib.NumberTheory.Zsqrtd.Basic -import Mathlib.RingTheory.Prime -import FltRegular.FltThree.Primes - -theorem Zsqrtd.exists {d : ℤ} (a : ℤ√d) (him : a.im ≠ 0) : - ∃ c : ℤ√d, a.norm = c.norm ∧ 0 ≤ c.re ∧ c.im ≠ 0 := - by - cases' le_or_lt a.re 0 with hre hre - · use -a - simp only [hre, him, Zsqrtd.norm_neg, eq_self_iff_true, Zsqrtd.neg_im, Zsqrtd.neg_re, - and_self_iff, neg_nonneg, Ne, not_false_iff, neg_eq_zero] - · use a - simp only [hre.le, him, eq_self_iff_true, and_self_iff, Ne, not_false_iff] - --- Edwards p49 step (2') -theorem factors2 {a : ℤ√(-3)} (heven : Even a.norm) : ∃ b : ℤ√(-3), a.norm = 4 * b.norm := - by - have hparity : Even a.re ↔ Even a.im := by - have : ¬ Even (3 : ℤ) := by decide - simpa [this, two_ne_zero, Zsqrtd.norm_def, parity_simps] using heven - simp only [iff_iff_and_or_not_and_not, ← Int.odd_iff_not_even] at hparity - obtain ⟨⟨c, hc⟩, ⟨d, hd⟩⟩ | ⟨hre, him⟩ := hparity - · use ⟨c, d⟩ - simp only [Zsqrtd.norm_def, hc, hd] - ring - · cases' Int.four_dvd_add_or_sub_of_odd hre him with h4 h4 - · obtain ⟨v, hv⟩ := h4 - use ⟨v - a.im, v⟩ - rw [eq_comm, ← sub_eq_iff_eq_add] at hv - simp only [Zsqrtd.norm_def, ← hv] - ring - · obtain ⟨v, hv⟩ := h4 - use ⟨v + a.im, v⟩ - rw [sub_eq_iff_eq_add] at hv - simp only [Zsqrtd.norm_def, hv] - ring - -theorem Spts.mul_of_dvd' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime : Prime p.norm) : - ∃ u : ℤ√(-3), a = p * u ∨ a = star p * u := - by - obtain ⟨f, hf⟩ := hdvd - have h0 : p.norm ∣ p.re * a.im - a.re * p.im ∨ p.norm ∣ p.re * a.im + a.re * p.im := - by - apply hpprime.dvd_or_dvd - convert dvd_mul_right p.norm (a.im ^ 2 - p.im ^ 2 * f) using 1 - trans a.im ^ 2 * p.norm - p.im ^ 2 * (p.norm * f) - · rw [← hf, Zsqrtd.norm_def, Zsqrtd.norm_def] - ring - · rw [Zsqrtd.norm_def] - ring - obtain ⟨A, HA⟩ : ∃ A : Units ℤ, p.norm ∣ p.re * a.im + A * a.re * p.im := - by - cases' h0 with h0 h0 <;> [(use -1); (use 1)] <;> convert h0 using 1 <;> - simp only [Units.val_neg, Units.val_one, neg_mul, one_mul] - ring - have HAsq : (A : ℤ) ^ 2 = 1 := by - calc - (A : ℤ) ^ 2 = ((A ^ 2 : Units ℤ) : ℤ) := (Units.val_pow_eq_pow_val _ _).symm - _ = ((1 : Units ℤ) : ℤ) := (congr_arg _ (Int.units_sq A)) - _ = 1 := Units.val_one - - · set X : ℤ√(-3) := ⟨p.re * a.re - A * 3 * p.im * a.im, p.re * a.im + A * a.re * p.im⟩ with HX - obtain ⟨U, HU⟩ : (p.norm : ℤ√(-3)) ∣ X := - by - rw [Zsqrtd.intCast_dvd] - refine' ⟨_, HA⟩ - apply @Prime.dvd_of_dvd_pow _ _ _ hpprime _ 2 - have : X.re ^ 2 = X.norm - 3 * X.im ^ 2 := - by - rw [Zsqrtd.norm_def] - ring - rw [this] - apply dvd_sub - · use a.norm - trans - (p.re * a.re) ^ 2 + (A : ℤ) ^ 2 * (3 * p.im * a.im) ^ 2 + - 3 * ((p.re * a.im) ^ 2 + (A : ℤ) ^ 2 * (a.re * p.im) ^ 2) - · simp only [Zsqrtd.norm_def] - ring - · simp only [Zsqrtd.norm_def, HAsq] - ring - · apply dvd_mul_of_dvd_right - exact dvd_pow HA two_ne_zero - use U - suffices a = ⟨p.re, -A * p.im⟩ * U by - apply Or.imp _ _ (Int.units_eq_one_or A).symm <;> rintro rfl <;> simpa [Zsqrtd.ext] using this - apply Zsqrtd.eq_of_smul_eq_smul_left hpprime.ne_zero - have : p.norm = p.re ^ 2 + 3 * (A : ℤ) ^ 2 * p.im ^ 2 := - by - rw [Zsqrtd.norm_def, HAsq] - ring - rw [mul_comm _ U, ← mul_assoc, ← HU, HX] - simp only [Zsqrtd.ext_iff, neg_mul, add_zero, Zsqrtd.intCast_re, MulZeroClass.zero_mul, mul_neg, - Zsqrtd.mul_im, Zsqrtd.mul_re, neg_neg, MulZeroClass.mul_zero, neg_zero, Zsqrtd.intCast_im, - this] - constructor <;> ring - --- Edwards p49 step (3') -theorem Spts.mul_of_dvd'' {a p : ℤ√(-3)} (hdvd : p.norm ∣ a.norm) (hpprime : Prime p.norm) : - ∃ u : ℤ√(-3), (a = p * u ∨ a = star p * u) ∧ a.norm = p.norm * u.norm := - by - obtain ⟨u, hu⟩ := Spts.mul_of_dvd' hdvd hpprime - refine' ⟨u, hu, _⟩ - obtain rfl | rfl := hu - · rw [Zsqrtd.norm_mul] - · rw [Zsqrtd.norm_mul, Zsqrtd.norm_conj] - --- Edwards p49 step (4'), contraposed -theorem factors' (a : ℤ√(-3)) (f : ℤ) (g : ℤ) (hodd : Odd f) (hgpos : g ≠ 0) - (hfactor : f * g = a.norm) - (hnotform : ∀ f' : ℤ, f' ∣ g → Odd f' → ∃ p : ℤ√(-3), abs f' = p.norm) : - ∃ p : ℤ√(-3), abs f = p.norm := - by - induction' hg : g.natAbs using Nat.strong_induction_on with g'' IH generalizing a g - subst g'' - dsimp at IH - by_cases H : Even (Zsqrtd.norm a) - · obtain ⟨c, hc⟩ := factors2 H - have : 4 ∣ g := by - apply IsCoprime.dvd_of_dvd_mul_left - · show IsCoprime _ f - rw [Int.odd_iff_not_even, even_iff_two_dvd, ← Int.prime_two.coprime_iff_not_dvd] at hodd - convert hodd.pow_left - rw [sq] - norm_num - · rw [hfactor, hc] - exact dvd_mul_right _ _ - obtain ⟨g', rfl⟩ := this - have hg'pos : g' ≠ 0 := right_ne_zero_of_mul hgpos - refine' IH g'.natAbs _ c g' hg'pos _ _ rfl - · rw [Int.natAbs_mul] - apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hg'pos) - norm_num - · rw [← mul_right_inj' (four_ne_zero' ℤ), ← hc, ← hfactor, mul_left_comm] - · intro f' hf'dvd hf'odd - refine' hnotform f' _ hf'odd - exact hf'dvd.mul_left _ - · by_cases h : |g| = 1 - · apply_fun abs at hfactor - rw [abs_mul, h, mul_one, abs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) a)] at hfactor - exact ⟨_, hfactor⟩ - · rw [Int.abs_eq_natAbs, ← Int.ofNat_one, Int.natCast_inj] at h - obtain ⟨p, pprime, pdvd⟩ := Int.exists_prime_and_dvd h - have : p ∣ a.norm := by - rw [← hfactor] - exact pdvd.mul_left _ - have podd : Odd p := - Int.odd_iff_not_even.mpr - (by - intro X - apply H - apply even_iff_two_dvd.mpr - apply dvd_trans _ this - apply even_iff_two_dvd.mp X) - obtain ⟨A, HA⟩ := hnotform p pdvd podd - have pprime' := pprime.abs - rw [HA] at pprime' - have pdvd' : A.norm ∣ a.norm := by - rw [← hfactor, ← HA, abs_dvd] - exact dvd_mul_of_dvd_right pdvd _ - obtain ⟨c, -, hcd⟩ := Spts.mul_of_dvd'' pdvd' pprime' - obtain ⟨q, rfl⟩ := pdvd - have hqpos : q ≠ 0 := right_ne_zero_of_mul hgpos - have : (p.sign * q).natAbs = q.natAbs := by - rw [Int.natAbs_mul, Int.natAbs_sign_of_nonzero pprime.ne_zero, one_mul] - refine' IH q.natAbs _ c (p.sign * q) _ _ _ this - · rw [Int.natAbs_mul] - apply lt_mul_of_one_lt_left (Int.natAbs_pos.mpr hqpos) - rw [Int.prime_iff_natAbs_prime] at pprime - exact pprime.one_lt - · rwa [← Int.natAbs_eq_zero, this, Int.natAbs_eq_zero] - · - rw [← mul_right_inj' pprime'.ne_zero, ← hcd, mul_left_comm, ← hfactor, ← HA, ← - mul_assoc (|p|), mul_comm (|p|), Int.sign_mul_abs] - · intro f' hf'dvd hf'odd - refine' hnotform f' _ hf'odd - rw [← Int.dvd_natAbs, this, Int.dvd_natAbs] at hf'dvd - exact hf'dvd.mul_left _ - -theorem Zqrtd.factor_div (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) : - ∃ c m : ℤ√(-3), a = c + m * x ∧ c.norm < x ^ 2 := - by - obtain ⟨m, c, ha, hc⟩ := Int.factor_div a.re x hodd - obtain ⟨n, d, hb, hd⟩ := Int.factor_div a.im x hodd - set c' : ℤ√(-3) := ⟨c, d⟩ - refine' ⟨c', ⟨m, n⟩, _, _⟩ - · - simp only [Zsqrtd.ext_iff, ha, hb, add_zero, Zsqrtd.intCast_re, eq_self_iff_true, Zsqrtd.mul_im, - zero_add, Zsqrtd.add_im, and_self_iff, Zsqrtd.mul_re, MulZeroClass.mul_zero, Zsqrtd.add_re, - Zsqrtd.intCast_im] - · rw [← mul_lt_mul_left (by norm_num : (0 : ℤ) < 4)] - calc - 4 * c'.norm = (2 * c) ^ 2 + 3 * (2 * d) ^ 2 := - by - rw [Zsqrtd.norm_def] - ring - _ < x ^ 2 + 3 * x ^ 2 := (add_lt_add ?_ ?_) - _ = 4 * x ^ 2 := by ring - - · rw [mul_pow, ← Int.natAbs_pow_two c, ← Int.natAbs_pow_two x, ← mul_pow] - norm_cast - exact Nat.pow_lt_pow_left hc two_ne_zero - · rw [mul_pow, ← Int.natAbs_pow_two d, ← Int.natAbs_pow_two x, ← mul_pow, - mul_lt_mul_left (by norm_num : (0 : ℤ) < 3)] - norm_cast - exact Nat.pow_lt_pow_left hd two_ne_zero - -theorem Zqrtd.factor_div' (a : ℤ√(-3)) {x : ℤ} (hodd : Odd x) (h : 1 < |x|) - (hcoprime : IsCoprime a.re a.im) (hfactor : x ∣ a.norm) : - ∃ c m : ℤ√(-3), - a = c + m * x ∧ c.norm < x ^ 2 ∧ c ≠ 0 ∧ ∃ y, c.norm = x * y ∧ y.natAbs < x.natAbs := - by - obtain ⟨c, m, rfl, h2⟩ := Zqrtd.factor_div a hodd - refine' ⟨c, m, rfl, h2, _, _⟩ - · rintro rfl - apply h.ne' - rw [← Int.isUnit_iff_abs_eq] - apply hcoprime.isUnit_of_dvd' <;> - simp only [zero_add, mul_comm m, Zsqrtd.smul_re, Zsqrtd.smul_im, dvd_mul_right] - · obtain ⟨y, hy⟩ : x ∣ c.norm := - by - set e : ℤ := m.re ^ 2 * x + 2 * m.re * c.re + 3 * m.im ^ 2 * x + 6 * m.im * c.im with he - convert dvd_sub hfactor (dvd_mul_right x e) - rw [he, Zsqrtd.norm_def, Zsqrtd.norm_def] - simp only [Zsqrtd.intCast_re, Zsqrtd.mul_im, Zsqrtd.add_im, Zsqrtd.mul_re, Zsqrtd.add_re, - Zsqrtd.intCast_im] - ring - refine' ⟨y, hy, _⟩ - have h0'' : 0 < x.natAbs := by - zify - exact zero_lt_one.trans h - rw [← mul_lt_mul_left h0'', ← pow_two, ← Int.natAbs_mul, ← hy] - zify - rwa [← Int.natCast_natAbs x, Int.natAbs_pow_two x, ← Int.natCast_natAbs, - Int.natAbs_of_nonneg (Zsqrtd.norm_nonneg (by norm_num) c)] - --- Edwards p50 step (5') -theorem factors (a : ℤ√(-3)) (x : ℤ) (hcoprime : IsCoprime a.re a.im) (hodd : Odd x) - (hfactor : x ∣ a.norm) : ∃ c : ℤ√(-3), abs x = c.norm := - by - induction' hx' : x.natAbs using Nat.strong_induction_on with x' IH generalizing a x - subst hx' - have hneg1 : 1 ≤ a.norm := by - rw [← Int.sub_one_lt_iff, sub_self] - apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a) - rw [Ne, eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num : (-3 : ℤ) < 0)] - rintro rfl - rw [Zsqrtd.zero_im, Zsqrtd.zero_re] at hcoprime - exact not_isCoprime_zero_zero hcoprime - have h0 : x ≠ 0 := by - rintro rfl - simp only [even_zero, not_true, Int.odd_iff_not_even] at hodd - have h0' : 1 ≤ abs x := by rwa [← Int.sub_one_lt_iff, sub_self, abs_pos] - cases' h0'.eq_or_lt with h h - · rw [← h] - refine' ⟨⟨1, 0⟩, _⟩ - norm_num [Zsqrtd.norm_def] - obtain ⟨c', m, rfl, -, h1, ⟨y, hy, h3⟩⟩ := Zqrtd.factor_div' a hodd h hcoprime hfactor - have h4 : c'.norm ≠ 0 := by rwa [Ne, Zsqrtd.norm_eq_zero_iff (by norm_num) c'] - set g := Int.gcd c'.re c'.im with hg - have hgpos : 0 < g := by rwa [hg, Zsqrtd.gcd_pos_iff] - obtain ⟨C', HC', HCDcoprime⟩ := Zsqrtd.exists_coprime_of_gcd_pos hgpos - have h5 : x * y = (g : ℤ) ^ 2 * C'.norm := by - rw [← hy, HC', Zsqrtd.norm_mul, Zsqrtd.norm_intCast, ← pow_two] - obtain ⟨z, hz⟩ : (g : ℤ) ^ 2 ∣ y := - by - have : (g : ℤ) ^ 2 ∣ x * y := by - rw [h5] - exact dvd_mul_right _ _ - apply IsCoprime.dvd_of_dvd_mul_left _ this - apply isCoprime_of_prime_dvd - · contrapose! h0 - exact h0.2 - intro p hpprime hpdvdleft hpdvdright - have : ↑p ∣ c' + m * x := by - rw [HC'] - exact - dvd_add - (dvd_mul_of_dvd_left - ((Zsqrtd.intCast_dvd_intCast _ _).mpr (hpprime.dvd_of_dvd_pow hpdvdleft)) _) - (dvd_mul_of_dvd_right ((Zsqrtd.intCast_dvd_intCast _ _).mpr hpdvdright) _) - have := Zsqrtd.coprime_of_dvd_coprime hcoprime this - simp only [Zsqrtd.intCast_re, isCoprime_zero_right, Zsqrtd.intCast_im, hpprime.not_unit] at this - have h6 : x * z = C'.norm := by - apply Int.eq_of_mul_eq_mul_left (pow_ne_zero 2 <| Int.natCast_ne_zero_iff_pos.mpr hgpos) - rw [← h5, hz, mul_left_comm] - have h8 : z ≠ 0 := by - apply right_ne_zero_of_mul - apply right_ne_zero_of_mul - rwa [h6, ← h5, ← hy] - refine' factors' _ x z hodd h8 h6 _ - intro w hwdvd hwodd - refine' IH w.natAbs _ C' w HCDcoprime hwodd _ rfl - · - calc - w.natAbs ≤ z.natAbs := - Nat.le_of_dvd (Int.natAbs_pos.mpr h8) (Int.natAbs_dvd_natAbs.mpr hwdvd) - _ ≤ y.natAbs := by - rw [hz, Int.natAbs_mul] - exact Nat.le_mul_of_pos_left _ (pow_pos hgpos 2) - _ < x.natAbs := h3 - - · rw [← h6] - exact dvd_mul_of_dvd_right hwdvd x - -theorem Spts.eq_one {a : ℤ√(-3)} (h : a.norm = 1) : abs a.re = 1 ∧ a.im = 0 := by - suffices H : abs a.re = 1 by - refine' ⟨H, _⟩ - rw [Zsqrtd.norm_def, mul_assoc, ← Int.natAbs_mul_self' a.re, ← Int.abs_eq_natAbs, H, one_mul, - neg_mul, sub_neg_eq_add, add_right_eq_self, mul_eq_zero, mul_self_eq_zero] at h - exact h.resolve_left three_ne_zero - contrapose! h - cases' lt_or_gt_of_ne h with H H - · have : a.re = 0 := by rwa [← Int.abs_lt_one_iff] - simp only [Zsqrtd.norm_def, this, MulZeroClass.zero_mul, zero_sub, neg_mul, neg_neg] - by_cases hb : a.im = 0 - · simp [hb] - · have : 1 ≤ abs a.im := by rwa [← Int.abs_lt_one_iff, not_lt] at hb - have : 1 ≤ a.im ^ 2 := by - rw [← sq_abs] - exact pow_le_pow_left zero_le_one this 2 - linarith - · apply ne_of_gt - rw [Zsqrtd.norm_def, neg_mul, neg_mul, sub_neg_eq_add] - apply lt_add_of_lt_of_nonneg - · rw [← sq, ← sq_abs] - exact pow_lt_pow_left H zero_le_one two_ne_zero - · rw [mul_assoc] - exact mul_nonneg zero_lt_three.le (mul_self_nonneg _) - -theorem Spts.eq_one' {a : ℤ√(-3)} (h : a.norm = 1) : a = 1 ∨ a = -1 := by - simp only [Zsqrtd.ext_iff, Zsqrtd.one_re, Zsqrtd.one_im, Zsqrtd.neg_im, Zsqrtd.neg_re, neg_zero, - ← or_and_right, ← abs_eq (zero_le_one' ℤ), Spts.eq_one h, eq_self_iff_true, and_self_iff] - -theorem Spts.ne_zero_of_coprime' (a : ℤ√(-3)) (hcoprime : IsCoprime a.re a.im) : a.norm ≠ 0 := - by - contrapose! hcoprime with H - obtain ⟨rfl, rfl⟩ := (Zsqrtd.norm_eq_zero_iff (by norm_num) _).mp H - exact not_isCoprime_zero_zero - -theorem Spts.pos_of_coprime' {a : ℤ√(-3)} (hcoprime : IsCoprime a.re a.im) : 0 < a.norm := - by - apply lt_of_le_of_ne - · apply Zsqrtd.norm_nonneg - norm_num - · apply Ne.symm -- Porting note: `symm` fails - exact Spts.ne_zero_of_coprime' _ hcoprime - -theorem Spts.one_lt_of_im_ne_zero (a : ℤ√(-3)) (hb : a.im ≠ 0) : 1 < a.norm := - by - apply lt_of_le_of_ne - · rw [← Int.sub_one_lt_iff, sub_self] - apply lt_of_le_of_ne (Zsqrtd.norm_nonneg (by norm_num) a) - contrapose! hb - rw [eq_comm, Zsqrtd.norm_eq_zero_iff (by norm_num) a] at hb - rw [hb, Zsqrtd.zero_im] - · intro H - exact hb (Spts.eq_one H.symm).2 - -theorem Spts.not_two (a : ℤ√(-3)) : a.norm ≠ 2 := - by - rw [Zsqrtd.norm_def] - obtain him | him := eq_or_ne a.im 0 - · rw [him, MulZeroClass.mul_zero, sub_zero, ← Int.natAbs_mul_self, ← sq] - norm_cast - apply (Nat.pow_left_strictMono two_ne_zero).monotone.ne_of_lt_of_lt_nat 1 <;> norm_num - · apply ne_of_gt - apply lt_add_of_nonneg_of_lt (mul_self_nonneg a.re) - rw [← Int.add_one_le_iff] - rw [mul_assoc, neg_mul_eq_neg_mul, neg_neg] - refine' le_mul_of_one_le_right zero_lt_three.le _ - rwa [← Int.sub_one_lt_iff, sub_self, mul_self_pos] - -theorem Spts.four {p : ℤ√(-3)} (hfour : p.norm = 4) (hq : p.im ≠ 0) : abs p.re = 1 ∧ abs p.im = 1 := - by - suffices p.re ^ 2 = 1 ∧ p.im ^ 2 = 1 by - apply And.imp _ _ this <;> - · intro h - rwa [← sq_eq_sq (abs_nonneg (_ : ℤ)) zero_le_one, one_pow, sq_abs] - have hq : p.im ^ 2 = 1 := by - apply le_antisymm - · contrapose! hfour with hq' - apply ne_of_gt - rw [← Int.add_one_le_iff] at hq' - calc - 4 < 3 * 2 := by norm_num - _ ≤ 3 * p.im ^ 2 := (Int.mul_le_mul_of_nonneg_left hq' (by norm_num)) - _ ≤ p.re ^ 2 + 3 * p.im ^ 2 := (le_add_of_nonneg_left (pow_two_nonneg p.re)) - _ = p.norm := by - rw [Zsqrtd.norm_def] - ring - - · rw [← Int.sub_one_lt_iff, sub_self] - exact sq_pos_of_ne_zero hq - refine' ⟨_, hq⟩ - calc - p.re ^ 2 = p.re ^ 2 + 3 * p.im ^ 2 - 3 := by simp [hq] - _ = p.norm - 3 := by - rw [Zsqrtd.norm_def] - ring - _ = 1 := by - rw [hfour] - norm_num diff --git a/FltRegular/MayAssume/Lemmas.lean b/FltRegular/MayAssume/Lemmas.lean index de00d072..1bf82709 100644 --- a/FltRegular/MayAssume/Lemmas.lean +++ b/FltRegular/MayAssume/Lemmas.lean @@ -1,4 +1,4 @@ -import FltRegular.FltThree.FltThree +import Mathlib.NumberTheory.FLT.Three import Mathlib.Algebra.GCDMonoid.Finset import Mathlib.FieldTheory.Finite.Basic @@ -14,7 +14,7 @@ theorem p_ne_three {a b c : ℤ} {n : ℕ} (hprod : a * b * c ≠ 0) (h : a ^ n have ha : a ≠ 0 := fun ha => by simp [ha] at hprod have hb : b ≠ 0 := fun hb => by simp [hb] at hprod have hc : c ≠ 0 := fun hc => by simp [hc] at hprod - simp [hn, flt_three a b c ha hb hc] at h + exact fermatLastTheoremFor_iff_int.1 fermatLastTheoremThree a b c ha hb hc (hn ▸ h) theorem coprime {a b c : ℤ} {n : ℕ} (H : a ^ n + b ^ n = c ^ n) (hprod : a * b * c ≠ 0) : let d := ({a, b, c} : Finset ℤ).gcd id diff --git a/FltRegular/NumberTheory/Hilbert92.lean b/FltRegular/NumberTheory/Hilbert92.lean index 854e735e..df3153f5 100644 --- a/FltRegular/NumberTheory/Hilbert92.lean +++ b/FltRegular/NumberTheory/Hilbert92.lean @@ -130,13 +130,14 @@ lemma Subgroup.index_mono {G : Type*} [Group G] {H₁ H₂ : Subgroup G} (h : H [h₁ : Fintype (G ⧸ H₁)] : H₂.index < H₁.index := by rcases eq_or_ne H₂.index 0 with hn | hn - · rw [hn, index_eq_card] + · rw [hn, index_eq_card, Nat.card_eq_fintype_card] exact Fintype.card_pos apply lt_of_le_of_ne - · refine Nat.le_of_dvd (by rw [index_eq_card]; apply Fintype.card_pos) <| Subgroup.index_dvd_of_le h.le - · have := fintypeOfIndexNeZero hn - rw [←mul_one H₂.index, ←relindex_mul_index h.le, mul_comm, Ne, eq_comm] - simp [-one_mul, -Nat.one_mul, hn, h.not_le] + refine Nat.le_of_dvd (by rw [index_eq_card, Nat.card_eq_fintype_card]; apply Fintype.card_pos) + <| Subgroup.index_dvd_of_le h.le + have := fintypeOfIndexNeZero hn + rw [←mul_one H₂.index, ←relindex_mul_index h.le, mul_comm, Ne, eq_comm] + simp [-one_mul, -Nat.one_mul, hn, h.not_le] namespace systemOfUnits.IsFundamental diff --git a/lake-manifest.json b/lake-manifest.json index d59cf216..f723517e 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", + "rev": "937cd3219c0beffa7b623d2905707d1304da259e", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,7 +65,7 @@ "type": "git", "subDir": null, "scope": "", - "rev": "08bbfd6e4f66aaf6d3ef8e23fb18903707d1f14b", + "rev": "90ef20a210ecd605e8036b280b6b85b9043b5447", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": null,