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