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 ∈ ℝ
2 1re 1 ∈ ℝ
3 0lt1 0 < 1
4 1 2 3 ltleii 0 ≤ 1