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 e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 elicopnf 
 |-  ( 0 e. RR -> ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) ) )
3 1 2 ax-mp 
 |-  ( A e. ( 0 [,) +oo ) <-> ( A e. RR /\ 0 <_ A ) )