This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem logcxp

Description: Logarithm of a complex power. (Contributed by Mario Carneiro, 2-Aug-2014)

Ref Expression
Assertion logcxp 
|- ( ( A e. RR+ /\ B e. RR ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )

Proof

Step Hyp Ref Expression
1 rpcn 
 |-  ( A e. RR+ -> A e. CC )
2 1 adantr 
 |-  ( ( A e. RR+ /\ B e. RR ) -> A e. CC )
3 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
4 3 adantr 
 |-  ( ( A e. RR+ /\ B e. RR ) -> A =/= 0 )
5 simpr 
 |-  ( ( A e. RR+ /\ B e. RR ) -> B e. RR )
6 5 recnd 
 |-  ( ( A e. RR+ /\ B e. RR ) -> B e. CC )
7 cxpef 
 |-  ( ( A e. CC /\ A =/= 0 /\ B e. CC ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
8 2 4 6 7 syl3anc 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( A ^c B ) = ( exp ` ( B x. ( log ` A ) ) ) )
9 8 fveq2d 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( log ` ( A ^c B ) ) = ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) )
10 id 
 |-  ( B e. RR -> B e. RR )
11 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
12 remulcl 
 |-  ( ( B e. RR /\ ( log ` A ) e. RR ) -> ( B x. ( log ` A ) ) e. RR )
13 10 11 12 syl2anr 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( B x. ( log ` A ) ) e. RR )
14 13 relogefd 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( log ` ( exp ` ( B x. ( log ` A ) ) ) ) = ( B x. ( log ` A ) ) )
15 9 14 eqtrd 
 |-  ( ( A e. RR+ /\ B e. RR ) -> ( log ` ( A ^c B ) ) = ( B x. ( log ` A ) ) )