Theorem logcxp

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

	Ref	Expression
Assertion	logcxp	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to \log A^B=B\log A$$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
2	1	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A\in ℂ$$
3		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
4	3	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A\ne 0$$
5		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to B\in ℝ$$
6	5	recnd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to B\in ℂ$$
7		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
8	2 4 6 7	syl3anc	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A^B={\mathrm{e}}^{B\log A}$$
9	8	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to \log A^B=\log {\mathrm{e}}^{B\log A}$$
10		id	$$⊢B\in ℝ\to B\in ℝ$$
11		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
12		remulcl	$$⊢\left(B\in ℝ\wedge \log A\in ℝ\right)\to B\log A\in ℝ$$
13	10 11 12	syl2anr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to B\log A\in ℝ$$
14	13	relogefd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to \log {\mathrm{e}}^{B\log A}=B\log A$$
15	9 14	eqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to \log A^B=B\log A$$