rw[BrunTitchmarsh.card_Ioc_filter_dvd _ _ _ hd]
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d ≠ 0
⊢ (Finset.filter (fun x => d ∣ x) (Finset.Ioc (⌈x⌉₊ - 1) ⌊x + y⌋₊)).card = ⌊x + y⌋₊ / d - (⌈x⌉₊ - 1) / d
no goals