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

Theorem abelthlem7 23472
 Description: Lemma for abelth 23475. (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 23468 . . . 4
8 abelthlem6.1 . . . . 5
98eldifad 3402 . . . 4
107, 9ffvelrnd 6038 . . 3
1110abscld 13575 . 2
12 ax-1cn 9615 . . . . . 6
13 abelth.7 . . . . . . . 8
141, 2, 3, 4, 5, 6, 13, 8abelthlem7a 23471 . . . . . . 7
1514simpld 466 . . . . . 6
16 subcl 9894 . . . . . 6
1712, 15, 16sylancr 676 . . . . 5
18 fzfid 12224 . . . . . 6
19 elfznn0 11913 . . . . . . 7
20 nn0uz 11217 . . . . . . . . . 10
21 0zd 10973 . . . . . . . . . 10
221ffvelrnda 6037 . . . . . . . . . 10
2320, 21, 22serf 12279 . . . . . . . . 9
2423ffvelrnda 6037 . . . . . . . 8
25 expcl 12328 . . . . . . . . 9
2615, 25sylan 479 . . . . . . . 8
2724, 26mulcld 9681 . . . . . . 7
2819, 27sylan2 482 . . . . . 6
2918, 28fsumcl 13876 . . . . 5
3017, 29mulcld 9681 . . . 4
3130abscld 13575 . . 3
32 eqid 2471 . . . . . 6
33 abelthlem7.3 . . . . . . 7
3433nn0zd 11061 . . . . . 6
35 eluznn0 11251 . . . . . . . 8
3633, 35sylan 479 . . . . . . 7
37 fveq2 5879 . . . . . . . . 9
38 oveq2 6316 . . . . . . . . 9
3937, 38oveq12d 6326 . . . . . . . 8
40 eqid 2471 . . . . . . . 8
41 ovex 6336 . . . . . . . 8
4239, 40, 41fvmpt 5963 . . . . . . 7
4336, 42syl 17 . . . . . 6
4436, 27syldan 478 . . . . . 6
451, 2, 3, 4, 5abelthlem2 23466 . . . . . . . . . 10
4645simprd 470 . . . . . . . . 9
4746, 8sseldd 3419 . . . . . . . 8
481, 2, 3, 4, 5, 6, 13abelthlem5 23469 . . . . . . . 8
4947, 48mpdan 681 . . . . . . 7
5042adantl 473 . . . . . . . . 9
5150, 27eqeltrd 2549 . . . . . . . 8
5220, 33, 51iserex 13797 . . . . . . 7
5349, 52mpbid 215 . . . . . 6
5432, 34, 43, 44, 53isumcl 13899 . . . . 5
5517, 54mulcld 9681 . . . 4
5655abscld 13575 . . 3
58 peano2re 9824 . . . 4
593, 58syl 17 . . 3
60 abelthlem7.2 . . . 4
6160rpred 11364 . . 3
6259, 61remulcld 9689 . 2
631, 2, 3, 4, 5, 6, 13, 8abelthlem6 23470 . . . . 5
6420, 32, 33, 50, 27, 49isumsplit 13975 . . . . . 6
6564oveq2d 6324 . . . . 5
6617, 29, 54adddid 9685 . . . . 5
6763, 65, 663eqtrd 2509 . . . 4
6867fveq2d 5883 . . 3
6930, 55abstrid 13595 . . 3
7068, 69eqbrtrd 4416 . 2
713, 61remulcld 9689 . . . 4
7217abscld 13575 . . . . . 6
7324abscld 13575 . . . . . . . . 9
7419, 73sylan2 482 . . . . . . . 8
7518, 74fsumrecl 13877 . . . . . . 7
76 peano2re 9824 . . . . . . 7
7775, 76syl 17 . . . . . 6
7872, 77remulcld 9689 . . . . 5
7917, 29absmuld 13593 . . . . . 6
8029abscld 13575 . . . . . . 7
8117absge0d 13583 . . . . . . 7
8227abscld 13575 . . . . . . . . . . . 12
8319, 82sylan2 482 . . . . . . . . . . 11
8418, 83fsumrecl 13877 . . . . . . . . . 10
8518, 28fsumabs 13938 . . . . . . . . . 10
8615abscld 13575 . . . . . . . . . . . . . . 15
87 reexpcl 12327 . . . . . . . . . . . . . . 15
8886, 87sylan 479 . . . . . . . . . . . . . 14
89 1red 9676 . . . . . . . . . . . . . 14
9024absge0d 13583 . . . . . . . . . . . . . 14
9186adantr 472 . . . . . . . . . . . . . . 15
9215absge0d 13583 . . . . . . . . . . . . . . . 16
9392adantr 472 . . . . . . . . . . . . . . 15
94 0cn 9653 . . . . . . . . . . . . . . . . . . . 20
95 eqid 2471 . . . . . . . . . . . . . . . . . . . . 21
9695cnmetdval 21869 . . . . . . . . . . . . . . . . . . . 20
9715, 94, 96sylancl 675 . . . . . . . . . . . . . . . . . . 19
9815subid1d 9994 . . . . . . . . . . . . . . . . . . . 20
9998fveq2d 5883 . . . . . . . . . . . . . . . . . . 19
10097, 99eqtrd 2505 . . . . . . . . . . . . . . . . . 18
101 cnxmet 21871 . . . . . . . . . . . . . . . . . . . . 21
102 1rp 11329 . . . . . . . . . . . . . . . . . . . . . 22
103 rpxr 11332 . . . . . . . . . . . . . . . . . . . . . 22
104102, 103ax-mp 5 . . . . . . . . . . . . . . . . . . . . 21
105 elbl3 21485 . . . . . . . . . . . . . . . . . . . . 21
106101, 104, 105mpanl12 696 . . . . . . . . . . . . . . . . . . . 20
10794, 15, 106sylancr 676 . . . . . . . . . . . . . . . . . . 19
10847, 107mpbid 215 . . . . . . . . . . . . . . . . . 18
109100, 108eqbrtrrd 4418 . . . . . . . . . . . . . . . . 17
110 1re 9660 . . . . . . . . . . . . . . . . . 18
111 ltle 9740 . . . . . . . . . . . . . . . . . 18
11286, 110, 111sylancl 675 . . . . . . . . . . . . . . . . 17
113109, 112mpd 15 . . . . . . . . . . . . . . . 16
114113adantr 472 . . . . . . . . . . . . . . 15
115 simpr 468 . . . . . . . . . . . . . . 15
116 exple1 12370 . . . . . . . . . . . . . . 15
11791, 93, 114, 115, 116syl31anc 1295 . . . . . . . . . . . . . 14
11888, 89, 73, 90, 117lemul2ad 10569 . . . . . . . . . . . . 13
11924, 26absmuld 13593 . . . . . . . . . . . . . 14
120 absexp 13444 . . . . . . . . . . . . . . . 16
12115, 120sylan 479 . . . . . . . . . . . . . . 15
122121oveq2d 6324 . . . . . . . . . . . . . 14
123119, 122eqtr2d 2506 . . . . . . . . . . . . 13
12473recnd 9687 . . . . . . . . . . . . . 14
125124mulid1d 9678 . . . . . . . . . . . . 13
126118, 123, 1253brtr3d 4425 . . . . . . . . . . . 12
12719, 126sylan2 482 . . . . . . . . . . 11
12818, 83, 74, 127fsumle 13936 . . . . . . . . . 10
12980, 84, 75, 85, 128letrd 9809 . . . . . . . . 9
13075ltp1d 10559 . . . . . . . . 9
13180, 75, 77, 129, 130lelttrd 9810 . . . . . . . 8
13280, 77, 131ltled 9800 . . . . . . 7
13380, 77, 72, 81, 132lemul2ad 10569 . . . . . 6
13479, 133eqbrtrd 4416 . . . . 5
135 abelthlem7.5 . . . . . 6
136 0red 9662 . . . . . . . 8
13719, 90sylan2 482 . . . . . . . . 9
13818, 74, 137fsumge0 13932 . . . . . . . 8
139136, 75, 77, 138, 130lelttrd 9810 . . . . . . 7
140 ltmuldiv 10500 . . . . . . 7
14172, 61, 77, 139, 140syl112anc 1296 . . . . . 6
142135, 141mpbird 240 . . . . 5
14331, 78, 61, 134, 142lelttrd 9810 . . . 4
14417, 54absmuld 13593 . . . . 5
14554abscld 13575 . . . . . . 7
14639fveq2d 5883 . . . . . . . . . 10
147 eqid 2471 . . . . . . . . . 10
148 fvex 5889 . . . . . . . . . 10
149146, 147, 148fvmpt 5963 . . . . . . . . 9
15036, 149syl 17 . . . . . . . 8
15144abscld 13575 . . . . . . . 8
152 uzid 11197 . . . . . . . . . 10
15334, 152syl 17 . . . . . . . . 9
154 oveq2 6316 . . . . . . . . . . . 12
155 eqid 2471 . . . . . . . . . . . 12
156 ovex 6336 . . . . . . . . . . . 12
157154, 155, 156fvmpt 5963 . . . . . . . . . . 11
15836, 157syl 17 . . . . . . . . . 10
15936, 88syldan 478 . . . . . . . . . 10
160158, 159eqeltrd 2549 . . . . . . . . 9
161151recnd 9687 . . . . . . . . . 10
162150, 161eqeltrd 2549 . . . . . . . . 9
16386recnd 9687 . . . . . . . . . . 11
164 absidm 13463 . . . . . . . . . . . . 13
16515, 164syl 17 . . . . . . . . . . . 12
166165, 109eqbrtrd 4416 . . . . . . . . . . 11
167163, 166, 33, 158geolim2 14004 . . . . . . . . . 10
168 seqex 12253 . . . . . . . . . . 11
169 ovex 6336 . . . . . . . . . . 11
170168, 169breldm 5045 . . . . . . . . . 10
171167, 170syl 17 . . . . . . . . 9
172119, 122eqtrd 2505 . . . . . . . . . . . 12
17336, 172syldan 478 . . . . . . . . . . 11
17436, 73syldan 478 . . . . . . . . . . . 12
17561adantr 472 . . . . . . . . . . . 12
17686adantr 472 . . . . . . . . . . . . 13
17792adantr 472 . . . . . . . . . . . . 13
178176, 36, 177expge0d 12472 . . . . . . . . . . . 12
179 abelthlem7.4 . . . . . . . . . . . . . 14
18037fveq2d 5883 . . . . . . . . . . . . . . . 16
181180breq1d 4405 . . . . . . . . . . . . . . 15
182181rspccva 3135 . . . . . . . . . . . . . 14
183179, 182sylan 479 . . . . . . . . . . . . 13
184174, 175, 183ltled 9800 . . . . . . . . . . . 12
185174, 175, 159, 178, 184lemul1ad 10568 . . . . . . . . . . 11
186173, 185eqbrtrd 4416 . . . . . . . . . 10
187150fveq2d 5883 . . . . . . . . . . 11
188 absidm 13463 . . . . . . . . . . . 12
18944, 188syl 17 . . . . . . . . . . 11
190187, 189eqtrd 2505 . . . . . . . . . 10
191158oveq2d 6324 . . . . . . . . . 10
192186, 190, 1913brtr4d 4426 . . . . . . . . 9
19332, 153, 160, 162, 171, 61, 192cvgcmpce 13955 . . . . . . . 8
19432, 34, 150, 151, 193isumrecl 13903 . . . . . . 7
195 eldifsni 4089 . . . . . . . . . . . 12
1968, 195syl 17 . . . . . . . . . . 11
197196necomd 2698 . . . . . . . . . 10
198 subeq0 9920 . . . . . . . . . . . 12
199198necon3bid 2687 . . . . . . . . . . 11
20012, 15, 199sylancr 676 . . . . . . . . . 10
201197, 200mpbird 240 . . . . . . . . 9
20217, 201absrpcld 13587 . . . . . . . 8
20371, 202rerpdivcld 11392 . . . . . . 7
20432, 34, 43, 44, 53isumclim2 13896 . . . . . . . 8
20532, 34, 150, 161, 193isumclim2 13896 . . . . . . . 8
20636, 51syldan 478 . . . . . . . 8
20743fveq2d 5883 . . . . . . . . 9
208150, 207eqtr4d 2508 . . . . . . . 8
20932, 204, 205, 34, 206, 208iserabs 13952 . . . . . . 7
21086, 33reexpcld 12471 . . . . . . . . . 10
211 difrp 11360 . . . . . . . . . . . 12
21286, 110, 211sylancl 675 . . . . . . . . . . 11
213109, 212mpbid 215 . . . . . . . . . 10
214210, 213rerpdivcld 11392 . . . . . . . . 9
21561, 214remulcld 9689 . . . . . . . 8
216154oveq2d 6324 . . . . . . . . . . . 12
217 eqid 2471 . . . . . . . . . . . 12
218 ovex 6336 . . . . . . . . . . . 12
219216, 217, 218fvmpt 5963 . . . . . . . . . . 11
22036, 219syl 17 . . . . . . . . . 10
221175, 159remulcld 9689 . . . . . . . . . 10
22260rpcnd 11366 . . . . . . . . . . . 12
223160recnd 9687 . . . . . . . . . . . 12
224220, 191eqtr4d 2508 . . . . . . . . . . . 12
22532, 34, 222, 167, 223, 224isermulc2 13798 . . . . . . . . . . 11
226 seqex 12253 . . . . . . . . . . . 12
227 ovex 6336 . . . . . . . . . . . 12
228226, 227breldm 5045 . . . . . . . . . . 11
229225, 228syl 17 . . . . . . . . . 10
23032, 34, 150, 151, 220, 221, 186, 193, 229isumle 13979 . . . . . . . . 9
231221recnd 9687 . . . . . . . . . 10
23232, 34, 220, 231, 225isumclim 13895 . . . . . . . . 9
233230, 232breqtrd 4420 . . . . . . . 8
23460, 213rpdivcld 11381 . . . . . . . . . 10
235234rpred 11364 . . . . . . . . 9
236210recnd 9687 . . . . . . . . . . 11
237213rpcnd 11366 . . . . . . . . . . 11
238213rpne0d 11369 . . . . . . . . . . 11
239222, 236, 237, 238div12d 10441 . . . . . . . . . 10
240 1red 9676 . . . . . . . . . . . 12
241234rpge0d 11368 . . . . . . . . . . . 12
242 exple1 12370 . . . . . . . . . . . . 13
24386, 92, 113, 33, 242syl31anc 1295 . . . . . . . . . . . 12
244210, 240, 235, 241, 243lemul1ad 10568 . . . . . . . . . . 11
245234rpcnd 11366 . . . . . . . . . . . 12
246245mulid2d 9679 . . . . . . . . . . 11
247244, 246breqtrd 4420 . . . . . . . . . 10
248239, 247eqbrtrd 4416 . . . . . . . . 9
24914simprd 470 . . . . . . . . . . . . . 14
250 resubcl 9958 . . . . . . . . . . . . . . . . 17
251110, 86, 250sylancr 676 . . . . . . . . . . . . . . . 16
2523, 251remulcld 9689 . . . . . . . . . . . . . . 15
25372, 252, 60lemul2d 11405 . . . . . . . . . . . . . 14
254249, 253mpbid 215 . . . . . . . . . . . . 13
2553recnd 9687 . . . . . . . . . . . . . . 15
256222, 255, 237mul12d 9860 . . . . . . . . . . . . . 14
257222, 237mulcomd 9682 . . . . . . . . . . . . . . 15
258257oveq2d 6324 . . . . . . . . . . . . . 14
259255, 237, 222mul12d 9860 . . . . . . . . . . . . . 14
260256, 258, 2593eqtrd 2509 . . . . . . . . . . . . 13
261254, 260breqtrd 4420 . . . . . . . . . . . 12
262251, 71remulcld 9689 . . . . . . . . . . . . 13
26361, 262, 202lemuldivd 11410 . . . . . . . . . . . 12
264261, 263mpbid 215 . . . . . . . . . . 11
26571recnd 9687 . . . . . . . . . . . 12
26672recnd 9687 . . . . . . . . . . . 12
267202rpne0d 11369 . . . . . . . . . . . 12
268237, 265, 266, 267divassd 10440 . . . . . . . . . . 11
269264, 268breqtrd 4420 . . . . . . . . . 10
270 posdif 10128 . . . . . . . . . . . . 13
27186, 110, 270sylancl 675 . . . . . . . . . . . 12
272109, 271mpbid 215 . . . . . . . . . . 11
273 ledivmul 10503 . . . . . . . . . . 11
27461, 203, 251, 272, 273syl112anc 1296 . . . . . . . . . 10
275269, 274mpbird 240 . . . . . . . . 9
276215, 235, 203, 248, 275letrd 9809 . . . . . . . 8
277194, 215, 203, 233, 276letrd 9809 . . . . . . 7
278145, 194, 203, 209, 277letrd 9809 . . . . . 6
279145, 71, 202lemuldiv2d 11411 . . . . . 6
280278, 279mpbird 240 . . . . 5
281144, 280eqbrtrd 4416 . . . 4
28231, 56, 61, 71, 143, 281ltleaddd 10255 . . 3
283 1cnd 9677 . . . . 5
284255, 283, 222adddird 9686 . . . 4
285222mulid2d 9679 . . . . 5
286285oveq2d 6324 . . . 4
287265, 222addcomd 9853 . . . 4
288284, 286, 2873eqtrd 2509 . . 3
289282, 288breqtrrd 4422 . 2
29011, 57, 62, 70, 289lelttrd 9810 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 189   wa 376   wceq 1452   wcel 1904   wne 2641  wral 2756  crab 2760   cdif 3387   wss 3390  csn 3959   class class class wbr 4395   cmpt 4454   cdm 4839   ccom 4843  wf 5585  cfv 5589  (class class class)co 6308  cc 9555  cr 9556  cc0 9557  c1 9558   caddc 9560   cmul 9562  cxr 9692   clt 9693   cle 9694   cmin 9880   cdiv 10291  cn0 10893  cz 10961  cuz 11182  crp 11325  cfz 11810   cseq 12251  cexp 12310  cabs 13374   cli 13625  csu 13829  cxmt 19032  cbl 19034 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-8 1906  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-rep 4508  ax-sep 4518  ax-nul 4527  ax-pow 4579  ax-pr 4639  ax-un 6602  ax-inf2 8164  ax-cnex 9613  ax-resscn 9614  ax-1cn 9615  ax-icn 9616  ax-addcl 9617  ax-addrcl 9618  ax-mulcl 9619  ax-mulrcl 9620  ax-mulcom 9621  ax-addass 9622  ax-mulass 9623  ax-distr 9624  ax-i2m1 9625  ax-1ne0 9626  ax-1rid 9627  ax-rnegex 9628  ax-rrecex 9629  ax-cnre 9630  ax-pre-lttri 9631  ax-pre-lttrn 9632  ax-pre-ltadd 9633  ax-pre-mulgt0 9634  ax-pre-sup 9635  ax-addf 9636  ax-mulf 9637 This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3or 1008  df-3an 1009  df-tru 1455  df-fal 1458  df-ex 1672  df-nf 1676  df-sb 1806  df-eu 2323  df-mo 2324  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-nel 2644  df-ral 2761  df-rex 2762  df-reu 2763  df-rmo 2764  df-rab 2765  df-v 3033  df-sbc 3256  df-csb 3350  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-pss 3406  df-nul 3723  df-if 3873  df-pw 3944  df-sn 3960  df-pr 3962  df-tp 3964  df-op 3966  df-uni 4191  df-int 4227  df-iun 4271  df-br 4396  df-opab 4455  df-mpt 4456  df-tr 4491  df-eprel 4750  df-id 4754  df-po 4760  df-so 4761  df-fr 4798  df-se 4799  df-we 4800  df-xp 4845  df-rel 4846  df-cnv 4847  df-co 4848  df-dm 4849  df-rn 4850  df-res 4851  df-ima 4852  df-pred 5387  df-ord 5433  df-on 5434  df-lim 5435  df-suc 5436  df-iota 5553  df-fun 5591  df-fn 5592  df-f 5593  df-f1 5594  df-fo 5595  df-f1o 5596  df-fv 5597  df-isom 5598  df-riota 6270  df-ov 6311  df-oprab 6312  df-mpt2 6313  df-om 6712  df-1st 6812  df-2nd 6813  df-wrecs 7046  df-recs 7108  df-rdg 7146  df-1o 7200  df-oadd 7204  df-er 7381  df-map 7492  df-pm 7493  df-en 7588  df-dom 7589  df-sdom 7590  df-fin 7591  df-sup 7974  df-inf 7975  df-oi 8043  df-card 8391  df-pnf 9695  df-mnf 9696  df-xr 9697  df-ltxr 9698  df-le 9699  df-sub 9882  df-neg 9883  df-div 10292  df-nn 10632  df-2 10690  df-3 10691  df-n0 10894  df-z 10962  df-uz 11183  df-rp 11326  df-xadd 11433  df-ico 11666  df-icc 11667  df-fz 11811  df-fzo 11943  df-fl 12061  df-seq 12252  df-exp 12311  df-hash 12554  df-shft 13207  df-cj 13239  df-re 13240  df-im 13241  df-sqrt 13375  df-abs 13376  df-limsup 13603  df-clim 13629  df-rlim 13630  df-sum 13830  df-psmet 19039  df-xmet 19040  df-met 19041  df-bl 19042 This theorem is referenced by:  abelthlem8  23473
 Copyright terms: Public domain W3C validator