book集

section 準備
subsection 10 = 3⋅3 + 1
!thm `\n ∈ 𝕄` ◀ 𝕄0s , W. at \n=3..10
prf goal / W. -| 𝕄0s , `\n-1 ∈ 𝕄` p; goal -| 𝕄0s , W. h;
!let/thm L10 <- `3 ⋅ 3 + 1 = 10` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 , *𝕄
prf L6 <- `3 + 3 = 6` -| +𝕄 , 1. , 2. , 3. , 4. , 5. , 6. , `3 ∈ 𝕄` , `2 ∈ 𝕄` , `1 ∈ 𝕄` , 𝕄0s p;
    L9 <- `6 + 3 = 9` -| +𝕄 , 1. , 2. , 3. , 7. , 8. , 9. , `6 ∈ 𝕄` , `2 ∈ 𝕄` , `1 ∈ 𝕄` , 𝕄0s p;
    L33 <- `3 ⋅ 3 = 9` -| *𝕄 , L0+ , L6 , L9 , 1. , 2. , 3. , `3 ∈ 𝕄` , `2 ∈ 𝕄` , `1 ∈ 𝕄` , 𝕄0s p;
    L10 -| L33 , +1 , 10. , `9 ∈ 𝕄` p;
    L10 -| W. , 𝕄0s , IND𝕄 , +𝕄 , *𝕄 h;

subsection 10 の冪
txt \(10^i\) を3で割った余りは1（\(10 = 3 \cdot 3 + 1\) から帰納法で）。
let/thm L10↑ <- `i ∈ 𝕄 ⟹ [ ∃ c ∈ 𝕄 . 10 ↑ i = 3 ⋅ c + 1 ]` ◀ W. , 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1.
prf Lb <- `10 ↑ 0 = 3 ⋅ 0 + 1` -| ↑𝕄 , *𝕄 , L0+ , `10 ∈ 𝕄` , `3 ∈ 𝕄` , `1 ∈ 𝕄` p;
    Le1 <- `c ∈ 𝕄 ⟹ (3 ⋅ c + 1) ⋅ 10 = 3 ⋅ (c ⋅ 10) + 10` -| Rdist , ⋅A , ⋅C , L⋅1 , ⋅∈𝕄 , `3 ∈ 𝕄` , `10 ∈ 𝕄` , `1 ∈ 𝕄` v;
    Le2 <- `c ∈ 𝕄 ⟹ 3 ⋅ (c ⋅ 10 + 3) + 1 = 3 ⋅ (c ⋅ 10) + 10` -| Ldist , +A , L10 , ⋅∈𝕄 , `3 ∈ 𝕄` , `10 ∈ 𝕄` , `1 ∈ 𝕄` v;
    Ls <- `i ∈ 𝕄 and [ ∃ c ∈ 𝕄 . 10 ↑ i = 3 ⋅ c + 1 ] ⟹ [ ∃ c ∈ 𝕄 . 10 ↑ { i suc } = 3 ⋅ c + 1 ]` -| ↑𝕄 , Le1 , Le2 , ⋅∈𝕄 , +∈𝕄 , `3 ∈ 𝕄` , `10 ∈ 𝕄` v;
    L10↑ -| IND𝕄[C_:=`\{ cls i | [ ∃ c ∈ 𝕄 . 10 ↑ i = 3 ⋅ c + 1 ] \}`] , Lb , Ls , 𝕄0s v;
    L10↑ -| W. , 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. h;

subsection 3 の倍数を足しても変わらない
let/thm L3t <- `[ x ; t col ∈ 𝕄 ] ⟹ (3 ∣ x + 3 ⋅ t ⟺ 3 ∣ x)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄
prf D1 <- `[ x ; t ; k col ∈ 𝕄 ] and x = 3 ⋅ k ⟹ x + 3 ⋅ t = 3 ⋅ (k + t)` -| Ldist , `3 ∈ 𝕄` p;
    D2 <- `[ x ; t ; e col ∈ 𝕄 ] and x + 3 ⋅ t = 3 ⋅ (e + t) ⟹ x = 3 ⋅ e` -| Ldist , +K , +C , ⋅∈𝕄 , `3 ∈ 𝕄` v;
    D0 <- `[ x ; y ; z col ∈ 𝕄 ] and (x + y) + z = 0 + z ⟹ x = 0` -| +C , +K , L+=0 , +∈𝕄 , 𝕄0s p;
    D3 <- `[ x ; e ; k col ∈ 𝕄 ] and x + 3 ⋅ (e + k) = 3 ⋅ k ⟹ x = 3 ⋅ 0` -| D0 , Ldist , +A , L0+ , *𝕄 , ⋅∈𝕄 , `3 ∈ 𝕄` v;
    L3t / ∣. [⇒ / ≤. / <. -| Ltot / ≤. / <. , L<≤ / ≤. / <. , D2 , D3 , 𝕄0s , +C || <= -| D1 , +∈𝕄] v;
    L3t -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h;

newpage
section 主定理
word ap
txt 各桁を \(d(0), d(1), \ldots\)（\(d(i)\) は \(10^i\) の位）とし、\(N(n) = \sum_{i\lt n} d(i) \cdot 10^i\)、\(S(n) = \sum_{i\lt n} d(i)\) とします。
txt ここでは \(N\)・\(S\) を漸化式を満たす関数として仮定します（存在は示しません）。各 \(d(i)\) は自然数であればよく、10 未満でなくても成り立ちます。したがって主定理は「そのような \(N\)・\(S\) があれば」という条件付きの形です。
txt 証明：\(10^i = 3c + 1\) なので \(d \cdot 10^i = d + 3dc\)。足し合わせると \(N(n) = S(n) + 3t\) の形になり（帰納法）、3 の倍数を足しても 3 で割り切れるかは変わりません。
thm `\\{ And [ ∀ i ∈ 𝕄 . d ap (i) ∈ 𝕄 ] \\ N ap (0) = 0 \\ [ ∀ i ∈ 𝕄 . N ap (i suc) = N ap (i) + d ap (i) ⋅ 10 ↑ i ] \\ S ap (0) = 0 \\ [ ∀ i ∈ 𝕄 . S ap (i suc) = S ap (i) + d ap (i) ] \\} and n ∈ 𝕄 ⟹ (3 ∣ N ap (n) ⟺ 3 ∣ S ap (n))` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1.
prf hyD <- `[ ∀ i ∈ 𝕄 . |d ap (i) ∈ 𝕄 ]` ;
    hyN0 <- `|N ap (0) = 0` ;
    hyNS <- `[ ∀ i ∈ 𝕄 . |N ap (i suc) = |N ap (i) + |d ap (i) ⋅ 10 ↑ i ]` ;
    hyS0 <- `|S ap (0) = 0` ;
    hySS <- `[ ∀ i ∈ 𝕄 . |S ap (i suc) = |S ap (i) + |d ap (i) ]` ;
    LS∈ <- `n ∈ 𝕄 ⟹ |S ap (n) ∈ 𝕄` -| IND𝕄[C_:=`\{ cls n | |S ap (n) ∈ 𝕄 \}`] , hyS0 , hySS , hyD , 𝕄0s , +∈𝕄 v;
    E1 <- `[ a ; c col ∈ 𝕄 ] ⟹ a ⋅ (3 ⋅ c + 1) = 3 ⋅ (a ⋅ c) + a` -| Ldist , L⋅1 , ⋅A , ⋅C , ⋅∈𝕄 , `3 ∈ 𝕄` , `1 ∈ 𝕄` v;
    E2 <- `[ s ; t ; a ; u col ∈ 𝕄 ] ⟹ (s + 3 ⋅ t) + (3 ⋅ u + a) = (s + a) + 3 ⋅ (t + u)` -| Ldist , +A , +C , ⋅∈𝕄 , +∈𝕄 , `3 ∈ 𝕄` v;
    Lb <- `|N ap (0) = |S ap (0) + 3 ⋅ 0` -| hyN0 , hyS0 , +𝕄 , *𝕄 , `3 ∈ 𝕄` , 𝕄0s p;
    Ls <- `m ∈ 𝕄 and [ ∃ t ∈ 𝕄 . |N ap (m) = |S ap (m) + 3 ⋅ t ] ⟹ [ ∃ t ∈ 𝕄 . |N ap (m suc) = |S ap (m suc) + 3 ⋅ t ]` -| hyNS , hySS , hyD , L10↑ , E1 , E2 , LS∈ , ⋅∈𝕄 , +∈𝕄 v;
    LNS <- `n ∈ 𝕄 ⟹ [ ∃ t ∈ 𝕄 . |N ap (n) = |S ap (n) + 3 ⋅ t ]` -| IND𝕄[C_:=`\{ cls n | [ ∃ t ∈ 𝕄 . |N ap (n) = |S ap (n) + 3 ⋅ t ] \}`] , Lb , Ls , 𝕄0s v;
    hyn <- `|n ∈ 𝕄` ;
    Lfix <- `3 ∣ |N ap (|n) ⟺ 3 ∣ |S ap (|n)` -| LNS , L3t , LS∈ , hyn p;
    goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. h[fix];

articles3/85.book

`articles3/85.book`