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

Theorem iseraltlem3 12467
 Description: Lemma for iseralt 12468. From iseraltlem2 12466, we have and , and we also have for each by the definition of the partial sum , so combining the inequalities we get , so and . Thus, both even and odd partial sums are Cauchy if converges to . (Contributed by Mario Carneiro, 6-Apr-2015.)
Hypotheses
Ref Expression
iseralt.1
iseralt.2
iseralt.3
iseralt.4
iseralt.5
iseralt.6
Assertion
Ref Expression
iseraltlem3
Distinct variable groups:   ,   ,   ,   ,   ,   ,   ,

Proof of Theorem iseraltlem3
StepHypRef Expression
1 1re 9080 . . . . . . . . . . 11
21renegcli 9352 . . . . . . . . . 10
32a1i 11 . . . . . . . . 9
4 ax-1cn 9038 . . . . . . . . . . 11
5 ax-1ne0 9049 . . . . . . . . . . 11
64, 5negne0i 9365 . . . . . . . . . 10
76a1i 11 . . . . . . . . 9
8 iseralt.1 . . . . . . . . . . 11
9 uzssz 10495 . . . . . . . . . . 11
108, 9eqsstri 3370 . . . . . . . . . 10
11 simp2 958 . . . . . . . . . 10
1210, 11sseldi 3338 . . . . . . . . 9
133, 7, 12reexpclzd 11538 . . . . . . . 8
1413recnd 9104 . . . . . . 7
15 iseralt.2 . . . . . . . . . . 11
16 iseralt.6 . . . . . . . . . . . 12
172a1i 11 . . . . . . . . . . . . . 14
186a1i 11 . . . . . . . . . . . . . 14
19 simpr 448 . . . . . . . . . . . . . . 15
2010, 19sseldi 3338 . . . . . . . . . . . . . 14
2117, 18, 20reexpclzd 11538 . . . . . . . . . . . . 13
22 iseralt.3 . . . . . . . . . . . . . 14
2322ffvelrnda 5862 . . . . . . . . . . . . 13
2421, 23remulcld 9106 . . . . . . . . . . . 12
2516, 24eqeltrd 2509 . . . . . . . . . . 11
268, 15, 25serfre 11342 . . . . . . . . . 10
27263ad2ant1 978 . . . . . . . . 9
2811, 8syl6eleq 2525 . . . . . . . . . . 11
29 2nn0 10228 . . . . . . . . . . . 12
30 simp3 959 . . . . . . . . . . . 12
31 nn0mulcl 10246 . . . . . . . . . . . 12
3229, 30, 31sylancr 645 . . . . . . . . . . 11
33 uzaddcl 10523 . . . . . . . . . . 11
3428, 32, 33syl2anc 643 . . . . . . . . . 10
3534, 8syl6eleqr 2526 . . . . . . . . 9
3627, 35ffvelrnd 5863 . . . . . . . 8
3736recnd 9104 . . . . . . 7
3827, 11ffvelrnd 5863 . . . . . . . 8
3938recnd 9104 . . . . . . 7
4014, 37, 39subdid 9479 . . . . . 6
4140fveq2d 5724 . . . . 5
4236, 38resubcld 9455 . . . . . . 7
4342recnd 9104 . . . . . 6
4414, 43absmuld 12246 . . . . 5
4541, 44eqtr3d 2469 . . . 4
463recnd 9104 . . . . . . 7
47 absexpz 12100 . . . . . . 7
4846, 7, 12, 47syl3anc 1184 . . . . . 6
494absnegi 12193 . . . . . . . . 9
50 abs1 12092 . . . . . . . . 9
5149, 50eqtri 2455 . . . . . . . 8
5251oveq1i 6083 . . . . . . 7
53 1exp 11399 . . . . . . . 8
5412, 53syl 16 . . . . . . 7
5552, 54syl5eq 2479 . . . . . 6
5648, 55eqtrd 2467 . . . . 5
5756oveq1d 6088 . . . 4
5843abscld 12228 . . . . . 6
5958recnd 9104 . . . . 5
6059mulid2d 9096 . . . 4
6145, 57, 603eqtrd 2471 . . 3
6213, 38remulcld 9106 . . . . . 6
63223ad2ant1 978 . . . . . . 7
648peano2uzs 10521 . . . . . . . 8
65643ad2ant2 979 . . . . . . 7
6663, 65ffvelrnd 5863 . . . . . 6
6762, 66resubcld 9455 . . . . 5
688peano2uzs 10521 . . . . . . . 8
6935, 68syl 16 . . . . . . 7
7027, 69ffvelrnd 5863 . . . . . 6
7113, 70remulcld 9106 . . . . 5
7213, 36remulcld 9106 . . . . 5
73 seqp1 11328 . . . . . . . . . . 11
7428, 73syl 16 . . . . . . . . . 10
7516ralrimiva 2781 . . . . . . . . . . . . 13
76753ad2ant1 978 . . . . . . . . . . . 12
77 fveq2 5720 . . . . . . . . . . . . . 14
78 oveq2 6081 . . . . . . . . . . . . . . 15
79 fveq2 5720 . . . . . . . . . . . . . . 15
8078, 79oveq12d 6091 . . . . . . . . . . . . . 14
8177, 80eqeq12d 2449 . . . . . . . . . . . . 13
8281rspcv 3040 . . . . . . . . . . . 12
8365, 76, 82sylc 58 . . . . . . . . . . 11
8483oveq2d 6089 . . . . . . . . . 10
8546, 7, 12expp1zd 11522 . . . . . . . . . . . . . 14
86 neg1cn 10057 . . . . . . . . . . . . . . 15
87 mulcom 9066 . . . . . . . . . . . . . . 15
8814, 86, 87sylancl 644 . . . . . . . . . . . . . 14
8914mulm1d 9475 . . . . . . . . . . . . . 14
9085, 88, 893eqtrd 2471 . . . . . . . . . . . . 13
9190oveq1d 6088 . . . . . . . . . . . 12
9266recnd 9104 . . . . . . . . . . . . 13
9314, 92mulneg1d 9476 . . . . . . . . . . . 12
9491, 93eqtrd 2467 . . . . . . . . . . 11
9594oveq2d 6089 . . . . . . . . . 10
9674, 84, 953eqtrd 2471 . . . . . . . . 9
9713, 66remulcld 9106 . . . . . . . . . . 11
9897recnd 9104 . . . . . . . . . 10
9939, 98negsubd 9407 . . . . . . . . 9
10096, 99eqtrd 2467 . . . . . . . 8
101100oveq2d 6089 . . . . . . 7
10214, 39, 98subdid 9479 . . . . . . 7
10312zcnd 10366 . . . . . . . . . . . . . . 15
1041032timesd 10200 . . . . . . . . . . . . . 14
105104oveq2d 6089 . . . . . . . . . . . . 13
106 2z 10302 . . . . . . . . . . . . . . 15
107106a1i 11 . . . . . . . . . . . . . 14
108 expmulz 11416 . . . . . . . . . . . . . 14
10946, 7, 107, 12, 108syl22anc 1185 . . . . . . . . . . . . 13
110105, 109eqtr3d 2469 . . . . . . . . . . . 12
111 sqneg 11432 . . . . . . . . . . . . . . 15
1124, 111ax-mp 8 . . . . . . . . . . . . . 14
113 sq1 11466 . . . . . . . . . . . . . 14
114112, 113eqtri 2455 . . . . . . . . . . . . 13
115114oveq1i 6083 . . . . . . . . . . . 12
116110, 115syl6eq 2483 . . . . . . . . . . 11
117 expaddz 11414 . . . . . . . . . . . 12
11846, 7, 12, 12, 117syl22anc 1185 . . . . . . . . . . 11
119116, 118, 543eqtr3d 2475 . . . . . . . . . 10
120119oveq1d 6088 . . . . . . . . 9
12114, 14, 92mulassd 9101 . . . . . . . . 9
12292mulid2d 9096 . . . . . . . . 9
123120, 121, 1223eqtr3d 2475 . . . . . . . 8
124123oveq2d 6089 . . . . . . 7
125101, 102, 1243eqtrd 2471 . . . . . 6
126 iseralt.4 . . . . . . . . . . 11
127 iseralt.5 . . . . . . . . . . 11
1288, 15, 22, 126, 127, 16iseraltlem2 12466 . . . . . . . . . 10
12964, 128syl3an2 1218 . . . . . . . . 9
1304a1i 11 . . . . . . . . . . . 12
13132nn0cnd 10266 . . . . . . . . . . . 12
132103, 130, 131add32d 9278 . . . . . . . . . . 11
133132fveq2d 5724 . . . . . . . . . 10
13490, 133oveq12d 6091 . . . . . . . . 9
13590oveq1d 6088 . . . . . . . . 9
136129, 134, 1353brtr3d 4233 . . . . . . . 8
13770recnd 9104 . . . . . . . . 9
13814, 137mulneg1d 9476 . . . . . . . 8
13927, 65ffvelrnd 5863 . . . . . . . . . 10
140139recnd 9104 . . . . . . . . 9
14114, 140mulneg1d 9476 . . . . . . . 8
142136, 138, 1413brtr3d 4233 . . . . . . 7
14313, 139remulcld 9106 . . . . . . . 8
144143, 71lenegd 9595 . . . . . . 7
145142, 144mpbird 224 . . . . . 6
146125, 145eqbrtrrd 4226 . . . . 5
147 seqp1 11328 . . . . . . . . . 10
14834, 147syl 16 . . . . . . . . 9
149 fveq2 5720 . . . . . . . . . . . . . 14
150 oveq2 6081 . . . . . . . . . . . . . . 15
151 fveq2 5720 . . . . . . . . . . . . . . 15
152150, 151oveq12d 6091 . . . . . . . . . . . . . 14
153149, 152eqeq12d 2449 . . . . . . . . . . . . 13
154153rspcv 3040 . . . . . . . . . . . 12
15569, 76, 154sylc 58 . . . . . . . . . . 11
15610, 65sseldi 3338 . . . . . . . . . . . . . . 15
15732nn0zd 10363 . . . . . . . . . . . . . . 15
158 expaddz 11414 . . . . . . . . . . . . . . 15
15946, 7, 156, 157, 158syl22anc 1185 . . . . . . . . . . . . . 14
16030nn0zd 10363 . . . . . . . . . . . . . . . . 17
161 expmulz 11416 . . . . . . . . . . . . . . . . 17
16246, 7, 107, 160, 161syl22anc 1185 . . . . . . . . . . . . . . . 16
163114oveq1i 6083 . . . . . . . . . . . . . . . . 17
164 1exp 11399 . . . . . . . . . . . . . . . . . 18
165160, 164syl 16 . . . . . . . . . . . . . . . . 17
166163, 165syl5eq 2479 . . . . . . . . . . . . . . . 16
167162, 166eqtrd 2467 . . . . . . . . . . . . . . 15
16890, 167oveq12d 6091 . . . . . . . . . . . . . 14
169159, 168eqtrd 2467 . . . . . . . . . . . . 13
170132oveq2d 6089 . . . . . . . . . . . . 13
17114negcld 9388 . . . . . . . . . . . . . 14
172171mulid1d 9095 . . . . . . . . . . . . 13
173169, 170, 1723eqtr3d 2475 . . . . . . . . . . . 12
174173oveq1d 6088 . . . . . . . . . . 11
17563, 69ffvelrnd 5863 . . . . . . . . . . . . 13
176175recnd 9104 . . . . . . . . . . . 12
17714, 176mulneg1d 9476 . . . . . . . . . . 11
178155, 174, 1773eqtrd 2471 . . . . . . . . . 10
179178oveq2d 6089 . . . . . . . . 9
18013, 175remulcld 9106 . . . . . . . . . . 11
181180recnd 9104 . . . . . . . . . 10
18237, 181negsubd 9407 . . . . . . . . 9
183148, 179, 1823eqtrd 2471 . . . . . . . 8
184183oveq2d 6089 . . . . . . 7
18514, 37, 181subdid 9479 . . . . . . 7
186119oveq1d 6088 . . . . . . . . 9
18714, 14, 176mulassd 9101 . . . . . . . . 9
188176mulid2d 9096 . . . . . . . . 9
189186, 187, 1883eqtr3d 2475 . . . . . . . 8
190189oveq2d 6089 . . . . . . 7
191184, 185, 1903eqtrd 2471 . . . . . 6
192 simp1 957 . . . . . . . 8
1938, 15, 22, 126, 127iseraltlem1 12465 . . . . . . . 8
194192, 69, 193syl2anc 643 . . . . . . 7
19572, 175subge02d 9608 . . . . . . 7
196194, 195mpbid 202 . . . . . 6
197191, 196eqbrtrd 4224 . . . . 5
19867, 71, 72, 146, 197letrd 9217 . . . 4
19962, 66readdcld 9105 . . . . 5
2008, 15, 22, 126, 127, 16iseraltlem2 12466 . . . . 5
2018, 15, 22, 126, 127iseraltlem1 12465 . . . . . . 7
202192, 65, 201syl2anc 643 . . . . . 6
20362, 66addge01d 9604 . . . . . 6
204202, 203mpbid 202 . . . . 5
20572, 62, 199, 200, 204letrd 9217 . . . 4
20672, 62, 66absdifled 12227 . . . 4
207198, 205, 206mpbir2and 889 . . 3
20861, 207eqbrtrrd 4226 . 2
20914, 137, 39subdid 9479 . . . . . 6
210209fveq2d 5724 . . . . 5
21170, 38resubcld 9455 . . . . . . 7
212211recnd 9104 . . . . . 6
21314, 212absmuld 12246 . . . . 5
214210, 213eqtr3d 2469 . . . 4
21556oveq1d 6088 . . . 4
216212abscld 12228 . . . . . 6
217216recnd 9104 . . . . 5
218217mulid2d 9096 . . . 4
219214, 215, 2183eqtrd 2471 . . 3
22071, 72, 199, 197, 205letrd 9217 . . . 4
22171, 62, 66absdifled 12227 . . . 4
222146, 220, 221mpbir2and 889 . . 3
223219, 222eqbrtrrd 4226 . 2
224208, 223jca 519 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   w3a 936   wceq 1652   wcel 1725   wne 2598  wral 2697   class class class wbr 4204  wf 5442  cfv 5446  (class class class)co 6073  cc 8978  cr 8979  cc0 8980  c1 8981   caddc 8983   cmul 8985   cle 9111   cmin 9281  cneg 9282  c2 10039  cn0 10211  cz 10272  cuz 10478   cseq 11313  cexp 11372  cabs 12029   cli 12268 This theorem is referenced by:  iseralt  12468 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4693  ax-cnex 9036  ax-resscn 9037  ax-1cn 9038  ax-icn 9039  ax-addcl 9040  ax-addrcl 9041  ax-mulcl 9042  ax-mulrcl 9043  ax-mulcom 9044  ax-addass 9045  ax-mulass 9046  ax-distr 9047  ax-i2m1 9048  ax-1ne0 9049  ax-1rid 9050  ax-rnegex 9051  ax-rrecex 9052  ax-cnre 9053  ax-pre-lttri 9054  ax-pre-lttrn 9055  ax-pre-ltadd 9056  ax-pre-mulgt0 9057  ax-pre-sup 9058 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-nel 2601  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-om 4838  df-xp 4876  df-rel 4877  df-cnv 4878  df-co 4879  df-dm 4880  df-rn 4881  df-res 4882  df-ima 4883  df-iota 5410  df-fun 5448  df-fn 5449  df-f 5450  df-f1 5451  df-fo 5452  df-f1o 5453  df-fv 5454  df-ov 6076  df-oprab 6077  df-mpt2 6078  df-1st 6341  df-2nd 6342  df-riota 6541  df-recs 6625  df-rdg 6660  df-er 6897  df-pm 7013  df-en 7102  df-dom 7103  df-sdom 7104  df-sup 7438  df-pnf 9112  df-mnf 9113  df-xr 9114  df-ltxr 9115  df-le 9116  df-sub 9283  df-neg 9284  df-div 9668  df-nn 9991  df-2 10048  df-3 10049  df-n0 10212  df-z 10273  df-uz 10479  df-rp 10603  df-fz 11034  df-fl 11192  df-seq 11314  df-exp 11373  df-cj 11894  df-re 11895  df-im 11896  df-sqr 12030  df-abs 12031  df-clim 12272  df-rlim 12273
 Copyright terms: Public domain W3C validator