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