Theorem abscxp

Description: Absolute value of a power, when the base is real. (Contributed by Mario Carneiro, 15-Sep-2014)

	Ref	Expression
Assertion	abscxp	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \left|A^B\right|=A^{\Re \left(B\right)}$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to B\in ℂ$$
2		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
3	2	recnd	$$⊢A\in {ℝ}^{+}\to \log A\in ℂ$$
4	3	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \log A\in ℂ$$
5	1 4	mulcld	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to B\log A\in ℂ$$
6		absef	$$⊢B\log A\in ℂ\to \left|{\mathrm{e}}^{B\log A}\right|={\mathrm{e}}^{\Re \left(B\log A\right)}$$
7	5 6	syl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \left|{\mathrm{e}}^{B\log A}\right|={\mathrm{e}}^{\Re \left(B\log A\right)}$$
8		remul2	$$⊢\left(\log A\in ℝ\wedge B\in ℂ\right)\to \Re \left(\log AB\right)=\log A\Re \left(B\right)$$
9	2 8	sylan	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(\log AB\right)=\log A\Re \left(B\right)$$
10	1 4	mulcomd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to B\log A=\log AB$$
11	10	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(B\log A\right)=\Re \left(\log AB\right)$$
12		recl	$$⊢B\in ℂ\to \Re \left(B\right)\in ℝ$$
13	12	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(B\right)\in ℝ$$
14	13	recnd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(B\right)\in ℂ$$
15	14 4	mulcomd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(B\right)\log A=\log A\Re \left(B\right)$$
16	9 11 15	3eqtr4d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \Re \left(B\log A\right)=\Re \left(B\right)\log A$$
17	16	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to {\mathrm{e}}^{\Re \left(B\log A\right)}={\mathrm{e}}^{\Re \left(B\right)\log A}$$
18	7 17	eqtrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \left|{\mathrm{e}}^{B\log A}\right|={\mathrm{e}}^{\Re \left(B\right)\log A}$$
19		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
20	19	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to A\in ℂ$$
21		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
22	21	adantr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to A\ne 0$$
23		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
24	20 22 1 23	syl3anc	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
25	24	fveq2d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \left|A^B\right|=\left|{\mathrm{e}}^{B\log A}\right|$$
26		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge \Re \left(B\right)\in ℂ\right)\to A^{\Re \left(B\right)}={\mathrm{e}}^{\Re \left(B\right)\log A}$$
27	20 22 14 26	syl3anc	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to A^{\Re \left(B\right)}={\mathrm{e}}^{\Re \left(B\right)\log A}$$
28	18 25 27	3eqtr4d	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℂ\right)\to \left|A^B\right|=A^{\Re \left(B\right)}$$