素数は無限にある。2以上の数が素因数をもつことから示す。

1 素因数の存在

2以上の \(n\) が素数でなければ、\(1\) でも \(n\) でもない約数 \(d\)（\(2 \le d < n\)）があり、\(d\) の素因数は \(n\) の素因数（\(n\) についての強い帰納法 SIND）。
Lpf … \(n \in \mathbb{M} , 2 \le n \Longrightarrow \exists p \in \mathbb{P} . p \mid n\) \(\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}\)

2 主定理

\(n\) より大きい素数がある、すなわち素数は無限にある（ユークリッドの証明）。
\(n\) 以下の \(0\) でないすべての数で割り切れる \(N \neq 0\) がある（\(n\) についての帰納法・次は \(N \cdot (n+1)\)）。
\(N+1 \ge 2\) の素因数を \(p\) とする。\(p \le n\) なら \(p \mid N\) と \(p \mid N+1\) が矛盾するので \(n < p\)。
LN … \(n \in \mathbb{M} \Longrightarrow \exists N \in \mathbb{M} . N \neq 0 , \forall d \in \mathbb{M} . ( d \neq 0 , d \le n \Longrightarrow d \mid N )\) \(\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}\) ，Lpf
Lcop … \(p \in \mathbb{P} , N \in \mathbb{M} , p \mid N , p \mid N + 1 \Longrightarrow {\perp}\) \(\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}\) ，Lpf ，LN
Linf … \(n \in \mathbb{M} \Longrightarrow \exists p \in \mathbb{P} . n < p\) \(\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}\) ，Lpf ，LN ，Lcop