Source indexedtheorem · leanprover/lean4:v4.32.0

Sieve.prime_dvd_primorial_iff

PrimeNumberTheoremAnd.Mathlib.NumberTheory.Sieve.SelbergBounds · PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/SelbergBounds.lean:63 to 77

Mathematical statement

Exact Lean statement

theorem prime_dvd_primorial_iff (n p : ℕ) (hp : p.Prime) :
    p ∣ primorial n ↔ p ≤ n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem prime_dvd_primorial_iff (n p : ℕ) (hp : p.Prime) :    p ∣ primorial n ↔ p ≤ n := by  unfold primorial  constructor  · intro h    obtain ⟨q, hq⟩ : ∃ i, i ∈ Finset.filter Nat.Prime (Finset.range (n + 1)) ∧ p ∣ i :=      hp.prime.exists_mem_finset_dvd h    rw [Finset.mem_filter, Finset.mem_range] at hq    rw [prime_dvd_prime_iff_eq (Nat.Prime.prime hp) (Nat.Prime.prime hq.1.2)] at hq    rw [hq.2]    exact Nat.lt_succ_iff.mp hq.1.1  · intro h    apply Finset.dvd_prod_of_mem    rw [Finset.mem_filter, Finset.mem_range]    exact ⟨Nat.lt_succ_iff.mpr h, hp⟩