Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > elrege0 | Structured version Visualization version GIF version |
Description: The predicate "is a nonnegative real". (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 18-Jun-2014.) |
Ref | Expression |
---|---|
elrege0 | ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 0re 9919 | . 2 ⊢ 0 ∈ ℝ | |
2 | elicopnf 12140 | . 2 ⊢ (0 ∈ ℝ → (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ∈ (0[,)+∞) ↔ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴)) |
Copyright terms: Public domain | W3C validator |