Metamath Proof Explorer

Theorem reefcl

Description: The exponential function is real if its argument is real. (Contributed by NM, 27-Apr-2005) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion reefcl 
|- ( A e. RR -> ( exp ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 recn 
 |-  ( A e. RR -> A e. CC )
2 efval 
 |-  ( A e. CC -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
3 1 2 syl 
 |-  ( A e. RR -> ( exp ` A ) = sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) )
4 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
5 0zd 
 |-  ( A e. RR -> 0 e. ZZ )
6 eqid 
 |-  ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) )
7 6 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
8 7 adantl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( A ^ k ) / ( ! ` k ) ) )
9 reeftcl 
 |-  ( ( A e. RR /\ k e. NN0 ) -> ( ( A ^ k ) / ( ! ` k ) ) e. RR )
10 6 efcllem 
 |-  ( A e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
11 1 10 syl 
 |-  ( A e. RR -> seq 0 ( + , ( n e. NN0 |-> ( ( A ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
12 4 5 8 9 11 isumrecl 
 |-  ( A e. RR -> sum_ k e. NN0 ( ( A ^ k ) / ( ! ` k ) ) e. RR )
13 3 12 eqeltrd 
 |-  ( A e. RR -> ( exp ` A ) e. RR )