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 e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
	1arith.2	|- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }
Assertion	1arith2	|- A. z e. NN E! g e. R ( M ` z ) = g

Proof

Step	Hyp	Ref	Expression
1		1arith.1	|- M = ( n e. NN |-> ( p e. Prime |-> ( p pCnt n ) ) )
2		1arith.2	|- R = { e e. ( NN0 ^m Prime ) | ( `' e " NN ) e. Fin }
3	1 2	1arith	|- M : NN -1-1-onto-> R
4		f1ocnv	|- ( M : NN -1-1-onto-> R -> `' M : R -1-1-onto-> NN )
5	3 4	ax-mp	|- `' M : R -1-1-onto-> NN
6		f1ofveu	|- ( ( `' M : R -1-1-onto-> NN /\ z e. NN ) -> E! g e. R ( `' M ` g ) = z )
7	5 6	mpan	|- ( z e. NN -> E! g e. R ( `' M ` g ) = z )
8		f1ocnvfvb	|- ( ( M : NN -1-1-onto-> R /\ z e. NN /\ g e. R ) -> ( ( M ` z ) = g <-> ( `' M ` g ) = z ) )
9	3 8	mp3an1	|- ( ( z e. NN /\ g e. R ) -> ( ( M ` z ) = g <-> ( `' M ` g ) = z ) )
10	9	reubidva	|- ( z e. NN -> ( E! g e. R ( M ` z ) = g <-> E! g e. R ( `' M ` g ) = z ) )
11	7 10	mpbird	|- ( z e. NN -> E! g e. R ( M ` z ) = g )
12	11	rgen	|- A. z e. NN E! g e. R ( M ` z ) = g