1 合同

自然数の範囲で、\(x \equiv y \pmod m\) を「\(x + ms = y + mt\) となる自然数 \(s, t\) がある」と書きます。
Cr … \(x , m \in \mathbb{M} \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = x + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Cs … \(x , y , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = y + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . y + m \cdot i = x + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Ct … \(x , y , z , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = y + m \cdot j , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . y + m \cdot i = z + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = z + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Cm … \(x , y , c , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = y + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . c \cdot x + m \cdot i = c \cdot y + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Cp … \(x , y , u , v , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = u + m \cdot j , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . y + m \cdot i = v + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x \cdot y + m \cdot i = u \cdot v + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)

2 逆元

\(a\) と \(m\) が互いに素なら、Bézout（60c）の \(as + mt = 1\)（\(s, t\) は整数）から、\(ay \equiv 1\) となる自然数 \(y\) が取れます。
Li1 … \(a , m , s , t \in \mathbb{M} , a \cdot s + m \cdot t = 1 \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot s + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Li2 … \(a , m , s , n \in \mathbb{M} , a \cdot s + m \cdot ( - n ) = 1 \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot s + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Li3b … \(a , m , n , t , k \in \mathbb{M} , m \cdot t = 1 + a \cdot n , m = k + 1 \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot ( n \cdot k ) + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Li3 … \(a , m , n , t \in \mathbb{M} , a \cdot ( - n ) + m \cdot t = 1 , m \neq 0 \Longrightarrow \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot w + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) Li3b ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lbad … \(a , m , n , k \in \mathbb{M} , a \cdot ( - n ) + m \cdot ( - k ) = 1 \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Linv1 … \(a , m \in \mathbb{M} , m \neq 0 , \forall d \in \mathbb{M} . ( d \mid a , d \mid m \Longrightarrow d = 1 ) \Longrightarrow \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot w + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) Li1 ，Li2 ，Li3 ，Lbad ，Bezout ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)

3 剰余の一意性

\(0 \le x, y < m\) の範囲では、\(x \equiv y \pmod m\) なら \(x = y\)。
LU1 … \(x , y , m , c \in \mathbb{M} , x + m \cdot c = y , y < m \Longrightarrow c = 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
LUc … \(x , y , m , i , j , c \in \mathbb{M} , x + m \cdot i = y + m \cdot j , i = j + c , y < m \Longrightarrow x = y\) \(\blacktriangleleft\) LU1 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
LU … \(x , y , m \in \mathbb{M} , x < m , y < m , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = y + m \cdot j \Longrightarrow x = y\) \(\blacktriangleleft\) LUc ，LU1 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)

4 単元（掛けて 1 に合同になる元）

\(x\) に対し \(xy \equiv 1\) となる自然数 \(y\) があるとき、\(x\) を（\(m\) を法とする）単元と呼びます。単元の積は単元、合同な元も単元です。
Uc … \(x , z , m \in \mathbb{M} , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x \cdot w + m \cdot i = 1 + m \cdot j , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . z \cdot w + m \cdot i = 1 + m \cdot j \Longrightarrow \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . ( x \cdot z ) \cdot w + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) Cp ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Ucg … \(x , z , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = z + m \cdot j , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x \cdot w + m \cdot i = 1 + m \cdot j \Longrightarrow \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . z \cdot w + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) Cp ，Cs ，Ct ，Cr ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
LDs … \(d , x , p , q \in \mathbb{M} , d \cdot p = x + d \cdot q \Longrightarrow d \mid x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)

5 単元と互いに素

単元と法 \(m\) の公約数は 1 だけです（\(sy + mi = 1 + mj\) の両辺を割り切るので 1 を割り切る）。
Ld1 … \(d \in \mathbb{M} , d \mid 1 \Longrightarrow d = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lcop … \(s , m , d \in \mathbb{M} , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . s \cdot w + m \cdot i = 1 + m \cdot j , d \mid s , d \mid m \Longrightarrow d = 1\) \(\blacktriangleleft\) Ld1 ，LDs ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)

6 既約剰余系

\(R\) を、\(m\) 未満で \(m\) と互いに素な自然数全体とします（\(R\) の個数が \(\varphi(m)\)）。\(R\) の元は単元で、\(m\) 未満の単元は \(R\) の元です。
Lr1 … \(a , m , r \in \mathbb{M} , m \neq 0 , \forall r \, ( r \in R \Longleftrightarrow r \in \mathbb{M} , r < m , \forall d \in \mathbb{M} . ( d \mid r , d \mid m \Longrightarrow d = 1 ) ) , r \in R \Longrightarrow \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . r \cdot w + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) Linv1 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lr2 … \(m , r \in \mathbb{M} , \forall r \, ( r \in R \Longleftrightarrow r \in \mathbb{M} , r < m , \forall d \in \mathbb{M} . ( d \mid r , d \mid m \Longrightarrow d = 1 ) ) , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . r \cdot w + m \cdot i = 1 + m \cdot j , r < m \Longrightarrow r \in R\) \(\blacktriangleleft\) Lcop ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lrem … \(n , m \in \mathbb{M} , m \neq 0 , \forall r \, ( r \in R \Longleftrightarrow r \in \mathbb{M} , r < m , \forall d \in \mathbb{M} . ( d \mid r , d \mid m \Longrightarrow d = 1 ) ) , \exists w \in \mathbb{M} . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . n \cdot w + m \cdot i = 1 + m \cdot j \Longrightarrow \exists s \in R . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . n + m \cdot i = s + m \cdot j\) \(\blacktriangleleft\) Lr2 ，Ucg ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lx0 … \(a , y , r , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . ( a \cdot y ) \cdot r + m \cdot i = r + m \cdot j\) \(\blacktriangleleft\) Cp ，Cr ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lx1 … \(a , y , r , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . y \cdot ( a \cdot r ) + m \cdot i = r + m \cdot j , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot ( y \cdot r ) + m \cdot i = r + m \cdot j\) \(\blacktriangleleft\) Lx0 ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Ucm … \(x , y , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x \cdot y + m \cdot i = 1 + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . y \cdot x + m \cdot i = 1 + m \cdot j\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)