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