Primes in progressions, Euclid's way: every challenge is settled

Claim 118

Status

verified

Claimed

24

Measured

24

Label

no improvement

Signed commit

63189c7c0f31aa19dde11bdf6c2417b72357283e

Verification runs

Candidate

{"proofs":{"Lemma.primes_mod_10_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n    ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n  have hk0 : k ≠ 0 := by omega\n  let b := k * n.factorial\n  have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n    rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n    have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n    calc\n      1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n      _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n        sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n  let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n  haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n  have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n    rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n    exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n  have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n    have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n    rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n    exact h0\n  have hpb : ¬p ∣ b := by\n    intro hd\n    have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n    have := hroot\n    rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n    exact one_ne_zero this\n  refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩\n  · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)\n  · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=\n      ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)\n    haveI : NeZero (k : ZMod p) :=\n      NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)\n    have : k = orderOf (b : ZMod p) := by\n      have := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf\n      simpa using this\n    rw [← this] at hdiv\n    have h2 := hprime.1.two_le\n    have : (p - 1) % k = 0 := Nat.mod_eq_zero_of_dvd hdiv\n    have hpk : p % k = ((p - 1) % k + 1 % k) % k := by\n      rw [← Nat.add_mod]; congr 1; omega\n    rw [hpk, this, Nat.mod_eq_of_lt hk1]\n    simp [Nat.mod_eq_of_lt hk1]\n\ntheorem infinite (k : ℕ) (hk : 1 < k) : Set.Infinite {p : ℕ | p.Prime ∧ p % k = 1} := by\n  apply Set.infinite_of_forall_exists_gt\n  intro n\n  obtain ⟨p, hp, hnp, hpk⟩ := exists_prime_gt_modEq_one' k n hk\n  exact ⟨p, ⟨hp, hpk⟩, hnp⟩\n\nend Lemma.Cyc\n\ntheorem Lemma.primes_mod_10_eq_1 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 1} :=\n  Lemma.Cyc.infinite 10 (by norm_num)\n","Lemma.primes_mod_10_eq_9":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.P54\n\ntheorem z5 : (5 : ZMod 5) = 0 := by decide\n\ntheorem nsq2 : ∀ r : ZMod 5, ((2 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem nsq3 : ∀ r : ZMod 5, ((3 : ℕ) : ZMod 5) ≠ r * r := by decide\n\ntheorem key (y : ℕ) (hy : 2 ∣ y) (hy0 : 0 < y) (q : ℕ) (hq : q.Prime)\n    (hd : q ∣ 5 * y ^ 2 - 1) : (q % 5 = 1 ∨ q % 5 = 4) ∧ ¬ q ∣ y := by\n  haveI := Fact.mk hq\n  haveI : Fact (Nat.Prime 5) := Fact.mk Nat.prime_five\n  have h1 : ((5 * y ^ 2 - 1 : ℕ) : ZMod q) = 0 :=\n    (CharP.cast_eq_zero_iff (ZMod q) q _).2 hd\n  have h5 : 1 ≤ 5 * y ^ 2 := by\n    have : 1 ≤ y ^ 2 := Nat.one_le_pow _ _ hy0\n    omega\n  have h2 : (5 : ZMod q) * (y : ZMod q) ^ 2 = 1 := by\n    rw [Nat.cast_sub h5] at h1\n    push_cast at h1\n    linear_combination h1\n  have hndvd : ¬ q ∣ y := by\n    intro hqy\n    have : (y : ZMod q) = 0 := (CharP.cast_eq_zero_iff (ZMod q) q _).2 hqy\n    rw [this] at h2\n    simp at h2\n  refine ⟨?_, hndvd⟩\n  have hq2 : q ≠ 2 := by\n    rintro rfl\n    exact hndvd hy\n  have hq5 : q ≠ 5 := by\n    rintro rfl\n    have : (5 : ZMod 5) = 0 := z5\n    rw [this] at h2\n    simp at h2\n  have hsq : IsSquare ((5 : ℕ) : ZMod q) := ⟨5 * y, by push_cast; linear_combination (-5) * h2⟩\n  obtain ⟨r, hr⟩ :=\n    (ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one (p := 5) (q := q) (by norm_num) hq2).2 hsq\n  rw [← ZMod.natCast_mod q 5] at hr\n  have hlt := Nat.mod_lt q (by norm_num : 5 > 0)\n  generalize hm : q % 5 = m at hr hlt\n  obtain h | h | h | h | h : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega\n  · subst h\n    exact absurd ((Nat.prime_dvd_prime_iff_eq Nat.prime_five hq).1\n      (Nat.dvd_of_mod_eq_zero hm)).symm hq5\n  · exact Or.inl h\n  · subst h\n    exact absurd hr (nsq2 r)\n  · subst h\n    exact absurd hr (nsq3 r)\n  · exact Or.inr h\n\ntheorem exists4 (N : ℕ) (hN : N % 5 = 4)\n    (hf : ∀ q, q.Prime → q ∣ N → q % 5 = 1 ∨ q % 5 = 4) :\n    ∃ q, q.Prime ∧ q ∣ N ∧ q % 5 = 4 := by\n  induction N using Nat.strong_induction_on with\n  | _ N ih =>\n    have hN1 : N ≠ 1 := by omega\n    have hq := Nat.minFac_prime hN1\n    have hqd := Nat.minFac_dvd N\n    rcases hf _ hq hqd with h | h\n    · obtain ⟨k, hk⟩ := hqd\n      have hk5 : k % 5 = 4 := by\n        rw [hk, Nat.mul_mod, h] at hN\n        omega\n      have hklt : k < N := by\n        have := hq.two_le\n        have hk0 : 0 < k := by omega\n        rw [hk]\n        nlinarith\n      have hdiv : k ∣ N := Dvd.intro_left _ hk.symm\n      obtain ⟨p, hp, hpd, hp4⟩ :=\n        ih k hklt hk5 (fun p hp hpd => hf p hp (hpd.trans hdiv))\n      exact ⟨p, hp, hpd.trans hdiv, hp4⟩\n    · exact ⟨_, hq, hqd, h⟩\n\nend Lemma.P54\n\ntheorem Lemma.aux54 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 5 = 4} := by\n  apply Set.infinite_of_forall_exists_gt\n  intro n\n  have hy2 : 2 ∣ (n + 5).factorial := Nat.dvd_factorial (by norm_num) (by omega)\n  have hy0 : 0 < (n + 5).factorial := Nat.factorial_pos _\n  have hN : (5 * (n + 5).factorial ^ 2 - 1) % 5 = 4 := by\n    have : 1 ≤ (n + 5).factorial ^ 2 := Nat.one_le_pow _ _ hy0\n    omega\n  obtain ⟨q, hq, hqd, hq4⟩ := Lemma.P54.exists4 _ hN\n    (fun q hq hd => (Lemma.P54.key _ hy2 hy0 q hq hd).1)\n  refine ⟨q, ⟨hq, hq4⟩, ?_⟩\n  by_contra hle\n  push_neg at hle\n  exact (Lemma.P54.key _ hy2 hy0 q hq hqd).2 (Nat.dvd_factorial hq.pos (by omega))\n\ntheorem Lemma.primes_mod_10_eq_9 :\n    Set.Infinite {p : ℕ | p.Prime ∧ p % 10 = 9} := by\n  refine Lemma.aux54.mono ?_\n  rintro p ⟨hp, h4⟩\n  refine ⟨hp, ?_⟩\n  rcases hp.eq_two_or_odd with h2 | h2\n  · subst h2; simp at h4\n  · omega\n","Lemma.primes_mod_11_eq_1":"import Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity\n\nnamespace Lemma.Cyc\n\nopen Polynomial Nat\n\ntheorem exists_prime_gt_modEq_one' (k n : ℕ) (hk1 : 1 < k) :\n    ∃ p : ℕ, p.Prime ∧ n < p ∧ p % k = 1 := by\n  have hk0 : k ≠ 0 := by omega\n  let b := k * n.factorial\n  have hgt : 1 < (eval (b : ℤ) (cyclotomic k ℤ)).natAbs := by\n    rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩\n    have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos\n    calc\n      1 ≤ b - 1 := Nat.le_sub_one_of_lt hb\n      _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=\n        sub_one_lt_natAbs_cyclotomic_eval hk1 (Nat.succ_le_iff.1 hb).ne'\n  let p := minFac (eval (b : ℤ) (cyclotomic k ℤ)).natAbs\n  haveI hprime : Fact p.Prime := ⟨minFac_prime (Nat.ne_of_lt hgt).symm⟩\n  have h0 : ((eval (b : ℤ) (cyclotomic k ℤ) : ℤ) : ZMod p) = 0 := by\n    rw [ZMod.intCast_zmod_eq_zero_iff_dvd]\n    exact Int.ofNat_dvd_left.2 (minFac_dvd _)\n  have hroot : IsRoot (cyclotomic k (ZMod p)) (b : ZMod p) := by\n    have : ((b : ℤ) : ZMod p) = (b : ZMod p) := by push_cast; rfl\n    rw [IsRoot.def, ← this, ← map_cyclotomic_int k (ZMod p), eval_intCast_map]\n    exact h0\n  have hpb : ¬p ∣ b := by\n    intro hd\n    have hb0 : (b : ZMod p) = 0 := (CharP.cast_eq_zero_iff (ZMod p) p b).2 hd\n    have := hroot\n    rw [IsRoot.def, hb0, ← coeff_zero_eq_eval_zero, cyclotomic_coeff_zero _ hk1] at this\n    exa
… (truncated; the full value is in this page's JSON)