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