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

Theorem climcndslem1 13661
Description: Lemma for climcnds 13663: bound the original series by the condensed series. (Contributed by Mario Carneiro, 18-Jul-2014.)
Hypotheses
Ref Expression
climcnds.1
climcnds.2
climcnds.3
climcnds.4
Assertion
Ref Expression
climcndslem1
Distinct variable groups:   , ,   , ,   , ,

Proof of Theorem climcndslem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 oveq1 6303 . . . . . . . . . . 11
2 0p1e1 10672 . . . . . . . . . . 11
31, 2syl6eq 2514 . . . . . . . . . 10
43oveq2d 6312 . . . . . . . . 9
5 2cn 10631 . . . . . . . . . . 11
6 exp1 12172 . . . . . . . . . . 11
75, 6ax-mp 5 . . . . . . . . . 10
8 df-2 10619 . . . . . . . . . 10
97, 8eqtri 2486 . . . . . . . . 9
104, 9syl6eq 2514 . . . . . . . 8
1110oveq1d 6311 . . . . . . 7
12 ax-1cn 9571 . . . . . . . 8
1312, 12pncan3oi 9859 . . . . . . 7
1411, 13syl6eq 2514 . . . . . 6
1514fveq2d 5875 . . . . 5
16 fveq2 5871 . . . . 5
1715, 16breq12d 4465 . . . 4
1817imbi2d 316 . . 3
19 oveq1 6303 . . . . . . . 8
2019oveq2d 6312 . . . . . . 7
2120oveq1d 6311 . . . . . 6
2221fveq2d 5875 . . . . 5
23 fveq2 5871 . . . . 5
2422, 23breq12d 4465 . . . 4
2524imbi2d 316 . . 3
26 oveq1 6303 . . . . . . . 8
2726oveq2d 6312 . . . . . . 7
2827oveq1d 6311 . . . . . 6
2928fveq2d 5875 . . . . 5
30 fveq2 5871 . . . . 5
3129, 30breq12d 4465 . . . 4
3231imbi2d 316 . . 3
33 oveq1 6303 . . . . . . . 8
3433oveq2d 6312 . . . . . . 7
3534oveq1d 6311 . . . . . 6
3635fveq2d 5875 . . . . 5
37 fveq2 5871 . . . . 5
3836, 37breq12d 4465 . . . 4
3938imbi2d 316 . . 3
40 1nn 10572 . . . . . . 7
41 climcnds.1 . . . . . . . 8
4241ralrimiva 2871 . . . . . . 7
43 fveq2 5871 . . . . . . . . 9
4443eleq1d 2526 . . . . . . . 8
4544rspcv 3206 . . . . . . 7
4640, 42, 45mpsyl 63 . . . . . 6
4746leidd 10144 . . . . 5
4846recnd 9643 . . . . . 6
4948mulid2d 9635 . . . . 5
5047, 49breqtrrd 4478 . . . 4
51 1z 10919 . . . . 5
52 eqidd 2458 . . . . 5
5351, 52seq1i 12121 . . . 4
54 0z 10900 . . . . 5
55 0nn0 10835 . . . . . 6
56 climcnds.4 . . . . . . 7
5756ralrimiva 2871 . . . . . 6
58 fveq2 5871 . . . . . . . 8
59 oveq2 6304 . . . . . . . . . 10
60 exp0 12170 . . . . . . . . . . 11
615, 60ax-mp 5 . . . . . . . . . 10
6259, 61syl6eq 2514 . . . . . . . . 9
6362fveq2d 5875 . . . . . . . . 9
6462, 63oveq12d 6314 . . . . . . . 8
6558, 64eqeq12d 2479 . . . . . . 7
6665rspcv 3206 . . . . . 6
6755, 57, 66mpsyl 63 . . . . 5
6854, 67seq1i 12121 . . . 4
6950, 53, 683brtr4d 4482 . . 3
70 fzfid 12083 . . . . . . . . 9
71 simpl 457 . . . . . . . . . . 11
7271adantr 465 . . . . . . . . . 10
73 2nn 10718 . . . . . . . . . . . 12
74 peano2nn0 10861 . . . . . . . . . . . . 13
7574adantl 466 . . . . . . . . . . . 12
76 nnexpcl 12179 . . . . . . . . . . . 12
7773, 75, 76sylancr 663 . . . . . . . . . . 11
78 elfzuz 11713 . . . . . . . . . . 11
79 eluznn 11181 . . . . . . . . . . 11
8077, 78, 79syl2an 477 . . . . . . . . . 10
8172, 80, 41syl2anc 661 . . . . . . . . 9
8242adantr 465 . . . . . . . . . . 11
83 fveq2 5871 . . . . . . . . . . . . 13
8483eleq1d 2526 . . . . . . . . . . . 12
8584rspcv 3206 . . . . . . . . . . 11
8677, 82, 85sylc 60 . . . . . . . . . 10
8786adantr 465 . . . . . . . . 9
88 simpr 461 . . . . . . . . . . . 12
89 simplll 759 . . . . . . . . . . . . 13
9077adantr 465 . . . . . . . . . . . . . 14
91 elfzuz 11713 . . . . . . . . . . . . . 14
9290, 91, 79syl2an 477 . . . . . . . . . . . . 13
9389, 92, 41syl2anc 661 . . . . . . . . . . . 12
94 simplll 759 . . . . . . . . . . . . 13
95 elfzuz 11713 . . . . . . . . . . . . . 14
9690, 95, 79syl2an 477 . . . . . . . . . . . . 13
97 climcnds.3 . . . . . . . . . . . . 13
9894, 96, 97syl2anc 661 . . . . . . . . . . . 12
9988, 93, 98monoord2 12138 . . . . . . . . . . 11
10099ralrimiva 2871 . . . . . . . . . 10
101 fveq2 5871 . . . . . . . . . . . 12
102101breq1d 4462 . . . . . . . . . . 11
103102rspccva 3209 . . . . . . . . . 10
104100, 78, 103syl2an 477 . . . . . . . . 9
10570, 81, 87, 104fsumle 13613 . . . . . . . 8
106 fzfid 12083 . . . . . . . . . . . . 13
107 hashcl 12428 . . . . . . . . . . . . 13
108106, 107syl 16 . . . . . . . . . . . 12
109108nn0cnd 10879 . . . . . . . . . . 11
11077nnred 10576 . . . . . . . . . . . 12
111110recnd 9643 . . . . . . . . . . 11
112 hashcl 12428 . . . . . . . . . . . . 13
11370, 112syl 16 . . . . . . . . . . . 12
114113nn0cnd 10879 . . . . . . . . . . 11
115 2z 10921 . . . . . . . . . . . . . . . . . . . 20
116 zexpcl 12181 . . . . . . . . . . . . . . . . . . . 20
117115, 75, 116sylancr 663 . . . . . . . . . . . . . . . . . . 19
118 nn0p1nn 10860 . . . . . . . . . . . . . . . . . . . . . . 23
119118adantl 466 . . . . . . . . . . . . . . . . . . . . . 22
120 nnuz 11145 . . . . . . . . . . . . . . . . . . . . . 22
121119, 120syl6eleq 2555 . . . . . . . . . . . . . . . . . . . . 21
122 2re 10630 . . . . . . . . . . . . . . . . . . . . . 22
123 1le2 10774 . . . . . . . . . . . . . . . . . . . . . 22
124 leexp2a 12221 . . . . . . . . . . . . . . . . . . . . . 22
125122, 123, 124mp3an12 1314 . . . . . . . . . . . . . . . . . . . . 21
126121, 125syl 16 . . . . . . . . . . . . . . . . . . . 20
1277, 126syl5eqbrr 4486 . . . . . . . . . . . . . . . . . . 19
128115eluz1i 11117 . . . . . . . . . . . . . . . . . . 19
129117, 127, 128sylanbrc 664 . . . . . . . . . . . . . . . . . 18
130 uz2m1nn 11185 . . . . . . . . . . . . . . . . . 18
131129, 130syl 16 . . . . . . . . . . . . . . . . 17
132131, 120syl6eleq 2555 . . . . . . . . . . . . . . . 16
133 peano2zm 10932 . . . . . . . . . . . . . . . . . 18
134117, 133syl 16 . . . . . . . . . . . . . . . . 17
135 peano2nn0 10861 . . . . . . . . . . . . . . . . . . . 20
13675, 135syl 16 . . . . . . . . . . . . . . . . . . 19
137 zexpcl 12181 . . . . . . . . . . . . . . . . . . 19
138115, 136, 137sylancr 663 . . . . . . . . . . . . . . . . . 18
139 peano2zm 10932 . . . . . . . . . . . . . . . . . 18
140138, 139syl 16 . . . . . . . . . . . . . . . . 17
141117zred 10994 . . . . . . . . . . . . . . . . . 18
142138zred 10994 . . . . . . . . . . . . . . . . . 18
143 1red 9632 . . . . . . . . . . . . . . . . . 18
14475nn0zd 10992 . . . . . . . . . . . . . . . . . . 19
145 uzid 11124 . . . . . . . . . . . . . . . . . . 19
146 peano2uz 11163 . . . . . . . . . . . . . . . . . . 19
147 leexp2a 12221 . . . . . . . . . . . . . . . . . . . 20
148122, 123, 147mp3an12 1314 . . . . . . . . . . . . . . . . . . 19
149144, 145, 146, 1484syl 21 . . . . . . . . . . . . . . . . . 18
150141, 142, 143, 149lesub1dd 10193 . . . . . . . . . . . . . . . . 17
151 eluz2 11116 . . . . . . . . . . . . . . . . 17
152134, 140, 150, 151syl3anbrc 1180 . . . . . . . . . . . . . . . 16
153 elfzuzb 11711 . . . . . . . . . . . . . . . 16
154132, 152, 153sylanbrc 664 . . . . . . . . . . . . . . 15
155 fzsplit 11740 . . . . . . . . . . . . . . 15
156154, 155syl 16 . . . . . . . . . . . . . 14
157 npcan 9852 . . . . . . . . . . . . . . . . 17
158111, 12, 157sylancl 662 . . . . . . . . . . . . . . . 16
159158oveq1d 6311 . . . . . . . . . . . . . . 15
160159uneq2d 3657 . . . . . . . . . . . . . 14
161156, 160eqtrd 2498 . . . . . . . . . . . . 13
162161fveq2d 5875 . . . . . . . . . . . 12
163 expp1 12173 . . . . . . . . . . . . . . . . 17
1645, 75, 163sylancr 663 . . . . . . . . . . . . . . . 16
165111times2d 10807 . . . . . . . . . . . . . . . 16
166164, 165eqtrd 2498 . . . . . . . . . . . . . . 15
167166oveq1d 6311 . . . . . . . . . . . . . 14
168 1cnd 9633 . . . . . . . . . . . . . . 15
169111, 111, 168addsubd 9975 . . . . . . . . . . . . . 14
170167, 169eqtrd 2498 . . . . . . . . . . . . 13
171 uztrn 11126 . . . . . . . . . . . . . . . . 17
172152, 132, 171syl2anc 661 . . . . . . . . . . . . . . . 16
173172, 120syl6eleqr 2556 . . . . . . . . . . . . . . 15
174173nnnn0d 10877 . . . . . . . . . . . . . 14
175 hashfz1 12419 . . . . . . . . . . . . . 14
176174, 175syl 16 . . . . . . . . . . . . 13
177131nnnn0d 10877 . . . . . . . . . . . . . . 15
178 hashfz1 12419 . . . . . . . . . . . . . . 15
179177, 178syl 16 . . . . . . . . . . . . . 14
180179oveq1d 6311 . . . . . . . . . . . . 13
181170, 176, 1803eqtr4d 2508 . . . . . . . . . . . 12
182110ltm1d 10503 . . . . . . . . . . . . . 14
183 fzdisj 11741 . . . . . . . . . . . . . 14
184182, 183syl 16 . . . . . . . . . . . . 13
185 hashun 12450 . . . . . . . . . . . . 13
186106, 70, 184, 185syl3anc 1228 . . . . . . . . . . . 12
187162, 181, 1863eqtr3d 2506 . . . . . . . . . . 11
188109, 111, 114, 187addcanad 9806 . . . . . . . . . 10
189188oveq1d 6311 . . . . . . . . 9
19057adantr 465 . . . . . . . . . 10
191 fveq2 5871 . . . . . . . . . . . 12
192 oveq2 6304 . . . . . . . . . . . . 13
193192fveq2d 5875 . . . . . . . . . . . . 13
194192, 193oveq12d 6314 . . . . . . . . . . . 12
195191, 194eqeq12d 2479 . . . . . . . . . . 11
196195rspcv 3206 . . . . . . . . . 10
19775, 190, 196sylc 60 . . . . . . . . 9
19886recnd 9643 . . . . . . . . . 10
199 fsumconst 13605 . . . . . . . . . 10
20070, 198, 199syl2anc 661 . . . . . . . . 9
201189, 197, 2003eqtr4d 2508 . . . . . . . 8
202105, 201breqtrrd 4478 . . . . . . 7
203 elfznn 11743 . . . . . . . . . 10
20471, 203, 41syl2an 477 . . . . . . . . 9
205106, 204fsumrecl 13556 . . . . . . . 8
20670, 81fsumrecl 13556 . . . . . . . 8
207 nn0uz 11144 . . . . . . . . . 10
208 0zd 10901 . . . . . . . . . 10
209 simpr 461 . . . . . . . . . . . . . 14
210 nnexpcl 12179 . . . . . . . . . . . . . 14
21173, 209, 210sylancr 663 . . . . . . . . . . . . 13
212211nnred 10576 . . . . . . . . . . . 12
21342adantr 465 . . . . . . . . . . . . 13
214 fveq2 5871 . . . . . . . . . . . . . . 15
215214eleq1d 2526 . . . . . . . . . . . . . 14
216215rspcv 3206 . . . . . . . . . . . . 13
217211, 213, 216sylc 60 . . . . . . . . . . . 12
218212, 217remulcld 9645 . . . . . . . . . . 11
21956, 218eqeltrd 2545 . . . . . . . . . 10
220207, 208, 219serfre 12136 . . . . . . . . 9
221220ffvelrnda 6031 . . . . . . . 8
222141, 86remulcld 9645 . . . . . . . . 9
223197, 222eqeltrd 2545 . . . . . . . 8
224 le2add 10059 . . . . . . . 8
225205, 206, 221, 223, 224syl22anc 1229 . . . . . . 7
226202, 225mpan2d 674 . . . . . 6
227 eqidd 2458 . . . . . . . . 9
22841recnd 9643 . . . . . . . . . 10
22971, 203, 228syl2an 477 . . . . . . . . 9
230227, 132, 229fsumser 13552 . . . . . . . 8