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

Metamath Proof Explorer

Theorem cxpge0

Description: Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 2-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 leloe ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
4 3 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 ↔ ( 0 < 𝐴 ∨ 0 = 𝐴 ) ) )
5 elrp ⊢ ( 𝐴 ∈ ℝ+ ↔ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
6 rpcxpcl ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → ( 𝐴 ↑𝑐 𝐵 ) ∈ ℝ+ )
7 6 rpge0d ⊢ ( ( 𝐴 ∈ ℝ+ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )
8 7 ex ⊢ ( 𝐴 ∈ ℝ+ → ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
9 5 8 sylbir ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) → ( 𝐵 ∈ ℝ → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
10 9 impancom ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 < 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
11 0le1 ⊢ 0 ≤ 1
12 0cn ⊢ 0 ∈ ℂ
13 cxp0 ⊢ ( 0 ∈ ℂ → ( 0 ↑𝑐 0 ) = 1 )
14 12 13 ax-mp ⊢ ( 0 ↑𝑐 0 ) = 1
15 11 14 breqtrri ⊢ 0 ≤ ( 0 ↑𝑐 0 )
16 simpr ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → 𝐵 = 0 )
17 16 oveq2d ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → ( 0 ↑𝑐 𝐵 ) = ( 0 ↑𝑐 0 ) )
18 15 17 breqtrrid ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 = 0 ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
19 0le0 ⊢ 0 ≤ 0
20 recn ⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℂ )
21 0cxp ⊢ ( ( 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
22 20 21 sylan ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → ( 0 ↑𝑐 𝐵 ) = 0 )
23 19 22 breqtrrid ⊢ ( ( 𝐵 ∈ ℝ ∧ 𝐵 ≠ 0 ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
24 18 23 pm2.61dane ⊢ ( 𝐵 ∈ ℝ → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
25 24 adantl ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 0 ↑𝑐 𝐵 ) )
26 oveq1 ⊢ ( 0 = 𝐴 → ( 0 ↑𝑐 𝐵 ) = ( 𝐴 ↑𝑐 𝐵 ) )
27 26 breq2d ⊢ ( 0 = 𝐴 → ( 0 ≤ ( 0 ↑𝑐 𝐵 ) ↔ 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
28 25 27 syl5ibcom ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 = 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
29 10 28 jaod ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( ( 0 < 𝐴 ∨ 0 = 𝐴 ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
30 4 29 sylbid ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ) → ( 0 ≤ 𝐴 → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) ) )
31 30 3impia ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )
32 31 3com23 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ∧ 𝐵 ∈ ℝ ) → 0 ≤ ( 𝐴 ↑𝑐 𝐵 ) )