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 ) ) |