Metamath Proof Explorer

Theorem logcxp0

Description: Logarithm of a complex power. Generalization of logcxp . (Contributed by AV, 22-May-2020)

Ref Expression
Assertion logcxp0 
|- ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )

Proof

Step Hyp Ref Expression
1 eldifi 
 |-  ( A e. ( CC \ { 0 } ) -> A e. CC )
2 1 3ad2ant1 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> A e. CC )
3 eldifsni 
 |-  ( A e. ( CC \ { 0 } ) -> A =/= 0 )
4 3 3ad2ant1 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> A =/= 0 )
5 simp2 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> B e. CC )
6 2 4 5 cxpefd 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
7 6 fveq2d 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( log ` ( A ^c B ) ) = ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) )
8 logef 
 |-  ( ( B x. ( log ` A ) ) e. ran log -> ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( B x. ( log ` A ) ) )
9 8 3ad2ant3 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( B x. ( log ` A ) ) )
10 7 9 eqtrd 
 |-  ( ( A e. ( CC \ { 0 } ) /\ B e. CC /\ ( B x. ( log ` A ) ) e. ran log ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )