Theorem rpcxpcl

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

	Ref	Expression
Assertion	rpcxpcl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )

Proof

Step	Hyp	Ref	Expression
1		rprege0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) )
2		recxpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
3	2	3expa	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
4	1 3	sylan	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )
5		id	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ )
6		relogcl	⊢ ( 𝐴 ∈ ℝ+ → ( log ‘ 𝐴 ) ∈ ℝ )
7		remulcl	⊢ ( ( 𝐵 ∈ ℝ ∧ ( log ‘ 𝐴 ) ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
8	5 6 7	syl2anr	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
9		efgt0	⊢ ( ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ → 0 < ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
10	8 9	syl	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 0 < ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
11		rpcnne0	⊢ ( 𝐴 ∈ ℝ+ → ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) )
12		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
13		cxpef	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
14	13	3expa	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐴 ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
15	11 12 14	syl2an	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) = ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) )
16	10 15	breqtrrd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 0 < ( 𝐴 ↑𝑐 𝐵 ) )
17	4 16	elrpd	⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )