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=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
	1arith.2	$$⊢R=\left\{e\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
Assertion	1arith2	$$⊢\forall z\in \mathbb{N}\exists !g\in RM\left(z\right)=g$$

Proof

Step	Hyp	Ref	Expression
1		1arith.1	$$⊢M=\left(n\in \mathbb{N}⟼\left(p\in \mathbb{P}⟼p\mathrm{pCnt}n\right)\right)$$
2		1arith.2	$$⊢R=\left\{e\in \left({{\mathbb{N}}_0}^{\mathbb{P}}\right)|e^{-1}\left[\mathbb{N}\right]\in \mathrm{Fin}\right\}$$
3	1 2	1arith	$$⊢M:\mathbb{N}\underset{1-1\; onto}{⟶}R$$
4		f1ocnv	$$⊢M:\mathbb{N}\underset{1-1\; onto}{⟶}R\to M^{-1}:R\underset{1-1\; onto}{⟶}\mathbb{N}$$
5	3 4	ax-mp	$$⊢M^{-1}:R\underset{1-1\; onto}{⟶}\mathbb{N}$$
6		f1ofveu	$$⊢\left(M^{-1}:R\underset{1-1\; onto}{⟶}\mathbb{N}\wedge z\in \mathbb{N}\right)\to \exists !g\in R{M}^{-1}\left(g\right)=z$$
7	5 6	mpan	$$⊢z\in \mathbb{N}\to \exists !g\in R{M}^{-1}\left(g\right)=z$$
8		f1ocnvfvb	$$⊢\left(M:\mathbb{N}\underset{1-1\; onto}{⟶}R\wedge z\in \mathbb{N}\wedge g\in R\right)\to \left(M\left(z\right)=g\leftrightarrow M^{-1}\left(g\right)=z\right)$$
9	3 8	mp3an1	$$⊢\left(z\in \mathbb{N}\wedge g\in R\right)\to \left(M\left(z\right)=g\leftrightarrow M^{-1}\left(g\right)=z\right)$$
10	9	reubidva	$$⊢z\in \mathbb{N}\to \left(\exists !g\in RM\left(z\right)=g\leftrightarrow \exists !g\in R{M}^{-1}\left(g\right)=z\right)$$
11	7 10	mpbird	$$⊢z\in \mathbb{N}\to \exists !g\in RM\left(z\right)=g$$
12	11	rgen	$$⊢\forall z\in \mathbb{N}\exists !g\in RM\left(z\right)=g$$