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

source

theorem int.sum_mod {n : ℕ} (x : fin n → ℤ) (a : ℤ) :

finset.univ.sum (λ (i : fin n), x i) % a = finset.univ.sum (λ (i : fin n), x i % a) % a

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

source

theorem fin.succ_mod_self {n : ℕ} (hn : 1 < n) :

n.succ % n = 1

source

theorem fin.succ_pow_mod_self {n a : ℕ} (ha : 1 < a) :

a.succ ^ n % a = 1

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

source

theorem int.mul_nat_succ_pow_mod_nat (a : ℤ) {b n : ℕ} (hb : 1 < b) :

a * ↑(b.succ ^ n) % ↑b = a % ↑b

source

theorem nat_repr_mod_eq_sum_repr_mod {a n : ℕ} (x : fin n → ℤ) (ha : 1 < a) :

finset.univ.sum (λ (i : fin n), x i * ↑(a.succ) ^ ↑i) % ↑a = finset.univ.sum (λ (i : fin n), x i) % ↑a

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

source

theorem nat_dvd_repr_iff_nat_dvd_sum_repr {a n : ℕ} (x : fin n → ℤ) (ha : 1 < a) :

↑a ∣ finset.univ.sum (λ (i : fin n), x i * ↑(a.succ) ^ ↑i) ↔ ↑a ∣ finset.univ.sum (λ (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