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 baseb + 1
byb
is equal to the remainder of dividing the sum of its digits byb
nat_dvd_repr_iff_nat_dvd_sum_repr
: this says that a number in baseb + 1
is divisible byb
if and only if the sum of its digits is divisible byb
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