1 準備

1.1 割り算

Ldiv … \(a , d \in \mathbb{M} , d \neq 0 \Longrightarrow \exists q \in \mathbb{M} . \exists r \in \mathbb{M} . a = d \cdot q + r , r < d\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

2 主定理

\(p\) が素数で \(p \mid ab\) なら \(p \mid a\) か \(p \mid b\)（ユークリッドの補題）。
\(0 < x < p\) で \(p \mid xb\) なら \(p \mid b\) を \(x\) についての強い帰納法（SIND𝕄）で示す：\(p = xq + r\)（\(r < x\)）と割ると \(r \neq 0\)（\(x\) は \(p\) を割らない）で \(p \mid rb\)。
LG … \(p \in \mathbb{P} , x , b \in \mathbb{M} , x \neq 0 , x < p , p \mid x \cdot b \Longrightarrow p \mid b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1.
Euclid … \(p \in \mathbb{P} , a , b \in \mathbb{M} , p \mid a \cdot b \Longrightarrow p \mid a \mathbin{\rm o\!r} p \mid b\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1.