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 mulid1
 |-  ( A e. CC -> ( A x. 1 ) = A )
9 7 8 syl5eq
 |-  ( 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 ) )