1 整数

1.1 1以上の自然数

\(\mathbb{N} = \{ n \in \mathbb{M} \mid n \neq 0 \}\)。
word(,s) … \(\mathbb{N}\)
ℕ. … \(\mathbb{N} = \mathbb{M} \mathop\setminus 1\)

1.2 整数

負の数は \(-n\)（\(n \in \mathbb{N}\)）で表す。\(\mathbb{Z} = \mathbb{M} \cup \{ -n \mid n \in \mathbb{N} \}\)。
word(s,s) … \(-\)  \(-\)
^-. … \([-] \stackrel{\star}{=} \; [\stackrel{\text{^}}{-}]\)
word(,s) … \(\mathbb{Z}\)
ℤ. … \(\mathbb{Z} = \mathbb{M} \cup ( - \mathbb{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}\)

1.3 整数の加法

\(m - n = m + (-n)\)。加法の性質は自然数のものがそのまま使える。
word(ss,s) … \(-\)
−. … \(m - n = m + ( - n )\)
+ℤ … +𝕄 \(, \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}\)
+∈ℤ … \(m , n \in \mathbb{Z} \Longrightarrow m + n \in \mathbb{Z}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ
\(0 \in \text{unit} ( \mathbb{Z} , [+] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ
\(( \mathbb{Z} , [+] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ

1.4 整数の乗法

\(m \cdot (-n) = -(m \cdot n)\)、\((-m) \cdot (-n) = m \cdot n\)。
*ℤ … *𝕄 \(, \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}\)
⋅∈ℤ … \(m , n \in \mathbb{Z} \Longrightarrow m \cdot n \in \mathbb{Z}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄 ，-ℤ ，*ℤ
\(1 \in \text{unit} ( \mathbb{Z} , [\cdot] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄 ，-ℤ ，*ℤ
\(( \mathbb{Z} , [\cdot] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，+𝕄 ，-ℤ ，*ℤ

1.5 整数の順序

\(m \le n \iff n - m \in \mathbb{M}\)。
word(ss,p) … \(\le\)  \(<\)
≤. … \(m , n \in \mathbb{Z} \Longrightarrow ( m \le n \Longleftrightarrow n + ( - m ) \in \mathbb{M} )\)
<. … \(m < n \Longleftrightarrow m \le n , m \neq n\)
≤:R … \(m \in \mathbb{Z} \Longrightarrow m \le m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤:T … \(m , n , k \in \mathbb{Z} , m \le n , n \le k \Longrightarrow m \le k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤:A … \(m , n \in \mathbb{Z} , m \le n , n \le m \Longrightarrow m = n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤:tot … \(m , n \in \mathbb{Z} \Longrightarrow m \le n \mathbin{\rm o\!r} n \le m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤+ … \(m , n , k \in \mathbb{Z} , m \le n \Longrightarrow m + k \le n + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤⋅ … \(m , n , k \in \mathbb{Z} , 0 \le k , m \le n \Longrightarrow m \cdot k \le n \cdot k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ
≤⊂ … \(m , n \in \mathbb{M} \Longrightarrow ( m \le n \Longleftrightarrow m \subset n )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ax_s ，-ℤ ，+ℤ ，*ℤ