Metamath Proof Explorer

Theorem ecxp

Description: Write the exponential function as an exponent to the power _e . (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion ecxp 
|- ( A e. CC -> ( _e ^c A ) = ( exp ` A ) )

Proof

Step Hyp Ref Expression
1 ere 
 |-  _e e. RR
2 1 recni 
 |-  _e e. CC
3 ene0 
 |-  _e =/= 0
4 cxpef 
 |-  ( ( _e e. CC /\ _e =/= 0 /\ A e. CC ) -> ( _e ^c A ) = ( exp ` ( A x. ( log ` _e ) ) ) )
5 2 3 4 mp3an12 
 |-  ( A e. CC -> ( _e ^c A ) = ( exp ` ( A x. ( log ` _e ) ) ) )
6 loge 
 |-  ( log ` _e ) = 1
7 6 oveq2i 
 |-  ( A x. ( log ` _e ) ) = ( A x. 1 )
8 mulrid 
 |-  ( A e. CC -> ( A x. 1 ) = A )
9 7 8 eqtrid 
 |-  ( A e. CC -> ( A x. ( log ` _e ) ) = A )
10 9 fveq2d 
 |-  ( A e. CC -> ( exp ` ( A x. ( log ` _e ) ) ) = ( exp ` A ) )
11 5 10 eqtrd 
 |-  ( A e. CC -> ( _e ^c A ) = ( exp ` A ) )