6.8 積

word(s,s) … \(\mathrm{\Pi}\)
積 \(\Pi f\) は、空の写像で 1、1点 \(\langle x, y\rangle\) を足すと \(y\) が掛けられる（AxΠ）。和 AxΣ の積版。
AxΠ … \(\begin{cases} \mathrm{\Pi} \emptyset = 1 \\ X \stackrel{\#}= k \in \mathbb{M} , f \in X \to V , x \notin X \Longrightarrow \mathrm{\Pi} ( f \cup \{ \langle x , y \rangle \} ) = \mathrm{\Pi} f \cdot y \end{cases}\)

7 整数

7.1 整数

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}\)
𝕄⊂ℤ … \(x \in \mathbb{M} \Longrightarrow x \in \mathbb{Z}\) \(\blacktriangleleft\) \(\mathbb{W}.\)

7.2 整数の加法

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𝕄 ，ax_s ，-ℤ ，+ℤ
\(0 \in \text{unit} ( \mathbb{Z} , [+] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ
\(( \mathbb{Z} , [+] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ

7.3 整数の乗法

⋅ℤ … ⋅𝕄 \(, \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𝕄 ，ax_s ，+𝕄 ，-ℤ ，⋅ℤ
↑∈ℤ … \(m \in \mathbb{Z} , n \in \mathbb{M} \Longrightarrow m ^ n \in \mathbb{Z}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，-ℤ ，⋅ℤ ，↑𝕄
\(1 \in \text{unit} ( \mathbb{Z} , [\cdot] )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，-ℤ ，⋅ℤ
\(( \mathbb{Z} , [\cdot] ) :\underline{2}\mathsf{C}\mathsf{A}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，-ℤ ，⋅ℤ
ℤ は可換半環（csemiring）。
\(( \mathbb{Z} , [+] , [\cdot] ) \text{csemiring}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ
積 \(\Pi f\) は、値が可換半環 \(S\) の元なら \(S\) の元（個数 \(k\) についての帰納法）。
L⨉S … \(( S , [+] , [\cdot] ) \text{csemiring} , X \stackrel{\#}= k \in \mathbb{M} , f \in X \to S \Longrightarrow \mathrm{\Pi} f \in S\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΠ
積は添字の置き換えで変わらない：全単射 \(u : X \to Y\) と \(g : Y \to S\) について \(\Pi (g \circ u) = \Pi g\)（個数についての帰納法）。
L⨉perm … \(( S , [+] , [\cdot] ) \text{csemiring} , X \stackrel{\#}= k \in \mathbb{M} , u \in X \stackrel{\rm IS}\to Y , g \in Y \to S \Longrightarrow \mathrm{\Pi} ( g \circ u ) = \mathrm{\Pi} g\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，AxΠ

7.4 整数の順序

整数の順序は、差が自然数になること。
≤ℤ … \(m , n \in \mathbb{Z} \Longrightarrow ( m \le n \Longleftrightarrow n + ( - m ) \in \mathbb{M} )\)
≤ℤ:R … \(m \in \mathbb{Z} \Longrightarrow m \le m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ
≤ℤ:T … \(m , n , k \in \mathbb{Z} , m \le n , n \le k \Longrightarrow m \le k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ
≤ℤ:A … \(m , n \in \mathbb{Z} , m \le n , n \le m \Longrightarrow m = n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ
≤ℤ:tot … \(m , n \in \mathbb{Z} \Longrightarrow m \le n \mathbin{\rm o\!r} n \le m\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ
≤ℤ+ … \(m , n , k \in \mathbb{Z} , m \le n \Longrightarrow m + k \le n + k\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ
⋅- … \(b , x \in \mathbb{Z} \Longrightarrow b \cdot ( - x ) = - ( b \cdot x )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，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𝕄 ，ax_s ，-ℤ ，+ℤ ，⋅ℤ ，≤ℤ