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

Theorem eftlub 12703
 Description: An upper bound on the absolute value of the infinite tail of the series expansion of the exponential function on the closed unit disk. (Contributed by Paul Chapman, 19-Jan-2008.) (Proof shortened by Mario Carneiro, 29-Apr-2014.)
Hypotheses
Ref Expression
eftl.1
eftl.2
eftl.3
eftl.4
eftl.5
eftl.6
Assertion
Ref Expression
eftlub
Distinct variable groups:   ,,   ,   ,   ,,   ,
Allowed substitution hints:   ()   ()   ()   (,)

Proof of Theorem eftlub
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eftl.5 . . . 4
2 eftl.4 . . . . 5
32nnnn0d 10267 . . . 4
4 eftl.1 . . . . 5
54eftlcl 12701 . . . 4
61, 3, 5syl2anc 643 . . 3
76abscld 12231 . 2
81abscld 12231 . . 3
9 eftl.2 . . . 4
109reeftlcl 12702 . . 3
118, 3, 10syl2anc 643 . 2
128, 3reexpcld 11533 . . 3
13 peano2nn0 10253 . . . . . 6
143, 13syl 16 . . . . 5
1514nn0red 10268 . . . 4
16 faccl 11569 . . . . . 6
173, 16syl 16 . . . . 5
1817, 2nnmulcld 10040 . . . 4
1915, 18nndivred 10041 . . 3
2012, 19remulcld 9109 . 2
21 eqid 2436 . . 3
222nnzd 10367 . . . 4
23 eqidd 2437 . . . 4
24 eluznn0 10539 . . . . . 6
253, 24sylan 458 . . . . 5
264eftval 12672 . . . . . . 7
2726adantl 453 . . . . . 6
28 eftcl 12669 . . . . . . 7
291, 28sylan 458 . . . . . 6
3027, 29eqeltrd 2510 . . . . 5
3125, 30syldan 457 . . . 4
324eftlcvg 12700 . . . . 5
331, 3, 32syl2anc 643 . . . 4
3421, 22, 23, 31, 33isumclim2 12535 . . 3
35 eqidd 2437 . . . 4
369eftval 12672 . . . . . . . 8
3736adantl 453 . . . . . . 7
38 reeftcl 12670 . . . . . . . 8
398, 38sylan 458 . . . . . . 7
4037, 39eqeltrd 2510 . . . . . 6
4125, 40syldan 457 . . . . 5
4241recnd 9107 . . . 4
438recnd 9107 . . . . 5
449eftlcvg 12700 . . . . 5
4543, 3, 44syl2anc 643 . . . 4
4621, 22, 35, 42, 45isumclim2 12535 . . 3
47 eftabs 12671 . . . . . 6
481, 47sylan 458 . . . . 5
4927fveq2d 5725 . . . . 5
5048, 49, 373eqtr4rd 2479 . . . 4
5125, 50syldan 457 . . 3
5221, 34, 46, 22, 31, 51iserabs 12587 . 2
53 nn0uz 10513 . . . 4
54 0z 10286 . . . . 5
5554a1i 11 . . . 4
562nncnd 10009 . . . . 5
57 nn0cn 10224 . . . . 5
58 nn0ex 10220 . . . . . . . 8
5958mptex 5959 . . . . . . 7
609, 59eqeltri 2506 . . . . . 6
6160shftval4 11885 . . . . 5
6256, 57, 61syl2an 464 . . . 4
63 nn0addcl 10248 . . . . . . 7
643, 63sylan 458 . . . . . 6
659eftval 12672 . . . . . 6
6664, 65syl 16 . . . . 5
678adantr 452 . . . . . 6
68 reeftcl 12670 . . . . . 6
6967, 64, 68syl2anc 643 . . . . 5
7066, 69eqeltrd 2510 . . . 4
71 oveq2 6082 . . . . . . 7
7271oveq2d 6090 . . . . . 6
73 eftl.3 . . . . . 6
74 ovex 6099 . . . . . 6
7572, 73, 74fvmpt 5799 . . . . 5
7675adantl 453 . . . 4
7712, 17nndivred 10041 . . . . . 6
7877adantr 452 . . . . 5
792peano2nnd 10010 . . . . . . 7
8079nnrecred 10038 . . . . . 6
81 reexpcl 11391 . . . . . 6
8280, 81sylan 458 . . . . 5
8378, 82remulcld 9109 . . . 4
8467, 64reexpcld 11533 . . . . . . 7
8512adantr 452 . . . . . . 7
86 faccl 11569 . . . . . . . . . 10
8764, 86syl 16 . . . . . . . . 9
8887nnred 10008 . . . . . . . 8
8988, 83remulcld 9109 . . . . . . 7
903adantr 452 . . . . . . . 8
91 uzid 10493 . . . . . . . . . 10
9222, 91syl 16 . . . . . . . . 9
93 uzaddcl 10526 . . . . . . . . 9
9492, 93sylan 458 . . . . . . . 8
951absge0d 12239 . . . . . . . . 9
9695adantr 452 . . . . . . . 8
97 eftl.6 . . . . . . . . 9
9897adantr 452 . . . . . . . 8
9967, 90, 94, 96, 98leexp2rd 11549 . . . . . . 7
10017adantr 452 . . . . . . . . . . . 12
101 nnexpcl 11387 . . . . . . . . . . . . 13
10279, 101sylan 458 . . . . . . . . . . . 12
103100, 102nnmulcld 10040 . . . . . . . . . . 11
104103nnred 10008 . . . . . . . . . 10
1058, 3, 95expge0d 11534 . . . . . . . . . . . 12
10612, 105jca 519 . . . . . . . . . . 11
107106adantr 452 . . . . . . . . . 10
108 faclbnd6 11583 . . . . . . . . . . 11
1093, 108sylan 458 . . . . . . . . . 10
110 lemul1a 9857 . . . . . . . . . 10
111104, 88, 107, 109, 110syl31anc 1187 . . . . . . . . 9
11288, 85remulcld 9109 . . . . . . . . . 10
113103nnrpd 10640 . . . . . . . . . 10
11485, 112, 113lemuldiv2d 10687 . . . . . . . . 9
115111, 114mpbid 202 . . . . . . . 8
11687nncnd 10009 . . . . . . . . . 10
11712recnd 9107 . . . . . . . . . . 11
118117adantr 452 . . . . . . . . . 10
119103nncnd 10009 . . . . . . . . . 10
120103nnne0d 10037 . . . . . . . . . 10
121116, 118, 119, 120divassd 9818 . . . . . . . . 9
12279nncnd 10009 . . . . . . . . . . . . . 14
123122adantr 452 . . . . . . . . . . . . 13
12479adantr 452 . . . . . . . . . . . . . 14
125124nnne0d 10037 . . . . . . . . . . . . 13
126 nn0z 10297 . . . . . . . . . . . . . 14
127126adantl 453 . . . . . . . . . . . . 13
128123, 125, 127exprecd 11524 . . . . . . . . . . . 12
129128oveq2d 6090 . . . . . . . . . . 11
13077recnd 9107 . . . . . . . . . . . . 13
131130adantr 452 . . . . . . . . . . . 12
132102nncnd 10009 . . . . . . . . . . . 12
133102nnne0d 10037 . . . . . . . . . . . 12
134131, 132, 133divrecd 9786 . . . . . . . . . . 11
13517nncnd 10009 . . . . . . . . . . . . 13
136135adantr 452 . . . . . . . . . . . 12
137 facne0 11570 . . . . . . . . . . . . . 14
1383, 137syl 16 . . . . . . . . . . . . 13
139138adantr 452 . . . . . . . . . . . 12
140118, 136, 132, 139, 133divdiv1d 9814 . . . . . . . . . . 11
141129, 134, 1403eqtr2rd 2475 . . . . . . . . . 10
142141oveq2d 6090 . . . . . . . . 9
143121, 142eqtrd 2468 . . . . . . . 8
144115, 143breqtrd 4229 . . . . . . 7
14584, 85, 89, 99, 144letrd 9220 . . . . . 6
14687nngt0d 10036 . . . . . . 7
147 ledivmul 9876 . . . . . . 7
14884, 83, 88, 146, 147syl112anc 1188 . . . . . 6
149145, 148mpbird 224 . . . . 5
15066, 149eqbrtrd 4225 . . . 4
15122znegcld 10370 . . . . . 6
15260seqshft 11893 . . . . . 6
15354, 151, 152sylancr 645 . . . . 5
154 0cn 9077 . . . . . . . . . . . 12
155 subneg 9343 . . . . . . . . . . . 12
156154, 155mpan 652 . . . . . . . . . . 11
157 addid2 9242 . . . . . . . . . . 11
158156, 157eqtrd 2468 . . . . . . . . . 10
15956, 158syl 16 . . . . . . . . 9
160159seqeq1d 11322 . . . . . . . 8
161160, 46eqbrtrd 4225 . . . . . . 7
162 seqex 11318 . . . . . . . 8
163 climshft 12363 . . . . . . . 8
164151, 162, 163sylancl 644 . . . . . . 7
165161, 164mpbird 224 . . . . . 6
166 ovex 6099 . . . . . . 7
167 sumex 12474 . . . . . . 7
168166, 167breldm 5067 . . . . . 6
169165, 168syl 16 . . . . 5
170153, 169eqeltrd 2510 . . . 4
1712nnge1d 10035 . . . . . . . . . 10
172 1nn 10004 . . . . . . . . . . 11
173 nnleltp1 10322 . . . . . . . . . . 11
174172, 2, 173sylancr 645 . . . . . . . . . 10
175171, 174mpbid 202 . . . . . . . . 9
17614nn0ge0d 10270 . . . . . . . . . 10
17715, 176absidd 12218 . . . . . . . . 9
178175, 177breqtrrd 4231 . . . . . . . 8
179 eqid 2436 . . . . . . . . . 10
180 ovex 6099 . . . . . . . . . 10
18171, 179, 180fvmpt 5799 . . . . . . . . 9
182181adantl 453 . . . . . . . 8
183122, 178, 182georeclim 12642 . . . . . . 7
18482recnd 9107 . . . . . . . 8
185182, 184eqeltrd 2510 . . . . . . 7
186182oveq2d 6090 . . . . . . . 8
18776, 186eqtr4d 2471 . . . . . . 7
18853, 55, 130, 183, 185, 187isermulc2 12444 . . . . . 6
189 ax-1cn 9041 . . . . . . . . . . 11
190 pncan 9304 . . . . . . . . . . 11
19156, 189, 190sylancl 644 . . . . . . . . . 10
192191oveq2d 6090 . . . . . . . . 9
193192oveq2d 6090 . . . . . . . 8
19415, 2nndivred 10041 . . . . . . . . . 10
195194recnd 9107 . . . . . . . . 9
196117, 195, 135, 138div23d 9820 . . . . . . . 8
197193, 196eqtr4d 2471 . . . . . . 7
198117, 195, 135, 138divassd 9818 . . . . . . 7
1992nnne0d 10037 . . . . . . . . . 10
200122, 56, 135, 199, 138divdiv1d 9814 . . . . . . . . 9
20156, 135mulcomd 9102 . . . . . . . . . 10
202201oveq2d 6090 . . . . . . . . 9
203200, 202eqtrd 2468 . . . . . . . 8
204203oveq2d 6090 . . . . . . 7
205197, 198, 2043eqtrd 2472 . . . . . 6
206188, 205breqtrd 4229 . . . . 5
207 seqex 11318 . . . . . 6
208 ovex 6099 . . . . . 6
209207, 208breldm 5067 . . . . 5
210206, 209syl 16 . . . 4
21153, 55, 62, 70, 76, 83, 150, 170, 210isumle 12617 . . 3
212 eqid 2436 . . . . 5
213 fveq2 5721 . . . . 5
21456addid2d 9260 . . . . . . . . 9
215214fveq2d 5725 . . . . . . . 8
216215eleq2d 2503 . . . . . . 7
217216biimpa 471 . . . . . 6
218217, 42syldan 457 . . . . 5
21953, 212, 213, 22, 55, 218isumshft 12612 . . . 4
220215sumeq1d 12488 . . . 4
221219, 220eqtr3d 2470 . . 3
22283recnd 9107 . . . 4
22353, 55, 76, 222, 206isumclim 12534 . . 3
224211, 221, 2233brtr3d 4234 . 2
2257, 11, 20, 52, 224letrd 9220 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725   wne 2599  cvv 2949   class class class wbr 4205   cmpt 4259   cdm 4871  cfv 5447  (class class class)co 6074  cc 8981  cr 8982  cc0 8983  c1 8984   caddc 8986   cmul 8988   clt 9113   cle 9114   cmin 9284  cneg 9285   cdiv 9670  cn 9993  cn0 10214  cz 10275  cuz 10481   cseq 11316  cexp 11375  cfa 11559   cshi 11874  cabs 12032   cli 12271  csu 12472 This theorem is referenced by:  ef01bndlem  12778  eirrlem  12796  dveflem  19856  subfaclim  24867 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 2417  ax-rep 4313  ax-sep 4323  ax-nul 4331  ax-pow 4370  ax-pr 4396  ax-un 4694  ax-inf2 7589  ax-cnex 9039  ax-resscn 9040  ax-1cn 9041  ax-icn 9042  ax-addcl 9043  ax-addrcl 9044  ax-mulcl 9045  ax-mulrcl 9046  ax-mulcom 9047  ax-addass 9048  ax-mulass 9049  ax-distr 9050  ax-i2m1 9051  ax-1ne0 9052  ax-1rid 9053  ax-rnegex 9054  ax-rrecex 9055  ax-cnre 9056  ax-pre-lttri 9057  ax-pre-lttrn 9058  ax-pre-ltadd 9059  ax-pre-mulgt0 9060  ax-pre-sup 9061  ax-addf 9062  ax-mulf 9063 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 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2703  df-rex 2704  df-reu 2705  df-rmo 2706  df-rab 2707  df-v 2951  df-sbc 3155  df-csb 3245  df-dif 3316  df-un 3318  df-in 3320  df-ss 3327  df-pss 3329  df-nul 3622  df-if 3733  df-pw 3794  df-sn 3813  df-pr 3814  df-tp 3815  df-op 3816  df-uni 4009  df-int 4044  df-iun 4088  df-br 4206  df-opab 4260  df-mpt 4261  df-tr 4296  df-eprel 4487  df-id 4491  df-po 4496  df-so 4497  df-fr 4534  df-se 4535  df-we 4536  df-ord 4577  df-on 4578  df-lim 4579  df-suc 4580  df-om 4839  df-xp 4877  df-rel 4878  df-cnv 4879  df-co 4880  df-dm 4881  df-rn 4882  df-res 4883  df-ima 4884  df-iota 5411  df-fun 5449  df-fn 5450  df-f 5451  df-f1 5452  df-fo 5453  df-f1o 5454  df-fv 5455  df-isom 5456  df-ov 6077  df-oprab 6078  df-mpt2 6079  df-1st 6342  df-2nd 6343  df-riota 6542  df-recs 6626  df-rdg 6661  df-1o 6717  df-oadd 6721  df-er 6898  df-pm 7014  df-en 7103  df-dom 7104  df-sdom 7105  df-fin 7106  df-sup 7439  df-oi 7472  df-card 7819  df-pnf 9115  df-mnf 9116  df-xr 9117  df-ltxr 9118  df-le 9119  df-sub 9286  df-neg 9287  df-div 9671  df-nn 9994  df-2 10051  df-3 10052  df-n0 10215  df-z 10276  df-uz 10482  df-rp 10606  df-ico 10915  df-fz 11037  df-fzo 11129  df-fl 11195  df-seq 11317  df-exp 11376  df-fac 11560  df-hash 11612  df-shft 11875  df-cj 11897  df-re 11898  df-im 11899  df-sqr 12033  df-abs 12034  df-limsup 12258  df-clim 12275  df-rlim 12276  df-sum 12473
 Copyright terms: Public domain W3C validator