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

Theorem prmreclem4 14437
 Description: Lemma for prmrec 14440. Show by induction that the indexed (nondisjoint) union  is at most the size of the prime reciprocal series. The key counting lemma is hashdvds 14305, to show that the number of numbers in that divide is at most . (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
prmreclem4
Distinct variable groups:   ,,,   ,,,   ,M,,   ,,,   ,   ,N`,,

Proof of Theorem prmreclem4
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq2 6304 . . . . . . 7
21iuneq1d 4355 . . . . . 6
32fveq2d 5875 . . . . 5
41sumeq1d 13523 . . . . . 6
54oveq2d 6312 . . . . 5
63, 5breq12d 4465 . . . 4
76imbi2d 316 . . 3
8 oveq2 6304 . . . . . . 7
98iuneq1d 4355 . . . . . 6
109fveq2d 5875 . . . . 5
118sumeq1d 13523 . . . . . 6
1211oveq2d 6312 . . . . 5
1310, 12breq12d 4465 . . . 4
1413imbi2d 316 . . 3
15 oveq2 6304 . . . . . . 7
1615iuneq1d 4355 . . . . . 6
1716fveq2d 5875 . . . . 5
1815sumeq1d 13523 . . . . . 6
1918oveq2d 6312 . . . . 5
2017, 19breq12d 4465 . . . 4
2120imbi2d 316 . . 3
22 oveq2 6304 . . . . . . 7
2322iuneq1d 4355 . . . . . 6
2423fveq2d 5875 . . . . 5
2522sumeq1d 13523 . . . . . 6
2625oveq2d 6312 . . . . 5
2724, 26breq12d 4465 . . . 4
2827imbi2d 316 . . 3
29 0le0 10650 . . . . . 6
30 prmrec.3 . . . . . . . 8
3130nncnd 10577 . . . . . . 7
3231mul01d 9800 . . . . . 6
3329, 32syl5breqr 4488 . . . . 5
34 prmrec.2 . . . . . . . . . . . 12
3534nnred 10576 . . . . . . . . . . 11
3635ltp1d 10501 . . . . . . . . . 10
3734nnzd 10993 . . . . . . . . . . . 12
3837peano2zd 10997 . . . . . . . . . . 11
39 fzn 11731 . . . . . . . . . . 11
4038, 37, 39syl2anc 661 . . . . . . . . . 10
4136, 40mpbid 210 . . . . . . . . 9
4241iuneq1d 4355 . . . . . . . 8
43 0iun 4387 . . . . . . . 8
4442, 43syl6eq 2514 . . . . . . 7
4544fveq2d 5875 . . . . . 6
46 hash0 12437 . . . . . 6
4745, 46syl6eq 2514 . . . . 5
4841sumeq1d 13523 . . . . . . 7
49 sum0 13543 . . . . . . 7
5048, 49syl6eq 2514 . . . . . 6
5150oveq2d 6312 . . . . 5
5233, 47, 513brtr4d 4482 . . . 4
5352a1i 11 . . 3
54 fzfi 12082 . . . . . . . . . . 11
55 elfzuz 11713 . . . . . . . . . . . . . . 15
5634peano2nnd 10578 . . . . . . . . . . . . . . . . 17
57 eluznn 11181 . . . . . . . . . . . . . . . . 17
5856, 57sylan 471 . . . . . . . . . . . . . . . 16
59 eleq1 2529 . . . . . . . . . . . . . . . . . . . . 21
60 breq1 4455 . . . . . . . . . . . . . . . . . . . . 21
6159, 60anbi12d 710 . . . . . . . . . . . . . . . . . . . 20
6261rabbidv 3101 . . . . . . . . . . . . . . . . . . 19
63 prmrec.7 . . . . . . . . . . . . . . . . . . 19
64 ovex 6324 . . . . . . . . . . . . . . . . . . . 20
6564rabex 4603 . . . . . . . . . . . . . . . . . . 19
6662, 63, 65fvmpt 5956 . . . . . . . . . . . . . . . . . 18
6766adantl 466 . . . . . . . . . . . . . . . . 17
68 ssrab2 3584 . . . . . . . . . . . . . . . . 17
6967, 68syl6eqss 3553 . . . . . . . . . . . . . . . 16
7058, 69syldan 470 . . . . . . . . . . . . . . 15
7155, 70sylan2 474 . . . . . . . . . . . . . 14
7271ralrimiva 2871 . . . . . . . . . . . . 13
7372adantr 465 . . . . . . . . . . . 12
74 iunss 4371 . . . . . . . . . . . 12
7573, 74sylibr 212 . . . . . . . . . . 11
76 ssfi 7760 . . . . . . . . . . 11
7754, 75, 76sylancr 663 . . . . . . . . . 10
78 hashcl 12428 . . . . . . . . . 10
7977, 78syl 16 . . . . . . . . 9
8079nn0red 10878 . . . . . . . 8
8130nnred 10576 . . . . . . . . . 10
8281adantr 465 . . . . . . . . 9
83 fzfid 12083 . . . . . . . . . 10
8456adantr 465 . . . . . . . . . . . 12
8584, 55, 57syl2an 477 . . . . . . . . . . 11
86 nnrecre 10597 . . . . . . . . . . . 12
87 0re 9617 . . . . . . . . . . . 12
88 ifcl 3983 . . . . . . . . . . . 12
8986, 87, 88sylancl 662 . . . . . . . . . . 11
9085, 89syl 16 . . . . . . . . . 10
9183, 90fsumrecl 13556 . . . . . . . . 9
9282, 91remulcld 9645 . . . . . . . 8
93 prmnn 14220 . . . . . . . . . . . 12
94 nnrecre 10597 . . . . . . . . . . . 12
9593, 94syl 16 . . . . . . . . . . 11
9695adantl 466 . . . . . . . . . 10
97 0red 9618 . . . . . . . . . 10
9896, 97ifclda 3973 . . . . . . . . 9
9982, 98remulcld 9645 . . . . . . . 8
10080, 92, 99leadd1d 10171 . . . . . . 7
101 eluzp1p1 11135 . . . . . . . . . . . . 13
102101adantl 466 . . . . . . . . . . . 12
103 simpl 457 . . . . . . . . . . . . 13
104 elfzuz 11713 . . . . . . . . . . . . 13
10589recnd 9643 . . . . . . . . . . . . . 14
10658, 105syl 16 . . . . . . . . . . . . 13
107103, 104, 106syl2an 477 . . . . . . . . . . . 12
108 eleq1 2529 . . . . . . . . . . . . 13
109 oveq2 6304 . . . . . . . . . . . . 13
110108, 109ifbieq1d 3964 . . . . . . . . . . . 12
111102, 107, 110fsumm1 13566 . . . . . . . . . . 11
112 eluzelz 11119 . . . . . . . . . . . . . . . . 17
113112adantl 466 . . . . . . . . . . . . . . . 16
114113zcnd 10995 . . . . . . . . . . . . . . 15
115 ax-1cn 9571 . . . . . . . . . . . . . . 15
116 pncan 9849 . . . . . . . . . . . . . . 15
117114, 115, 116sylancl 662 . . . . . . . . . . . . . 14
118117oveq2d 6312 . . . . . . . . . . . . 13
119118sumeq1d 13523 . . . . . . . . . . . 12
120119oveq1d 6311 . . . . . . . . . . 11
121111, 120eqtrd 2498 . . . . . . . . . 10
122121oveq2d 6312 . . . . . . . . 9
12331adantr 465 . . . . . . . . . 10
12491recnd 9643 . . . . . . . . . 10
12598recnd 9643 . . . . . . . . . 10
126123, 124, 125adddid 9641 . . . . . . . . 9
127122, 126eqtrd 2498 . . . . . . . 8
128127breq2d 4464 . . . . . . 7
129100, 128bitr4d 256 . . . . . 6
130104, 70sylan2 474 . . . . . . . . . . . . . 14
131130ralrimiva 2871 . . . . . . . . . . . . 13
132131adantr 465 . . . . . . . . . . . 12
133 iunss 4371 . . . . . . . . . . . 12
134132, 133sylibr 212 . . . . . . . . . . 11
135 ssfi 7760 . . . . . . . . . . 11
13654, 134, 135sylancr 663 . . . . . . . . . 10
137 hashcl 12428 . . . . . . . . . 10
138136, 137syl 16 . . . . . . . . 9
139138nn0red 10878 . . . . . . . 8
140 eluznn 11181 . . . . . . . . . . . . . . 15
14134, 140sylan 471 . . . . . . . . . . . . . 14
142141peano2nnd 10578 . . . . . . . . . . . . 13
14369ralrimiva 2871 . . . . . . . . . . . . . 14
144143adantr 465 . . . . . . . . . . . . 13
145 fveq2 5871 . . . . . . . . . . . . . . 15
146145sseq1d 3530 . . . . . . . . . . . . . 14
147146rspcv 3206 . . . . . . . . . . . . 13
148142, 144, 147sylc 60 . . . . . . . . . . . 12
149 ssfi 7760 . . . . . . . . . . . 12
15054, 148, 149sylancr 663 . . . . . . . . . . 11
151 hashcl 12428 . . . . . . . . . . 11
152150, 151syl 16 . . . . . . . . . 10
153152nn0red 10878 . . . . . . . . 9
15480, 153readdcld 9644 . . . . . . . 8
15580, 99readdcld 9644 . . . . . . . 8
15638adantr 465 . . . . . . . . . . . . 13
157 simpr 461 . . . . . . . . . . . . . 14
15834nncnd 10577 . . . . . . . . . . . . . . . . 17
159158adantr 465 . . . . . . . . . . . . . . . 16
160 pncan 9849 . . . . . . . . . . . . . . . 16
161159, 115, 160sylancl 662 . . . . . . . . . . . . . . 15
162161fveq2d 5875 . . . . . . . . . . . . . 14
163157, 162eleqtrrd 2548 . . . . . . . . . . . . 13
164 fzsuc2 11766 . . . . . . . . . . . . 13
165156, 163, 164syl2anc 661 . . . . . . . . . . . 12
166165iuneq1d 4355 . . . . . . . . . . 11
167 iunxun 4412 . . . . . . . . . . . 12
168 ovex 6324 . . . . . . . . . . . . . 14
169168, 145iunxsn 4410 . . . . . . . . . . . . 13
170169uneq2i 3654 . . . . . . . . . . . 12
171167, 170eqtri 2486 . . . . . . . . . . 11
172166, 171syl6eq 2514 . . . . . . . . . 10
173172fveq2d 5875 . . . . . . . . 9
174 hashun2 12451 . . . . . . . . . 10
17577, 150, 174syl2anc 661 . . . . . . . . 9
176173, 175eqbrtrd 4472 . . . . . . . 8
17782, 142nndivred 10609 . . . . . . . . . . . . . 14
178 flle 11936 . . . . . . . . . . . . . 14
179177, 178syl 16 . . . . . . . . . . . . 13
180 elfznn 11743 . . . . . . . . . . . . . . . . . . 19
181180nncnd 10577 . . . . . . . . . . . . . . . . . 18
182181subid1d 9943 . . . . . . . . . . . . . . . . 17
183182breq2d 4464 . . . . . . . . . . . . . . . 16
184183rabbiia 3098 . . . . . . . . . . . . . . 15
185184fveq2i 5874 . . . . . . . . . . . . . 14
186 1zzd 10920 . . . . . . . . . . . . . . . 16
18730nnnn0d 10877 . . . . . . . . . . . . . . . . . 18
188 nn0uz 11144 . . . . . . . . . . . . . . . . . . 19
189 1m1e0 10629 . . . . . . . . . . . . . . . . . . . 20
190189fveq2i 5874 . . . . . . . . . . . . . . . . . . 19
191188, 190eqtr4i 2489 . . . . . . . . . . . . . . . . . 18
192187, 191syl6eleq 2555 . . . . . . . . . . . . . . . . 17
193192adantr 465 . . . . . . . . . . . . . . . 16
194 0zd 10901 . . . . . . . . . . . . . . . 16
195142, 186, 193, 194hashdvds 14305 . . . . . . . . . . . . . . 15
196123subid1d 9943 . . . . . . . . . . . . . . . . . 18
197196oveq1d 6311 . . . . . . . . . . . . . . . . 17
198197fveq2d 5875 . . . . . . . . . . . . . . . 16