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 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ → 0 ≤ A B

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 leloe ⊢ 0 ∈ ℝ ∧ A ∈ ℝ → 0 ≤ A ↔ 0 < A ∨ 0 = A
3 1 2 mpan ⊢ A ∈ ℝ → 0 ≤ A ↔ 0 < A ∨ 0 = A
4 3 adantr ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A ↔ 0 < A ∨ 0 = A
5 elrp ⊢ A ∈ ℝ + ↔ A ∈ ℝ ∧ 0 < A
6 rpcxpcl ⊢ A ∈ ℝ + ∧ B ∈ ℝ → A B ∈ ℝ +
7 6 rpge0d ⊢ A ∈ ℝ + ∧ B ∈ ℝ → 0 ≤ A B
8 7 ex ⊢ A ∈ ℝ + → B ∈ ℝ → 0 ≤ A B
9 5 8 sylbir ⊢ A ∈ ℝ ∧ 0 < A → B ∈ ℝ → 0 ≤ A B
10 9 impancom ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A → 0 ≤ A B
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 ⊢ B ∈ ℝ ∧ B = 0 → B = 0
17 16 oveq2d ⊢ B ∈ ℝ ∧ B = 0 → 0 B = 0 0
18 15 17 breqtrrid ⊢ B ∈ ℝ ∧ B = 0 → 0 ≤ 0 B
19 0le0 ⊢ 0 ≤ 0
20 recn ⊢ B ∈ ℝ → B ∈ ℂ
21 0cxp ⊢ B ∈ ℂ ∧ B ≠ 0 → 0 B = 0
22 20 21 sylan ⊢ B ∈ ℝ ∧ B ≠ 0 → 0 B = 0
23 19 22 breqtrrid ⊢ B ∈ ℝ ∧ B ≠ 0 → 0 ≤ 0 B
24 18 23 pm2.61dane ⊢ B ∈ ℝ → 0 ≤ 0 B
25 24 adantl ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ 0 B
26 oveq1 ⊢ 0 = A → 0 B = A B
27 26 breq2d ⊢ 0 = A → 0 ≤ 0 B ↔ 0 ≤ A B
28 25 27 syl5ibcom ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 = A → 0 ≤ A B
29 10 28 jaod ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 < A ∨ 0 = A → 0 ≤ A B
30 4 29 sylbid ⊢ A ∈ ℝ ∧ B ∈ ℝ → 0 ≤ A → 0 ≤ A B
31 30 3impia ⊢ A ∈ ℝ ∧ B ∈ ℝ ∧ 0 ≤ A → 0 ≤ A B
32 31 3com23 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ → 0 ≤ A B