2 整数

word(s,s) … \(-\)
word(ss,s) … \(-\)
−. … \(m - n = m + ( - n )\)

word(,s) … \(\mathbb{Z}\)
ℤ. … \(\mathbb{Z} = \{ z \mid z \in \mathbb{M} \mathbin{\rm o\!r} \exists n \in \mathbb{N} . z = - n \}\)
-ℤ … \(\begin{cases} - 0 = 0 \\ n \in \mathbb{N} \Longrightarrow - n \notin \mathbb{M} \\ m , n \in \mathbb{N} , - m = - n \Longrightarrow m = n \\ n \in \mathbb{M} \Longrightarrow - ( - n ) = n \end{cases}\)
+ℤ … +𝕄 \(, \begin{cases} n , k \in \mathbb{M} \Longrightarrow ( n + k ) - n = k \\ m , k \in \mathbb{M} \Longrightarrow m - ( m + k ) = - k \\ m \in \mathbb{M} , n \in \mathbb{Z} \Longrightarrow ( - m ) + n = - ( m - n ) \end{cases}\)
+ℤ' … +𝕄 \(, \begin{cases} m , n , k \in \mathbb{M} , m = n + k \Longrightarrow m + ( - n ) = k , ( - n ) + m = k \\ m , n , k \in \mathbb{M} , n = m + k \Longrightarrow m + ( - n ) = - k , ( - n ) + m = - k \\ m , n \in \mathbb{M} \Longrightarrow ( - m ) + ( - n ) = - ( m + n ) \end{cases}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
Lcs … \(z \in \mathbb{Z} \Longrightarrow z \in \mathbb{M} \mathbin{\rm o\!r} \exists q \in \mathbb{M} . z = - q\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
+∈ℤ … \(( \mathbb{Z} , [+] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
+ℤ:C … \(( \mathbb{Z} , [+] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
+ℤ- … \(m \in \mathbb{Z} \Longrightarrow - m \in \mathbb{Z} , m + ( - m ) = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
Lrep … \(m \in \mathbb{Z} \Longrightarrow \exists p , q \, p \in \mathbb{M} , q \in \mathbb{M} , m = p + ( - q )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
L+pq … \(p , q , r , s \in \mathbb{M} \Longrightarrow ( p + ( - q ) ) + ( r + ( - s ) ) = ( p + r ) + ( - ( q + s ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
+ℤ:A … \(( \mathbb{Z} , [+] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
L+0ℤ … \(x \in \mathbb{Z} \Longrightarrow x + 0 = x , 0 + x = x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
⋅ℤ … ⋅𝕄 \(, \begin{cases} m , n \in \mathbb{M} \Longrightarrow m \cdot ( - n ) = - ( m \cdot n ) = ( - m ) \cdot n \\ m , n \in \mathbb{M} \Longrightarrow ( - m ) \cdot ( - n ) = m \cdot n \end{cases}\)
⋅∈ℤ … \(( \mathbb{Z} , [\cdot] ) :\underline{2}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄
⋅ℤ:C … \(( \mathbb{Z} , [\cdot] ) :\mathsf{C}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄
Lz⋅ … \(x \in \mathbb{Z} \Longrightarrow 0 \cdot x = 0 , x \cdot 0 = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄
⋅ℤ:A … \(( \mathbb{Z} , [\cdot] ) :\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄
Linv … \(u , v \in \mathbb{Z} , u + v = 0 \Longrightarrow v = - u\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
L-+ … \(y , z \in \mathbb{Z} \Longrightarrow - ( y + z ) = ( - y ) + ( - z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄
⋅ℤ+ … \(( \mathbb{Z} , [+] , [\cdot] ) :\mathsf{D}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄
L1ℤ … \(1 \in \mathbb{Z} , \forall x \in \mathbb{Z} . ( x \cdot 1 = x , 1 \cdot x = x )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Ax+𝕄 ，⋅𝕄

3 順序

word(ss,p) … \(\le\)
word(ss,p) … \(<\)
≤. … \(m , n \in \mathbb{Z} \Longrightarrow ( m \le n \Longleftrightarrow ( - m ) + n \in \mathbb{M} )\)
<. … \(m < n \Longleftrightarrow m \le n , m \neq n\)
L≤R … \(n \in \mathbb{M} \Longrightarrow n \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
L≤T … \(x , y , z \in \mathbb{M} , x \le y , y \le z \Longrightarrow x \le z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
Lanti … \(x , y \in \mathbb{M} , x \le y , y \le x \Longrightarrow x = y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
Ltot … \(m , n \in \mathbb{M} \Longrightarrow m \le n \mathbin{\rm o\!r} n < m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
L<A … \(x , y \in \mathbb{M} , x < y \Longrightarrow \neg y < x , x \le y\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
L<+k … \(k , d \in \mathbb{M} , k \neq 0 \Longrightarrow d < d + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
L<0 … \(z \in \mathbb{M} \Longrightarrow \neg z < 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
L≤< … \(a , b \in \mathbb{M} , a \le b \Longrightarrow a = b \mathbin{\rm o\!r} a < b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
L<s≤ … \(m , n \in \mathbb{M} , m < ( n + 1 ) \Longrightarrow m \le n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄 ，↑𝕄
SIND … \(\forall n \in \mathbb{M} . ( \forall z \in \mathbb{M} . ( z < n \Longrightarrow z \in E ) \Longrightarrow n \in E ) , n \in \mathbb{M} \Longrightarrow n \in E\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，\(0 \in \mathbb{M}\)

4 約数

word(ss,p) … \(\mid\)
∣. … \(d \mid n \Longleftrightarrow \exists k \in \mathbb{M} . n = d \cdot k\)
∣R … \(n \in \mathbb{M} \Longrightarrow n \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
∣⋅ … \(p , m \in \mathbb{M} \Longrightarrow p \mid p \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄
∣⋅R … \(n , m \in \mathbb{M} \Longrightarrow m \mid n \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
∣T … \(p , d , n \in \mathbb{M} , p \mid d , d \mid n \Longrightarrow p \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
∣M … \(d , n , m \in \mathbb{M} , d \mid n \Longrightarrow d \mid n \cdot m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
∣+ … \(d , a , b \in \mathbb{M} , d \mid a , d \mid b \Longrightarrow d \mid a + b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄
LDs … \(d , x , p , q \in \mathbb{M} , d \cdot p = x + d \cdot q \Longrightarrow d \mid x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄
∣sub … \(d , u , v \in \mathbb{M} , d \mid u + v , d \mid u \Longrightarrow d \mid v\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Ax+𝕄 ，⋅𝕄
Rdist … \(x , y , z \in \mathbb{M} \Longrightarrow ( x + y ) \cdot z = x \cdot z + y \cdot z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax+𝕄 ，⋅𝕄