This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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