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

Metamath Proof Explorer

Theorem elrege0

Description: The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 18-Jun-2014)

Ref Expression
Assertion elrege0 ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 elicopnf ⊢ 0 ∈ ℝ → A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A
3 1 2 ax-mp ⊢ A ∈ 0 +∞ ↔ A ∈ ℝ ∧ 0 ≤ A