# Metamath Proof Explorer

## Theorem 1arith2

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a finite monotonic 1-based sequence of primes. Every positive integer has a unique prime factorization. Theorem 1.10 in ApostolNT p. 17. This is Metamath 100 proof #80. (Contributed by Paul Chapman, 17-Nov-2012) (Revised by Mario Carneiro, 30-May-2014)

Ref Expression
Hypotheses 1arith.1 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
1arith.2 𝑅 = { 𝑒 ∈ ( ℕ0𝑚 ℙ ) ∣ ( 𝑒 “ ℕ ) ∈ Fin }
Assertion 1arith2 𝑧 ∈ ℕ ∃! 𝑔𝑅 ( 𝑀𝑧 ) = 𝑔

### Proof

Step Hyp Ref Expression
1 1arith.1 𝑀 = ( 𝑛 ∈ ℕ ↦ ( 𝑝 ∈ ℙ ↦ ( 𝑝 pCnt 𝑛 ) ) )
2 1arith.2 𝑅 = { 𝑒 ∈ ( ℕ0𝑚 ℙ ) ∣ ( 𝑒 “ ℕ ) ∈ Fin }
3 1 2 1arith 𝑀 : ℕ –1-1-onto𝑅
4 f1ocnv ( 𝑀 : ℕ –1-1-onto𝑅 𝑀 : 𝑅1-1-onto→ ℕ )
5 3 4 ax-mp 𝑀 : 𝑅1-1-onto→ ℕ
6 f1ofveu ( ( 𝑀 : 𝑅1-1-onto→ ℕ ∧ 𝑧 ∈ ℕ ) → ∃! 𝑔𝑅 ( 𝑀𝑔 ) = 𝑧 )
7 5 6 mpan ( 𝑧 ∈ ℕ → ∃! 𝑔𝑅 ( 𝑀𝑔 ) = 𝑧 )
8 f1ocnvfvb ( ( 𝑀 : ℕ –1-1-onto𝑅𝑧 ∈ ℕ ∧ 𝑔𝑅 ) → ( ( 𝑀𝑧 ) = 𝑔 ↔ ( 𝑀𝑔 ) = 𝑧 ) )
9 3 8 mp3an1 ( ( 𝑧 ∈ ℕ ∧ 𝑔𝑅 ) → ( ( 𝑀𝑧 ) = 𝑔 ↔ ( 𝑀𝑔 ) = 𝑧 ) )
10 9 reubidva ( 𝑧 ∈ ℕ → ( ∃! 𝑔𝑅 ( 𝑀𝑧 ) = 𝑔 ↔ ∃! 𝑔𝑅 ( 𝑀𝑔 ) = 𝑧 ) )
11 7 10 mpbird ( 𝑧 ∈ ℕ → ∃! 𝑔𝑅 ( 𝑀𝑧 ) = 𝑔 )
12 11 rgen 𝑧 ∈ ℕ ∃! 𝑔𝑅 ( 𝑀𝑧 ) = 𝑔