Theorem recxpcl

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

	Ref	Expression
Assertion	recxpcl	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		recn	⊢ ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
2		recn	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
3		cxpval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
4	1 2 3	syl2an	⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
5	4	3adant2	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) = if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) )
6		1re	⊢ 1 ∈ ℝ
7		0re	⊢ 0 ∈ ℝ
8	6 7	ifcli	⊢ if ( 𝐵 = 0 , 1 , 0 ) ∈ ℝ
9	8	a1i	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 = 0 ) → if ( 𝐵 = 0 , 1 , 0 ) ∈ ℝ )
10		df-ne	⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
11		simpl3	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐵 ∈ ℝ )
12		simpl1	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ )
13		simpl2	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 0 ≤ 𝐴 )
14		simpr	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 )
15	12 13 14	ne0gt0d	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 0 < 𝐴 )
16	12 15	elrpd	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ ℝ+ )
17	16	relogcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( log ‘ 𝐴 ) ∈ ℝ )
18	11 17	remulcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( 𝐵 · ( log ‘ 𝐴 ) ) ∈ ℝ )
19	18	reefcld	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ 𝐴 ≠ 0 ) → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
20	10 19	sylan2br	⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) ∧ ¬ 𝐴 = 0 ) → ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ∈ ℝ )
21	9 20	ifclda	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → if ( 𝐴 = 0 , if ( 𝐵 = 0 , 1 , 0 ) , ( exp ‘ ( 𝐵 · ( log ‘ 𝐴 ) ) ) ) ∈ ℝ )
22	5 21	eqeltrd	⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )