English
Let p be a natural number and L a nonempty list of digits with digits less than p. Then (p − 1) times the sum of divisions of the fixed value by p^{i+1} equals the value minus the sum of the digits.
Русский
Пусть p — натуральное число, а L — непустой список цифр, каждая цифра меньше p. Тогда (p−1) умножить на сумму делений фиксированного значения на p^{i+1} равняется значению минус сумма цифр.
LaTeX
$$$ (p - 1) \sum_{i=0}^{|L|-1} \frac{\operatorname{ofDigits}(p,L)}{p^{i+1}} = \operatorname{ofDigits}(p,L) - \sum L $$
Lean4
theorem sub_one_mul_sum_div_pow_eq_sub_sum_digits {p : ℕ} (L : List ℕ) {h_nonempty}
(h_ne_zero : L.getLast h_nonempty ≠ 0) (h_lt : ∀ l ∈ L, l < p) :
(p - 1) * ∑ i ∈ range L.length, (ofDigits p L) / p ^ i.succ = (ofDigits p L) - L.sum :=
by
obtain h | rfl | h : 1 < p ∨ 1 = p ∨ p < 1 := trichotomous 1 p
·
induction L with
| nil => simp [ofDigits]
| cons hd tl
ih =>
simp only [List.length_cons, List.sum_cons, self_div_pow_eq_ofDigits_drop _ _ h,
digits_ofDigits p h (hd :: tl) h_lt (fun _ => h_ne_zero)]
simp only [ofDigits]
rw [sum_range_succ, Nat.cast_id]
simp only [List.drop, List.drop_length]
obtain rfl | h' := em <| tl = []
· simp [ofDigits]
· have w₁' := fun l hl ↦ h_lt l <| List.mem_cons_of_mem hd hl
have w₂' := fun (h : tl ≠ []) ↦ (List.getLast_cons h) ▸ h_ne_zero
have ih := ih (w₂' h') w₁'
simp only [self_div_pow_eq_ofDigits_drop _ _ h, digits_ofDigits p h tl w₁' w₂', ← Nat.one_add] at ih
have := sum_singleton (fun x ↦ ofDigits p <| tl.drop x) tl.length
rw [← Ico_succ_singleton, List.drop_length, ofDigits] at this
have h₁ : 1 ≤ tl.length := List.length_pos_iff.mpr h'
rw [← sum_range_add_sum_Ico _ <| h₁, ← add_zero (∑ x ∈ Ico _ _, ofDigits p (tl.drop x)), ← this,
sum_Ico_consecutive _ h₁ <| (le_add_right tl.length 1), ← sum_Ico_add _ 0 tl.length 1, Ico_zero_eq_range,
mul_add, mul_add, ih, range_one, sum_singleton, List.drop, ofDigits, mul_zero, add_zero, ←
Nat.add_sub_assoc <| sum_le_ofDigits _ <| Nat.le_of_lt h]
nth_rw 2 [← one_mul <| ofDigits p tl]
rw [← add_mul, Nat.sub_add_cancel (one_le_of_lt h), Nat.add_sub_add_left]
· simp [ofDigits_one]
· simp [lt_one_iff.mp h]
cases L
· rfl
· simp [ofDigits]
