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

 Description: Lemma for radcnvlt1 19794, radcnvle 19796. If is a point closer to zero than and the power series converges at , then it converges absolutely at , even if the terms in the sequence are multiplied by . (Contributed by Mario Carneiro, 31-Mar-2015.)
Hypotheses
Ref Expression
pser.g
psergf.x
Assertion
Ref Expression
Distinct variable groups:   ,,,   ,   ,   ,   ,   ,
Allowed substitution hints:   (,)   (,)   (,)   (,)   (,)

Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nn0uz 10262 . . 3
2 0z 10035 . . . 4
32a1i 10 . . 3
4 1rp 10358 . . . 4
54a1i 10 . . 3
6 radcnvlem2.y . . . 4
7 pser.g . . . . 5
87pserval2 19787 . . . 4
96, 8sylan 457 . . 3
10 fvex 5539 . . . . 5
1110a1i 10 . . . 4
12 radcnvlem2.c . . . 4
13 radcnv.a . . . . . 6
147, 13, 6psergf 19788 . . . . 5
15 ffvelrn 5663 . . . . 5
1614, 15sylan 457 . . . 4
171, 3, 11, 12, 16serf0 12153 . . 3
181, 3, 5, 9, 17climi0 11986 . 2
19 simprl 732 . . . . 5
20 nn0re 9974 . . . . . . . . 9
2120adantl 452 . . . . . . . 8
22 psergf.x . . . . . . . . . . . 12
2322adantr 451 . . . . . . . . . . 11
2423abscld 11918 . . . . . . . . . 10
256adantr 451 . . . . . . . . . . 11
2625abscld 11918 . . . . . . . . . 10
27 0re 8838 . . . . . . . . . . . . . 14
2827a1i 10 . . . . . . . . . . . . 13
2922abscld 11918 . . . . . . . . . . . . 13
306abscld 11918 . . . . . . . . . . . . 13
3122absge0d 11926 . . . . . . . . . . . . 13
32 radcnvlem2.a . . . . . . . . . . . . 13
3328, 29, 30, 31, 32lelttrd 8974 . . . . . . . . . . . 12
3433gt0ne0d 9337 . . . . . . . . . . 11
3534adantr 451 . . . . . . . . . 10
3624, 26, 35redivcld 9588 . . . . . . . . 9
37 reexpcl 11120 . . . . . . . . 9
3836, 37sylan 457 . . . . . . . 8
3921, 38remulcld 8863 . . . . . . 7
40 eqid 2283 . . . . . . 7
4139, 40fmptd 5684 . . . . . 6
42 ffvelrn 5663 . . . . . 6
4341, 42sylan 457 . . . . 5
44 nn0re 9974 . . . . . . . . . . 11
4544adantl 452 . . . . . . . . . 10
467, 13, 22psergf 19788 . . . . . . . . . . . 12
47 ffvelrn 5663 . . . . . . . . . . . 12
4846, 47sylan 457 . . . . . . . . . . 11
4948abscld 11918 . . . . . . . . . 10
5045, 49remulcld 8863 . . . . . . . . 9
51 radcnvlem1.h . . . . . . . . 9
5250, 51fmptd 5684 . . . . . . . 8
5352adantr 451 . . . . . . 7
54 ffvelrn 5663 . . . . . . 7
5553, 54sylan 457 . . . . . 6
5655recnd 8861 . . . . 5
5729, 30, 34redivcld 9588 . . . . . . . 8
5857recnd 8861 . . . . . . 7
59 divge0 9625 . . . . . . . . . 10
6029, 31, 30, 33, 59syl22anc 1183 . . . . . . . . 9
6157, 60absidd 11905 . . . . . . . 8
6230recnd 8861 . . . . . . . . . . 11
6362mulid1d 8852 . . . . . . . . . 10
6432, 63breqtrrd 4049 . . . . . . . . 9
65 1re 8837 . . . . . . . . . . 11
6665a1i 10 . . . . . . . . . 10
67 ltdivmul 9628 . . . . . . . . . 10
6829, 66, 30, 33, 67syl112anc 1186 . . . . . . . . 9
6964, 68mpbird 223 . . . . . . . 8
7061, 69eqbrtrd 4043 . . . . . . 7
7140geomulcvg 12332 . . . . . . 7
7258, 70, 71syl2anc 642 . . . . . 6
7372adantr 451 . . . . 5
7465a1i 10 . . . . 5
7546ad2antrr 706 . . . . . . . . . 10
76 eluznn0 10288 . . . . . . . . . . 11
7719, 76sylan 457 . . . . . . . . . 10
7875, 77, 47syl2anc 642 . . . . . . . . 9
7978abscld 11918 . . . . . . . 8
8036adantr 451 . . . . . . . . 9
8180, 77reexpcld 11262 . . . . . . . 8
8277nn0red 10019 . . . . . . . 8
8377nn0ge0d 10021 . . . . . . . 8
8413ad2antrr 706 . . . . . . . . . . . . . . 15
85 ffvelrn 5663 . . . . . . . . . . . . . . 15
8684, 77, 85syl2anc 642 . . . . . . . . . . . . . 14
876ad2antrr 706 . . . . . . . . . . . . . . 15
8887, 77expcld 11245 . . . . . . . . . . . . . 14
8986, 88mulcld 8855 . . . . . . . . . . . . 13
9089abscld 11918 . . . . . . . . . . . 12
9165a1i 10 . . . . . . . . . . . 12
9222ad2antrr 706 . . . . . . . . . . . . . 14
9392abscld 11918 . . . . . . . . . . . . 13
9493, 77reexpcld 11262 . . . . . . . . . . . 12
9592absge0d 11926 . . . . . . . . . . . . 13
9693, 77, 95expge0d 11263 . . . . . . . . . . . 12
97 simprr 733 . . . . . . . . . . . . . 14
98 fveq2 5525 . . . . . . . . . . . . . . . . . 18
99 oveq2 5866 . . . . . . . . . . . . . . . . . 18
10098, 99oveq12d 5876 . . . . . . . . . . . . . . . . 17
101100fveq2d 5529 . . . . . . . . . . . . . . . 16
102101breq1d 4033 . . . . . . . . . . . . . . 15
103102rspccva 2883 . . . . . . . . . . . . . 14
10497, 103sylan 457 . . . . . . . . . . . . 13
105 ltle 8910 . . . . . . . . . . . . . 14
10690, 65, 105sylancl 643 . . . . . . . . . . . . 13
107104, 106mpd 14 . . . . . . . . . . . 12
10890, 91, 94, 96, 107lemul1ad 9696 . . . . . . . . . . 11
10992, 77expcld 11245 . . . . . . . . . . . . . 14
11086, 109mulcld 8855 . . . . . . . . . . . . 13
111110, 88absmuld 11936 . . . . . . . . . . . 12
11289, 109absmuld 11936 . . . . . . . . . . . . 13
11386, 88, 109mul32d 9022 . . . . . . . . . . . . . 14
114113fveq2d 5529 . . . . . . . . . . . . 13
11592, 77absexpd 11934 . . . . . . . . . . . . . 14
116115oveq2d 5874 . . . . . . . . . . . . 13
117112, 114, 1163eqtr3d 2323 . . . . . . . . . . . 12
11887, 77absexpd 11934 . . . . . . . . . . . . 13
119118oveq2d 5874 . . . . . . . . . . . 12
120111, 117, 1193eqtr3d 2323 . . . . . . . . . . 11
12194recnd 8861 . . . . . . . . . . . 12
122121mulid2d 8853 . . . . . . . . . . 11
123108, 120, 1223brtr3d 4052 . . . . . . . . . 10
124110abscld 11918 . . . . . . . . . . 11
12526adantr 451 . . . . . . . . . . . 12
126125, 77reexpcld 11262 . . . . . . . . . . 11
127 eluzelz 10238 . . . . . . . . . . . . 13
128127adantl 452 . . . . . . . . . . . 12
12933ad2antrr 706 . . . . . . . . . . . 12
130 expgt0 11135 . . . . . . . . . . . 12
131125, 128, 129, 130syl3anc 1182 . . . . . . . . . . 11
132 lemuldiv 9635 . . . . . . . . . . 11
133124, 94, 126, 131, 132syl112anc 1186 . . . . . . . . . 10
134123, 133mpbid 201 . . . . . . . . 9
1357pserval2 19787 . . . . . . . . . . 11
13692, 77, 135syl2anc 642 . . . . . . . . . 10
137136fveq2d 5529 . . . . . . . . 9
13824recnd 8861 . . . . . . . . . . 11
139138adantr 451 . . . . . . . . . 10
14026recnd 8861 . . . . . . . . . . 11
141140adantr 451 . . . . . . . . . 10
14234ad2antrr 706 . . . . . . . . . 10
143139, 141, 142, 77expdivd 11259 . . . . . . . . 9
144134, 137, 1433brtr4d 4053 . . . . . . . 8
14579, 81, 82, 83, 144lemul2ad 9697 . . . . . . 7
14682, 79remulcld 8863 . . . . . . . 8
14778absge0d 11926 . . . . . . . . 9
14882, 79, 83, 147mulge0d 9349 . . . . . . . 8
149146, 148absidd 11905 . . . . . . 7
15082, 81remulcld 8863 . . . . . . . . 9
151150recnd 8861 . . . . . . . 8
152151mulid2d 8853 . . . . . . 7
153145, 149, 1523brtr4d 4053 . . . . . 6
154 ovex 5883 . . . . . . . 8
15551fvmpt2 5608 . . . . . . . 8
15677, 154, 155sylancl 643 . . . . . . 7
157156fveq2d 5529 . . . . . 6
158 id 19 . . . . . . . . . 10
159 oveq2 5866 . . . . . . . . . 10
160158, 159oveq12d 5876 . . . . . . . . 9
161 ovex 5883 . . . . . . . . 9
162160, 40, 161fvmpt 5602 . . . . . . . 8
16377, 162syl 15 . . . . . . 7
164163oveq2d 5874 . . . . . 6
165153, 157, 1643brtr4d 4053 . . . . 5
1661, 19, 43, 56, 73, 74, 165cvgcmpce 12276 . . . 4
167166expr 598 . . 3
168167rexlimdva 2667 . 2
16918, 168mpd 14 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   wceq 1623   wcel 1684   wne 2446  wral 2543  wrex 2544  cvv 2788   class class class wbr 4023   cmpt 4077   cdm 4689  wf 5251  cfv 5255  (class class class)co 5858  cc 8735  cr 8736  cc0 8737  c1 8738   caddc 8740   cmul 8742   clt 8867   cle 8868   cdiv 9423  cn0 9965  cz 10024  cuz 10230  crp 10354   cseq 11046  cexp 11104  cabs 11719   cli 11958 This theorem is referenced by:  radcnvlem2  19790  radcnvlt1  19794 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-inf2 7342  ax-cnex 8793  ax-resscn 8794  ax-1cn 8795  ax-icn 8796  ax-addcl 8797  ax-addrcl 8798  ax-mulcl 8799  ax-mulrcl 8800  ax-mulcom 8801  ax-addass 8802  ax-mulass 8803  ax-distr 8804  ax-i2m1 8805  ax-1ne0 8806  ax-1rid 8807  ax-rnegex 8808  ax-rrecex 8809  ax-cnre 8810  ax-pre-lttri 8811  ax-pre-lttrn 8812  ax-pre-ltadd 8813  ax-pre-mulgt0 8814  ax-pre-sup 8815  ax-addf 8816  ax-mulf 8817 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-nel 2449  df-ral 2548  df-rex 2549  df-reu 2550  df-rmo 2551  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-se 4353  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-isom 5264  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-pm 6775  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-sup 7194  df-oi 7225  df-card 7572  df-pnf 8869  df-mnf 8870  df-xr 8871  df-ltxr 8872  df-le 8873  df-sub 9039  df-neg 9040  df-div 9424  df-nn 9747  df-2 9804  df-3 9805  df-n0 9966  df-z 10025  df-uz 10231  df-rp 10355  df-ico 10662  df-fz 10783  df-fzo 10871  df-fl 10925  df-seq 11047  df-exp 11105  df-hash 11338  df-cj 11584  df-re 11585  df-im 11586  df-sqr 11720  df-abs 11721  df-limsup 11945  df-clim 11962  df-rlim 11963  df-sum 12159
 Copyright terms: Public domain W3C validator