book集

section 自然数

subsection 代数の言葉
word :2 :C :A
lower :2
lower :C
lower :A
word unit
lower unit
br
word :２ :Ｃ :Ａ :Ｄ
lower :２
lower :Ｃ
lower :Ａ
lower :Ｄ

subsection 自然数の記号、加法
txt 0以上の自然数\({\tt n}\)に対し
word \n
word 𝕄 ℕ
prop ℕ. <- `ℕ =_ \{ cls n ∈ 𝕄 | n {/}= 0 \}`
br
word + ^*+ *^+ ^^+
prop *^+.
prop ^*+.
prop ^^+.
br
txt 1以上の自然数\({\tt n}\)に対し
prop \n. <- `\n = (\n-1) + 1`
prop Peano1 <- `n ∈ 𝕄 ⟹ n + 1 ∈ ℕ`
prop Peano2 <- `[ m ; n col ∈ 𝕄 ] and m + 1 = n + 1 ⟹ m = n`
prop INDC <- `0 ∈_ D_ and [ ∀ m ∈ 𝕄 . (m ∈_ D_ ⟹ m + 1 ∈_ D_) ] ⟹ 𝕄 ⊂_ D_`
prop +𝕄 <- `\\{ And m ∈ 𝕄 ⟹ m + 0 = m \\ [ m ; n col ∈ 𝕄 ] ⟹ m + (n + 1) = (m + n) + 1 \\}`
props Ax+𝕄 <- Peano1 , Peano2 , INDC , +𝕄 , `0 ∈ 𝕄`
thm `\n ∈ 𝕄` ◀ W. , Ax+𝕄 at \n=1..10
prf goal -| \n. , `\n-1 ∈ 𝕄` , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` v; goal -| W. , Ax+𝕄 h;

subsection 加法の性質
let/thm +𝕄:2 <- `(𝕄 , [+]) :2` ◀ W. , Ax+𝕄
prf +𝕄:2 -| INDC[D_:=`\{ cls n | m + n ∈ 𝕄 \}`] , Peano1 , ℕ. , +𝕄 v; +𝕄:2 -| W. , Ax+𝕄 h;
thm `0 ∈_ unit (𝕄 , [+])` ◀ W. , Ax+𝕄
prf L0 <- `m ∈ 𝕄 ⟹ 0 + m = m` -| INDC[D_:=`\{ cls m | 0 + m = m \}`] , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` , +𝕄 v;
    goal /// W.'!=. -| L0 , +𝕄 , `0 ∈ 𝕄` p; goal -| W. , Ax+𝕄 h;
let/thm +𝕄:C <- `(𝕄 , [+]) :C` ◀ W. , Ax+𝕄
prf Ls <- `[ m ; n col ∈ 𝕄 ] ⟹ (m + 1) + n = (m + n) + 1` -| INDC[D_:=`\{ cls n | (m + 1) + n = (m + n) + 1 \}`] , Peano1 , ℕ. , +𝕄 v;
    +𝕄:C -| INDC[D_:=`\{ cls n | m + n = n + m \}`] , +𝕄 , `0 ∈_ unit (𝕄 , [+])` , Ls v; +𝕄:C -| W. , Ax+𝕄 h;
let/thm +𝕄:A <- `(𝕄 , [+]) :A` ◀ W. , Ax+𝕄
prf +𝕄:A -| INDC[D_:=`\{ cls k | (m + n) + k = m + (n + k) \}`] , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` , +𝕄 , +𝕄:2 v; +𝕄:A -| W. , Ax+𝕄 h;

!let/thm Lpred <- `k ∈ 𝕄 and k {/}= 0 ⟹ [ ∃ j ∈ 𝕄 . k = j + 1 ]` ◀ W. , Ax+𝕄
prf Lpred -| INDC[D_:=`\{ cls k | k = 0 or [ ∃ j ∈ 𝕄 . k = j + 1 ] \}`] v; Lpred -| W. , Ax+𝕄 h;
thm `ℕ = 𝕄 ^*+ 1` ◀ W. , Ax+𝕄
prf goal / =. / ^*+. -| ℕ. , Lpred , Peano1 , `0 ∈ 𝕄` p; goal -| W. , Ax+𝕄 h;

subsection 乗法
word ⋅
prop ⋅𝕄 <- `\\{ And m ∈ 𝕄 ⟹ m ⋅ 0 = 0 \\ [ m ; n col ∈ 𝕄 ] ⟹ m ⋅ (n + 1) = m ⋅ n + m \\}`
word* ↑
word_alias ↑* ↑ [tex:\uparrow]
prop ↑𝕄 <- `\\{ And m ↑ 0 = 1 \\ n ∈ 𝕄 ⟹ m ↑ { n + 1 } = m ↑ n ⋅ m \\}`

let/thm ⋅𝕄:2 <- `(𝕄 , [⋅]) :2` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ⋅𝕄:2 -| INDC[D_:=`\{ cls n | m ⋅ n ∈ 𝕄 \}`] , `0 ∈ 𝕄` , ⋅𝕄 , +𝕄:2 v; ⋅𝕄:2 -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ⋅𝕄:C <- `(𝕄 , [⋅]) :C` ◀ W. , Ax+𝕄 , ⋅𝕄
prf L0 <- `m ∈ 𝕄 ⟹ 0 ⋅ m = 0` -| INDC[D_:=`\{ cls m | 0 ⋅ m = 0 \}`] , `0 ∈ 𝕄` , ⋅𝕄 , +𝕄 v;
    Hs <- `[ x ; y ; z col ∈ 𝕄 ] ⟹ x + (y + (z + 1)) = (x + z) + (y + 1)` -| +𝕄 , +𝕄:A , +𝕄:C , +𝕄:2 v;
    Sa <- `[ m ; n col ∈ 𝕄 ] ⟹ (m ⋅ n + n) + (m + 1) = m ⋅ n + (n + (m + 1))` -| +𝕄:A , ⋅𝕄:2 , Peano1 , ℕ. v;
    Sb <- `[ m ; n col ∈ 𝕄 ] ⟹ (m + 1) ⋅ (n + 1) = (m + 1) ⋅ n + (m + 1) and m ⋅ (n + 1) = m ⋅ n + m` -| ⋅𝕄 , Peano1 , ℕ. v;
    Ss <- `[ m ; n col ∈ 𝕄 ] and (m + 1) ⋅ n = m ⋅ n + n ⟹ (m + 1) ⋅ (n + 1) = m ⋅ (n + 1) + (n + 1)` -| Sa , Sb , Hs , ⋅𝕄:2 v;
    Ls <- `[ m ; n col ∈ 𝕄 ] ⟹ (m + 1) ⋅ n = m ⋅ n + n` -| INDC[D_:=`\{ cls n | (m + 1) ⋅ n = m ⋅ n + n \}`] , Peano1 , ℕ. , `0 ∈ 𝕄` , ⋅𝕄 , +𝕄 , Ss v;
    ⋅𝕄:C -| INDC[D_:=`\{ cls n | m ⋅ n = n ⋅ m \}`] , ⋅𝕄 , L0 , Ls v; ⋅𝕄:C -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ⋅𝕄+ <- `(𝕄 , [+] , [⋅]) :Ｄ` ◀ W. , Ax+𝕄 , ⋅𝕄
prf Pa <- `[ m ; n ; k col ∈ 𝕄 ] ⟹ m ⋅ (n + (k + 1)) = m ⋅ (n + k) + m` -| +𝕄 , ⋅𝕄 , +𝕄:2 v;
    Pb <- `[ m ; n ; k col ∈ 𝕄 ] ⟹ m ⋅ n + m ⋅ (k + 1) = (m ⋅ n + m ⋅ k) + m` -| ⋅𝕄 , +𝕄:A , ⋅𝕄:2 v;
    Ps <- `[ m ; n ; k col ∈ 𝕄 ] and m ⋅ (n + k) = m ⋅ n + m ⋅ k ⟹ m ⋅ (n + (k + 1)) = m ⋅ n + m ⋅ (k + 1)` -| Pa , Pb v;
    ⋅𝕄+ -| INDC[D_:=`\{ cls k | m ⋅ (n + k) = m ⋅ n + m ⋅ k \}`] , +𝕄 , ⋅𝕄 , ⋅𝕄:2 , Ps v; ⋅𝕄+ -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ⋅𝕄:A <- `(𝕄 , [⋅]) :A` ◀ W. , Ax+𝕄 , ⋅𝕄
prf Aa <- `[ m ; n ; k col ∈ 𝕄 ] ⟹ (m ⋅ n) ⋅ (k + 1) = (m ⋅ n) ⋅ k + m ⋅ n and m ⋅ (n ⋅ (k + 1)) = m ⋅ (n ⋅ k) + m ⋅ n` -| ⋅𝕄 , ⋅𝕄+ , ⋅𝕄:2 , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` v;
    As <- `[ m ; n ; k col ∈ 𝕄 ] and (m ⋅ n) ⋅ k = m ⋅ (n ⋅ k) ⟹ (m ⋅ n) ⋅ (k + 1) = m ⋅ (n ⋅ (k + 1))` -| Aa v;
    ⋅𝕄:A -| INDC[D_:=`\{ cls k | (m ⋅ n) ⋅ k = m ⋅ (n ⋅ k) \}`] , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` , ⋅𝕄 , +𝕄 , +𝕄:2 , ⋅𝕄:2 , As v; ⋅𝕄:A -| W. , Ax+𝕄 , ⋅𝕄 h;

let/thm ⋅𝕄:1 <- `1 ∈_ unit (𝕄 , [⋅])` ◀ W. , Ax+𝕄 , ⋅𝕄
prf L1 <- `m ∈ 𝕄 ⟹ m ⋅ 1 = m and 1 ⋅ m = m` -| 1. , 2. , 3. , 4. , 5. , ⋅𝕄 , ⋅𝕄:C , +𝕄:C , +𝕄 , `0 ∈ 𝕄` , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` v;
    ⋅𝕄:1 /// W.'!1.!=. -| L1 , `1 ∈ 𝕄` p; ⋅𝕄:1 -| W. , Ax+𝕄 , ⋅𝕄 h;

subsection 三分律
let/thm Lz0 <- `[ x ; y col ∈ 𝕄 ] and x + y = 0 ⟹ x = 0 and y = 0` ◀ W. , Ax+𝕄
prf Lz0 -| Peano1 , ℕ. , +𝕄 , +𝕄:2 , Lpred v; Lz0 -| W. , Ax+𝕄 h;
let/thm Ltri <- `[ m ; n col ∈ 𝕄 ] ⟹ [ ∃ k ∈ 𝕄 . m = n + k ] or [ ∃ k ∈ 𝕄 . n = m + k ]` ◀ W. , Ax+𝕄
prf Ts <- `[ m ; n col ∈ 𝕄 ] and ([ ∃ k ∈ 𝕄 . m = n + k ] or [ ∃ k ∈ 𝕄 . n = m + k ]) ⟹ [ ∃ k ∈ 𝕄 . m = (n + 1) + k ] or [ ∃ k ∈ 𝕄 . (n + 1) = m + k ]` -| Lpred , +𝕄 , +𝕄:C , +𝕄:2 , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` v;
    Ltri -| INDC[D_:=`\{ cls n | [ ∃ k ∈ 𝕄 . m = n + k ] or [ ∃ k ∈ 𝕄 . n = m + k ] \}`] , Peano1 , Peano2 , ℕ. , `0 ∈ 𝕄` , +𝕄:C , +𝕄 , `0 ∈ 𝕄` , Ts v; Ltri -| W. , Ax+𝕄 h;

newpage
section 整数
word -
word −
prop −. <- `m − n = m + (- n)`
br
word ℤ
prop ℤ. <- `ℤ =_ \{ cls z | z ∈ 𝕄 or [ ∃ n ∈ ℕ . z = - n ] \}`
prop -ℤ <- `\\{ And - 0 = 0 \\ n ∈ ℕ ⟹ - n {/}∈ 𝕄 \\ [ m ; n col ∈ ℕ ] and - m = - n ⟹ m = n \\ n ∈ 𝕄 ⟹ - (- n) = n \\}`
prop +ℤ <- `@+𝕄 and \\{ And [ n ; k col ∈ 𝕄 ] ⟹ (n + k) − n = k \\ [ m ; k col ∈ 𝕄 ] ⟹ m − (m + k) = - k \\ m ∈ 𝕄 and n ∈ ℤ ⟹ (- m) + n = - (m − n) \\}`
let/thm +ℤ' <- `@+𝕄 and \\{ And [ m ; n ; k col ∈ 𝕄 ] and m = n + k ⟹ m + (- n) = k and (- n) + m = k \\ [ m ; n ; k col ∈ 𝕄 ] and n = m + k ⟹ m + (- n) = - k and (- n) + m = - k \\ [ m ; n col ∈ 𝕄 ] ⟹ (- m) + (- n) = - (m + n) \\}` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf Q1a <- `[ n ; k col ∈ 𝕄 ] ⟹ (n + k) + (- n) = k` -| +ℤ , W. v;
    Q1b <- `[ n ; k col ∈ 𝕄 ] ⟹ (- n) + (n + k) = k` -| +ℤ , -ℤ , +𝕄:2 , ℤ. v;
    Q1 <- `[ n ; k col ∈ 𝕄 ] ⟹ (n + k) + (- n) = k and (- n) + (n + k) = k` -| Q1a , Q1b v;
    Q2a <- `[ m ; k col ∈ 𝕄 ] ⟹ m + (- (m + k)) = - k` -| +ℤ , W. v;
    Q2b <- `[ m ; k col ∈ 𝕄 ] ⟹ (- (m + k)) + m = - k` -| +ℤ , +𝕄:2 , ℤ. v;
    Q2 <- `[ m ; k col ∈ 𝕄 ] ⟹ m + (- (m + k)) = - k and (- (m + k)) + m = - k` -| Q2a , Q2b v;
    Q3 <- `[ m ; n col ∈ 𝕄 ] ⟹ (- m) + (- n) = - (m + n)` -| +ℤ , W. , `0 ∈ 𝕄` , +𝕄:2 v;
    +ℤ' -| Q1 , Q2 , Q3 , +ℤ v; +ℤ' -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm Lcs <- `z ∈ ℤ ⟹ z ∈ 𝕄 or [ ∃ q ∈ 𝕄 . z = - q ]` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf Lcs -| ℤ. , ℕ. v; Lcs -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm +∈ℤ <- `(ℤ , [+]) :2` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf C1 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ ℤ` -| +𝕄:2 , ℤ. p;
    C2 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + (- n) ∈ ℤ and (- n) + m ∈ ℤ` -| ℤ. , ℕ. , Ltri , +ℤ' v;
    C3 <- `[ m ; n col ∈ 𝕄 ] ⟹ (- m) + (- n) ∈ ℤ` -| ℤ. , ℕ. , +ℤ' , +𝕄:2 v;
    +∈ℤ -| C1 , C2 , C3 , Lcs v; +∈ℤ -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm +ℤ:C <- `(ℤ , [+]) :C` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf +ℤ:C -| +𝕄:C , Ltri , +ℤ' , Lcs v; +ℤ:C -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm +ℤ- <- `m ∈ ℤ ⟹ - m ∈ ℤ and m + (- m) = 0` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf +ℤ- -| ℤ. , -ℤ , ℕ. , +ℤ' , `0 ∈ 𝕄` v; +ℤ- -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm Lrep <- `m ∈ ℤ ⟹ [ ∃ p ; q \, p ∈ 𝕄 and q ∈ 𝕄 and m = p + (- q) ]` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf Lrep -| Lcs , +ℤ' , +𝕄:C , `0 ∈ 𝕄` v; Lrep -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm L+pq <- `[ p ; q ; r ; s col ∈ 𝕄 ] ⟹ (p + (- q)) + (r + (- s)) = (p + r) + (- (q + s))` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf T1 <- `[ x ; b ; k col ∈ 𝕄 ] ⟹ (x + (b + k)) + (- (x + b)) = (b + k) + (- b)` -| +𝕄:A , +𝕄:2 , +ℤ' v;
    T2 <- `[ x ; a ; k col ∈ 𝕄 ] ⟹ (x + a) + (- (x + (a + k))) = a + (- (a + k))` -| +𝕄:A , +𝕄:2 , +ℤ' v;
    Ltr <- `[ x ; a ; b col ∈ 𝕄 ] ⟹ (x + a) + (- (x + b)) = a + (- b)` -| T1 , T2 , Ltri v;
    M1 <- `[ a ; b ; c ; d col ∈ 𝕄 ] ⟹ (a + b) + (c + d) = (a + c) + (b + d)` -| +𝕄:A , +𝕄:C , +𝕄:2 v;
    M2 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ (a + b) + c = (a + c) + b` -| +𝕄:A , +𝕄:C v;
    A1 <- `[ p ; q ; r ; s ; i ; j col ∈ 𝕄 ] and p = q + i and r = s + j ⟹ (p + (- q)) + (r + (- s)) = (p + r) + (- (q + s))` -| M1 , +ℤ' , +𝕄:2 v;
    A2 <- `[ p ; q ; r ; s ; i ; j col ∈ 𝕄 ] and p = q + i and s = r + j ⟹ (p + (- q)) + (r + (- s)) = (p + r) + (- (q + s))` -| M2 , +𝕄:A , Ltr , +ℤ' , +𝕄:2 p;
    Cm <- `[ i ; j col ∈ 𝕄 ] ⟹ (- i) + j = j + (- i)` -| +ℤ' , Ltri v;
    A3 <- `[ p ; q ; r ; s ; i ; j col ∈ 𝕄 ] and q = p + i and r = s + j ⟹ (p + (- q)) + (r + (- s)) = (p + r) + (- (q + s))` -| Cm , M2 , +𝕄:A , Ltr , +ℤ' , +𝕄:2 p;
    A4 <- `[ p ; q ; r ; s ; i ; j col ∈ 𝕄 ] and q = p + i and s = r + j ⟹ (p + (- q)) + (r + (- s)) = (p + r) + (- (q + s))` -| M1 , +ℤ' , +𝕄:2 v;
    L+pq -| A1 , A2 , A3 , A4 , Ltri v; L+pq -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm +ℤ:A <- `(ℤ , [+]) :A` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf AS <- `[ p ; q ; r ; s ; t ; u col ∈ 𝕄 ] ⟹ (p + (- q)) + ((r + (- s)) + (t + (- u))) = ((p + (- q)) + (r + (- s))) + (t + (- u))` -| L+pq , +𝕄:A , +𝕄:2 v;
    +ℤ:A -| AS , Lrep v; +ℤ:A -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm L+0ℤ <- `x ∈ ℤ ⟹ x + 0 = x and 0 + x = x` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf L+0ℤ -| Lcs , +ℤ' , +𝕄:C , `0 ∈ 𝕄` v; L+0ℤ -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
prop ⋅ℤ <- `@⋅𝕄 and \\{ And [ m ; n col ∈ 𝕄 ] ⟹ [ chain m ⋅ (- n) = - (m ⋅ n) = (- m) ⋅ n ] \\ [ m ; n col ∈ 𝕄 ] ⟹ (- m) ⋅ (- n) = m ⋅ n \\}`
let/thm ⋅∈ℤ <- `(ℤ , [⋅]) :2` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf C1 <- `[ m ; n col ∈ 𝕄 ] ⟹ m ⋅ n ∈ ℤ` -| ⋅𝕄:2 , ℤ. p;
    C2 <- `[ m ; n col ∈ 𝕄 ] ⟹ m ⋅ (- n) ∈ ℤ and (- n) ⋅ m ∈ ℤ` -| ℤ. , -ℤ , ℕ. , ⋅𝕄:2 , ⋅ℤ v;
    C3 <- `[ m ; n col ∈ 𝕄 ] ⟹ (- m) ⋅ (- n) ∈ ℤ` -| ⋅𝕄:2 , ⋅ℤ , ℤ. p;
    ⋅∈ℤ -| C1 , C2 , C3 , Lcs v; ⋅∈ℤ -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm ⋅ℤ:C <- `(ℤ , [⋅]) :C` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf ⋅ℤ:C -| ⋅𝕄:C , ⋅ℤ , Lcs v; ⋅ℤ:C -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm Lz⋅ <- `x ∈ ℤ ⟹ 0 ⋅ x = 0 and x ⋅ 0 = 0` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf Lz⋅ -| ⋅ℤ , -ℤ , ⋅𝕄:C , Lcs , `0 ∈ 𝕄` v; Lz⋅ -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm ⋅ℤ:A <- `(ℤ , [⋅]) :A` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf A0 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ a ⋅ (b ⋅ c) = (a ⋅ b) ⋅ c` -| ⋅𝕄:A p;
    A1 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ a ⋅ (b ⋅ (- c)) = (a ⋅ b) ⋅ (- c)` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A2 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ a ⋅ ((- b) ⋅ c) = (a ⋅ (- b)) ⋅ c` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A3 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ a ⋅ ((- b) ⋅ (- c)) = (a ⋅ (- b)) ⋅ (- c)` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A4 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ (- a) ⋅ (b ⋅ c) = ((- a) ⋅ b) ⋅ c` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A5 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ (- a) ⋅ (b ⋅ (- c)) = ((- a) ⋅ b) ⋅ (- c)` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A6 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ (- a) ⋅ ((- b) ⋅ c) = ((- a) ⋅ (- b)) ⋅ c` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    A7 <- `[ a ; b ; c col ∈ 𝕄 ] ⟹ (- a) ⋅ ((- b) ⋅ (- c)) = ((- a) ⋅ (- b)) ⋅ (- c)` -| ⋅𝕄:A , ⋅𝕄:2 , ⋅ℤ p;
    ⋅ℤ:A -| A0 , A1 , A2 , A3 , A4 , A5 , A6 , A7 , Lcs v; ⋅ℤ:A -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm Linv <- `[ u ; v col ∈ ℤ ] and u + v = 0 ⟹ v = - u` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf Linv -| +ℤ:A , +ℤ- , L+0ℤ v; Linv -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm L-+ <- `[ y ; z col ∈ ℤ ] ⟹ - (y + z) = (- y) + (- z)` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄
prf L-+ -| +ℤ:A , +ℤ:C , +ℤ- , +∈ℤ , L+0ℤ v; L-+ -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 h;
let/thm ⋅ℤ+ <- `(ℤ , [+] , [⋅]) :Ｄ` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf D1 <- `[ a ; q ; k col ∈ 𝕄 ] ⟹ a ⋅ ((q + k) + (- q)) = a ⋅ (q + k) + (- (a ⋅ q))` -| ⋅𝕄+ , ⋅𝕄:2 , +𝕄:2 , +ℤ' v;
    D2 <- `[ a ; p ; k col ∈ 𝕄 ] ⟹ a ⋅ (p + (- (p + k))) = a ⋅ p + (- (a ⋅ (p + k)))` -| ⋅𝕄+ , ⋅𝕄:2 , +𝕄:2 , +ℤ' , ⋅ℤ v;
    D <- `[ a ; p ; q col ∈ 𝕄 ] ⟹ a ⋅ (p + (- q)) = a ⋅ p + (- (a ⋅ q))` -| D1 , D2 , Ltri v;
    Nm1 <- `a ∈ 𝕄 and x ∈ ℤ ⟹ (- a) ⋅ x = - (a ⋅ x)` -| ⋅ℤ , -ℤ , ⋅𝕄:2 , Lcs v;
    P1 <- `[ a ; p ; q ; r ; s col ∈ 𝕄 ] ⟹ a ⋅ ((p + (- q)) + (r + (- s))) = a ⋅ (p + (- q)) + a ⋅ (r + (- s))` -| L+pq , D , ⋅𝕄+ , ⋅𝕄:2 , +𝕄:2 v;
    P <- `a ∈ 𝕄 and [ n ; k col ∈ ℤ ] ⟹ a ⋅ (n + k) = a ⋅ n + a ⋅ k` -| Lrep , P1 v;
    Nn <- `a ∈ 𝕄 and [ n ; k col ∈ ℤ ] ⟹ (- a) ⋅ (n + k) = (- a) ⋅ n + (- a) ⋅ k` -| Nm1 , L-+ , P , ⋅∈ℤ , +∈ℤ , ℤ. v;
    ⋅ℤ+ -| Lcs , P , Nn v; ⋅ℤ+ -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm L1ℤ <- `1 ∈ ℤ and [ ∀ x ∈ ℤ . (x ⋅ 1 = x and 1 ⋅ x = x) ]` ◀ W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄
prf L1ℤ -| ⋅𝕄:2 , `1 ∈_ unit (𝕄 , [⋅])` , `1 ∈ 𝕄` , `2 ∈ 𝕄` , `3 ∈ 𝕄` , `4 ∈ 𝕄` , `5 ∈ 𝕄` , ℤ. , Lcs , ⋅ℤ , ⋅ℤ:C , ⋅∈ℤ v; L1ℤ -| W. , ℤ. , -ℤ , +ℤ , ⋅ℤ , Ax+𝕄 , ⋅𝕄 h;

section 順序
word ≤
word <
prop ≤. <- `[ m ; n col ∈ ℤ ] ⟹ (m ≤ n ⟺ (- m) + n ∈ 𝕄)`
prop <. <- `m < n ⟺ m ≤ n and m {/}= n`
!prop/thm ≤.' <- `[ m ; n col ∈ 𝕄 ] ⟹ (m ≤ n ⟺ [ ∃ k ∈ 𝕄 . m + k = n ])` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf ≤.' / ≤. -| +ℤ' , +ℤ:A , +ℤ- , L+0ℤ , ℤ. , +∈ℤ , -ℤ , ℕ. , `0 ∈ 𝕄` , +ℤ:C v; ≤.' -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L≤R <- `n ∈ 𝕄 ⟹ n ≤ n` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L≤R -| ≤.' , +𝕄 , `0 ∈ 𝕄` p; L≤R -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L≤T <- `[ x ; y ; z col ∈ 𝕄 ] and x ≤ y and y ≤ z ⟹ x ≤ z` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L≤T -| ≤.' , +𝕄:A , +𝕄:2 v; L≤T -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm Lanti <- `[ x ; y col ∈ 𝕄 ] and x ≤ y and y ≤ x ⟹ x = y` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf Mz <- `x ∈ 𝕄 ⟹ x ∈ ℤ` -| ℤ. p;
    Lanti -| ≤.' , +ℤ:A , +ℤ:C , +ℤ- , L+0ℤ , Mz , Lz0 v; Lanti -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm Ltot <- `[ m ; n col ∈ 𝕄 ] ⟹ m ≤ n or n < m` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf Ltot / <. -| ≤.' , Ltri v; Ltot -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L<A <- `[ x ; y col ∈ 𝕄 ] and x < y ⟹ ¬ y < x and x ≤ y` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L<A / <. -| Lanti v; L<A -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L<+k <- `[ k ; d col ∈ 𝕄 ] and k {/}= 0 ⟹ d < d + k` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L<+k / <. -| ≤.' , +ℤ:A , +ℤ- , L+0ℤ , ℤ. , +𝕄:2 v; L<+k -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L<0 <- `z ∈ 𝕄 ⟹ ¬ z < 0` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L<0 / <. -| ≤.' , Lz0 , `0 ∈ 𝕄` v; L<0 -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
let/thm L≤< <- `[ a ; b col ∈ 𝕄 ] and a ≤ b ⟹ a = b or a < b` ◀ W. , Ax+𝕄
prf L≤< / <. -| O p; L≤< -| W. , Ax+𝕄 h;
let/thm L<s≤ <- `[ m ; n col ∈ 𝕄 ] and m < (n + 1) ⟹ m ≤ n` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄
prf L<s≤ / <. -| ≤.' , Lpred , +𝕄 , +𝕄:2 , Peano1 , Peano2 , ℕ. v; L<s≤ -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 , ↑𝕄 h;
prop/thm SIND <- `[ ∀ n ∈ 𝕄 . ([ ∀ z ∈ 𝕄 . (z < n ⟹ z ∈_ E_) ] ⟹ n ∈_ E_) ] and n ∈ 𝕄 ⟹ n ∈_ E_` ◀ W. , ℤ. , -ℤ , +ℤ , Peano1 , Peano2 , ℕ. , INDC , +𝕄 , ⋅𝕄 , ↑𝕄 , `0 ∈ 𝕄`
prf Lb <- `[ ∀ z ∈ 𝕄 . (z < 0 ⟹ z ∈_ E_) ]` --| L<0 v;
    Ls <- `[ ∀ n ∈ 𝕄 . ([ ∀ z ∈ 𝕄 . (z < n ⟹ z ∈_ E_) ] ⟹ n ∈_ E_) ] and b ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < b ⟹ z ∈_ E_) ] ⟹ [ ∀ z ∈ 𝕄 . (z < (b + 1) ⟹ z ∈_ E_) ]` --| L<s≤ , L≤< v;
    SIND --| INDC[D_:=`\{ cls b | [ ∀ z ∈ 𝕄 . (z < b ⟹ z ∈_ E_) ] \}`] , Lb , Ls v;
    SIND -| W. , ℤ. , -ℤ , +ℤ , Peano1 , Peano2 , ℕ. , INDC , +𝕄 , ⋅𝕄 , ↑𝕄 , `0 ∈ 𝕄` h[lift];

section 約数
word ∣
prop ∣. <- `d ∣ n ⟺ [ ∃ k ∈ 𝕄 . n = d ⋅ k ]`
let/thm ∣R <- `n ∈ 𝕄 ⟹ n ∣ n` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ∣R / ∣. -| `1 ∈_ unit (𝕄 , [⋅])` v; ∣R -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ∣⋅ <- `[ p ; m col ∈ 𝕄 ] ⟹ p ∣ p ⋅ m` ◀ W. , Ax+𝕄
prf ∣⋅ / ∣. -| O p; ∣⋅ -| W. , Ax+𝕄 h;
let/thm ∣⋅R <- `[ n ; m col ∈ 𝕄 ] ⟹ m ∣ n ⋅ m` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ∣⋅R / ∣. -| ⋅𝕄:C p; ∣⋅R -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ∣T <- `[ p ; d ; n col ∈ 𝕄 ] and p ∣ d and d ∣ n ⟹ p ∣ n` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ∣T / ∣. -| ⋅𝕄:A , ⋅𝕄:2 v; ∣T -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ∣M <- `[ d ; n ; m col ∈ 𝕄 ] and d ∣ n ⟹ d ∣ n ⋅ m` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ∣M / ∣. -| ⋅𝕄:A , ⋅𝕄:2 v; ∣M -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm ∣+ <- `[ d ; a ; b col ∈ 𝕄 ] and d ∣ a and d ∣ b ⟹ d ∣ a + b` ◀ W. , Ax+𝕄 , ⋅𝕄
prf ∣+ / ∣. -| ⋅𝕄+ , +𝕄:2 v; ∣+ -| W. , Ax+𝕄 , ⋅𝕄 h;
let/thm LDs <- `[ d ; x ; p ; q col ∈ 𝕄 ] and d ⋅ p = x + d ⋅ q ⟹ d ∣ x` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄
prf D2 <- `[ d ; x ; p ; q ; c col ∈ 𝕄 ] and d ⋅ p = x + d ⋅ q and p = q + c ⟹ x = d ⋅ c` -| ⋅𝕄+ , +ℤ:A , +ℤ- , L+0ℤ , ℤ. , +𝕄:C , ⋅𝕄:2 v;
    D3a <- `[ d ; x ; p ; q ; c col ∈ 𝕄 ] and q = p + c ⟹ d ⋅ q = d ⋅ p + d ⋅ c` -| ⋅𝕄+ v;
    D3c <- `[ x ; y ; z col ∈ 𝕄 ] ⟹ x + (y + z) = (x + z) + y` -| +𝕄:A , +𝕄:C v;
    D3z <- `m ∈ 𝕄 ⟹ 0 + m = m` -| +𝕄:C , +𝕄 , `0 ∈ 𝕄` v;
    D3r <- `[ x ; a ; b col ∈ 𝕄 ] and a = x + (a + b) ⟹ (x + b) + a = 0 + a` -| D3c , D3z v;
    D3d <- `[ x ; a ; b col ∈ 𝕄 ] and a = x + (a + b) ⟹ x + b = 0` -| +ℤ:A , +ℤ- , L+0ℤ , ℤ. , D3r , +𝕄:2 v;
    D3 <- `[ d ; x ; p ; q ; c col ∈ 𝕄 ] and d ⋅ p = x + d ⋅ q and q = p + c ⟹ x = 0` -| D3a , D3d , Lz0 , ⋅𝕄:2 v;
    LDs / ∣. -| Ltri , D2 , D3 , ⋅𝕄 v;
    LDs -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm ∣sub <- `[ d ; u ; v col ∈ 𝕄 ] and d ∣ u + v and d ∣ u ⟹ d ∣ v` ◀ W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄
prf E1 <- `[ d ; u ; v ; p ; q col ∈ 𝕄 ] and u + v = d ⋅ p and u = d ⋅ q ⟹ d ⋅ p = v + d ⋅ q` -| +𝕄:C v;
    E2 <- `[ d ; u ; v col ∈ 𝕄 ] and d ∣ u + v and d ∣ u ⟹ [ ∃ p ; q ∈ 𝕄 . d ⋅ p = v + d ⋅ q ]` / ∣. -| E1 v;
    ∣sub -| E2 , LDs v; ∣sub -| W. , ℤ. , -ℤ , +ℤ , Ax+𝕄 , ⋅𝕄 h;
let/thm Rdist <- `[ x ; y ; z col ∈ 𝕄 ] ⟹ (x + y) ⋅ z = x ⋅ z + y ⋅ z` ◀ W. , Ax+𝕄 , ⋅𝕄
prf Rdist -| ⋅𝕄+ , ⋅𝕄:C , +𝕄:2 v; Rdist -| W. , Ax+𝕄 , ⋅𝕄 h;

articles2/zztrial_2209638_bfd5a5.book

`articles2/zztrial_2209638_bfd5a5.book`