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

Metamath Proof Explorer

Theorem cxpge0d

Description: Nonnegative exponentiation with a real exponent is nonnegative. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses recxpcld.1 ⊢ φ → A ∈ ℝ
recxpcld.2 ⊢ φ → 0 ≤ A
recxpcld.3 ⊢ φ → B ∈ ℝ
Assertion cxpge0d ⊢ φ → 0 ≤ A B

Proof

Step Hyp Ref Expression
1 recxpcld.1 ⊢ φ → A ∈ ℝ
2 recxpcld.2 ⊢ φ → 0 ≤ A
3 recxpcld.3 ⊢ φ → B ∈ ℝ
4 cxpge0 ⊢ A ∈ ℝ ∧ 0 ≤ A ∧ B ∈ ℝ → 0 ≤ A B
5 1 2 3 4 syl3anc ⊢ φ → 0 ≤ A B