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

Theorem abelthlem7 20355
 Description: Lemma for abelth 20358. (Contributed by Mario Carneiro, 2-Apr-2015.)
Hypotheses
Ref Expression
abelth.1
abelth.2
abelth.3
abelth.4
abelth.5
abelth.6
abelth.7
abelthlem6.1
abelthlem7.2
abelthlem7.3
abelthlem7.4
abelthlem7.5
Assertion
Ref Expression
abelthlem7
Distinct variable groups:   ,,,,   ,,,,   ,,,,   ,,,,   ,,   ,,,   ,,,
Allowed substitution hints:   ()   ()   (,,,)   (,)

Proof of Theorem abelthlem7
StepHypRef Expression
1 abelth.1 . . . . 5
2 abelth.2 . . . . 5
3 abelth.3 . . . . 5
4 abelth.4 . . . . 5
5 abelth.5 . . . . 5
6 abelth.6 . . . . 5
71, 2, 3, 4, 5, 6abelthlem4 20351 . . . 4
8 abelthlem6.1 . . . . 5
98eldifad 3333 . . . 4
107, 9ffvelrnd 5872 . . 3
1110abscld 12239 . 2
12 ax-1cn 9049 . . . . . 6
13 abelth.7 . . . . . . . 8
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 20354 . . . . . . 7
1514simpld 447 . . . . . 6
16 subcl 9306 . . . . . 6
1712, 15, 16sylancr 646 . . . . 5
18 fzfid 11313 . . . . . 6
19 elfznn0 11084 . . . . . . 7
20 nn0uz 10521 . . . . . . . . . 10
21 0z 10294 . . . . . . . . . . 11
2221a1i 11 . . . . . . . . . 10
231ffvelrnda 5871 . . . . . . . . . 10
2420, 22, 23serf 11352 . . . . . . . . 9
2524ffvelrnda 5871 . . . . . . . 8
26 expcl 11400 . . . . . . . . 9
2715, 26sylan 459 . . . . . . . 8
2825, 27mulcld 9109 . . . . . . 7
2919, 28sylan2 462 . . . . . 6
3018, 29fsumcl 12528 . . . . 5
3117, 30mulcld 9109 . . . 4
3231abscld 12239 . . 3
33 eqid 2437 . . . . . 6
34 abelthlem7.3 . . . . . . 7
3534nn0zd 10374 . . . . . 6
36 eluznn0 10547 . . . . . . . 8
3734, 36sylan 459 . . . . . . 7
38 fveq2 5729 . . . . . . . . 9
39 oveq2 6090 . . . . . . . . 9
4038, 39oveq12d 6100 . . . . . . . 8
41 eqid 2437 . . . . . . . 8
42 ovex 6107 . . . . . . . 8
4340, 41, 42fvmpt 5807 . . . . . . 7
4437, 43syl 16 . . . . . 6
4537, 28syldan 458 . . . . . 6
461, 2, 3, 4, 5abelthlem2 20349 . . . . . . . . . 10
4746simprd 451 . . . . . . . . 9
4847, 8sseldd 3350 . . . . . . . 8
491, 2, 3, 4, 5, 6, 13abelthlem5 20352 . . . . . . . 8
5048, 49mpdan 651 . . . . . . 7
5143adantl 454 . . . . . . . . 9
5251, 28eqeltrd 2511 . . . . . . . 8
5320, 34, 52iserex 12451 . . . . . . 7
5450, 53mpbid 203 . . . . . 6
5533, 35, 44, 45, 54isumcl 12546 . . . . 5
5617, 55mulcld 9109 . . . 4
5756abscld 12239 . . 3
59 peano2re 9240 . . . 4
603, 59syl 16 . . 3
61 abelthlem7.2 . . . 4
6261rpred 10649 . . 3
6360, 62remulcld 9117 . 2
641, 2, 3, 4, 5, 6, 13, 8abelthlem6 20353 . . . . 5
6520, 33, 34, 51, 28, 50isumsplit 12621 . . . . . 6
6665oveq2d 6098 . . . . 5
6717, 30, 55adddid 9113 . . . . 5
6864, 66, 673eqtrd 2473 . . . 4
6968fveq2d 5733 . . 3
7031, 56abstrid 12259 . . 3
7169, 70eqbrtrd 4233 . 2
723, 62remulcld 9117 . . . 4
7317abscld 12239 . . . . . 6
7425abscld 12239 . . . . . . . . 9
7519, 74sylan2 462 . . . . . . . 8
7618, 75fsumrecl 12529 . . . . . . 7
77 peano2re 9240 . . . . . . 7
7876, 77syl 16 . . . . . 6
7973, 78remulcld 9117 . . . . 5
8017, 30absmuld 12257 . . . . . 6
8130abscld 12239 . . . . . . 7
8217absge0d 12247 . . . . . . 7
8328abscld 12239 . . . . . . . . . . . 12
8419, 83sylan2 462 . . . . . . . . . . 11
8518, 84fsumrecl 12529 . . . . . . . . . 10
8618, 29fsumabs 12581 . . . . . . . . . 10
8715abscld 12239 . . . . . . . . . . . . . . 15
88 reexpcl 11399 . . . . . . . . . . . . . . 15
8987, 88sylan 459 . . . . . . . . . . . . . 14
90 1re 9091 . . . . . . . . . . . . . . 15
9190a1i 11 . . . . . . . . . . . . . 14
9225absge0d 12247 . . . . . . . . . . . . . 14
9387adantr 453 . . . . . . . . . . . . . . 15
9415absge0d 12247 . . . . . . . . . . . . . . . 16
9594adantr 453 . . . . . . . . . . . . . . 15
96 0cn 9085 . . . . . . . . . . . . . . . . . . . 20
97 eqid 2437 . . . . . . . . . . . . . . . . . . . . 21
9897cnmetdval 18806 . . . . . . . . . . . . . . . . . . . 20
9915, 96, 98sylancl 645 . . . . . . . . . . . . . . . . . . 19
10015subid1d 9401 . . . . . . . . . . . . . . . . . . . 20
101100fveq2d 5733 . . . . . . . . . . . . . . . . . . 19
10299, 101eqtrd 2469 . . . . . . . . . . . . . . . . . 18
103 cnxmet 18808 . . . . . . . . . . . . . . . . . . . . 21
104 1rp 10617 . . . . . . . . . . . . . . . . . . . . . 22
105 rpxr 10620 . . . . . . . . . . . . . . . . . . . . . 22
106104, 105ax-mp 8 . . . . . . . . . . . . . . . . . . . . 21
107 elbl3 18423 . . . . . . . . . . . . . . . . . . . . 21
108103, 106, 107mpanl12 665 . . . . . . . . . . . . . . . . . . . 20
10996, 15, 108sylancr 646 . . . . . . . . . . . . . . . . . . 19
11048, 109mpbid 203 . . . . . . . . . . . . . . . . . 18
111102, 110eqbrtrrd 4235 . . . . . . . . . . . . . . . . 17
112 ltle 9164 . . . . . . . . . . . . . . . . . 18
11387, 90, 112sylancl 645 . . . . . . . . . . . . . . . . 17
114111, 113mpd 15 . . . . . . . . . . . . . . . 16
115114adantr 453 . . . . . . . . . . . . . . 15
116 simpr 449 . . . . . . . . . . . . . . 15
117 exple1 11440 . . . . . . . . . . . . . . 15
11893, 95, 115, 116, 117syl31anc 1188 . . . . . . . . . . . . . 14
11989, 91, 74, 92, 118lemul2ad 9952 . . . . . . . . . . . . 13
12025, 27absmuld 12257 . . . . . . . . . . . . . 14
121 absexp 12110 . . . . . . . . . . . . . . . 16
12215, 121sylan 459 . . . . . . . . . . . . . . 15
123122oveq2d 6098 . . . . . . . . . . . . . 14
124120, 123eqtr2d 2470 . . . . . . . . . . . . 13
12574recnd 9115 . . . . . . . . . . . . . 14
126125mulid1d 9106 . . . . . . . . . . . . 13
127119, 124, 1263brtr3d 4242 . . . . . . . . . . . 12
12819, 127sylan2 462 . . . . . . . . . . 11
12918, 84, 75, 128fsumle 12579 . . . . . . . . . 10
13081, 85, 76, 86, 129letrd 9228 . . . . . . . . 9
13176ltp1d 9942 . . . . . . . . 9
13281, 76, 78, 130, 131lelttrd 9229 . . . . . . . 8
13381, 78, 132ltled 9222 . . . . . . 7
13481, 78, 73, 82, 133lemul2ad 9952 . . . . . 6
13580, 134eqbrtrd 4233 . . . . 5
136 abelthlem7.5 . . . . . 6
137 0re 9092 . . . . . . . . 9
138137a1i 11 . . . . . . . 8
13919, 92sylan2 462 . . . . . . . . 9
14018, 75, 139fsumge0 12575 . . . . . . . 8
141138, 76, 78, 140, 131lelttrd 9229 . . . . . . 7
142 ltmuldiv 9881 . . . . . . 7
14373, 62, 78, 141, 142syl112anc 1189 . . . . . 6
144136, 143mpbird 225 . . . . 5
14532, 79, 62, 135, 144lelttrd 9229 . . . 4
14617, 55absmuld 12257 . . . . 5
14755abscld 12239 . . . . . . 7
14840fveq2d 5733 . . . . . . . . . 10
149 eqid 2437 . . . . . . . . . 10
150 fvex 5743 . . . . . . . . . 10
151148, 149, 150fvmpt 5807 . . . . . . . . 9
15237, 151syl 16 . . . . . . . 8
15345abscld 12239 . . . . . . . 8
154 uzid 10501 . . . . . . . . . 10
15535, 154syl 16 . . . . . . . . 9
156 oveq2 6090 . . . . . . . . . . . 12
157 eqid 2437 . . . . . . . . . . . 12
158 ovex 6107 . . . . . . . . . . . 12
159156, 157, 158fvmpt 5807 . . . . . . . . . . 11
16037, 159syl 16 . . . . . . . . . 10
16137, 89syldan 458 . . . . . . . . . 10
162160, 161eqeltrd 2511 . . . . . . . . 9
163153recnd 9115 . . . . . . . . . 10
164152, 163eqeltrd 2511 . . . . . . . . 9
16587recnd 9115 . . . . . . . . . . 11
166 absidm 12128 . . . . . . . . . . . . 13
16715, 166syl 16 . . . . . . . . . . . 12
168167, 111eqbrtrd 4233 . . . . . . . . . . 11
169165, 168, 34, 160geolim2 12649 . . . . . . . . . 10
170 seqex 11326 . . . . . . . . . . 11
171 ovex 6107 . . . . . . . . . . 11
172170, 171breldm 5075 . . . . . . . . . 10
173169, 172syl 16 . . . . . . . . 9
174120, 123eqtrd 2469 . . . . . . . . . . . 12
17537, 174syldan 458 . . . . . . . . . . 11
17637, 74syldan 458 . . . . . . . . . . . 12
17762adantr 453 . . . . . . . . . . . 12
17887adantr 453 . . . . . . . . . . . . 13
17994adantr 453 . . . . . . . . . . . . 13
180178, 37, 179expge0d 11542 . . . . . . . . . . . 12
181 abelthlem7.4 . . . . . . . . . . . . . 14
18238fveq2d 5733 . . . . . . . . . . . . . . . 16
183182breq1d 4223 . . . . . . . . . . . . . . 15
184183rspccva 3052 . . . . . . . . . . . . . 14
185181, 184sylan 459 . . . . . . . . . . . . 13
186176, 177, 185ltled 9222 . . . . . . . . . . . 12
187176, 177, 161, 180, 186lemul1ad 9951 . . . . . . . . . . 11
188175, 187eqbrtrd 4233 . . . . . . . . . 10
189152fveq2d 5733 . . . . . . . . . . 11
190 absidm 12128 . . . . . . . . . . . 12
19145, 190syl 16 . . . . . . . . . . 11
192189, 191eqtrd 2469 . . . . . . . . . 10
193160oveq2d 6098 . . . . . . . . . 10
194188, 192, 1933brtr4d 4243 . . . . . . . . 9
19533, 155, 162, 164, 173, 62, 194cvgcmpce 12598 . . . . . . . 8
19633, 35, 152, 153, 195isumrecl 12550 . . . . . . 7
197 eldifsni 3929 . . . . . . . . . . . 12
1988, 197syl 16 . . . . . . . . . . 11
199198necomd 2688 . . . . . . . . . 10
200 subeq0 9328 . . . . . . . . . . . 12
201200necon3bid 2637 . . . . . . . . . . 11
20212, 15, 201sylancr 646 . . . . . . . . . 10
203199, 202mpbird 225 . . . . . . . . 9
20417, 203absrpcld 12251 . . . . . . . 8
20572, 204rerpdivcld 10676 . . . . . . 7
20633, 35, 44, 45, 54isumclim2 12543 . . . . . . . 8
20733, 35, 152, 163, 195isumclim2 12543 . . . . . . . 8
20837, 52syldan 458 . . . . . . . 8
20944fveq2d 5733 . . . . . . . . 9
210152, 209eqtr4d 2472 . . . . . . . 8
21133, 206, 207, 35, 208, 210iserabs 12595 . . . . . . 7
21287, 34reexpcld 11541 . . . . . . . . . 10
213 difrp 10646 . . . . . . . . . . . 12
21487, 90, 213sylancl 645 . . . . . . . . . . 11
215111, 214mpbid 203 . . . . . . . . . 10
216212, 215rerpdivcld 10676 . . . . . . . . 9
21762, 216remulcld 9117 . . . . . . . 8
218156oveq2d 6098 . . . . . . . . . . . 12
219 eqid 2437 . . . . . . . . . . . 12
220 ovex 6107 . . . . . . . . . . . 12
221218, 219, 220fvmpt 5807 . . . . . . . . . . 11
22237, 221syl 16 . . . . . . . . . 10
223177, 161remulcld 9117 . . . . . . . . . 10
22461rpcnd 10651 . . . . . . . . . . . 12
225162recnd 9115 . . . . . . . . . . . 12
226222, 193eqtr4d 2472 . . . . . . . . . . . 12
22733, 35, 224, 169, 225, 226isermulc2 12452 . . . . . . . . . . 11
228 seqex 11326 . . . . . . . . . . . 12
229 ovex 6107 . . . . . . . . . . . 12
230228, 229breldm 5075 . . . . . . . . . . 11
231227, 230syl 16 . . . . . . . . . 10
23233, 35, 152, 153, 222, 223, 188, 195, 231isumle 12625 . . . . . . . . 9
233223recnd 9115 . . . . . . . . . 10
23433, 35, 222, 233, 227isumclim 12542 . . . . . . . . 9
235232, 234breqtrd 4237 . . . . . . . 8
23661, 215rpdivcld 10666 . . . . . . . . . 10
237236rpred 10649 . . . . . . . . 9
238212recnd 9115 . . . . . . . . . . 11
239215rpcnd 10651 . . . . . . . . . . 11
240215rpne0d 10654 . . . . . . . . . . 11
241224, 238, 239, 240div12d 9827 . . . . . . . . . 10
24290a1i 11 . . . . . . . . . . . 12
243236rpge0d 10653 . . . . . . . . . . . 12
244 exple1 11440 . . . . . . . . . . . . 13
24587, 94, 114, 34, 244syl31anc 1188 . . . . . . . . . . . 12
246212, 242, 237, 243, 245lemul1ad 9951 . . . . . . . . . . 11
247236rpcnd 10651 . . . . . . . . . . . 12
248247mulid2d 9107 . . . . . . . . . . 11
249246, 248breqtrd 4237 . . . . . . . . . 10
250241, 249eqbrtrd 4233 . . . . . . . . 9
25114simprd 451 . . . . . . . . . . . . . 14
252 resubcl 9366 . . . . . . . . . . . . . . . . 17
25390, 87, 252sylancr 646 . . . . . . . . . . . . . . . 16
2543, 253remulcld 9117 . . . . . . . . . . . . . . 15
25573, 254, 61lemul2d 10689 . . . . . . . . . . . . . 14
256251, 255mpbid 203 . . . . . . . . . . . . 13
2573recnd 9115 . . . . . . . . . . . . . . 15
258224, 257, 239mul12d 9276 . . . . . . . . . . . . . 14
259224, 239mulcomd 9110 . . . . . . . . . . . . . . 15
260259oveq2d 6098 . . . . . . . . . . . . . 14
261257, 239, 224mul12d 9276 . . . . . . . . . . . . . 14
262258, 260, 2613eqtrd 2473 . . . . . . . . . . . . 13
263256, 262breqtrd 4237 . . . . . . . . . . . 12
264253, 72remulcld 9117 . . . . . . . . . . . . 13
26562, 264, 204lemuldivd 10694 . . . . . . . . . . . 12
266263, 265mpbid 203 . . . . . . . . . . 11
26772recnd 9115 . . . . . . . . . . . 12
26873recnd 9115 . . . . . . . . . . . 12
269204rpne0d 10654 . . . . . . . . . . . 12
270239, 267, 268, 269divassd 9826 . . . . . . . . . . 11
271266, 270breqtrd 4237 . . . . . . . . . 10
272 posdif 9522 . . . . . . . . . . . . 13
27387, 90, 272sylancl 645 . . . . . . . . . . . 12
274111, 273mpbid 203 . . . . . . . . . . 11
275 ledivmul 9884 . . . . . . . . . . 11
27662, 205, 253, 274, 275syl112anc 1189 . . . . . . . . . 10
277271, 276mpbird 225 . . . . . . . . 9
278217, 237, 205, 250, 277letrd 9228 . . . . . . . 8
279196, 217, 205, 235, 278letrd 9228 . . . . . . 7
280147, 196, 205, 211, 279letrd 9228 . . . . . 6
281147, 72, 204lemuldiv2d 10695 . . . . . 6
282280, 281mpbird 225 . . . . 5
283146, 282eqbrtrd 4233 . . . 4
28432, 57, 62, 72, 145, 283ltleaddd 9647 . . 3
28512a1i 11 . . . . 5
286257, 285, 224adddird 9114 . . . 4
287224mulid2d 9107 . . . . 5
288287oveq2d 6098 . . . 4
289267, 224addcomd 9269 . . . 4
290286, 288, 2893eqtrd 2473 . . 3
291284, 290breqtrrd 4239 . 2
29211, 58, 63, 71, 291lelttrd 9229 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 178   wa 360   wceq 1653   wcel 1726   wne 2600  wral 2706  crab 2710   cdif 3318   wss 3321  csn 3815   class class class wbr 4213   cmpt 4267   cdm 4879   ccom 4883  wf 5451  cfv 5455  (class class class)co 6082  cc 8989  cr 8990  cc0 8991  c1 8992   caddc 8994   cmul 8996  cxr 9120   clt 9121   cle 9122   cmin 9292   cdiv 9678  cn0 10222  cz 10283  cuz 10489  crp 10613  cfz 11044   cseq 11324  cexp 11383  cabs 12040   cli 12279  csu 12480  cxmt 16687  cbl 16689 This theorem is referenced by:  abelthlem8  20356 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2418  ax-rep 4321  ax-sep 4331  ax-nul 4339  ax-pow 4378  ax-pr 4404  ax-un 4702  ax-inf2 7597  ax-cnex 9047  ax-resscn 9048  ax-1cn 9049  ax-icn 9050  ax-addcl 9051  ax-addrcl 9052  ax-mulcl 9053  ax-mulrcl 9054  ax-mulcom 9055  ax-addass 9056  ax-mulass 9057  ax-distr 9058  ax-i2m1 9059  ax-1ne0 9060  ax-1rid 9061  ax-rnegex 9062  ax-rrecex 9063  ax-cnre 9064  ax-pre-lttri 9065  ax-pre-lttrn 9066  ax-pre-ltadd 9067  ax-pre-mulgt0 9068  ax-pre-sup 9069  ax-addf 9070  ax-mulf 9071 This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2286  df-mo 2287  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-nel 2603  df-ral 2711  df-rex 2712  df-reu 2713  df-rmo 2714  df-rab 2715  df-v 2959  df-sbc 3163  df-csb 3253  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-pss 3337  df-nul 3630  df-if 3741  df-pw 3802  df-sn 3821  df-pr 3822  df-tp 3823  df-op 3824  df-uni 4017  df-int 4052  df-iun 4096  df-br 4214  df-opab 4268  df-mpt 4269  df-tr 4304  df-eprel 4495  df-id 4499  df-po 4504  df-so 4505  df-fr 4542  df-se 4543  df-we 4544  df-ord 4585  df-on 4586  df-lim 4587  df-suc 4588  df-om 4847  df-xp 4885  df-rel 4886  df-cnv 4887  df-co 4888  df-dm 4889  df-rn 4890  df-res 4891  df-ima 4892  df-iota 5419  df-fun 5457  df-fn 5458  df-f 5459  df-f1 5460  df-fo 5461  df-f1o 5462  df-fv 5463  df-isom 5464  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-1st 6350  df-2nd 6351  df-riota 6550  df-recs 6634  df-rdg 6669  df-1o 6725  df-oadd 6729  df-er 6906  df-map 7021  df-pm 7022  df-en 7111  df-dom 7112  df-sdom 7113  df-fin 7114  df-sup 7447  df-oi 7480  df-card 7827  df-pnf 9123  df-mnf 9124  df-xr 9125  df-ltxr 9126  df-le 9127  df-sub 9294  df-neg 9295  df-div 9679  df-nn 10002  df-2 10059  df-3 10060  df-n0 10223  df-z 10284  df-uz 10490  df-rp 10614  df-xadd 10712  df-ico 10923  df-icc 10924  df-fz 11045  df-fzo 11137  df-fl 11203  df-seq 11325  df-exp 11384  df-hash 11620  df-shft 11883  df-cj 11905  df-re 11906  df-im 11907  df-sqr 12041  df-abs 12042  df-limsup 12266  df-clim 12283  df-rlim 12284  df-sum 12481  df-psmet 16695  df-xmet 16696  df-met 16697  df-bl 16698
 Copyright terms: Public domain W3C validator