# 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 ≤ ( 𝐴𝑐 𝐵 ) )