Metamath Proof Explorer

Theorem 0le2

Description: The number 0 is less than or equal to 2. (Contributed by David A. Wheeler, 7-Dec-2018)

Ref Expression
Assertion 0le2 
|- 0 <_ 2

Proof

Step Hyp Ref Expression
1 0le1 
 |-  0 <_ 1
2 1re 
 |-  1 e. RR
3 2 2 addge0i 
 |-  ( ( 0 <_ 1 /\ 0 <_ 1 ) -> 0 <_ ( 1 + 1 ) )
4 1 1 3 mp2an 
 |-  0 <_ ( 1 + 1 )
5 df-2 
 |-  2 = ( 1 + 1 )
6 4 5 breqtrri 
 |-  0 <_ 2