Metamath Proof Explorer

Theorem rpge0

Description: A positive real is greater than or equal to zero. (Contributed by NM, 22-Feb-2008)

Ref Expression
Assertion rpge0 
|- ( A e. RR+ -> 0 <_ A )

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 rpgt0 
 |-  ( A e. RR+ -> 0 < A )
3 0re 
 |-  0 e. RR
4 ltle 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
5 3 4 mpan 
 |-  ( A e. RR -> ( 0 < A -> 0 <_ A ) )
6 1 2 5 sylc 
 |-  ( A e. RR+ -> 0 <_ A )