Metamath Proof Explorer

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 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ )