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 e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
Assertion eftlcl 
|- ( ( A e. CC /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. CC )

Proof

Step Hyp Ref Expression
1 eftl.1 
 |-  F = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
2 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
3 nn0z 
 |-  ( M e. NN0 -> M e. ZZ )
4 3 adantl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> M e. ZZ )
5 eqidd 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( F ` k ) )
6 eluznn0 
 |-  ( ( M e. NN0 /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
7 6 adantll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> k e. NN0 )
8 1 eftval 
 |-  ( k e. NN0 -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
9 7 8 syl 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
10 simpll 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> A e. CC )
11 eftcl 
 |-  ( ( A e. CC /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
12 10 7 11 syl2anc 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( ( A ^ k ) / ( ! ` k ) ) e. CC )
13 9 12 eqeltrd 
 |-  ( ( ( A e. CC /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
14 1 eftlcvg 
 |-  ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
15 2 4 5 13 14 isumcl 
 |-  ( ( A e. CC /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. CC )