book集

section 整数の計算
txt standard_math/1-4 の整数に、整数の問題でよく使う事実を足します。
let/thm 𝕄⊂ℤ <- `x ∈ 𝕄 ⟹ x ∈ ℤ` ◀ W.
prf 𝕄⊂ℤ /// W.'!𝕄.!=. -| O p; 𝕄⊂ℤ -| W. h;
let/thm ⋅0 <- `x ∈ ℤ ⟹ x ⋅ 0 = 0` ◀ W. , ax_s , +𝕄 , -ℤ , *ℤ
prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p;
    ⋅0 /// W.'!𝕄.!=. -| *𝕄 , *ℤ , -ℤ , 0⋅ , L0 v;
    ⋅0 -| W. , ax_s , +𝕄 , -ℤ , *ℤ h;
let/thm ⋅- <- `[ b ; x col ∈ ℤ ] ⟹ b ⋅ (- x) = - (b ⋅ x)` ◀ W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ
prf ⋅- -| Linv , ⋅ℤ+ , +ℤ- , ⋅0 , ⋅∈ℤ v; ⋅- -| W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ h;
let/thm +⋅ <- `[ a ; b ; c col ∈ ℤ ] ⟹ (a + b) ⋅ c = a ⋅ c + b ⋅ c` ◀ W. , ax_s , -ℤ , +ℤ , *ℤ
prf +⋅ -| ⋅ℤ+ , ⋅ℤ:C , +∈ℤ v; +⋅ -| W. , ax_s , -ℤ , +ℤ , *ℤ h;

section 順序と強い帰納法
txt 自然数の順序は \(\subset\)（小なりは \(\in\)）。\(y \neq 0\) なら \(x \in x + y\)（∈+）。
let/thm ⊂+ <- `[ x ; y col ∈ 𝕄 ] ⟹ x ⊂ x + y` ◀ W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ
prf ⊂+ -| ≤⊂ , ≤. , +ℤ' , 𝕄⊂ℤ , +∈𝕄 v; ⊂+ -| W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ h;
let/thm ∈+ <- `[ x ; y col ∈ 𝕄 ] and y {/}= 0 ⟹ x ∈ x + y` ◀ W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ
prf K <- `[ x ; y col ∈ 𝕄 ] and x + y = x ⟹ y = 0` -| +ℤ' , +ℤ- , 𝕄⊂ℤ v;
    ∈+ -| ⊂+ , K , <𝕄:r , ⊊.. , +∈𝕄 v;
    ∈+ -| W. , ax_s , +𝕄 , -ℤ , +ℤ , *ℤ h;
txt 強い帰納法：\(m\) より小さいすべての数で成り立てば \(m\) でも成り立つなら、すべての自然数で成り立つ。
prop/thm SINDC <- `[ ∀ m ∈ 𝕄 . ([ ∀ z ∈ m . z ∈_ D_ ] ⟹ m ∈_ D_) ] and n ∈ 𝕄 ⟹ n ∈_ D_` ◀ W. , ax_s
prf Lb <- `[ ∀ z ∈ 0 . z ∈_ D_ ]` -| 0.' {D_.-} p;
    Ls <- `[ ∀ m ∈ 𝕄 . ([ ∀ z ∈ m . z ∈_ D_ ] ⟹ m ∈_ D_) ] and m ∈ 𝕄 and [ ∀ z ∈ m . z ∈_ D_ ] ⟹ [ ∀ z ∈ m suc . z ∈_ D_ ]` -| suc.' {D_.-} p;
    SINDC -| INDC[D_:=`\{ cls m | [ ∀ z ∈ m . z ∈_ D_ ] \}`] , Lb , Ls , Lsucin , 𝕄1 {D_.-} v;
    SINDC -| W. , ax_s h;

articles4/0-z.book

`articles4/0-z.book`