English
Let a ≤ b and r > 0 be integers, and v an integer. Then the number of integers x in [a, b) with x ≡ v (mod r) equals max( ceil((b − v)/r) − ceil((a − v)/r), 0 ).
Русский
Пусть a ≤ b и r > 0 — целые числа, и v — целое число. Тогда количество целых x в интервале [a, b), удовлетворяющих x ≡ v (mod r), равно max( ceil((b − v)/r) − ceil((a − v)/r), 0 ).
LaTeX
$$$\#\{x \in \mathrm{Ico}\ a\ b \;|\; x \equiv v \,[ZMOD\ r]\} = \max\left( \left\lceil \frac{b - v}{r} \right\rceil - \left\lceil \frac{a - v}{r} \right\rceil, 0 \right)$$$
Lean4
/-- There are `⌈(b - v) / r⌉ - ⌈(a - v) / r⌉` numbers congruent to `v` mod `r` in `[a, b)`,
if `a ≤ b`. -/
theorem Ico_filter_modEq_card (v : ℤ) :
#({x ∈ Ico a b | x ≡ v [ZMOD r]}) = max (⌈(b - v) / (r : ℚ)⌉ - ⌈(a - v) / (r : ℚ)⌉) 0 := by
simp [Ico_filter_modEq_eq, Ico_filter_dvd_eq, hr]
