Source indexedtheorem · leanprover/lean4:v4.32.0

BrunTitchmarsh.range_filter_isPrimePow_subset_union

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:377 to 398

Mathematical statement

Exact Lean statement

theorem range_filter_isPrimePow_subset_union (N : ℕ) :
    ((Finset.range N).filter IsPrimePow) ⊆ (Finset.range N).filter Nat.Prime ∪
      ((Finset.Ico 1 (Nat.ceil (Real.sqrt N))) ×ˢ Finset.range (Nat.log 2 N + 1)).image
        (fun p ↦ p.1 ^ p.2)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem range_filter_isPrimePow_subset_union (N : ℕ) :    ((Finset.range N).filter IsPrimePow) ⊆ (Finset.range N).filter Nat.Prime ∪      ((Finset.Ico 1 (Nat.ceil (Real.sqrt N))) ×ˢ Finset.range (Nat.log 2 N + 1)).image        (fun p ↦ p.1 ^ p.2) := by  intro n  simp only [Finset.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_union,    Finset.mem_image, Finset.mem_product, Prod.exists, and_imp]  intro hnN hnprime  rcases prime_or_pow N n hnN hnprime with hp | ⟨m, hm, k, hk, h⟩  · left    exact ⟨hnN, hp⟩  · right    refine ⟨m, k, ?_⟩    by_cases hm : m = 0    · rw [hm, zero_pow] at h      · exact False.elim (hnprime.ne_zero h)      · rintro rfl        simp only [pow_zero] at h        exact False.elim (hnprime.ne_one h)    rw [Nat.lt_ceil, Nat.lt_succ_iff]    have : 1 ≤ m := by omega    aesop