Metamath Proof Explorer


Theorem eftlcl

Description: Closure of the sum of an infinite tail of the series defining the exponential function. (Contributed by Paul Chapman, 17-Jan-2008) (Revised by Mario Carneiro, 30-Apr-2014)

Ref Expression
Hypothesis eftl.1 F = n 0 A n n !
Assertion eftlcl A M 0 k M F k

Proof

Step Hyp Ref Expression
1 eftl.1 F = n 0 A n n !
2 eqid M = M
3 nn0z M 0 M
4 3 adantl A M 0 M
5 eqidd A M 0 k M F k = F k
6 eluznn0 M 0 k M k 0
7 6 adantll A M 0 k M k 0
8 1 eftval k 0 F k = A k k !
9 7 8 syl A M 0 k M F k = A k k !
10 simpll A M 0 k M A
11 eftcl A k 0 A k k !
12 10 7 11 syl2anc A M 0 k M A k k !
13 9 12 eqeltrd A M 0 k M F k
14 1 eftlcvg A M 0 seq M + F dom
15 2 4 5 13 14 isumcl A M 0 k M F k