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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，-ℤ ，+ℤ ，⋅ℤ
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，-ℤ ，+ℤ ，⋅ℤ
Lbad … \(a , m , n , k \in \mathbb{M} , a \cdot ( - n ) + m \cdot ( - k ) = 1 \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，-ℤ ，+ℤ ，⋅ℤ
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄 ，-ℤ ，+ℤ ，⋅ℤ

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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
LDs … \(d , x , p , q \in \mathbb{M} , d \cdot p = x + d \cdot q \Longrightarrow d \mid x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

5 単元と互いに素

単元と法 \(m\) の公約数は 1 だけです（\(sy + mi = 1 + mj\) の両辺を割り切るので 1 を割り切る）。
Ld1 … \(d \in \mathbb{M} , d \mid 1 \Longrightarrow d = 1\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
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}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄

7 置換

\(R\) の元 \(r\) を \(ar\) を \(m\) で割った余りに写す対応 \(u\)（\(\langle r, s\rangle \in u\) は \(r, s \in R\) かつ \(ar \equiv s\)）が \(R\) から \(R\) への全単射であることを示します。
Lu1 … \(\forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) \Longrightarrow ( \langle r , s \rangle \in u \Longleftrightarrow r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lex … \(a , m , y , 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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , r \in R \Longrightarrow \exists s \in R . \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lu1 ，Lr1 ，Lrem ，Uc ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lq1 … \(a , m , r , s \in \mathbb{M} , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \langle r , s \rangle \in u \Longrightarrow r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j\) \(\blacktriangleleft\) Lu1 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lq1c … \(a , m , r , s \in \mathbb{M} , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \langle r , s \rangle \in u \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j\) \(\blacktriangleleft\) Lq1 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lq2 … \(x , s , z , m \in \mathbb{M} , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = s + m \cdot j , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . x + m \cdot i = z + m \cdot j \Longrightarrow \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . s + m \cdot i = z + m \cdot j\) \(\blacktriangleleft\) Cs ，Ct ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Luq … \(a , m , r , s , z \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \langle r , s \rangle \in u , \langle r , z \rangle \in u \Longrightarrow s = z\) \(\blacktriangleleft\) Lq1 ，Lq2 ，Lr< ，LU ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Linj … \(a , m , y , r , z , s \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , \langle r , s \rangle \in u , \langle z , s \rangle \in u \Longrightarrow r = z\) \(\blacktriangleleft\) Lq1 ，Lr< ，LU ，Lx1 ，Cm ，Cs ，Ct ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lsur1 … \(a , m , y , s \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 i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , s \in R \Longrightarrow \exists r \in R . \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j\) \(\blacktriangleleft\) Lr1 ，Lrem ，Uc ，Ucm ，Lx1 ，Cm ，Cs ，Ct ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lsur … \(a , m , y , s \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , s \in R \Longrightarrow \exists r \in R . \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lsur1 ，Lu1 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb1 … \(a , m \in \mathbb{M} , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) \Longrightarrow u \subset R \times R\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb2e … \(a , m , y , 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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , r \in R \Longrightarrow \exists s \, \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lex ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb2u … \(a , 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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) \Longrightarrow \forall s , z \, ( \langle r , s \rangle \in u , \langle r , z \rangle \in u \Longrightarrow s = z )\) \(\blacktriangleleft\) Luq ，Lq1 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb2 … \(a , m , y , 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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , r \in R \Longrightarrow \exists! s \, \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lb2e ，Lb2u ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb3e … \(a , m , y , s \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , s \in R \Longrightarrow \exists r \, \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lsur ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb3u … \(a , m , y , s \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j \Longrightarrow \forall r , z \, ( \langle r , s \rangle \in u , \langle z , s \rangle \in u \Longrightarrow r = z )\) \(\blacktriangleleft\) Linj ，Lq1 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lb3 … \(a , m , y , s \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j , s \in R \Longrightarrow \exists! r \, \langle r , s \rangle \in u\) \(\blacktriangleleft\) Lb3e ，Lb3u ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄
Lbij … \(a , m , y \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 ) ) , \forall p \, ( p \in u \Longleftrightarrow \exists r , s \, p = \langle r , s \rangle , r \in R , s \in R , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot r + m \cdot i = s + m \cdot j ) , \exists i \in \mathbb{M} . \exists j \in \mathbb{M} . a \cdot y + m \cdot i = 1 + m \cdot j \Longrightarrow u \in R \stackrel{\rm IS}\to R\) \(\blacktriangleleft\) Lb1 ，Lb2 ，Lb3 ，\(\mathbb{W}.\) ，Ax𝕄 ，ax_s ，+𝕄 ，⋅𝕄