Source indexedtheorem · leanprover/lean4:v4.32.0

BrunTitchmarsh.primesBetween_subset

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:61 to 77

Mathematical statement

Exact Lean statement

theorem primesBetween_subset :
  (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter Nat.Prime ⊆
    (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter
      (fun d ↦ ∀ p : ℕ, p.Prime → p ≤ z → ¬p ∣ d) ∪
      (Finset.Icc 1 (Nat.floor z))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem primesBetween_subset :  (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter Nat.Prime ⊆    (Finset.Icc (Nat.ceil x) (Nat.floor (x+y))).filter      (fun d ↦ ∀ p : ℕ, p.Prime → p ≤ z → ¬p ∣ d) ∪      (Finset.Icc 1 (Nat.floor z)) := by  intro p  simp only [Finset.mem_filter, Finset.mem_Icc, Nat.ceil_le, Finset.mem_union, and_imp]  intro hx hxy hp  by_cases hpz : p ≤ z  · right    rw [Nat.le_floor_iff (by linarith)]    have := hp.ne_zero    exact ⟨by omega, hpz⟩  · refine Or.inl ⟨⟨hx, hxy⟩, fun q hq hqz ↦ ?_⟩    rw [hp.dvd_iff_eq (hq.ne_one)]    rintro rfl    exact hpz hqz