ユークリッドの補題：素数 \(p\) が積 \(ab\) を割れば \(a\) か \(b\) を割る（割り算の定理から）。

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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，1. ，2. ，3. ，4. ，5.

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\) Ldiv ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，1. ，2. ，3. ，4. ，5.
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\) Ldiv ，LG ，\(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，1. ，2. ，3. ，4. ，5.