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

Theorem abelthlem9 19832
 Description: Lemma for abelth 19833. By adjusting the constant term, we can assume that the entire series converges to . (Contributed by Mario Carneiro, 1-Apr-2015.)
Hypotheses
Ref Expression
abelth.1
abelth.2
abelth.3
abelth.4
abelth.5
abelth.6
Assertion
Ref Expression
abelthlem9
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,   ,,,,   ,,   ,,,,
Allowed substitution hints:   ()   ()   (,,)

Proof of Theorem abelthlem9
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abelth.1 . . . . . . 7
2 0nn0 9996 . . . . . . . 8
32a1i 10 . . . . . . 7
4 ffvelrn 5679 . . . . . . 7
51, 3, 4syl2an 463 . . . . . 6
6 nn0uz 10278 . . . . . . . 8
7 0z 10051 . . . . . . . . 9
87a1i 10 . . . . . . . 8
9 eqidd 2297 . . . . . . . 8
10 ffvelrn 5679 . . . . . . . . 9
111, 10sylan 457 . . . . . . . 8
12 abelth.2 . . . . . . . 8
136, 8, 9, 11, 12isumcl 12240 . . . . . . 7
1413adantr 451 . . . . . 6
155, 14subcld 9173 . . . . 5
16 ffvelrn 5679 . . . . . 6
171, 16sylan 457 . . . . 5
18 ifcl 3614 . . . . 5
1915, 17, 18syl2anc 642 . . . 4
20 eqid 2296 . . . 4
2119, 20fmptd 5700 . . 3
222a1i 10 . . . . . 6
23 ffvelrn 5679 . . . . . . 7
2421, 23sylan 457 . . . . . 6
25 1e0p1 10168 . . . . . . . . . 10
26 1z 10069 . . . . . . . . . 10
2725, 26eqeltrri 2367 . . . . . . . . 9
2827a1i 10 . . . . . . . 8
29 nnuz 10279 . . . . . . . . . . 11
3025fveq2i 5544 . . . . . . . . . . 11
3129, 30eqtri 2316 . . . . . . . . . 10
3231eleq2i 2360 . . . . . . . . 9
33 nnnn0 9988 . . . . . . . . . . . 12
3433adantl 452 . . . . . . . . . . 11
35 eqeq1 2302 . . . . . . . . . . . . 13
36 fveq2 5541 . . . . . . . . . . . . 13
3735, 36ifbieq2d 3598 . . . . . . . . . . . 12
38 ovex 5899 . . . . . . . . . . . . 13
39 fvex 5555 . . . . . . . . . . . . 13
4038, 39ifex 3636 . . . . . . . . . . . 12
4137, 20, 40fvmpt 5618 . . . . . . . . . . 11
4234, 41syl 15 . . . . . . . . . 10
43 nnne0 9794 . . . . . . . . . . . . 13
4443adantl 452 . . . . . . . . . . . 12
4544neneqd 2475 . . . . . . . . . . 11
46 iffalse 3585 . . . . . . . . . . 11
4745, 46syl 15 . . . . . . . . . 10
4842, 47eqtrd 2328 . . . . . . . . 9
4932, 48sylan2br 462 . . . . . . . 8
5028, 49seqfeq 11087 . . . . . . 7
516, 8, 9, 11, 12isumclim2 12237 . . . . . . . . 9
526, 22, 17, 51clim2ser 12144 . . . . . . . 8
53 seq1 11075 . . . . . . . . . 10
547, 53ax-mp 8 . . . . . . . . 9
5554oveq2i 5885 . . . . . . . 8
5652, 55syl6breq 4078 . . . . . . 7
5750, 56eqbrtrd 4059 . . . . . 6
586, 22, 24, 57clim2ser2 12145 . . . . 5
59 seq1 11075 . . . . . . . . 9
607, 59ax-mp 8 . . . . . . . 8
61 iftrue 3584 . . . . . . . . . 10
6261, 20, 38fvmpt 5618 . . . . . . . . 9
632, 62ax-mp 8 . . . . . . . 8
6460, 63eqtri 2316 . . . . . . 7
6564oveq2i 5885 . . . . . 6
661, 2, 4sylancl 643 . . . . . . 7
67 npncan2 9090 . . . . . . 7
6813, 66, 67syl2anc 642 . . . . . 6
6965, 68syl5eq 2340 . . . . 5
7058, 69breqtrd 4063 . . . 4
71 seqex 11064 . . . . 5
72 c0ex 8848 . . . . 5
7371, 72breldm 4899 . . . 4
7470, 73syl 15 . . 3
75 abelth.3 . . 3
76 abelth.4 . . 3
77 abelth.5 . . 3
78 eqid 2296 . . 3
7921, 74, 75, 76, 77, 78, 70abelthlem8 19831 . 2
801, 12, 75, 76, 77abelthlem2 19824 . . . . . . . . . . . . . 14
8180simpld 445 . . . . . . . . . . . . 13
8281adantr 451 . . . . . . . . . . . 12
8341adantl 452 . . . . . . . . . . . . . . 15
84 oveq1 5881 . . . . . . . . . . . . . . . 16
85 nn0z 10062 . . . . . . . . . . . . . . . . 17
86 1exp 11147 . . . . . . . . . . . . . . . . 17
8785, 86syl 15 . . . . . . . . . . . . . . . 16
8884, 87sylan9eq 2348 . . . . . . . . . . . . . . 15
8983, 88oveq12d 5892 . . . . . . . . . . . . . 14
9089sumeq2dv 12192 . . . . . . . . . . . . 13
91 sumex 12176 . . . . . . . . . . . . 13
9290, 78, 91fvmpt 5618 . . . . . . . . . . . 12
9382, 92syl 15 . . . . . . . . . . 11
947a1i 10 . . . . . . . . . . . 12
9541adantl 452 . . . . . . . . . . . . 13
9666, 13subcld 9173 . . . . . . . . . . . . . . . 16
9796ad2antrr 706 . . . . . . . . . . . . . . 15
98 ffvelrn 5679 . . . . . . . . . . . . . . . . 17
991, 98sylan 457 . . . . . . . . . . . . . . . 16
10099adantlr 695 . . . . . . . . . . . . . . 15
101 ifcl 3614 . . . . . . . . . . . . . . 15
10297, 100, 101syl2anc 642 . . . . . . . . . . . . . 14
103102mulid1d 8868 . . . . . . . . . . . . 13
10495, 103eqtr4d 2331 . . . . . . . . . . . 12
105103, 102eqeltrd 2370 . . . . . . . . . . . 12
106 oveq1 5881 . . . . . . . . . . . . . . . . . . . . . . 23
107 nn0z 10062 . . . . . . . . . . . . . . . . . . . . . . . 24
108 1exp 11147 . . . . . . . . . . . . . . . . . . . . . . . 24
109107, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . 23
110106, 109sylan9eq 2348 . . . . . . . . . . . . . . . . . . . . . 22
111110oveq2d 5890 . . . . . . . . . . . . . . . . . . . . 21
112111sumeq2dv 12192 . . . . . . . . . . . . . . . . . . . 20
113 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . 22
114113oveq1d 5889 . . . . . . . . . . . . . . . . . . . . 21
115114cbvsumv 12185 . . . . . . . . . . . . . . . . . . . 20
116112, 115syl6eq 2344 . . . . . . . . . . . . . . . . . . 19
117 abelth.6 . . . . . . . . . . . . . . . . . . 19
118 sumex 12176 . . . . . . . . . . . . . . . . . . 19
119116, 117, 118fvmpt 5618 . . . . . . . . . . . . . . . . . 18
12081, 119syl 15 . . . . . . . . . . . . . . . . 17
12111mulid1d 8868 . . . . . . . . . . . . . . . . . 18
122121sumeq2dv 12192 . . . . . . . . . . . . . . . . 17
123120, 122eqtrd 2328 . . . . . . . . . . . . . . . 16
124123oveq1d 5889 . . . . . . . . . . . . . . 15
12513subidd 9161 . . . . . . . . . . . . . . 15
126124, 125eqtrd 2328 . . . . . . . . . . . . . 14
12770, 126breqtrrd 4065 . . . . . . . . . . . . 13
128127adantr 451 . . . . . . . . . . . 12
1296, 94, 104, 105, 128isumclim 12236 . . . . . . . . . . 11
13093, 129eqtrd 2328 . . . . . . . . . 10
131 oveq1 5881 . . . . . . . . . . . . . . 15
13241, 131oveqan12rd 5894 . . . . . . . . . . . . . 14
133132sumeq2dv 12192 . . . . . . . . . . . . 13
134 sumex 12176 . . . . . . . . . . . . 13
135133, 78, 134fvmpt 5618 . . . . . . . . . . . 12
136135adantl 452 . . . . . . . . . . 11
137 oveq2 5882 . . . . . . . . . . . . . . 15
13837, 137oveq12d 5892 . . . . . . . . . . . . . 14
139 eqid 2296 . . . . . . . . . . . . . 14
140 ovex 5899 . . . . . . . . . . . . . 14
141138, 139, 140fvmpt 5618 . . . . . . . . . . . . 13
142141adantl 452 . . . . . . . . . . . 12
143 ssrab2 3271 . . . . . . . . . . . . . . . . 17
14477, 143eqsstri 3221 . . . . . . . . . . . . . . . 16
145144a1i 10 . . . . . . . . . . . . . . 15
146145sselda 3193 . . . . . . . . . . . . . 14
147 expcl 11137 . . . . . . . . . . . . . 14
148146, 147sylan 457 . . . . . . . . . . . . 13
149102, 148mulcld 8871 . . . . . . . . . . . 12
1502a1i 10 . . . . . . . . . . . . . 14
15119adantlr 695 . . . . . . . . . . . . . . . . 17
152 expcl 11137 . . . . . . . . . . . . . . . . . 18
153146, 152sylan 457 . . . . . . . . . . . . . . . . 17
154151, 153mulcld 8871 . . . . . . . . . . . . . . . 16
155154, 139fmptd 5700 . . . . . . . . . . . . . . 15
156 ffvelrn 5679 . . . . . . . . . . . . . . 15
157155, 156sylan 457 . . . . . . . . . . . . . 14
15847oveq1d 5889 . . . . . . . . . . . . . . . . . . 19
15934, 141syl 15 . . . . . . . . . . . . . . . . . . 19
16036, 137oveq12d 5892 . . . . . . . . . . . . . . . . . . . . 21
161 eqid 2296 . . . . . . . . . . . . . . . . . . . . 21
162 ovex 5899 . . . . . . . . . . . . . . . . . . . . 21
163160, 161, 162fvmpt 5618 . . . . . . . . . . . . . . . . . . . 20
16434, 163syl 15 . . . . . . . . . . . . . . . . . . 19
165158, 159, 1643eqtr4d 2338 . . . . . . . . . . . . . . . . . 18
16632, 165sylan2br 462 . . . . . . . . . . . . . . . . 17
16728, 166seqfeq 11087 . . . . . . . . . . . . . . . 16
168167adantr 451 . . . . . . . . . . . . . . 15
16917adantlr 695 . . . . . . . . . . . . . . . . . . . 20
170169, 153mulcld 8871 . . . . . . . . . . . . . . . . . . 19
171170, 161fmptd 5700 . . . . . . . . . . . . . . . . . 18
172 ffvelrn 5679 . . . . . . . . . . . . . . . . . 18
173171, 172sylan 457 . . . . . . . . . . . . . . . . 17
174163adantl 452 . . . . . . . . . . . . . . . . . . 19
175100, 148mulcld 8871 . . . . . . . . . . . . . . . . . . 19
1761, 12, 75, 76, 77abelthlem3 19825 . . . . . . . . . . . . . . . . . . 19
1776, 94, 174, 175, 176isumclim2 12237 . . . . . . . . . . . . . . . . . 18
178 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . 23
179 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . 23
180178, 179oveq12d 5892 . . . . . . . . . . . . . . . . . . . . . 22
181180cbvsumv 12185 . . . . . . . . . . . . . . . . . . . . 21
182131oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . 22
183182sumeq2sdv 12193 . . . . . . . . . . . . . . . . . . . . 21
184181, 183syl5eq 2340 . . . . . . . . . . . . . . . . . . . 20
185 sumex 12176 . . . . . . . . . . . . . . . . . . . 20
186184, 117, 185fvmpt 5618 . . . . . . . . . . . . . . . . . . 19
187186adantl 452 . . . . . . . . . . . . . . . . . 18
188177, 187breqtrrd 4065 . . . . . . . . . . . . . . . . 17
1896, 150, 173, 188clim2ser 12144 . . . . . . . . . . . . . . . 16
190 seq1 11075 . . . . . . . . . . . . . . . . . . . 20
1917, 190ax-mp 8 . . . . . . . . . . . . . . . . . . 19
192 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . 22
193 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . 22
194192, 193oveq12d 5892 . . . . . . . . . . . . . . . . . . . . 21
195 ovex 5899 . . . . . . . . . . . . . . . . . . . . 21
196194, 161, 195fvmpt 5618 . . . . . . . . . . . . . . . . . . . 20
1972, 196ax-mp 8 . . . . . . . . . . . . . . . . . . 19
198191, 197eqtri 2316 . . . . . . . . . . . . . . . . . 18
199146exp0d 11255 . . . . . . . . . . . . . . . . . . . 20
200199oveq2d 5890 . . . . . . . . . . . . . . . . . . 19
20166adantr 451 . . . . . . . . . . . . . . . . . . . 20
202201mulid1d 8868 . . . . . . . . . . . . . . . . . . 19
203200, 202eqtrd 2328 . . . . . . . . . . . . . . . . . 18
204198, 203syl5eq 2340 . . . . . . . . . . . . . . . . 17
205204oveq2d 5890 . . . . . . . . . . . . . . . 16
206189, 205breqtrd 4063 . . . . . . . . . . . . . . 15
207168, 206eqbrtrd 4059 . . . . . . . . . . . . . 14
2086, 150, 157, 207clim2ser2 12145 . . . . . . . . . . . . 13
209 seq1 11075 . . . . . . . . . . . . . . . . . 18
2107, 209ax-mp 8 . . . . . . . . . . . . . . . . 17
21161, 193oveq12d 5892 . . . . . . . . . . . . . . . . . . 19
212 ovex 5899 . . . . . . . . . . . . . . . . . . 19
213211, 139, 212fvmpt 5618 . . . . . . . . . . . . . . . . . 18
2142, 213ax-mp 8 . . . . . . . . . . . . . . . . 17
215210, 214eqtri 2316 . . . . . . . . . . . . . . . 16
216199oveq2d 5890 . . . . . . . . . . . . . . . . 17
21713adantr 451 . . . . . . . . . . . . . . . . . . 19
218201, 217subcld 9173 . . . . . . . . . . . . . . . . . 18
219218mulid1d 8868 . . . . . . . . . . . . . . . . 17
220216, 219eqtrd 2328 . . . . . . . . . . . . . . . 16
221215, 220syl5eq 2340 . . . . . . . . . . . . . . 15
222221oveq2d 5890 . . . . . . . . . . . . . 14
2231, 12, 75, 76, 77, 117abelthlem4 19826 . . . . . . . . . . . . . . . 16
224 ffvelrn 5679 . . . . . . . . . . . . . . . 16
225223, 224sylan 457 . . . . . . . . . . . . . . 15
226225, 201, 217npncand 9197 . . . . . . . . . . . . . 14
227222, 226eqtrd 2328 . . . . . . . . . . . . 13
228208, 227breqtrd 4063 . . . . . . . . . . . 12
2296, 94, 142, 149, 228isumclim 12236 . . . . . . . . . . 11
230136, 229eqtrd 2328 . . . . . . . . . 10
231130, 230oveq12d 5892 . . . . . . . . 9
232223adantr 451 . . . . . . . . . . 11
233 ffvelrn 5679 . . . . . . . . . . 11
234232, 82, 233syl2anc 642 . . . . . . . . . 10
235234, 225, 217nnncan2d 9208 . . . . . . . . 9
236231, 235eqtrd 2328 . . . . . . . 8
237236fveq2d 5545 . . . . . . 7
238237breq1d 4049 . . . . . 6
239238imbi2d 307 . . . . 5
240239ralbidva 2572 . . . 4
241240rexbidv 2577 . . 3