This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 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