Bézout の定理の別証明：\(as + bt\)（\(s, t\) は整数）の形の正の自然数のうち最小のものが最大公約数になる（Metamath の bezout と同じ方法）。60b は互除法の漸化式（gcd の公理 gcd𝕄）を使う証明で、こちらは gcd の公理を使わない。

1 準備

整数 \(\mathbb{Z}\) の計算（\(a + (-(gq))\) の展開）と、整数の場合分け（自然数か、自然数の符号を変えたもの）。
ZC … \(m \in \mathbb{Z} \Longrightarrow m \in \mathbb{M} \mathbin{\rm o\!r} \exists a \in \mathbb{M} . m = - a\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\)
Lng … \(x , y \in \mathbb{Z} \Longrightarrow x \cdot ( - y ) = - ( x \cdot y )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC
LAC … \(x , y , u , w \in \mathbb{Z} \Longrightarrow ( x + y ) + ( u + w ) = ( x + u ) + ( y + w )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng
LRg … \(a , b , c , d , s , t , q \in \mathbb{Z} \Longrightarrow ( a \cdot c + b \cdot d ) + ( - ( ( a \cdot s + b \cdot t ) \cdot q ) ) = a \cdot ( c + ( - ( s \cdot q ) ) ) + b \cdot ( d + ( - ( t \cdot q ) ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC

2 主定理

自然数 \(a, b\)（\(0\) でない方がある）に対し、\(as + bt\)（\(s, t\) は整数）の形の正の自然数の中で最小のものを \(g\) とする。最小の元が在ることは、\(x\) が最小でなければ \(x\) 未満にも無い、という強い帰納法（SIND）で示す。
Lleast … \(a , b \in \mathbb{M} , ( a \neq 0 \mathbin{\rm o\!r} b \neq 0 ) \Longrightarrow \exists g \in \mathbb{M} . ( g \neq 0 , \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . g = a \cdot s + b \cdot t , \forall z \in \mathbb{M} . ( ( z \neq 0 , \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . z = a \cdot s + b \cdot t ) \Longrightarrow g \le z ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg
\(g\) が最小なら \(g\) は \(as + bt\) の形の \(u\) を割る。\(u = gq + r\)（\(r < g\)）の余り \(r = u - gq\) も \(as + bt\) の形になり、\(r \neq 0\) なら \(g \le r\) と矛盾する。
Ldvd … \(a , b , g , u \in \mathbb{M} , g \neq 0 , \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . g = a \cdot s + b \cdot t , \forall z \in \mathbb{M} . ( ( z \neq 0 , \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . z = a \cdot s + b \cdot t ) \Longrightarrow g \le z ) , \exists c \in \mathbb{Z} . \exists d \in \mathbb{Z} . u = a \cdot c + b \cdot d \Longrightarrow g \mid u\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg ，Lleast
共通の約数 \(d\) は \(g = as + bt\) も割る。\(a = da'\)、\(b = db'\) なら \(g = d(a's + b't)\)。\(a's + b't\) は整数で、\(g\) が自然数・\(g \neq 0\) なので自然数。
LDz … \(d , a , b , s , t \in \mathbb{Z} \Longrightarrow ( d \cdot a ) \cdot s + ( d \cdot b ) \cdot t = d \cdot ( a \cdot s + b \cdot t )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg ，Lleast ，Ldvd
Lpos … \(d , g , z \in \mathbb{Z} , d \in \mathbb{N} , g \in \mathbb{M} , g \neq 0 , g = d \cdot z \Longrightarrow z \in \mathbb{M}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg ，Lleast ，Ldvd ，LDz
Ldg … \(d , a , b , g \in \mathbb{M} , g \neq 0 , d \mid a , d \mid b , \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . g = a \cdot s + b \cdot t \Longrightarrow d \mid g\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg ，Lleast ，Ldvd ，LDz ，Lpos
自然数 \(a, b\) に対し、\(g = as + bt\)（\(s, t\) は整数）で、\(g \mid a\)・\(g \mid b\)・共通の約数はすべて \(g\) を割る、という \(g\) がある（Bézout・\(g\) は最大公約数）。
Bezout … \(a , b \in \mathbb{M} \Longrightarrow \exists g \in \mathbb{M} . ( \exists s \in \mathbb{Z} . \exists t \in \mathbb{Z} . g = a \cdot s + b \cdot t , g \mid a , g \mid b , \forall d \in \mathbb{M} . ( d \mid a , d \mid b \Longrightarrow d \mid g ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，⋅ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，ZC ，Lng ，LAC ，LRg ，Lleast ，Ldvd ，LDz ，Lpos ，Ldg