Metamath Proof Explorer

Theorem xrge0ge0

Description: A nonnegative extended real is nonnegative. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Assertion xrge0ge0 
|- ( A e. ( 0 [,] +oo ) -> 0 <_ A )

Proof

Step Hyp Ref Expression
1 elxrge0 
 |-  ( A e. ( 0 [,] +oo ) <-> ( A e. RR* /\ 0 <_ A ) )
2 1 biimpi 
 |-  ( A e. ( 0 [,] +oo ) -> ( A e. RR* /\ 0 <_ A ) )
3 2 simprd 
 |-  ( A e. ( 0 [,] +oo ) -> 0 <_ A )