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

Theorem eftlub 13844
 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:   ,,   ,   ,   ,M,   ,

Proof of Theorem eftlub
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 eftl.5 . . . 4
2 eftl.4 . . . . 5
32nnnn0d 10877 . . . 4
4 eftl.1 . . . . 5
54eftlcl 13842 . . . 4
61, 3, 5syl2anc 661 . . 3
76abscld 13267 . 2
81abscld 13267 . . 3
9 eftl.2 . . . 4
109reeftlcl 13843 . . 3
118, 3, 10syl2anc 661 . 2
128, 3reexpcld 12327 . . 3
13 peano2nn0 10861 . . . . . 6
143, 13syl 16 . . . . 5
1514nn0red 10878 . . . 4
16 faccl 12363 . . . . . 6
173, 16syl 16 . . . . 5
1817, 2nnmulcld 10608 . . . 4
1915, 18nndivred 10609 . . 3
2012, 19remulcld 9645 . 2
21 eqid 2457 . . 3
222nnzd 10993 . . . 4
23 eqidd 2458 . . . 4
24 eluznn0 11180 . . . . . 6
253, 24sylan 471 . . . . 5
264eftval 13812 . . . . . . 7
2726adantl 466 . . . . . 6
28 eftcl 13809 . . . . . . 7
291, 28sylan 471 . . . . . 6
3027, 29eqeltrd 2545 . . . . 5
3125, 30syldan 470 . . . 4
324eftlcvg 13841 . . . . 5
331, 3, 32syl2anc 661 . . . 4
3421, 22, 23, 31, 33isumclim2 13573 . . 3
35 eqidd 2458 . . . 4
369eftval 13812 . . . . . . . 8
3736adantl 466 . . . . . . 7
38 reeftcl 13810 . . . . . . . 8
398, 38sylan 471 . . . . . . 7
4037, 39eqeltrd 2545 . . . . . 6
4125, 40syldan 470 . . . . 5
4241recnd 9643 . . . 4
438recnd 9643 . . . . 5
449eftlcvg 13841 . . . . 5
4543, 3, 44syl2anc 661 . . . 4
4621, 22, 35, 42, 45isumclim2 13573 . . 3
47 eftabs 13811 . . . . . 6
481, 47sylan 471 . . . . 5
4927fveq2d 5875 . . . . 5
5048, 49, 373eqtr4rd 2509 . . . 4
5125, 50syldan 470 . . 3
5221, 34, 46, 22, 31, 51iserabs 13629 . 2
53 nn0uz 11144 . . . 4
54 0zd 10901 . . . 4
552nncnd 10577 . . . . 5
56 nn0cn 10830 . . . . 5
57 nn0ex 10826 . . . . . . . 8
5857mptex 6143 . . . . . . 7
599, 58eqeltri 2541 . . . . . 6
6059shftval4 12910 . . . . 5
6155, 56, 60syl2an 477 . . . 4
62 nn0addcl 10856 . . . . . . 7
633, 62sylan 471 . . . . . 6
649eftval 13812 . . . . . 6
6563, 64syl 16 . . . . 5
668adantr 465 . . . . . 6
67 reeftcl 13810 . . . . . 6
6866, 63, 67syl2anc 661 . . . . 5
6965, 68eqeltrd 2545 . . . 4
70 oveq2 6304 . . . . . . 7
7170oveq2d 6312 . . . . . 6
72 eftl.3 . . . . . 6
73 ovex 6324 . . . . . 6
7471, 72, 73fvmpt 5956 . . . . 5
7574adantl 466 . . . 4
7612, 17nndivred 10609 . . . . . 6
7776adantr 465 . . . . 5
782peano2nnd 10578 . . . . . . 7
7978nnrecred 10606 . . . . . 6
80 reexpcl 12183 . . . . . 6
8179, 80sylan 471 . . . . 5
8277, 81remulcld 9645 . . . 4
8366, 63reexpcld 12327 . . . . . . 7
8412adantr 465 . . . . . . 7
85 faccl 12363 . . . . . . . . . 10
8663, 85syl 16 . . . . . . . . 9
8786nnred 10576 . . . . . . . 8
8887, 82remulcld 9645 . . . . . . 7
893adantr 465 . . . . . . . 8
90 uzid 11124 . . . . . . . . . 10
9122, 90syl 16 . . . . . . . . 9
92 uzaddcl 11166 . . . . . . . . 9
9391, 92sylan 471 . . . . . . . 8
941absge0d 13275 . . . . . . . . 9
9594adantr 465 . . . . . . . 8
96 eftl.6 . . . . . . . . 9
9796adantr 465 . . . . . . . 8
9866, 89, 93, 95, 97leexp2rd 12343 . . . . . . 7
9917adantr 465 . . . . . . . . . . . 12
100 nnexpcl 12179 . . . . . . . . . . . . 13
10178, 100sylan 471 . . . . . . . . . . . 12
10299, 101nnmulcld 10608 . . . . . . . . . . 11
103102nnred 10576 . . . . . . . . . 10
1048, 3, 94expge0d 12328 . . . . . . . . . . . 12
10512, 104jca 532 . . . . . . . . . . 11
106105adantr 465 . . . . . . . . . 10
107 faclbnd6 12377 . . . . . . . . . . 11
1083, 107sylan 471 . . . . . . . . . 10
109 lemul1a 10421 . . . . . . . . . 10
110103, 87, 106, 108, 109syl31anc 1231 . . . . . . . . 9
11187, 84remulcld 9645 . . . . . . . . . 10
112102nnrpd 11284 . . . . . . . . . 10
11384, 111, 112lemuldiv2d 11331 . . . . . . . . 9
114110, 113mpbid 210 . . . . . . . 8
11586nncnd 10577 . . . . . . . . . 10
11612recnd 9643 . . . . . . . . . . 11
117116adantr 465 . . . . . . . . . 10
118102nncnd 10577 . . . . . . . . . 10
119102nnne0d 10605 . . . . . . . . . 10
120115, 117, 118, 119divassd 10380 . . . . . . . . 9
12178nncnd 10577 . . . . . . . . . . . . . 14
122121adantr 465 . . . . . . . . . . . . 13
12378adantr 465 . . . . . . . . . . . . . 14
124123nnne0d 10605 . . . . . . . . . . . . 13
125 nn0z 10912 . . . . . . . . . . . . . 14
126125adantl 466 . . . . . . . . . . . . 13
127122, 124, 126exprecd 12318 . . . . . . . . . . . 12
128127oveq2d 6312 . . . . . . . . . . 11
12976recnd 9643 . . . . . . . . . . . . 13
130129adantr 465 . . . . . . . . . . . 12
131101nncnd 10577 . . . . . . . . . . . 12
132101nnne0d 10605 . . . . . . . . . . . 12
133130, 131, 132divrecd 10348 . . . . . . . . . . 11
13417nncnd 10577 . . . . . . . . . . . . 13
135134adantr 465 . . . . . . . . . . . 12
136 facne0 12364 . . . . . . . . . . . . . 14
1373, 136syl 16 . . . . . . . . . . . . 13
138137adantr 465 . . . . . . . . . . . 12
139117, 135, 131, 138, 132divdiv1d 10376 . . . . . . . . . . 11
140128, 133, 1393eqtr2rd 2505 . . . . . . . . . 10
141140oveq2d 6312 . . . . . . . . 9
142120, 141eqtrd 2498 . . . . . . . 8
143114, 142breqtrd 4476 . . . . . . 7
14483, 84, 88, 98, 143letrd 9760 . . . . . 6
14586nngt0d 10604 . . . . . . 7
146 ledivmul 10443 . . . . . . 7
14783, 82, 87, 145, 146syl112anc 1232 . . . . . 6
148144, 147mpbird 232 . . . . 5
14965, 148eqbrtrd 4472 . . . 4
150 0z 10900 . . . . . 6
15122znegcld 10996 . . . . . 6
15259seqshft 12918 . . . . . 6
153150, 151, 152sylancr 663 . . . . 5
154 0cn 9609 . . . . . . . . . . . 12
155 subneg 9891 . . . . . . . . . . . 12
156154, 155mpan 670 . . . . . . . . . . 11
157 addid2 9784 . . . . . . . . . . 11
158156, 157eqtrd 2498 . . . . . . . . . 10
15955, 158syl 16 . . . . . . . . 9
160159seqeq1d 12113 . . . . . . . 8
161160, 46eqbrtrd 4472 . . . . . . 7
162 seqex 12109 . . . . . . . 8
163 climshft 13399 . . . . . . . 8
164151, 162, 163sylancl 662 . . . . . . 7
165161, 164mpbird 232 . . . . . 6
166 ovex 6324 . . . . . . 7
167 sumex 13510 . . . . . . 7
168166, 167breldm 5212 . . . . . 6
169165, 168syl 16 . . . . 5
170153, 169eqeltrd 2545 . . . 4
1712nnge1d 10603 . . . . . . . . . 10
172 1nn 10572 . . . . . . . . . . 11
173 nnleltp1 10943 . . . . . . . . . . 11
174172, 2, 173sylancr 663 . . . . . . . . . 10
175171, 174mpbid 210 . . . . . . . . 9
17614nn0ge0d 10880 . . . . . . . . . 10
17715, 176absidd 13254 . . . . . . . . 9
178175, 177breqtrrd 4478 . . . . . . . 8
179 eqid 2457 . . . . . . . . . 10
180 ovex 6324 . . . . . . . . . 10
18170, 179, 180fvmpt 5956 . . . . . . . . 9
182181adantl 466 . . . . . . . 8
183121, 178, 182georeclim 13681 . . . . . . 7
18481recnd 9643 . . . . . . . 8
185182, 184eqeltrd 2545 . . . . . . 7
186182oveq2d 6312 . . . . . . . 8
18775, 186eqtr4d 2501 . . . . . . 7
18853, 54, 129, 183, 185, 187isermulc2 13480 . . . . . 6
189 ax-1cn 9571 . . . . . . . . . . 11
190 pncan 9849 . . . . . . . . . . 11
19155, 189, 190sylancl 662 . . . . . . . . . 10
192191oveq2d 6312 . . . . . . . . 9
193192oveq2d 6312 . . . . . . . 8
19415, 2nndivred 10609 . . . . . . . . . 10
195194recnd 9643 . . . . . . . . 9
196116, 195, 134, 137div23d 10382 . . . . . . . 8
197193, 196eqtr4d 2501 . . . . . . 7
198116, 195, 134, 137divassd 10380 . . . . . . 7
1992nnne0d 10605 . . . . . . . . . 10
200121, 55, 134, 199, 137divdiv1d 10376 . . . . . . . . 9
20155, 134mulcomd 9638 . . . . . . . . . 10
202201oveq2d 6312 . . . . . . . . 9
203200, 202eqtrd 2498 . . . . . . . 8
204203oveq2d 6312 . . . . . . 7
205197, 198, 2043eqtrd 2502 . . . . . 6
206188, 205breqtrd 4476 . . . . 5
207 seqex 12109 . . . . . 6
208 ovex 6324 . . . . . 6
209207, 208breldm 5212 . . . . 5
210206, 209syl 16 . . . 4
21153, 54, 61, 69, 75, 82, 149, 170, 210isumle 13656 . . 3
212 eqid 2457 . . . . 5
213 fveq2 5871 . . . . 5
21455addid2d 9802 . . . . . . . . 9
215214fveq2d 5875 . . . . . . . 8
216215eleq2d 2527 . . . . . . 7
217216biimpa 484 . . . . . 6
218217, 42syldan 470 . . . . 5
21953, 212, 213, 22, 54, 218isumshft 13651 . . . 4
220215sumeq1d 13523 . . . 4
221219, 220eqtr3d 2500 . . 3
22282recnd 9643 . . . 4
22353, 54, 75, 222, 206isumclim 13572 . . 3
224211, 221, 2233brtr3d 4481 . 2
2257, 11, 20, 52, 224letrd 9760 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  =/=wne 2652   cvv 3109   class class class wbr 4452  e.cmpt 4510  domcdm 5004  cfv 5593  (class class class)co 6296   cc 9511   cr 9512  0cc0 9513  1c1 9514   caddc 9516   cmul 9518   clt 9649   cle 9650   cmin 9828  -ucneg 9829   cdiv 10231   cn 10561   cn0 10820   cz 10889   cuz 11110  seqcseq 12107   cexp 12166   cfa 12353   cshi 12899   cabs 13067   cli 13307  sum_`csu 13508 This theorem is referenced by:  ef01bndlem  13919  eirrlem  13937  dveflem  22380  subfaclim  28632 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592  ax-inf2 8079  ax-cnex 9569  ax-resscn 9570  ax-1cn 9571  ax-icn 9572  ax-addcl 9573  ax-addrcl 9574  ax-mulcl 9575  ax-mulrcl 9576  ax-mulcom 9577  ax-addass 9578  ax-mulass 9579  ax-distr 9580  ax-i2m1 9581  ax-1ne0 9582  ax-1rid 9583  ax-rnegex 9584  ax-rrecex 9585  ax-cnre 9586  ax-pre-lttri 9587  ax-pre-lttrn 9588  ax-pre-ltadd 9589  ax-pre-mulgt0 9590  ax-pre-sup 9591  ax-addf 9592  ax-mulf 9593 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-fal 1401  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-se 4844  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-isom 5602  df-riota 6257  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-1st 6800  df-2nd 6801  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-pm 7442  df-en 7537  df-dom 7538  df-sdom 7539  df-fin 7540  df-sup 7921  df-oi 7956  df-card 8341  df-pnf 9651  df-mnf 9652  df-xr 9653  df-ltxr 9654  df-le 9655  df-sub 9830  df-neg 9831  df-div 10232  df-nn 10562  df-2 10619  df-3 10620  df-n0 10821  df-z 10890  df-uz 11111  df-rp 11250  df-ico 11564  df-fz 11702  df-fzo 11825  df-fl 11929  df-seq 12108  df-exp 12167  df-fac 12354  df-hash 12406  df-shft 12900  df-cj 12932  df-re 12933  df-im 12934  df-sqrt 13068  df-abs 13069  df-limsup 13294  df-clim 13311  df-rlim 13312  df-sum 13509
 Copyright terms: Public domain W3C validator