Metamath Proof Explorer

Theorem eff

Description: Domain and codomain of the exponential function. (Contributed by Paul Chapman, 22-Oct-2007) (Proof shortened by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion eff 
|- exp : CC --> CC

Proof

Step Hyp Ref Expression
1 df-ef 
 |-  exp = ( x e. CC |-> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) )
2 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
3 0zd 
 |-  ( x e. CC -> 0 e. ZZ )
4 eqid 
 |-  ( n e. NN0 |-> ( ( x ^ n ) / ( ! ` n ) ) ) = ( n e. NN0 |-> ( ( x ^ n ) / ( ! ` n ) ) )
5 4 eftval 
 |-  ( k e. NN0 -> ( ( n e. NN0 |-> ( ( x ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( x ^ k ) / ( ! ` k ) ) )
6 5 adantl 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( ( n e. NN0 |-> ( ( x ^ n ) / ( ! ` n ) ) ) ` k ) = ( ( x ^ k ) / ( ! ` k ) ) )
7 eftcl 
 |-  ( ( x e. CC /\ k e. NN0 ) -> ( ( x ^ k ) / ( ! ` k ) ) e. CC )
8 4 efcllem 
 |-  ( x e. CC -> seq 0 ( + , ( n e. NN0 |-> ( ( x ^ n ) / ( ! ` n ) ) ) ) e. dom ~~> )
9 2 3 6 7 8 isumcl 
 |-  ( x e. CC -> sum_ k e. NN0 ( ( x ^ k ) / ( ! ` k ) ) e. CC )
10 1 9 fmpti 
 |-  exp : CC --> CC