Useless and interesting fact(s) on naturals and integers

Sonia recently asked me: "Is there a way to prove that a number is divisible by 9, by looking at the sum of its digits?" So here is the generalised version of the question.

Main results

In both of the following results, b is a natural number greater than 1.

• nat_repr_mod_eq_sum_repr_mod: this says that the remainder of dividing a number in base b + 1 by b is equal to the remainder of dividing the sum of its digits by b
• nat_dvd_repr_iff_nat_dvd_sum_repr: this says that a number in base b + 1 is divisible by b if and only if the sum of its digits is divisible by b

theorem Int.sum_mod {n : ℕ} (x : Fin n → ℤ) (a : ℤ) : (∑ i : Fin n, x i) % a = (∑ i : Fin n, x i % a) % a

(∑ i, x i) % a = (∑ i, (x i % a)) % a

theorem Fin.succ_mod_self {n : ℕ} (hn : 1 < n) : n.succ % n = 1

theorem Fin.succ_pow_mod_self {n : ℕ} {a : ℕ} (ha : 1 < a) : a.succ ^ n % a = 1

a.succ ^ n % a = 1 when 1 < a

theorem Int.hMul_nat_succ_pow_mod_nat (a : ℤ) {b : ℕ} {n : ℕ} (hb : 1 < b) : a * ↑(b.succ ^ n) % ↑b = a % ↑b

theorem nat_repr_mod_eq_sum_repr_mod {a : ℕ} {n : ℕ} (x : Fin n → ℤ) (ha : 1 < a) : (∑ i : Fin n, x i * ↑a.succ ^ ↑i) % ↑a = (∑ i : Fin n, x i) % ↑a

(∑ i, (x i * a.succ ^ i)) % a = (∑ i, x i) % a

theorem nat_dvd_repr_iff_nat_dvd_sum_repr {a : ℕ} {n : ℕ} (x : Fin n → ℤ) (ha : 1 < a) : ↑a ∣ ∑ i : Fin n, x i * ↑a.succ ^ ↑i ↔ ↑a ∣ ∑ i : Fin n, x i

a ∣ (∑ i, (x i * a.succ ^ i)) ↔ a ∣ (∑ i, x i) in other words, a number in base a.succ is divisible by a, if and only if the sum of its digits is divisible by a