Database
REAL AND COMPLEX NUMBERS
Real and complex numbers - basic operations
Ordering on reals (cont.)
0le1
Next ⟩
relin01
Metamath Proof Explorer
Ascii
Structured
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