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=n0Ann!
Assertion eftlcl AM0kMFk

Proof

Step Hyp Ref Expression
1 eftl.1 F=n0Ann!
2 eqid M=M
3 nn0z M0M
4 3 adantl AM0M
5 eqidd AM0kMFk=Fk
6 eluznn0 M0kMk0
7 6 adantll AM0kMk0
8 1 eftval k0Fk=Akk!
9 7 8 syl AM0kMFk=Akk!
10 simpll AM0kMA
11 eftcl Ak0Akk!
12 10 7 11 syl2anc AM0kMAkk!
13 9 12 eqeltrd AM0kMFk
14 1 eftlcvg AM0seqM+Fdom
15 2 4 5 13 14 isumcl AM0kMFk