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∈ℕ⟼p∈ℙ⟼ppCntn
1arith.2 ⊢R=e∈ℕ0ℙ|e-1ℕ∈Fin
Assertion 1arith ⊢M:ℕ⟶1-1 ontoR

Proof

Step Hyp Ref Expression
1 1arith.1 ⊢M=n∈ℕ⟼p∈ℙ⟼ppCntn
2 1arith.2 ⊢R=e∈ℕ0ℙ|e-1ℕ∈Fin
3 prmex ⊢ℙ∈V
4 3 mptex ⊢p∈ℙ⟼ppCntn∈V
5 4 1 fnmpti ⊢MFnℕ
6 1 1arithlem3 ⊢x∈ℕ→M⁡x:ℙ⟶ℕ0
7 nn0ex ⊢ℕ0∈V
8 7 3 elmap ⊢M⁡x∈ℕ0ℙ↔M⁡x:ℙ⟶ℕ0
9 6 8 sylibr ⊢x∈ℕ→M⁡x∈ℕ0ℙ
10 fzfi ⊢1…x∈Fin
11 ffn ⊢M⁡x:ℙ⟶ℕ0→M⁡xFnℙ
12 elpreima ⊢M⁡xFnℙ→q∈M⁡x-1ℕ↔q∈ℙ∧M⁡x⁡q∈ℕ
13 6 11 12 3syl ⊢x∈ℕ→q∈M⁡x-1ℕ↔q∈ℙ∧M⁡x⁡q∈ℕ
14 1 1arithlem2 ⊢x∈ℕ∧q∈ℙ→M⁡x⁡q=qpCntx
15 14 eleq1d ⊢x∈ℕ∧q∈ℙ→M⁡x⁡q∈ℕ↔qpCntx∈ℕ
16 prmz ⊢q∈ℙ→q∈ℤ
17 id ⊢x∈ℕ→x∈ℕ
18 dvdsle ⊢q∈ℤ∧x∈ℕ→q∥x→q≤x
19 16 17 18 syl2anr ⊢x∈ℕ∧q∈ℙ→q∥x→q≤x
20 pcelnn ⊢q∈ℙ∧x∈ℕ→qpCntx∈ℕ↔q∥x
21 20 ancoms ⊢x∈ℕ∧q∈ℙ→qpCntx∈ℕ↔q∥x
22 prmnn ⊢q∈ℙ→q∈ℕ
23 nnuz ⊢ℕ=ℤ≥1
24 22 23 eleqtrdi ⊢q∈ℙ→q∈ℤ≥1
25 nnz ⊢x∈ℕ→x∈ℤ
26 elfz5 ⊢q∈ℤ≥1∧x∈ℤ→q∈1…x↔q≤x
27 24 25 26 syl2anr ⊢x∈ℕ∧q∈ℙ→q∈1…x↔q≤x
28 19 21 27 3imtr4d ⊢x∈ℕ∧q∈ℙ→qpCntx∈ℕ→q∈1…x
29 15 28 sylbid ⊢x∈ℕ∧q∈ℙ→M⁡x⁡q∈ℕ→q∈1…x
30 29 expimpd ⊢x∈ℕ→q∈ℙ∧M⁡x⁡q∈ℕ→q∈1…x
31 13 30 sylbid ⊢x∈ℕ→q∈M⁡x-1ℕ→q∈1…x
32 31 ssrdv ⊢x∈ℕ→M⁡x-1ℕ⊆1…x
33 ssfi ⊢1…x∈Fin∧M⁡x-1ℕ⊆1…x→M⁡x-1ℕ∈Fin
34 10 32 33 sylancr ⊢x∈ℕ→M⁡x-1ℕ∈Fin
35 cnveq ⊢e=M⁡x→e-1=M⁡x-1
36 35 imaeq1d ⊢e=M⁡x→e-1ℕ=M⁡x-1ℕ
37 36 eleq1d ⊢e=M⁡x→e-1ℕ∈Fin↔M⁡x-1ℕ∈Fin
38 37 2 elrab2 ⊢M⁡x∈R↔M⁡x∈ℕ0ℙ∧M⁡x-1ℕ∈Fin
39 9 34 38 sylanbrc ⊢x∈ℕ→M⁡x∈R
40 39 rgen ⊢∀x∈ℕM⁡x∈R
41 ffnfv ⊢M:ℕ⟶R↔MFnℕ∧∀x∈ℕM⁡x∈R
42 5 40 41 mpbir2an ⊢M:ℕ⟶R
43 14 adantlr ⊢x∈ℕ∧y∈ℕ∧q∈ℙ→M⁡x⁡q=qpCntx
44 1 1arithlem2 ⊢y∈ℕ∧q∈ℙ→M⁡y⁡q=qpCnty
45 44 adantll ⊢x∈ℕ∧y∈ℕ∧q∈ℙ→M⁡y⁡q=qpCnty
46 43 45 eqeq12d ⊢x∈ℕ∧y∈ℕ∧q∈ℙ→M⁡x⁡q=M⁡y⁡q↔qpCntx=qpCnty
47 46 ralbidva ⊢x∈ℕ∧y∈ℕ→∀q∈ℙM⁡x⁡q=M⁡y⁡q↔∀q∈ℙqpCntx=qpCnty
48 1 1arithlem3 ⊢y∈ℕ→M⁡y:ℙ⟶ℕ0
49 ffn ⊢M⁡y:ℙ⟶ℕ0→M⁡yFnℙ
50 eqfnfv ⊢M⁡xFnℙ∧M⁡yFnℙ→M⁡x=M⁡y↔∀q∈ℙM⁡x⁡q=M⁡y⁡q
51 11 49 50 syl2an ⊢M⁡x:ℙ⟶ℕ0∧M⁡y:ℙ⟶ℕ0→M⁡x=M⁡y↔∀q∈ℙM⁡x⁡q=M⁡y⁡q
52 6 48 51 syl2an ⊢x∈ℕ∧y∈ℕ→M⁡x=M⁡y↔∀q∈ℙM⁡x⁡q=M⁡y⁡q
53 nnnn0 ⊢x∈ℕ→x∈ℕ0
54 nnnn0 ⊢y∈ℕ→y∈ℕ0
55 pc11 ⊢x∈ℕ0∧y∈ℕ0→x=y↔∀q∈ℙqpCntx=qpCnty
56 53 54 55 syl2an ⊢x∈ℕ∧y∈ℕ→x=y↔∀q∈ℙqpCntx=qpCnty
57 47 52 56 3bitr4d ⊢x∈ℕ∧y∈ℕ→M⁡x=M⁡y↔x=y
58 57 biimpd ⊢x∈ℕ∧y∈ℕ→M⁡x=M⁡y→x=y
59 58 rgen2 ⊢∀x∈ℕ∀y∈ℕM⁡x=M⁡y→x=y
60 dff13 ⊢M:ℕ⟶1-1R↔M:ℕ⟶R∧∀x∈ℕ∀y∈ℕM⁡x=M⁡y→x=y
61 42 59 60 mpbir2an ⊢M:ℕ⟶1-1R
62 eqid ⊢g∈ℕ⟼ifg∈ℙgf⁡g1=g∈ℕ⟼ifg∈ℙgf⁡g1
63 cnveq ⊢e=f→e-1=f-1
64 63 imaeq1d ⊢e=f→e-1ℕ=f-1ℕ
65 64 eleq1d ⊢e=f→e-1ℕ∈Fin↔f-1ℕ∈Fin
66 65 2 elrab2 ⊢f∈R↔f∈ℕ0ℙ∧f-1ℕ∈Fin
67 66 simplbi ⊢f∈R→f∈ℕ0ℙ
68 7 3 elmap ⊢f∈ℕ0ℙ↔f:ℙ⟶ℕ0
69 67 68 sylib ⊢f∈R→f:ℙ⟶ℕ0
70 69 ad2antrr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→f:ℙ⟶ℕ0
71 simplr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→y∈ℝ
72 0re ⊢0∈ℝ
73 ifcl ⊢y∈ℝ∧0∈ℝ→if0≤yy0∈ℝ
74 71 72 73 sylancl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→if0≤yy0∈ℝ
75 max1 ⊢0∈ℝ∧y∈ℝ→0≤if0≤yy0
76 72 71 75 sylancr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→0≤if0≤yy0
77 flge0nn0 ⊢if0≤yy0∈ℝ∧0≤if0≤yy0→if0≤yy0∈ℕ0
78 74 76 77 syl2anc ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→if0≤yy0∈ℕ0
79 nn0p1nn ⊢if0≤yy0∈ℕ0→if0≤yy0+1∈ℕ
80 78 79 syl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→if0≤yy0+1∈ℕ
81 71 adantr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→y∈ℝ
82 80 adantr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→if0≤yy0+1∈ℕ
83 82 nnred ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→if0≤yy0+1∈ℝ
84 16 ssriv ⊢ℙ⊆ℤ
85 zssre ⊢ℤ⊆ℝ
86 84 85 sstri ⊢ℙ⊆ℝ
87 simprl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→q∈ℙ
88 86 87 sselid ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→q∈ℝ
89 74 adantr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→if0≤yy0∈ℝ
90 max2 ⊢0∈ℝ∧y∈ℝ→y≤if0≤yy0
91 72 81 90 sylancr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→y≤if0≤yy0
92 flltp1 ⊢if0≤yy0∈ℝ→if0≤yy0<if0≤yy0+1
93 89 92 syl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→if0≤yy0<if0≤yy0+1
94 81 89 83 91 93 lelttrd ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→y<if0≤yy0+1
95 simprr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→if0≤yy0+1≤q
96 81 83 88 94 95 ltletrd ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→y<q
97 81 88 ltnled ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→y<q↔¬q≤y
98 96 97 mpbid ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→¬q≤y
99 87 biantrurd ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q∈ℕ↔q∈ℙ∧f⁡q∈ℕ
100 70 adantr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f:ℙ⟶ℕ0
101 ffn ⊢f:ℙ⟶ℕ0→fFnℙ
102 elpreima ⊢fFnℙ→q∈f-1ℕ↔q∈ℙ∧f⁡q∈ℕ
103 100 101 102 3syl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→q∈f-1ℕ↔q∈ℙ∧f⁡q∈ℕ
104 99 103 bitr4d ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q∈ℕ↔q∈f-1ℕ
105 simplr ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→∀k∈f-1ℕk≤y
106 breq1 ⊢k=q→k≤y↔q≤y
107 106 rspccv ⊢∀k∈f-1ℕk≤y→q∈f-1ℕ→q≤y
108 105 107 syl ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→q∈f-1ℕ→q≤y
109 104 108 sylbid ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q∈ℕ→q≤y
110 98 109 mtod ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→¬f⁡q∈ℕ
111 100 87 ffvelcdmd ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q∈ℕ0
112 elnn0 ⊢f⁡q∈ℕ0↔f⁡q∈ℕ∨f⁡q=0
113 111 112 sylib ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q∈ℕ∨f⁡q=0
114 113 ord ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→¬f⁡q∈ℕ→f⁡q=0
115 110 114 mpd ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y∧q∈ℙ∧if0≤yy0+1≤q→f⁡q=0
116 1 62 70 80 115 1arithlem4 ⊢f∈R∧y∈ℝ∧∀k∈f-1ℕk≤y→∃x∈ℕf=M⁡x
117 cnvimass ⊢f-1ℕ⊆dom⁡f
118 69 fdmd ⊢f∈R→dom⁡f=ℙ
119 118 86 eqsstrdi ⊢f∈R→dom⁡f⊆ℝ
120 117 119 sstrid ⊢f∈R→f-1ℕ⊆ℝ
121 66 simprbi ⊢f∈R→f-1ℕ∈Fin
122 fimaxre2 ⊢f-1ℕ⊆ℝ∧f-1ℕ∈Fin→∃y∈ℝ∀k∈f-1ℕk≤y
123 120 121 122 syl2anc ⊢f∈R→∃y∈ℝ∀k∈f-1ℕk≤y
124 116 123 r19.29a ⊢f∈R→∃x∈ℕf=M⁡x
125 124 rgen ⊢∀f∈R∃x∈ℕf=M⁡x
126 dffo3 ⊢M:ℕ⟶ontoR↔M:ℕ⟶R∧∀f∈R∃x∈ℕf=M⁡x
127 42 125 126 mpbir2an ⊢M:ℕ⟶ontoR
128 df-f1o ⊢M:ℕ⟶1-1 ontoR↔M:ℕ⟶1-1R∧M:ℕ⟶ontoR
129 61 127 128 mpbir2an ⊢M:ℕ⟶1-1 ontoR