1 列の積

列 \(f\) は \(f(0), f(1), \ldots\) を値に持つものとし、\(f \prod k\) は最初の \(k\) 項の積 \(f(0) \cdot \ldots \cdot f(k-1)\)。\(+\)・\(\cdot\) と同じく漸化式を満たす演算として仮定します。
列の頭に1項を足せること（seq𝕄）も仮定します。
word(ss,s)F … \(\)
word(ss,s) … \(\prod\)
prod𝕄 … \(\begin{cases} f \prod 0 = 1 \\ k \in \mathbb{M} \Longrightarrow f \prod ( k \textit{+1} ) = ( f \prod k ) \cdot f ( k ) \end{cases}\)
seq𝕄 … \(\exists g \, ( g ( 0 ) = p , \forall i \in \mathbb{M} . g ( i \textit{+1} ) = f ( i ) )\)
\(f\) の最初の \(k\) 項が素数で昇順のとき \(f\) ℙasc \(k\) と書きます。
word(ss,p) … \(\mathbb{P}{\rm asc}\)
ℙasc. … \(f \mathbb{P}{\rm asc} k \Longleftrightarrow \forall i \in \mathbb{M} . ( i < k \Longrightarrow f ( i ) \in \mathbb{P} ) , \forall i \in \mathbb{M} . ( i \textit{+1} < k \Longrightarrow f ( i ) \le f ( i \textit{+1} ) )\)
EuclidΠ … \(p \in \mathbb{P} , k \in \mathbb{M} , f \mathbb{P}{\rm asc} k , p \mid f \prod k \Longrightarrow \exists j \in \mathbb{M} . j < k , p \mid f ( j )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，prod𝕄
Mono … \(l \in \mathbb{M} , f \mathbb{P}{\rm asc} l , m , j \in \mathbb{M} , m + j < l \Longrightarrow f ( j ) \le f ( m + j )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄
Lmin … \(n \in \mathbb{M} , 2 \le n \Longrightarrow \exists p \in \mathbb{M} . 2 \le p , p \mid n , \forall e \in \mathbb{M} . ( 2 \le e , e \mid n \Longrightarrow p \le e )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄
Lmp … \(n \in \mathbb{M} , n \neq 0 , p \in \mathbb{M} , 2 \le p , p \mid n , \forall e \in \mathbb{M} . ( 2 \le e , e \mid n \Longrightarrow p \le e ) \Longrightarrow p \in \mathbb{P}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄

2 主定理

2.1 一意性

昇順の素数の列 \(f\)（長さ \(k\)）・\(g\)（長さ \(l\)）の積が等しければ、長さも項も等しい。
最後の項 \(a = f(k-1)\)・\(b = g(l-1)\) はそれぞれ最大の項で、\(a\) は \(g\) のどれかの項に等しいので \(a \le b\)、同様に \(b \le a\)。積から \(a\) を消して（消去律 ⋅K）長さについての帰納法。
Uniq … \(k , l \in \mathbb{M} , f \mathbb{P}{\rm asc} k , g \mathbb{P}{\rm asc} l , f \prod k = g \prod l \Longrightarrow k = l , \forall i \in \mathbb{M} . ( i < k \Longrightarrow f ( i ) = g ( i ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，prod𝕄

2.2 存在

\(n \ge 2\) の最小の約数 \(p \ge 2\) は素数で、\(n = p m\)。\(m\) の素因数はどれも \(n\) を割るので \(p\) 以上。\(m\) の列の頭に \(p\) を足す。\(n\) についての強い帰納法。
Exist … \(n \in \mathbb{M} , 2 \le n \Longrightarrow \exists k \in \mathbb{M} . \exists f \, ( f \mathbb{P}{\rm asc} k , n = f \prod k )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，𝕄0s ，IND𝕄 ，suc𝕄 ，+𝕄 ，*𝕄 ，1. ，prod𝕄 ，seq𝕄