Metamath Proof Explorer

Theorem 1arith

Description: Fundamental theorem of arithmetic, where a prime factorization is represented as a sequence of prime exponents, for which only finitely many primes have nonzero exponent. The function M maps the set of positive integers one-to-one onto the set of prime factorizations R . (Contributed by Paul Chapman, 17-Nov-2012) (Proof shortened 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 1arith 
|- M : NN -1-1-onto-> R

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 prmex 
 |-  Prime e. _V
4 3 mptex 
 |-  ( p e. Prime |-> ( p pCnt n ) ) e. _V
5 4 1 fnmpti 
 |-  M Fn NN
6 1 1arithlem3 
 |-  ( x e. NN -> ( M ` x ) : Prime --> NN0 )
7 nn0ex 
 |-  NN0 e. _V
8 7 3 elmap 
 |-  ( ( M ` x ) e. ( NN0 ^m Prime ) <-> ( M ` x ) : Prime --> NN0 )
9 6 8 sylibr 
 |-  ( x e. NN -> ( M ` x ) e. ( NN0 ^m Prime ) )
10 fzfi 
 |-  ( 1 ... x ) e. Fin
11 ffn 
 |-  ( ( M ` x ) : Prime --> NN0 -> ( M ` x ) Fn Prime )
12 elpreima 
 |-  ( ( M ` x ) Fn Prime -> ( q e. ( `' ( M ` x ) " NN ) <-> ( q e. Prime /\ ( ( M ` x ) ` q ) e. NN ) ) )
13 6 11 12 3syl 
 |-  ( x e. NN -> ( q e. ( `' ( M ` x ) " NN ) <-> ( q e. Prime /\ ( ( M ` x ) ` q ) e. NN ) ) )
14 1 1arithlem2 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( ( M ` x ) ` q ) = ( q pCnt x ) )
15 14 eleq1d 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( ( ( M ` x ) ` q ) e. NN <-> ( q pCnt x ) e. NN ) )
16 prmz 
 |-  ( q e. Prime -> q e. ZZ )
17 id 
 |-  ( x e. NN -> x e. NN )
18 dvdsle 
 |-  ( ( q e. ZZ /\ x e. NN ) -> ( q || x -> q <_ x ) )
19 16 17 18 syl2anr 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( q || x -> q <_ x ) )
20 pcelnn 
 |-  ( ( q e. Prime /\ x e. NN ) -> ( ( q pCnt x ) e. NN <-> q || x ) )
21 20 ancoms 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( ( q pCnt x ) e. NN <-> q || x ) )
22 prmnn 
 |-  ( q e. Prime -> q e. NN )
23 nnuz 
 |-  NN = ( ZZ>= ` 1 )
24 22 23 eleqtrdi 
 |-  ( q e. Prime -> q e. ( ZZ>= ` 1 ) )
25 nnz 
 |-  ( x e. NN -> x e. ZZ )
26 elfz5 
 |-  ( ( q e. ( ZZ>= ` 1 ) /\ x e. ZZ ) -> ( q e. ( 1 ... x ) <-> q <_ x ) )
27 24 25 26 syl2anr 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( q e. ( 1 ... x ) <-> q <_ x ) )
28 19 21 27 3imtr4d 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( ( q pCnt x ) e. NN -> q e. ( 1 ... x ) ) )
29 15 28 sylbid 
 |-  ( ( x e. NN /\ q e. Prime ) -> ( ( ( M ` x ) ` q ) e. NN -> q e. ( 1 ... x ) ) )
30 29 expimpd 
 |-  ( x e. NN -> ( ( q e. Prime /\ ( ( M ` x ) ` q ) e. NN ) -> q e. ( 1 ... x ) ) )
31 13 30 sylbid 
 |-  ( x e. NN -> ( q e. ( `' ( M ` x ) " NN ) -> q e. ( 1 ... x ) ) )
32 31 ssrdv 
 |-  ( x e. NN -> ( `' ( M ` x ) " NN ) C_ ( 1 ... x ) )
33 ssfi 
 |-  ( ( ( 1 ... x ) e. Fin /\ ( `' ( M ` x ) " NN ) C_ ( 1 ... x ) ) -> ( `' ( M ` x ) " NN ) e. Fin )
34 10 32 33 sylancr 
 |-  ( x e. NN -> ( `' ( M ` x ) " NN ) e. Fin )
35 cnveq 
 |-  ( e = ( M ` x ) -> `' e = `' ( M ` x ) )
36 35 imaeq1d 
 |-  ( e = ( M ` x ) -> ( `' e " NN ) = ( `' ( M ` x ) " NN ) )
37 36 eleq1d 
 |-  ( e = ( M ` x ) -> ( ( `' e " NN ) e. Fin <-> ( `' ( M ` x ) " NN ) e. Fin ) )
38 37 2 elrab2 
 |-  ( ( M ` x ) e. R <-> ( ( M ` x ) e. ( NN0 ^m Prime ) /\ ( `' ( M ` x ) " NN ) e. Fin ) )
39 9 34 38 sylanbrc 
 |-  ( x e. NN -> ( M ` x ) e. R )
40 39 rgen 
 |-  A. x e. NN ( M ` x ) e. R
41 ffnfv 
 |-  ( M : NN --> R <-> ( M Fn NN /\ A. x e. NN ( M ` x ) e. R ) )
42 5 40 41 mpbir2an 
 |-  M : NN --> R
43 14 adantlr 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ q e. Prime ) -> ( ( M ` x ) ` q ) = ( q pCnt x ) )
44 1 1arithlem2 
 |-  ( ( y e. NN /\ q e. Prime ) -> ( ( M ` y ) ` q ) = ( q pCnt y ) )
45 44 adantll 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ q e. Prime ) -> ( ( M ` y ) ` q ) = ( q pCnt y ) )
46 43 45 eqeq12d 
 |-  ( ( ( x e. NN /\ y e. NN ) /\ q e. Prime ) -> ( ( ( M ` x ) ` q ) = ( ( M ` y ) ` q ) <-> ( q pCnt x ) = ( q pCnt y ) ) )
47 46 ralbidva 
 |-  ( ( x e. NN /\ y e. NN ) -> ( A. q e. Prime ( ( M ` x ) ` q ) = ( ( M ` y ) ` q ) <-> A. q e. Prime ( q pCnt x ) = ( q pCnt y ) ) )
48 1 1arithlem3 
 |-  ( y e. NN -> ( M ` y ) : Prime --> NN0 )
49 ffn 
 |-  ( ( M ` y ) : Prime --> NN0 -> ( M ` y ) Fn Prime )
50 eqfnfv 
 |-  ( ( ( M ` x ) Fn Prime /\ ( M ` y ) Fn Prime ) -> ( ( M ` x ) = ( M ` y ) <-> A. q e. Prime ( ( M ` x ) ` q ) = ( ( M ` y ) ` q ) ) )
51 11 49 50 syl2an 
 |-  ( ( ( M ` x ) : Prime --> NN0 /\ ( M ` y ) : Prime --> NN0 ) -> ( ( M ` x ) = ( M ` y ) <-> A. q e. Prime ( ( M ` x ) ` q ) = ( ( M ` y ) ` q ) ) )
52 6 48 51 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( M ` x ) = ( M ` y ) <-> A. q e. Prime ( ( M ` x ) ` q ) = ( ( M ` y ) ` q ) ) )
53 nnnn0 
 |-  ( x e. NN -> x e. NN0 )
54 nnnn0 
 |-  ( y e. NN -> y e. NN0 )
55 pc11 
 |-  ( ( x e. NN0 /\ y e. NN0 ) -> ( x = y <-> A. q e. Prime ( q pCnt x ) = ( q pCnt y ) ) )
56 53 54 55 syl2an 
 |-  ( ( x e. NN /\ y e. NN ) -> ( x = y <-> A. q e. Prime ( q pCnt x ) = ( q pCnt y ) ) )
57 47 52 56 3bitr4d 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( M ` x ) = ( M ` y ) <-> x = y ) )
58 57 biimpd 
 |-  ( ( x e. NN /\ y e. NN ) -> ( ( M ` x ) = ( M ` y ) -> x = y ) )
59 58 rgen2 
 |-  A. x e. NN A. y e. NN ( ( M ` x ) = ( M ` y ) -> x = y )
60 dff13 
 |-  ( M : NN -1-1-> R <-> ( M : NN --> R /\ A. x e. NN A. y e. NN ( ( M ` x ) = ( M ` y ) -> x = y ) ) )
61 42 59 60 mpbir2an 
 |-  M : NN -1-1-> R
62 eqid 
 |-  ( g e. NN |-> if ( g e. Prime , ( g ^ ( f ` g ) ) , 1 ) ) = ( g e. NN |-> if ( g e. Prime , ( g ^ ( f ` g ) ) , 1 ) )
63 cnveq 
 |-  ( e = f -> `' e = `' f )
64 63 imaeq1d 
 |-  ( e = f -> ( `' e " NN ) = ( `' f " NN ) )
65 64 eleq1d 
 |-  ( e = f -> ( ( `' e " NN ) e. Fin <-> ( `' f " NN ) e. Fin ) )
66 65 2 elrab2 
 |-  ( f e. R <-> ( f e. ( NN0 ^m Prime ) /\ ( `' f " NN ) e. Fin ) )
67 66 simplbi 
 |-  ( f e. R -> f e. ( NN0 ^m Prime ) )
68 7 3 elmap 
 |-  ( f e. ( NN0 ^m Prime ) <-> f : Prime --> NN0 )
69 67 68 sylib 
 |-  ( f e. R -> f : Prime --> NN0 )
70 69 ad2antrr 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> f : Prime --> NN0 )
71 simplr 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> y e. RR )
72 0re 
 |-  0 e. RR
73 ifcl 
 |-  ( ( y e. RR /\ 0 e. RR ) -> if ( 0 <_ y , y , 0 ) e. RR )
74 71 72 73 sylancl 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> if ( 0 <_ y , y , 0 ) e. RR )
75 max1 
 |-  ( ( 0 e. RR /\ y e. RR ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
76 72 71 75 sylancr 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
77 flge0nn0 
 |-  ( ( if ( 0 <_ y , y , 0 ) e. RR /\ 0 <_ if ( 0 <_ y , y , 0 ) ) -> ( |_ ` if ( 0 <_ y , y , 0 ) ) e. NN0 )
78 74 76 77 syl2anc 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> ( |_ ` if ( 0 <_ y , y , 0 ) ) e. NN0 )
79 nn0p1nn 
 |-  ( ( |_ ` if ( 0 <_ y , y , 0 ) ) e. NN0 -> ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) e. NN )
80 78 79 syl 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) e. NN )
81 71 adantr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> y e. RR )
82 80 adantr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) e. NN )
83 82 nnred 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) e. RR )
84 16 ssriv 
 |-  Prime C_ ZZ
85 zssre 
 |-  ZZ C_ RR
86 84 85 sstri 
 |-  Prime C_ RR
87 simprl 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> q e. Prime )
88 86 87 sselid 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> q e. RR )
89 74 adantr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> if ( 0 <_ y , y , 0 ) e. RR )
90 max2 
 |-  ( ( 0 e. RR /\ y e. RR ) -> y <_ if ( 0 <_ y , y , 0 ) )
91 72 81 90 sylancr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> y <_ if ( 0 <_ y , y , 0 ) )
92 flltp1 
 |-  ( if ( 0 <_ y , y , 0 ) e. RR -> if ( 0 <_ y , y , 0 ) < ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) )
93 89 92 syl 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> if ( 0 <_ y , y , 0 ) < ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) )
94 81 89 83 91 93 lelttrd 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> y < ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) )
95 simprr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q )
96 81 83 88 94 95 ltletrd 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> y < q )
97 81 88 ltnled 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( y < q <-> -. q <_ y ) )
98 96 97 mpbid 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> -. q <_ y )
99 87 biantrurd 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( f ` q ) e. NN <-> ( q e. Prime /\ ( f ` q ) e. NN ) ) )
100 70 adantr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> f : Prime --> NN0 )
101 ffn 
 |-  ( f : Prime --> NN0 -> f Fn Prime )
102 elpreima 
 |-  ( f Fn Prime -> ( q e. ( `' f " NN ) <-> ( q e. Prime /\ ( f ` q ) e. NN ) ) )
103 100 101 102 3syl 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( q e. ( `' f " NN ) <-> ( q e. Prime /\ ( f ` q ) e. NN ) ) )
104 99 103 bitr4d 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( f ` q ) e. NN <-> q e. ( `' f " NN ) ) )
105 simplr 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> A. k e. ( `' f " NN ) k <_ y )
106 breq1 
 |-  ( k = q -> ( k <_ y <-> q <_ y ) )
107 106 rspccv 
 |-  ( A. k e. ( `' f " NN ) k <_ y -> ( q e. ( `' f " NN ) -> q <_ y ) )
108 105 107 syl 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( q e. ( `' f " NN ) -> q <_ y ) )
109 104 108 sylbid 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( f ` q ) e. NN -> q <_ y ) )
110 98 109 mtod 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> -. ( f ` q ) e. NN )
111 100 87 ffvelcdmd 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( f ` q ) e. NN0 )
112 elnn0 
 |-  ( ( f ` q ) e. NN0 <-> ( ( f ` q ) e. NN \/ ( f ` q ) = 0 ) )
113 111 112 sylib 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( ( f ` q ) e. NN \/ ( f ` q ) = 0 ) )
114 113 ord 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( -. ( f ` q ) e. NN -> ( f ` q ) = 0 ) )
115 110 114 mpd 
 |-  ( ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) /\ ( q e. Prime /\ ( ( |_ ` if ( 0 <_ y , y , 0 ) ) + 1 ) <_ q ) ) -> ( f ` q ) = 0 )
116 1 62 70 80 115 1arithlem4 
 |-  ( ( ( f e. R /\ y e. RR ) /\ A. k e. ( `' f " NN ) k <_ y ) -> E. x e. NN f = ( M ` x ) )
117 cnvimass 
 |-  ( `' f " NN ) C_ dom f
118 69 fdmd 
 |-  ( f e. R -> dom f = Prime )
119 118 86 eqsstrdi 
 |-  ( f e. R -> dom f C_ RR )
120 117 119 sstrid 
 |-  ( f e. R -> ( `' f " NN ) C_ RR )
121 66 simprbi 
 |-  ( f e. R -> ( `' f " NN ) e. Fin )
122 fimaxre2 
 |-  ( ( ( `' f " NN ) C_ RR /\ ( `' f " NN ) e. Fin ) -> E. y e. RR A. k e. ( `' f " NN ) k <_ y )
123 120 121 122 syl2anc 
 |-  ( f e. R -> E. y e. RR A. k e. ( `' f " NN ) k <_ y )
124 116 123 r19.29a 
 |-  ( f e. R -> E. x e. NN f = ( M ` x ) )
125 124 rgen 
 |-  A. f e. R E. x e. NN f = ( M ` x )
126 dffo3 
 |-  ( M : NN -onto-> R <-> ( M : NN --> R /\ A. f e. R E. x e. NN f = ( M ` x ) ) )
127 42 125 126 mpbir2an 
 |-  M : NN -onto-> R
128 df-f1o 
 |-  ( M : NN -1-1-onto-> R <-> ( M : NN -1-1-> R /\ M : NN -onto-> R ) )
129 61 127 128 mpbir2an 
 |-  M : NN -1-1-onto-> R