有限の場合の総和記号について勉強したことで任意桁数の場合の３の倍数の確認方法について形式化して証明することが出来そうです。ということでやってみました。
まず与えられた自然数が３の倍数かどうかの確認方法と普通の証明をざっと述べてみます。
３の倍数の確認方法：$N, i, a_i$を自然数として$a_i$は各桁の数を表します。従って$\sum_{i=0}^{N-1} a_i\cdot 10^i$が与えられた自然数です。確認方法は、
$$3 | \sum_{i=0}^{N-1} a_i\cdot 10^i \iff 3 | \sum_{i=0}^{N-1} a_i$$
が成り立つので、右辺の和（各桁の数の和）を計算して３の倍数かどうかみれば与えられた自然数（左辺の和）が３の倍数かどうかわかります。というわけで上記の式を証明します。
証明：
前の記事で紹介した定理divisable_add：$a,b,k$を自然数として$k|a$ならば$k|(a+b)$と$k|b$は同値。
を最後のステップで使いたいのです。そこで目標として$$\tag{A}\sum_{i=0}^{N-1} a_i\cdot 10^i=\sum_{i=0}^{N-1} a_i\cdot (10^i-1) + \sum_{i=0}^{N-1} a_i$$及び$$\tag{B}3| \sum_{i=0}^{N-1} a_i\cdot (10^i-1) $$を示すことにします。
(A)は総和の和は和の総和、ということで有限の総和では自明です。
(B)は$3 | 10^k - 1$であることを示し、さらに一般的に$ \forall i\in \mathbb{N}及び0\le m\in\mathbb{N}, m|f(i) \implies m| \sum_{i=0}^{N-1} a_i\cdot f(i)$を示すことで示すことができます。
上記の流れを形式化したものを示します。
example {N:ℕ} : 3∣ (∑ i in range N, (a i)*10^i) ↔ 3∣ (∑ i in range N, (a i)) := by
have h0 {k:ℕ} : 3∣ 10^k-1 := by sorry
have h5 {i:ℕ}: (a i)*(10^i-1)+(a i)=(a i)*10^i := by sorry
have h6: ∑ i in range N, (a i)*10^i=∑ i in range N, ( (a i)*(10^i-1)+(a i)) := by sorry
have h7: ∑ i in range N, ( (a i)*(10^i-1)+(a i))=(∑ i in range N, (a i)*(10^i-1)) + ∑ i in range N, (a i) := by sorry
have h8: 3∣ ∑ i in range N, (a i)*(10^i-1) := by sorry
rw [h6,h7]
apply divisable_add h8ただし補題h0〜h8の証明は一旦sorryとして流れだけ見えるようにしてあります。h5, h6, h7で(A)を示しています。またh0, h8で(B)を示しています。最後の２行で総和の式変形とdivisable_addによる同値条件から証明が終了します。
以下に形式証明を全部載せるのですが、全部で100行近くになってしまいました。特に解説は載せませんので、ご自身の環境で試していただければと思います。
上記のh0〜h8で一番行数がかかっているのはh0です。特に$10^{k+1}-1=10\cdot (10^k - 1)+9$という式変形で10行もかかっていていかにも下手くそな感じです,,, orz
import Mathlib.Data.Nat.GCD.Basic
import Mathlib.Algebra.BigOperators.Basic
import Mathlib.Data.Nat.Factorization.Basicopen BigOperators
open Finset
variable (a : ℕ → ℕ ) (f : ℕ → ℕ )
theorem divisable_add {a b k:ℕ } (h: k∣a) : k∣(a+b)↔k∣b := by
rcases h with ⟨m,hh⟩
constructor
· intro h1
rcases h1 with ⟨ n, h2⟩
rw [hh] at h2
have h3: b= k*n-k*m := by exact (tsub_eq_of_eq_add_rev (id h2.symm)).symm
have : b = k*(n-m) := by
rw [← Nat.mul_sub_left_distrib k n m] at h3; assumption
rw [this]
exact Nat.dvd_mul_right k (n - m)
intro h1
rcases h1 with ⟨ n,h2⟩
rw [hh,h2]
have : k*m+k*n=k*(m+n) := by exact (Nat.mul_add k m n).symm
rw [this]
exact Nat.dvd_mul_right k (m + n)
theorem divisable_add' {a b k: ℕ} : k∣ a → (k∣b ↔ k∣ (a+b)) := by
intro h'
symm
apply divisable_add h'
theorem sum_term_divisable {f:ℕ→ℕ} {d N:ℕ}: (∀ j:ℕ, d∣(f j)) → d∣∑ i in range N, (a i)*(f i) := by
intro h1
induction' N with k ih
· exact Nat.dvd_of_mod_eq_zero rflhave h2: d∣ (a k)*(f k) := by exact Dvd.dvd.mul_left (h1 k) (a k)
have h3: d∣ (a k)*(f k)+∑ i in range k, (a i)*(f i) ↔ d∣ ∑ i in range k, (a i)*(f i) := by
apply divisable_add h2
have h4: (a k)*(f k)+∑ i in range k, (a i)*(f i)=∑ i in range (Nat.succ k), (a i)*(f i) := by exact
(sum_range_succ_comm (fun x ↦ a x * f x) k).symm
rw [← h4,h3]
assumption
example {N:ℕ} : 3∣ (∑ i in range N, (a i)*10^i) ↔ 3∣ (∑ i in range N, (a i)) := by
have h0 {k:ℕ} : 3∣ 10^k-1 := by
induction' k with k ih
· simp
have h1: 10^(k+1)-1=10*(10^k-1)+9 := by
have h9: 9≤9 := by linarith
have asc: 10≤ 10*10^k := by
have : 1≤ 10^k := by exact Nat.one_le_pow' k 9
exact Nat.le_mul_of_pos_right 10 this
calc
10^(k+1)-1 = 10*10^k - 1 := by omega
_ = 9 - 9 + (10*10^k - 1) := by exact self_eq_add_left.mpr rfl
_ = 9 + (10*10^k - 1) - 9 := by rw [tsub_add_eq_add_tsub h9]
_ = 9 + 10*10^k - 1 - 9 := by omega
_ = 9 + 10*10^k - 10 := by exact rfl
_ = 9 + (10*10^k - 10) := by refine add_tsub_assoc_of_le asc 9
_ = 10*(10^k-1)+9 := by omega
rw [h1,add_comm]
have h2: 3∣9 := by norm_num
have h3: 3∣10*(10^k-1) := by omega
refine (divisable_add' h2).mp h3
have h5 {i:ℕ}: (a i)*(10^i-1)+(a i)=(a i)*10^i := by
have h4 {i:ℕ} : (a i)*10^i ≥ (a i) := by
have : 1≤ 10^i := by exact Nat.one_le_pow' i 9
exact Nat.le_mul_of_pos_right (a i) this
calc
(a i)*(10^i-1)+(a i)=(a i)*10^i - (a i) + (a i) := by rw [Nat.mul_sub_left_distrib (a i) (10^i) 1]; simp
_ = (a i)*10^i := by rw [Nat.sub_add_cancel h4]
have h6: ∑ i in range N, (a i)*10^i=∑ i in range N, ( (a i)*(10^i-1)+(a i)) := by
apply Finset.sum_congr
· rfl
intro x _
symm
apply h5
have h7: ∑ i in range N, ( (a i)*(10^i-1)+(a i))=(∑ i in range N, (a i)*(10^i-1)) + ∑ i in range N, (a i) := by
exact sum_add_distrib
have h8: 3∣ ∑ i in range N, (a i)*(10^i-1) := by
apply sum_term_divisable
apply h0
rw [h6,h7]
apply divisable_add h8
