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 | |
|
Assertion | eftlcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eftl.1 | |
|
2 | eqid | |
|
3 | nn0z | |
|
4 | 3 | adantl | |
5 | eqidd | |
|
6 | eluznn0 | |
|
7 | 6 | adantll | |
8 | 1 | eftval | |
9 | 7 8 | syl | |
10 | simpll | |
|
11 | eftcl | |
|
12 | 10 7 11 | syl2anc | |
13 | 9 12 | eqeltrd | |
14 | 1 | eftlcvg | |
15 | 2 4 5 13 14 | isumcl | |