Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  prmreclem5 Unicode version

Theorem prmreclem5 14438
 Description: Lemma for prmrec 14440. Here we show the inequality N 2 M by decomposing the set into the disjoint union of the set of those numbers that are not divisible by any "large" primes (above ) and the indexed union over of the numbers  that divide the prime . By prmreclem4 14437 the second of these has size less than times the prime reciprocal series, which is less than by assumption, we find that the complementary part must be at least large. (Contributed by Mario Carneiro, 6-Aug-2014.)
Hypotheses
Ref Expression
prmrec.1
prmrec.2
prmrec.3
prmrec.4
prmrec.5
prmrec.6
prmrec.7
Assertion
Ref Expression
prmreclem5
Distinct variable groups:   ,,,   ,,,   ,M,,   ,,,   ,   ,N`,,

Proof of Theorem prmreclem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prmrec.3 . . . 4
21nnred 10576 . . 3
32rehalfcld 10810 . 2
4 fzfi 12082 . . . . . 6
5 prmrec.4 . . . . . . 7
6 ssrab2 3584 . . . . . . 7
75, 6eqsstri 3533 . . . . . 6
8 ssfi 7760 . . . . . 6
94, 7, 8mp2an 672 . . . . 5
10 hashcl 12428 . . . . 5
119, 10ax-mp 5 . . . 4
1211nn0rei 10831 . . 3
1312a1i 11 . 2
14 2nn 10718 . . . . 5
15 prmrec.2 . . . . . 6
1615nnnn0d 10877 . . . . 5
17 nnexpcl 12179 . . . . 5
1814, 16, 17sylancr 663 . . . 4
1918nnred 10576 . . 3
201nnrpd 11284 . . . . 5
2120rpsqrtcld 13243 . . . 4
2221rpred 11285 . . 3
2319, 22remulcld 9645 . 2
242recnd 9643 . . . . . 6
25242halvesd 10809 . . . . 5
267a1i 11 . . . . . . . . 9
2715peano2nnd 10578 . . . . . . . . . . . . 13
28 elfzuz 11713 . . . . . . . . . . . . 13
29 eluznn 11181 . . . . . . . . . . . . 13
3027, 28, 29syl2an 477 . . . . . . . . . . . 12
31 eleq1 2529 . . . . . . . . . . . . . . . . 17
32 breq1 4455 . . . . . . . . . . . . . . . . 17
3331, 32anbi12d 710 . . . . . . . . . . . . . . . 16
3433rabbidv 3101 . . . . . . . . . . . . . . 15
35 prmrec.7 . . . . . . . . . . . . . . 15
36 ovex 6324 . . . . . . . . . . . . . . . 16
3736rabex 4603 . . . . . . . . . . . . . . 15
3834, 35, 37fvmpt 5956 . . . . . . . . . . . . . 14
3938adantl 466 . . . . . . . . . . . . 13
40 ssrab2 3584 . . . . . . . . . . . . 13
4139, 40syl6eqss 3553 . . . . . . . . . . . 12
4230, 41syldan 470 . . . . . . . . . . 11
4342ralrimiva 2871 . . . . . . . . . 10
44 iunss 4371 . . . . . . . . . 10
4543, 44sylibr 212 . . . . . . . . 9
4626, 45unssd 3679 . . . . . . . 8
47 breq1 4455 . . . . . . . . . . . . . . . . . 18
4847notbid 294 . . . . . . . . . . . . . . . . 17
4948cbvralv 3084 . . . . . . . . . . . . . . . 16
50 breq2 4456 . . . . . . . . . . . . . . . . . 18
5150notbid 294 . . . . . . . . . . . . . . . . 17
5251ralbidv 2896 . . . . . . . . . . . . . . . 16
5349, 52syl5bb 257 . . . . . . . . . . . . . . 15
5453, 5elrab2 3259 . . . . . . . . . . . . . 14
55 elun1 3670 . . . . . . . . . . . . . 14
5654, 55sylbir 213 . . . . . . . . . . . . 13
5756ex 434 . . . . . . . . . . . 12
5857adantl 466 . . . . . . . . . . 11
59 dfrex2 2908 . . . . . . . . . . . 12
60 eldifn 3626 . . . . . . . . . . . . . . . . . . . . 21
6160ad2antrl 727 . . . . . . . . . . . . . . . . . . . 20
62 eldifi 3625 . . . . . . . . . . . . . . . . . . . . . . . 24
6362ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23
64 prmnn 14220 . . . . . . . . . . . . . . . . . . . . . . 23
6563, 64syl 16 . . . . . . . . . . . . . . . . . . . . . 22
66 nnuz 11145 . . . . . . . . . . . . . . . . . . . . . 22
6765, 66syl6eleq 2555 . . . . . . . . . . . . . . . . . . . . 21
6815nnzd 10993 . . . . . . . . . . . . . . . . . . . . . 22
6968ad2antrr 725 . . . . . . . . . . . . . . . . . . . . 21
70 elfz5 11709 . . . . . . . . . . . . . . . . . . . . 21
7167, 69, 70syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
7261, 71mtbid 300 . . . . . . . . . . . . . . . . . . 19
7315nnred 10576 . . . . . . . . . . . . . . . . . . . . 21
7473ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
7565nnred 10576 . . . . . . . . . . . . . . . . . . . 20
7674, 75ltnled 9753 . . . . . . . . . . . . . . . . . . 19
7772, 76mpbird 232 . . . . . . . . . . . . . . . . . 18
78 prmz 14221 . . . . . . . . . . . . . . . . . . . 20
7963, 78syl 16 . . . . . . . . . . . . . . . . . . 19
80 zltp1le 10938 . . . . . . . . . . . . . . . . . . 19
8169, 79, 80syl2anc 661 . . . . . . . . . . . . . . . . . 18
8277, 81mpbid 210 . . . . . . . . . . . . . . . . 17
83 elfznn 11743 . . . . . . . . . . . . . . . . . . . 20
8483ad2antlr 726 . . . . . . . . . . . . . . . . . . 19
8584nnred 10576 . . . . . . . . . . . . . . . . . 18
862ad2antrr 725 . . . . . . . . . . . . . . . . . 18
87 simprr 757 . . . . . . . . . . . . . . . . . . 19
88 dvdsle 14031 . . . . . . . . . . . . . . . . . . . 20
8979, 84, 88syl2anc 661 . . . . . . . . . . . . . . . . . . 19
9087, 89mpd 15 . . . . . . . . . . . . . . . . . 18
91 elfzle2 11719 . . . . . . . . . . . . . . . . . . 19
9291ad2antlr 726 . . . . . . . . . . . . . . . . . 18
9375, 85, 86, 90, 92letrd 9760 . . . . . . . . . . . . . . . . 17
9468peano2zd 10997 . . . . . . . . . . . . . . . . . . 19
9594ad2antrr 725 . . . . . . . . . . . . . . . . . 18
961nnzd 10993 . . . . . . . . . . . . . . . . . . 19
9796ad2antrr 725 . . . . . . . . . . . . . . . . . 18
98 elfz 11707 . . . . . . . . . . . . . . . . . 18
9979, 95, 97, 98syl3anc 1228 . . . . . . . . . . . . . . . . 17
10082, 93, 99mpbir2and 922 . . . . . . . . . . . . . . . 16
101 simplr 755 . . . . . . . . . . . . . . . . . 18
10263, 87jca 532 . . . . . . . . . . . . . . . . . 18
10350anbi2d 703 . . . . . . . . . . . . . . . . . . 19
104103elrab 3257 . . . . . . . . . . . . . . . . . 18
105101, 102, 104sylanbrc 664 . . . . . . . . . . . . . . . . 17
106 eleq1 2529 . . . . . . . . . . . . . . . . . . . . 21
107106, 47anbi12d 710 . . . . . . . . . . . . . . . . . . . 20
108107rabbidv 3101 . . . . . . . . . . . . . . . . . . 19
10936rabex 4603 . . . . . . . . . . . . . . . . . . 19
110108, 35, 109fvmpt 5956 . . . . . . . . . . . . . . . . . 18
11165, 110syl 16 . . . . . . . . . . . . . . . . 17
112105, 111eleqtrrd 2548 . . . . . . . . . . . . . . . 16
113 fveq2 5871 . . . . . . . . . . . . . . . . . 18
114113eleq2d 2527 . . . . . . . . . . . . . . . . 17
115114rspcev 3210 . . . . . . . . . . . . . . . 16
116100, 112, 115syl2anc 661 . . . . . . . . . . . . . . 15
117 eliun 4335 . . . . . . . . . . . . . . 15
118116, 117sylibr 212 . . . . . . . . . . . . . 14
119 elun2 3671 . . . . . . . . . . . . . 14
120118, 119syl 16 . . . . . . . . . . . . 13
121120rexlimdvaa 2950 . . . . . . . . . . . 12
12259, 121syl5bir 218 . . . . . . . . . . 11
12358, 122pm2.61d 158 . . . . . . . . . 10
124123ex 434 . . . . . . . . 9
125124ssrdv 3509 . . . . . . . 8
12646, 125eqssd 3520 . . . . . . 7
127126fveq2d 5875 . . . . . 6
1281nnnn0d 10877 . . . . . . 7
129 hashfz1 12419 . . . . . . 7
130128, 129syl 16 . . . . . 6
131127, 130eqtr2d 2499 . . . . 5
1329a1i 11 . . . . . 6
133 ssfi 7760 . . . . . . 7
1344, 45, 133sylancr 663 . . . . . 6
135 simprr 757 . . . . . . . . . . . . . . . . 17
136 noel 3788 . . . . . . . . . . . . . . . . . 18
137 simprl 756 . . . . . . . . . . . . . . . . . . . . 21
138137biantrud 507 . . . . . . . . . . . . . . . . . . . 20
139 elin 3686 . . . . . . . . . . . . . . . . . . . 20
140138, 139syl6bbr 263 . . . . . . . . . . . . . . . . . . 19
14173ltp1d 10501 . . . . . . . . . . . . . . . . . . . . . 22
142 fzdisj 11741 . . . . . . . . . . . . . . . . . . . . . 22
143141, 142syl 16 . . . . . . . . . . . . . . . . . . . . 21
144143ad2antrr 725 . . . . . . . . . . . . . . . . . . . 20
145144eleq2d 2527 . . . . . . . . . . . . . . . . . . 19
146140, 145bitrd 253 . . . . . . . . . . . . . . . . . 18
147136, 146mtbiri 303 . . . . . . . . . . . . . . . . 17
148135, 147eldifd 3486 . . . . . . . . . . . . . . . 16
149 breq2 4456 . . . . . . . . . . . . . . . . . . . . 21
150149notbid 294 . . . . . . . . . . . . . . . . . . . 20
151150ralbidv 2896 . . . . . . . . . . . . . . . . . . 19
152151, 5elrab2 3259 . . . . . . . . . . . . . . . . . 18
153152simprbi 464 . . . . . . . . . . . . . . . . 17
154153ad2antlr 726 . . . . . . . . . . . . . . . 16
155 breq1 4455 . . . . . . . . . . . . . . . . . 18
156155notbid 294 . . . . . . . . . . . . . . . . 17
157156rspcv 3206 . . . . . . . . . . . . . . . 16
158148, 154, 157sylc 60 . . . . . . . . . . . . . . 15
159158expr 615 . . . . . . . . . . . . . 14
160 imnan 422 . . . . . . . . . . . . . 14
161159, 160sylib 196 . . . . . . . . . . . . 13
16230adantlr 714 . . . . . . . . . . . . . . . 16
163162, 38syl 16 . . . . . . . . . . . . . . 15
164163eleq2d 2527 . . . . . . . . . . . . . 14
165 breq2 4456 . . . . . . . . . . . . . . . . 17
166165anbi2d 703 . . . . . . . . . . . . . . . 16
167166elrab 3257 . . . . . . . . . . . . . . 15
168167simprbi 464 . . . . . . . . . . . . . 14
169164, 168syl6bi 228 . . . . . . . . . . . . 13
170161, 169mtod 177 . . . . . . . . . . . 12
171170nrexdv 2913 . . . . . . . . . . 11
172171, 117sylnibr 305 . . . . . . . . . 10
173172ex 434 . . . . . . . . 9
174 imnan 422 . . . . . . . . 9
175173, 174sylib 196 . . . . . . . 8
176 elin 3686 . . . . . . . 8
177175, 176sylnibr 305 . . . . . . 7
178177eq0rdv 3820 . . . . . 6
179 hashun 12450 . . . . . 6
180132, 134, 178, 179syl3anc 1228 . . . . 5
18125, 131, 1803eqtrd 2502 . . . 4
182 hashcl 12428 . . . . . . 7
183134, 182syl 16 . . . . . 6
184183nn0red 10878 . . . . 5
185 fzfid 12083 . . . . . . . 8
18627, 29sylan 471 . . . . . . . . . 10
187 nnrecre 10597 . . . . . . . . . . 11
188 0re 9617 . . . . . . . . . . 11
189 ifcl 3983 . . . . . . . . . . 11
190187, 188, 189sylancl 662 . . . . . . . . . 10
191186, 190syl 16 . . . . . . . . 9
19228, 191sylan2 474 . . . . . . . 8
193185, 192fsumrecl 13556 . . . . . . 7
1942, 193remulcld 9645 . . . . . 6
195 prmrec.1 . . . . . . . 8
196 prmrec.5 . . . . . . . 8
197 prmrec.6 . . . . . . . 8
198195, 15, 1, 5, 196, 197, 35prmreclem4 14437 . . . . . . 7
199 eluz 11123 . . . . . . . . . 10
20096, 68, 199syl2anc 661 . . . . . . . . 9
201 nnleltp1 10943 . . . . . . . . . 10
2021, 15, 201syl2anc 661 . . . . . . . . 9
203 fzn 11731 . . . . . . . . . 10
20494, 96, 203syl2anc 661 . . . . . . . . 9
205200, 202, 2043bitrd 279 . . . . . . . 8
206 0le0 10650 . . . . . . . . . 10
20724mul01d 9800 . . . . . . . . . 10
208206, 207syl5breqr 4488 . . . . . . . . 9
209 iuneq1 4344 . . . . . . . . . . . . 13
210 0iun 4387 . . . . . . . . . . . . 13
211209, 210syl6eq 2514 . . . . . . . . . . . 12
212211fveq2d 5875 . . . . . . . . . . 11
213 hash0 12437 . . . . . . . . . . 11
214212, 213syl6eq 2514 . . . . . . . . . 10
215 sumeq1 13511 . . . . . . . . . . . 12
216 sum0 13543 . . . . . . . . . . . 12
217215, 216syl6eq 2514 . . . . . . . . . . 11
218217oveq2d 6312 . . . . . . . . . 10
219214, 218breq12d 4465 . . . . . . . . 9
220208, 219syl5ibrcom 222 . . . . . . . 8
221205, 220sylbid 215 . . . . . . 7
222 uztric 11131 . . . . . . . 8
22368, 96, 222syl2anc 661 . . . . . . 7
224198, 221, 223mpjaod 381 . . . . . 6
225 eqid 2457 . . . . . . . . . 10
226 eleq1 2529 . . . . . . . . . . . . 13
227 oveq2 6304 . . . . . . . . . . . . 13
228226, 227ifbieq1d 3964 . . . . . . . . . . . 12