Source indexedtheorem · leanprover/lean4:v4.32.0

BrunTitchmarsh.Ioc_filter_dvd_eq

PrimeNumberTheoremAnd.BrunTitchmarsh · PrimeNumberTheoremAnd/BrunTitchmarsh.lean:101 to 113

Mathematical statement

Exact Lean statement

theorem Ioc_filter_dvd_eq (d a b : ℕ) (hd : d ≠ 0) :
  Finset.filter (fun x ↦ d ∣ x) (Finset.Ioc a b) =
    Finset.image (fun x ↦ x * d) (Finset.Ioc (a / d) (b / d))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Ioc_filter_dvd_eq (d a b : ℕ) (hd : d ≠ 0) :  Finset.filter (fun x ↦ d ∣ x) (Finset.Ioc a b) =    Finset.image (fun x ↦ x * d) (Finset.Ioc (a / d) (b / d)) := by  ext n  simp only [Finset.mem_filter, Finset.mem_Ioc, Finset.mem_image]  constructor  · intro hn    rcases hn with ⟨⟨han, hnb⟩, hd⟩    refine ⟨n/d, ⟨Nat.div_lt_div_of_lt_of_dvd hd han,      Nat.div_le_div_right (Nat.le_floor hnb)⟩, Nat.div_mul_cancel hd⟩  · rintro ⟨r, ⟨ha, ha'⟩, rfl⟩    refine ⟨⟨(Nat.div_lt_iff_lt_mul (by omega)).mp ha, Nat.mul_le_of_le_div d r b ha'⟩,      Nat.dvd_mul_left d r⟩