Theorem logcxp

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

	Ref	Expression
Assertion	logcxp	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rpcn	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ∈ ℂ )
2	1	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 ∈ ℂ )
3		rpne0	⊢ ( 𝐴 ∈ ℝ+ → 𝐴 ≠ 0 )
4	3	adantr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐴 ≠ 0 )
5		simpr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℝ )
6	5	recnd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 𝐵 ∈ ℂ )
7		cxpef	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
8	2 4 6 7	syl3anc	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
9	8	fveq2d	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
10		id	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
11		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
12		remulcl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
13	10 11 12	syl2anr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
14	13	relogefd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )
15	9 14	eqtrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( log ‘ ( 𝐴 ↑𝑐 𝐵 ) ) = ( 𝐵 · ( log ‘ 𝐴 ) ) )