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}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

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}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄
Lcop … \(p \in \mathbb{P} , N \in \mathbb{M} , p \mid N , p \mid N + 1 \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄
Linf … \(n \in \mathbb{M} \Longrightarrow \exists p \in \mathbb{P} . n < p\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄