Theorem logcxp0

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

	Ref	Expression
Assertion	logcxp0	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to \log A^B=B\log A$$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to A\in ℂ$$
2	1	3ad2ant1	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to A\in ℂ$$
3		eldifsni	$$⊢A\in \left(ℂ\setminus \left\{0\right\}\right)\to A\ne 0$$
4	3	3ad2ant1	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to A\ne 0$$
5		simp2	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to B\in ℂ$$
6	2 4 5	cxpefd	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to A^B={\mathrm{e}}^{B\log A}$$
7	6	fveq2d	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to \log A^B=\log {\mathrm{e}}^{B\log A}$$
8		logef	$$⊢B\log A\in \mathrm{ran}log\to \log {\mathrm{e}}^{B\log A}=B\log A$$
9	8	3ad2ant3	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to \log {\mathrm{e}}^{B\log A}=B\log A$$
10	7 9	eqtrd	$$⊢\left(A\in \left(ℂ\setminus \left\{0\right\}\right)\wedge B\in ℂ\wedge B\log A\in \mathrm{ran}log\right)\to \log A^B=B\log A$$