English
Let p be a natural number and n a nonnegative integer. Then (p − 1) times the sum over i up to log_p n of floor(n / p^{i+1}) equals n minus the sum of the base-p digits of n.
Русский
Пусть p — натуральное число, n — неотрицательное целое. Тогда (p−1) умножить сумму по i до log_p n floor(n / p^{i+1}) равняется n минус сумма цифр n в основания p.
LaTeX
$$$ (p - 1) \sum_{i \in \{0,\dots, \log_p n\}} \left\lfloor \frac{n}{p^{i+1}} \right\rfloor = n - (\mathrm{digits}_p(n)).\text{sum} $$$
Lean4
theorem sub_one_mul_sum_log_div_pow_eq_sub_sum_digits {p : ℕ} (n : ℕ) :
(p - 1) * ∑ i ∈ range (log p n).succ, n / p ^ i.succ = n - (p.digits n).sum :=
by
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
· rcases eq_or_ne n 0 with rfl | hn
· simp
· convert
sub_one_mul_sum_div_pow_eq_sub_sum_digits (p.digits n) (getLast_digit_ne_zero p hn) <|
(fun l a ↦ digits_lt_base h a)
· refine (digits_len p n h hn).symm
all_goals exact (ofDigits_digits p n).symm
· simp
· simp [lt_one_iff.mp h]
cases n
all_goals simp
