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

Theorem abelthlem9 20358
 Description: Lemma for abelth 20359. 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 10238 . . . . . . . 8
32a1i 11 . . . . . . 7
4 ffvelrn 5870 . . . . . . 7
51, 3, 4syl2an 465 . . . . . 6
6 nn0uz 10522 . . . . . . . 8
7 0z 10295 . . . . . . . . 9
87a1i 11 . . . . . . . 8
9 eqidd 2439 . . . . . . . 8
101ffvelrnda 5872 . . . . . . . 8
11 abelth.2 . . . . . . . 8
126, 8, 9, 10, 11isumcl 12547 . . . . . . 7
1312adantr 453 . . . . . 6
145, 13subcld 9413 . . . . 5
151ffvelrnda 5872 . . . . 5
16 ifcl 3777 . . . . 5
1714, 15, 16syl2anc 644 . . . 4
18 eqid 2438 . . . 4
1917, 18fmptd 5895 . . 3
202a1i 11 . . . . . 6
2119ffvelrnda 5872 . . . . . 6
22 1e0p1 10412 . . . . . . . . . 10
23 1z 10313 . . . . . . . . . 10
2422, 23eqeltrri 2509 . . . . . . . . 9
2524a1i 11 . . . . . . . 8
26 nnuz 10523 . . . . . . . . . . 11
2722fveq2i 5733 . . . . . . . . . . 11
2826, 27eqtri 2458 . . . . . . . . . 10
2928eleq2i 2502 . . . . . . . . 9
30 nnnn0 10230 . . . . . . . . . . . 12
3130adantl 454 . . . . . . . . . . 11
32 eqeq1 2444 . . . . . . . . . . . . 13
33 fveq2 5730 . . . . . . . . . . . . 13
3432, 33ifbieq2d 3761 . . . . . . . . . . . 12
35 ovex 6108 . . . . . . . . . . . . 13
36 fvex 5744 . . . . . . . . . . . . 13
3735, 36ifex 3799 . . . . . . . . . . . 12
3834, 18, 37fvmpt 5808 . . . . . . . . . . 11
3931, 38syl 16 . . . . . . . . . 10
40 nnne0 10034 . . . . . . . . . . . . 13
4140adantl 454 . . . . . . . . . . . 12
4241neneqd 2619 . . . . . . . . . . 11
43 iffalse 3748 . . . . . . . . . . 11
4442, 43syl 16 . . . . . . . . . 10
4539, 44eqtrd 2470 . . . . . . . . 9
4629, 45sylan2br 464 . . . . . . . 8
4725, 46seqfeq 11350 . . . . . . 7
486, 8, 9, 10, 11isumclim2 12544 . . . . . . . . 9
496, 20, 15, 48clim2ser 12450 . . . . . . . 8
50 seq1 11338 . . . . . . . . . 10
517, 50ax-mp 8 . . . . . . . . 9
5251oveq2i 6094 . . . . . . . 8
5349, 52syl6breq 4253 . . . . . . 7
5447, 53eqbrtrd 4234 . . . . . 6
556, 20, 21, 54clim2ser2 12451 . . . . 5
56 seq1 11338 . . . . . . . . 9
577, 56ax-mp 8 . . . . . . . 8
58 iftrue 3747 . . . . . . . . . 10
5958, 18, 35fvmpt 5808 . . . . . . . . 9
602, 59ax-mp 8 . . . . . . . 8
6157, 60eqtri 2458 . . . . . . 7
6261oveq2i 6094 . . . . . 6
631, 2, 4sylancl 645 . . . . . . 7
64 npncan2 9330 . . . . . . 7
6512, 63, 64syl2anc 644 . . . . . 6
6662, 65syl5eq 2482 . . . . 5
6755, 66breqtrd 4238 . . . 4
68 seqex 11327 . . . . 5
69 c0ex 9087 . . . . 5
7068, 69breldm 5076 . . . 4
7167, 70syl 16 . . 3
72 abelth.3 . . 3
73 abelth.4 . . 3
74 abelth.5 . . 3
75 eqid 2438 . . 3
7619, 71, 72, 73, 74, 75, 67abelthlem8 20357 . 2
771, 11, 72, 73, 74abelthlem2 20350 . . . . . . . . . . . . . 14
7877simpld 447 . . . . . . . . . . . . 13
7978adantr 453 . . . . . . . . . . . 12
8038adantl 454 . . . . . . . . . . . . . . 15
81 oveq1 6090 . . . . . . . . . . . . . . . 16
82 nn0z 10306 . . . . . . . . . . . . . . . . 17
83 1exp 11411 . . . . . . . . . . . . . . . . 17
8482, 83syl 16 . . . . . . . . . . . . . . . 16
8581, 84sylan9eq 2490 . . . . . . . . . . . . . . 15
8680, 85oveq12d 6101 . . . . . . . . . . . . . 14
8786sumeq2dv 12499 . . . . . . . . . . . . 13
88 sumex 12483 . . . . . . . . . . . . 13
8987, 75, 88fvmpt 5808 . . . . . . . . . . . 12
9079, 89syl 16 . . . . . . . . . . 11
917a1i 11 . . . . . . . . . . . 12
9238adantl 454 . . . . . . . . . . . . 13
9363, 12subcld 9413 . . . . . . . . . . . . . . . 16
9493ad2antrr 708 . . . . . . . . . . . . . . 15
951ffvelrnda 5872 . . . . . . . . . . . . . . . 16
9695adantlr 697 . . . . . . . . . . . . . . 15
97 ifcl 3777 . . . . . . . . . . . . . . 15
9894, 96, 97syl2anc 644 . . . . . . . . . . . . . 14
9998mulid1d 9107 . . . . . . . . . . . . 13
10092, 99eqtr4d 2473 . . . . . . . . . . . 12
10199, 98eqeltrd 2512 . . . . . . . . . . . 12
102 oveq1 6090 . . . . . . . . . . . . . . . . . . . . . . 23
103 nn0z 10306 . . . . . . . . . . . . . . . . . . . . . . . 24
104 1exp 11411 . . . . . . . . . . . . . . . . . . . . . . . 24
105103, 104syl 16 . . . . . . . . . . . . . . . . . . . . . . 23
106102, 105sylan9eq 2490 . . . . . . . . . . . . . . . . . . . . . 22
107106oveq2d 6099 . . . . . . . . . . . . . . . . . . . . 21
108107sumeq2dv 12499 . . . . . . . . . . . . . . . . . . . 20
109 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . 22
110109oveq1d 6098 . . . . . . . . . . . . . . . . . . . . 21
111110cbvsumv 12492 . . . . . . . . . . . . . . . . . . . 20
112108, 111syl6eq 2486 . . . . . . . . . . . . . . . . . . 19
113 abelth.6 . . . . . . . . . . . . . . . . . . 19
114 sumex 12483 . . . . . . . . . . . . . . . . . . 19
115112, 113, 114fvmpt 5808 . . . . . . . . . . . . . . . . . 18
11678, 115syl 16 . . . . . . . . . . . . . . . . 17
11710mulid1d 9107 . . . . . . . . . . . . . . . . . 18
118117sumeq2dv 12499 . . . . . . . . . . . . . . . . 17
119116, 118eqtrd 2470 . . . . . . . . . . . . . . . 16
120119oveq1d 6098 . . . . . . . . . . . . . . 15
12112subidd 9401 . . . . . . . . . . . . . . 15
122120, 121eqtrd 2470 . . . . . . . . . . . . . 14
12367, 122breqtrrd 4240 . . . . . . . . . . . . 13
124123adantr 453 . . . . . . . . . . . 12
1256, 91, 100, 101, 124isumclim 12543 . . . . . . . . . . 11
12690, 125eqtrd 2470 . . . . . . . . . 10
127 oveq1 6090 . . . . . . . . . . . . . . 15
12838, 127oveqan12rd 6103 . . . . . . . . . . . . . 14
129128sumeq2dv 12499 . . . . . . . . . . . . 13
130 sumex 12483 . . . . . . . . . . . . 13
131129, 75, 130fvmpt 5808 . . . . . . . . . . . 12
132131adantl 454 . . . . . . . . . . 11
133 oveq2 6091 . . . . . . . . . . . . . . 15
13434, 133oveq12d 6101 . . . . . . . . . . . . . 14
135 eqid 2438 . . . . . . . . . . . . . 14
136 ovex 6108 . . . . . . . . . . . . . 14
137134, 135, 136fvmpt 5808 . . . . . . . . . . . . 13
138137adantl 454 . . . . . . . . . . . 12
139 ssrab2 3430 . . . . . . . . . . . . . . . . 17
14074, 139eqsstri 3380 . . . . . . . . . . . . . . . 16
141140a1i 11 . . . . . . . . . . . . . . 15
142141sselda 3350 . . . . . . . . . . . . . 14
143 expcl 11401 . . . . . . . . . . . . . 14
144142, 143sylan 459 . . . . . . . . . . . . 13
14598, 144mulcld 9110 . . . . . . . . . . . 12
1462a1i 11 . . . . . . . . . . . . . 14
14717adantlr 697 . . . . . . . . . . . . . . . . 17
148 expcl 11401 . . . . . . . . . . . . . . . . . 18
149142, 148sylan 459 . . . . . . . . . . . . . . . . 17
150147, 149mulcld 9110 . . . . . . . . . . . . . . . 16
151150, 135fmptd 5895 . . . . . . . . . . . . . . 15
152151ffvelrnda 5872 . . . . . . . . . . . . . 14
15344oveq1d 6098 . . . . . . . . . . . . . . . . . . 19
15431, 137syl 16 . . . . . . . . . . . . . . . . . . 19
15533, 133oveq12d 6101 . . . . . . . . . . . . . . . . . . . . 21
156 eqid 2438 . . . . . . . . . . . . . . . . . . . . 21
157 ovex 6108 . . . . . . . . . . . . . . . . . . . . 21
158155, 156, 157fvmpt 5808 . . . . . . . . . . . . . . . . . . . 20
15931, 158syl 16 . . . . . . . . . . . . . . . . . . 19
160153, 154, 1593eqtr4d 2480 . . . . . . . . . . . . . . . . . 18
16129, 160sylan2br 464 . . . . . . . . . . . . . . . . 17
16225, 161seqfeq 11350 . . . . . . . . . . . . . . . 16
163162adantr 453 . . . . . . . . . . . . . . 15
16415adantlr 697 . . . . . . . . . . . . . . . . . . . 20
165164, 149mulcld 9110 . . . . . . . . . . . . . . . . . . 19
166165, 156fmptd 5895 . . . . . . . . . . . . . . . . . 18
167166ffvelrnda 5872 . . . . . . . . . . . . . . . . 17
168158adantl 454 . . . . . . . . . . . . . . . . . . 19
16996, 144mulcld 9110 . . . . . . . . . . . . . . . . . . 19
1701, 11, 72, 73, 74abelthlem3 20351 . . . . . . . . . . . . . . . . . . 19
1716, 91, 168, 169, 170isumclim2 12544 . . . . . . . . . . . . . . . . . 18
172 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . . 23
173 oveq2 6091 . . . . . . . . . . . . . . . . . . . . . . 23
174172, 173oveq12d 6101 . . . . . . . . . . . . . . . . . . . . . 22
175174cbvsumv 12492 . . . . . . . . . . . . . . . . . . . . 21
176127oveq2d 6099 . . . . . . . . . . . . . . . . . . . . . 22
177176sumeq2sdv 12500 . . . . . . . . . . . . . . . . . . . . 21
178175, 177syl5eq 2482 . . . . . . . . . . . . . . . . . . . 20
179 sumex 12483 . . . . . . . . . . . . . . . . . . . 20
180178, 113, 179fvmpt 5808 . . . . . . . . . . . . . . . . . . 19
181180adantl 454 . . . . . . . . . . . . . . . . . 18
182171, 181breqtrrd 4240 . . . . . . . . . . . . . . . . 17
1836, 146, 167, 182clim2ser 12450 . . . . . . . . . . . . . . . 16
184 seq1 11338 . . . . . . . . . . . . . . . . . . . 20
1857, 184ax-mp 8 . . . . . . . . . . . . . . . . . . 19
186 fveq2 5730 . . . . . . . . . . . . . . . . . . . . . 22
187 oveq2 6091 . . . . . . . . . . . . . . . . . . . . . 22
188186, 187oveq12d 6101 . . . . . . . . . . . . . . . . . . . . 21
189 ovex 6108 . . . . . . . . . . . . . . . . . . . . 21
190188, 156, 189fvmpt 5808 . . . . . . . . . . . . . . . . . . . 20
1912, 190ax-mp 8 . . . . . . . . . . . . . . . . . . 19
192185, 191eqtri 2458 . . . . . . . . . . . . . . . . . 18
193142exp0d 11519 . . . . . . . . . . . . . . . . . . . 20
194193oveq2d 6099 . . . . . . . . . . . . . . . . . . 19
19563adantr 453 . . . . . . . . . . . . . . . . . . . 20
196195mulid1d 9107 . . . . . . . . . . . . . . . . . . 19
197194, 196eqtrd 2470 . . . . . . . . . . . . . . . . . 18
198192, 197syl5eq 2482 . . . . . . . . . . . . . . . . 17
199198oveq2d 6099 . . . . . . . . . . . . . . . 16
200183, 199breqtrd 4238 . . . . . . . . . . . . . . 15
201163, 200eqbrtrd 4234 . . . . . . . . . . . . . 14
2026, 146, 152, 201clim2ser2 12451 . . . . . . . . . . . . 13
203 seq1 11338 . . . . . . . . . . . . . . . . . 18
2047, 203ax-mp 8 . . . . . . . . . . . . . . . . 17
20558, 187oveq12d 6101 . . . . . . . . . . . . . . . . . . 19
206 ovex 6108 . . . . . . . . . . . . . . . . . . 19
207205, 135, 206fvmpt 5808 . . . . . . . . . . . . . . . . . 18
2082, 207ax-mp 8 . . . . . . . . . . . . . . . . 17
209204, 208eqtri 2458 . . . . . . . . . . . . . . . 16
210193oveq2d 6099 . . . . . . . . . . . . . . . . 17
21112adantr 453 . . . . . . . . . . . . . . . . . . 19
212195, 211subcld 9413 . . . . . . . . . . . . . . . . . 18
213212mulid1d 9107 . . . . . . . . . . . . . . . . 17
214210, 213eqtrd 2470 . . . . . . . . . . . . . . . 16
215209, 214syl5eq 2482 . . . . . . . . . . . . . . 15
216215oveq2d 6099 . . . . . . . . . . . . . 14
2171, 11, 72, 73, 74, 113abelthlem4 20352 . . . . . . . . . . . . . . . 16
218217ffvelrnda 5872 . . . . . . . . . . . . . . 15
219218, 195, 211npncand 9437 . . . . . . . . . . . . . 14
220216, 219eqtrd 2470 . . . . . . . . . . . . 13
221202, 220breqtrd 4238 . . . . . . . . . . . 12
2226, 91, 138, 145, 221isumclim 12543 . . . . . . . . . . 11
223132, 222eqtrd 2470 . . . . . . . . . 10
224126, 223oveq12d 6101 . . . . . . . . 9
225217adantr 453 . . . . . . . . . . 11
226225, 79ffvelrnd 5873 . . . . . . . . . 10
227226, 218, 211nnncan2d 9448 . . . . . . . . 9
228224, 227eqtrd 2470 . . . . . . . 8
229228fveq2d 5734 . . . . . . 7
230229breq1d 4224 . . . . . 6
231230imbi2d 309 . . . . 5
232231ralbidva 2723 . . . 4
233232rexbidv 2728 . . 3