Metamath Proof Explorer

Theorem 0le1

Description: 0 is less than or equal to 1. (Contributed by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion 0le1 
|- 0 <_ 1

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1re 
 |-  1 e. RR
3 0lt1 
 |-  0 < 1
4 1 2 3 ltleii 
 |-  0 <_ 1