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 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
1arith.2 ⊢ R = e ∈ ℕ 0 ℙ | e -1 ℕ ∈ Fin
Assertion 1arith2 ⊢ ∀ z ∈ ℕ ∃! g ∈ R M ⁡ z = g

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢ M = n ∈ ℕ ⟼ p ∈ ℙ ⟼ p pCnt n
2 1arith.2 ⊢ R = e ∈ ℕ 0 ℙ | e -1 ℕ ∈ Fin
3 1 2 1arith ⊢ M : ℕ ⟶ 1-1 onto R
4 f1ocnv ⊢ M : ℕ ⟶ 1-1 onto R → M -1 : R ⟶ 1-1 onto ℕ
5 3 4 ax-mp ⊢ M -1 : R ⟶ 1-1 onto ℕ
6 f1ofveu ⊢ M -1 : R ⟶ 1-1 onto ℕ ∧ z ∈ ℕ → ∃! g ∈ R M -1 ⁡ g = z
7 5 6 mpan ⊢ z ∈ ℕ → ∃! g ∈ R M -1 ⁡ g = z
8 f1ocnvfvb ⊢ M : ℕ ⟶ 1-1 onto R ∧ z ∈ ℕ ∧ g ∈ R → M ⁡ z = g ↔ M -1 ⁡ g = z
9 3 8 mp3an1 ⊢ z ∈ ℕ ∧ g ∈ R → M ⁡ z = g ↔ M -1 ⁡ g = z
10 9 reubidva ⊢ z ∈ ℕ → ∃! g ∈ R M ⁡ z = g ↔ ∃! g ∈ R M -1 ⁡ g = z
11 7 10 mpbird ⊢ z ∈ ℕ → ∃! g ∈ R M ⁡ z = g
12 11 rgen ⊢ ∀ z ∈ ℕ ∃! g ∈ R M ⁡ z = g