Theorem rpcxpcl

Description: Positive real closure of the complex power function. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

Step	Hyp	Ref	Expression
1		rprege0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℝ\wedge 0\le A\right)$$
2		recxpcl	$$⊢\left(A\in ℝ\wedge 0\le A\wedge B\in ℝ\right)\to A^B\in ℝ$$
3	2	3expa	$$⊢\left(\left(A\in ℝ\wedge 0\le A\right)\wedge B\in ℝ\right)\to A^B\in ℝ$$
4	1 3	sylan	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A^B\in ℝ$$
5		id	$$⊢B\in ℝ\to B\in ℝ$$
6		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
7		remulcl	$$⊢\left(B\in ℝ\wedge \log A\in ℝ\right)\to B\log A\in ℝ$$
8	5 6 7	syl2anr	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to B\log A\in ℝ$$
9		efgt0	$$⊢B\log A\in ℝ\to 0<{\mathrm{e}}^{B\log A}$$
10	8 9	syl	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to 0<{\mathrm{e}}^{B\log A}$$
11		rpcnne0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℂ\wedge A\ne 0\right)$$
12		recn	$$⊢B\in ℝ\to B\in ℂ$$
13		cxpef	$$⊢\left(A\in ℂ\wedge A\ne 0\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
14	13	3expa	$$⊢\left(\left(A\in ℂ\wedge A\ne 0\right)\wedge B\in ℂ\right)\to A^B={\mathrm{e}}^{B\log A}$$
15	11 12 14	syl2an	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A^B={\mathrm{e}}^{B\log A}$$
16	10 15	breqtrrd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to 0<A^B$$
17	4 16	elrpd	$$⊢\left(A\in {ℝ}^{+}\wedge B\in ℝ\right)\to A^B\in {ℝ}^{+}$$