This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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