素因数分解：昇順の素数の列の積として書け、その列は一意であること。

1 列の積

列 \(f\) は \(f(0), f(1), \ldots\) を値に持つものとし、\(f \prod k\) は最初の \(k\) 項の積 \(f(0) \cdot \ldots \cdot f(k-1)\)。\(+\)・\(\cdot\) と同じく漸化式を満たす演算として仮定します。
列の頭に1項を足せること（SEQ）・積の漸化式（prod𝕄）は articles2/0 の公理。
\(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 + 1 ) < k \Longrightarrow f ( i ) \le f ( ( i + 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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，Lres ，LPH ，Π∈𝕄
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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，LPH
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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄
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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄

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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，Lres ，LPH ，Π∈𝕄 ，EuclidΠ ，Mono

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}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，Ldiv ，LG ，Euclid ，prod𝕄 ，Lres ，LPH ，Π∈𝕄 ，Lmin ，Lmp ，SEQ