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( floor((b − v)/r) − floor((a − v)/r), 0 ).
Русский
Пусть a ≤ b и r > 0 — целые числа, и v — целое число. Тогда количество целых x во множестве (a, b], удовлетворяющих x ≡ v (mod r), равно max( floor((b − v)/r) − floor((a − v)/r), 0 ).
LaTeX
$$$\#\{x \in \mathrm{Ioc}\ a\ b \;|\; x \equiv v \,[ZMOD\ r]\} = \max\left( \left\lfloor \frac{b - v}{r} \right\rfloor - \left\lfloor \frac{a - v}{r} \right\rfloor, 0 \right)$$$
Lean4
/-- There are `⌊(b - v) / r⌋ - ⌊(a - v) / r⌋` numbers congruent to `v` mod `r` in `(a, b]`,
if `a ≤ b`. -/
theorem Ioc_filter_modEq_card (v : ℤ) :
#({x ∈ Ioc a b | x ≡ v [ZMOD r]}) = max (⌊(b - v) / (r : ℚ)⌋ - ⌊(a - v) / (r : ℚ)⌋) 0 := by
simp [Ioc_filter_modEq_eq, Ioc_filter_dvd_eq, hr]
