lean-talk-sp24/LeanTalkSP24/infinitely_many_primes.lean

240 lines
6.9 KiB
Text
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

import Mathlib.Data.Nat.Prime
import Mathlib.Algebra.BigOperators.Order
import Mathlib.Tactic
import Mathlib.Tactic.IntervalCases
open BigOperators
theorem two_le {m : } (h0 : m ≠ 0) (h1 : m ≠ 1) : 2 ≤ m := by
have : m > 0 := Nat.pos_of_ne_zero h0
have : m >= 1 := this
have h1 : 1 ≠ m := Ne.symm h1
change ¬_ = _ at h1
have : m > 1 := Nat.lt_of_le_of_ne this h1
exact this
theorem exists_prime_factor {n : Nat} (h : 2 ≤ n) : ∃ p : Nat, p.Prime ∧ p n := by
by_cases np : n.Prime
· use n, np
induction' n using Nat.strong_induction_on with n ih
rw [Nat.prime_def_lt] at np
push_neg at np
rcases np h with ⟨m, mltn, mdvdn, mne1⟩
have : m ≠ 0 := by
intro mz
rw [mz, zero_dvd_iff] at mdvdn
-- linarith
rw [mz, mdvdn] at mltn
contradiction
have mgt2 : 2 ≤ m := two_le this mne1
by_cases mp : m.Prime
· use m, mp
. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
use p, pp
exact Nat.dvd_trans pdvd mdvdn
theorem primes_infinite : ∀ n, ∃ p > n, Nat.Prime p := by
intro n
have : 2 ≤ Nat.factorial (n + 1) + 1 := by
apply Nat.succ_le_succ
apply Nat.succ_le_of_lt
apply Nat.factorial_pos
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
refine' ⟨p, _, pp⟩
show p > n
by_contra ple
push_neg at ple
have : p Nat.factorial (n + 1) := by
apply Nat.dvd_factorial
apply pp.pos
linarith
have : p 1 := by
convert Nat.dvd_sub' pdvd this
simp
show False
have ple1 : p ≤ 1 := Nat.le_of_dvd (Nat.lt_succ_self 0) this
have plt1 : p > 1 := pp.one_lt
linarith
open Finset
section
variable {α : Type _} [DecidableEq α] (r s t : Finset α)
example : r ∩ (s t) ⊆ r ∩ s r ∩ t := by
rw [subset_iff]
intro x
rw [mem_inter, mem_union, mem_union, mem_inter, mem_inter]
tauto
example : r ∩ (s t) ⊆ r ∩ s r ∩ t := by
simp [subset_iff]
intro x
tauto
example : r ∩ s r ∩ t ⊆ r ∩ (s t) := by
simp [subset_iff]
intro x
tauto
example : r ∩ s r ∩ t = r ∩ (s t) := by
ext x
simp
tauto
end
theorem _root_.Nat.Prime.eq_of_dvd_of_prime {p q : }
(prime_p : Nat.Prime p) (prime_q : Nat.Prime q) (h : p q) :
p = q := by
cases prime_q.eq_one_or_self_of_dvd _ h
· linarith [prime_p.two_le]
assumption
theorem mem_of_dvd_prod_primes {s : Finset } {p : } (prime_p : p.Prime) :
(∀ n ∈ s, Nat.Prime n) → (p ∏ n in s, n) → p ∈ s := by
intro h₀ h₁
induction' s using Finset.induction_on with a s ans ih
· simp at h₁
linarith [prime_p.two_le]
simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
rw [mem_insert]
cases' h₁ with h₁ h₁
· left
exact prime_p.eq_of_dvd_of_prime h₀.1 h₁
right
exact ih h₀.2 h₁
theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by
intro s
by_contra h
push_neg at h
set s' := s.filter Nat.Prime with s'_def
have mem_s' : ∀ {n : }, n ∈ s' ↔ n.Prime := by
intro n
simp [s'_def]
apply h
have : 2 ≤ (∏ i in s', i) + 1 := by
apply Nat.succ_le_succ
apply Nat.succ_le_of_lt
apply Finset.prod_pos
intro n ns'
apply (mem_s'.mp ns').pos
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
have : p ∏ i in s', i := by
apply dvd_prod_of_mem
rw [mem_s']
apply pp
have : p 1 := by
convert Nat.dvd_sub' pdvd this
simp
show False
have := Nat.le_of_dvd zero_lt_one this
linarith [pp.two_le]
theorem bounded_of_ex_finset (Q : → Prop) :
(∃ s : Finset , ∀ k, Q k → k ∈ s) → ∃ n, ∀ k, Q k → k < n := by
rintro ⟨s, hs⟩
use s.sup id + 1
intro k Qk
apply Nat.lt_succ_of_le
show id k ≤ s.sup id
apply le_sup (hs k Qk)
theorem ex_finset_of_bounded (Q : → Prop) [DecidablePred Q] :
(∃ n, ∀ k, Q k → k ≤ n) → ∃ s : Finset , ∀ k, Q k ↔ k ∈ s := by
rintro ⟨n, hn⟩
use (range (n + 1)).filter Q
intro k
simp [Nat.lt_succ_iff]
exact hn k
theorem mod_4_eq_3_or_mod_4_eq_3 {m n : } (h : m * n % 4 = 3) : m % 4 = 3 n % 4 = 3 := by
revert h
rw [Nat.mul_mod]
have : m % 4 < 4 := Nat.mod_lt m (by norm_num)
interval_cases hm : m % 4 <;> simp [hm]
have : n % 4 < 4 := Nat.mod_lt n (by norm_num)
interval_cases hn : n % 4 <;> simp [hn]
theorem two_le_of_mod_4_eq_3 {n : } (h : n % 4 = 3) : 2 ≤ n := by
apply two_le <;>
· intro neq
rw [neq] at h
norm_num at h
theorem aux {m n : } (h₀ : m n) (h₁ : 2 ≤ m) (h₂ : m < n) : n / m n ∧ n / m < n := by
constructor
· exact Nat.div_dvd_of_dvd h₀
exact Nat.div_lt_self (lt_of_le_of_lt (zero_le _) h₂) h₁
theorem exists_prime_factor_mod_4_eq_3 {n : Nat} (h : n % 4 = 3) :
∃ p : Nat, p.Prime ∧ p n ∧ p % 4 = 3 := by
by_cases np : n.Prime
· use n
induction' n using Nat.strong_induction_on with n ih
rw [Nat.prime_def_lt] at np
push_neg at np
rcases np (two_le_of_mod_4_eq_3 h) with ⟨m, mltn, mdvdn, mne1⟩
have mge2 : 2 ≤ m := by
apply two_le _ mne1
intro mz
rw [mz, zero_dvd_iff] at mdvdn
linarith
have neq : m * (n / m) = n := Nat.mul_div_cancel' mdvdn
have : m % 4 = 3 n / m % 4 = 3 := by
apply mod_4_eq_3_or_mod_4_eq_3
rw [neq, h]
cases' this with h1 h1
· by_cases mp : m.Prime
· use m
rcases ih m mltn h1 mp with ⟨p, pp, pdvd, p4eq⟩
use p
exact ⟨pp, pdvd.trans mdvdn, p4eq⟩
obtain ⟨nmdvdn, nmltn⟩ := aux mdvdn mge2 mltn
by_cases nmp : (n / m).Prime
· use n / m
rcases ih (n / m) nmltn h1 nmp with ⟨p, pp, pdvd, p4eq⟩
use p
exact ⟨pp, pdvd.trans nmdvdn, p4eq⟩
theorem primes_mod_4_eq_3_infinite : ∀ n, ∃ p > n, Nat.Prime p ∧ p % 4 = 3 := by
by_contra h
push_neg at h
cases' h with n hn
have : ∃ s : Finset Nat, ∀ p : , p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by
apply ex_finset_of_bounded
use n
contrapose! hn
rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
exact ⟨p, pltn, pp, p4⟩
cases' this with s hs
have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by
rw [add_comm, Nat.add_mul_mod_self_left]
norm_num
rcases exists_prime_factor_mod_4_eq_3 h₁ with ⟨p, pp, pdvd, p4eq⟩
have ps : p ∈ s := by
rw [← hs p]
exact ⟨pp, p4eq⟩
have pne3 : p ≠ 3 := by
intro peq
rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd
rw [Nat.prime_three.dvd_mul] at pdvd
norm_num at pdvd
have : 3 ∈ s.erase 3 := by
apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
intro n
simp [← hs n]
tauto
simp at this
have : p 4 * ∏ i in erase s 3, i := by
apply dvd_trans _ (dvd_mul_left _ _)
apply dvd_prod_of_mem
simp
constructor <;> assumption
have : p 3 := by
convert Nat.dvd_sub' pdvd this
simp
have : p = 3 := by
apply pp.eq_of_dvd_of_prime Nat.prime_three this
contradiction