Metamath Proof Explorer

Theorem explog

Description: Exponentiation of a nonzero complex number to an integer power. (Contributed by Paul Chapman, 21-Apr-2008)

Ref Expression
Assertion explog 
|- ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )

Proof

Step Hyp Ref Expression
1 logcl 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( log ` A ) e. CC )
2 efexp 
 |-  ( ( ( log ` A ) e. CC /\ N e. ZZ ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( ( exp ` ( log ` A ) ) ^ N ) )
3 1 2 stoic3 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( exp ` ( N x. ( log ` A ) ) ) = ( ( exp ` ( log ` A ) ) ^ N ) )
4 eflog 
 |-  ( ( A e. CC /\ A =/= 0 ) -> ( exp ` ( log ` A ) ) = A )
5 4 3adant3 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( exp ` ( log ` A ) ) = A )
6 5 oveq1d 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( ( exp ` ( log ` A ) ) ^ N ) = ( A ^ N ) )
7 3 6 eqtr2d 
 |-  ( ( A e. CC /\ A =/= 0 /\ N e. ZZ ) -> ( A ^ N ) = ( exp ` ( N x. ( log ` A ) ) ) )