Divisibility tests for natural numbers in terms of digits.

We prove some divisibility tests based on digits, in particular completing Theorem #85 from https://www.cs.ru.nl/~freek/100/.

theorem Nat.modEq_three_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 3]

theorem Nat.modEq_nine_digits_sum (n : ℕ) : n ≡ (digits 10 n).sum [MOD 9]

theorem Nat.modEq_eleven_digits_sum (n : ℕ) : ↑n ≡ (List.map (fun (n : ℕ) => ↑n) (digits 10 n)).alternatingSum [ZMOD 11]

Divisibility

theorem Nat.dvd_iff_dvd_digits_sum (b b' : ℕ) (h : b' % b = 1) (n : ℕ) : b ∣ n ↔ b ∣ (b'.digits n).sum

theorem Nat.three_dvd_iff (n : ℕ) : 3 ∣ n ↔ 3 ∣ (digits 10 n).sum

Divisibility by 3 Rule

theorem Nat.nine_dvd_iff (n : ℕ) : 9 ∣ n ↔ 9 ∣ (digits 10 n).sum

theorem Nat.dvd_iff_dvd_ofDigits (b b' : ℕ) (c : ℤ) (h : ↑b ∣ ↑b' - c) (n : ℕ) : b ∣ n ↔ ↑b ∣ ofDigits c (b'.digits n)

theorem Nat.eleven_dvd_iff {n : ℕ} : 11 ∣ n ↔ 11 ∣ (List.map (fun (n : ℕ) => ↑n) (digits 10 n)).alternatingSum

theorem Nat.eleven_dvd_of_palindrome {n : ℕ} (p : (digits 10 n).Palindrome) (h : Even (digits 10 n).length) : 11 ∣ n