Metamath Proof Explorer

Theorem reeftlcl

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 reeftlcl 
|- ( ( A e. RR /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. RR )

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. RR /\ M e. NN0 ) -> M e. ZZ )
5 eqidd 
 |-  ( ( ( A e. RR /\ 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. RR /\ 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. RR /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
10 simpll 
 |-  ( ( ( A e. RR /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> A e. RR )
11 reeftcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
12 10 7 11 syl2anc 
 |-  ( ( ( A e. RR /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
13 9 12 eqeltrd 
 |-  ( ( ( A e. RR /\ M e. NN0 ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. RR )
14 recn 
 |-  ( A e. RR -> A e. CC )
15 1 eftlcvg 
 |-  ( ( A e. CC /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
16 14 15 sylan 
 |-  ( ( A e. RR /\ M e. NN0 ) -> seq M ( + , F ) e. dom ~~> )
17 2 4 5 13 16 isumrecl 
 |-  ( ( A e. RR /\ M e. NN0 ) -> sum_ k e. ( ZZ>= ` M ) ( F ` k ) e. RR )