Database
REAL AND COMPLEX NUMBERS
Integer sets
Some properties of specific numbers
halfge0
Next ⟩
halflt1
Metamath Proof Explorer
Ascii
Unicode
Theorem
halfge0
Description:
One-half is not negative.
(Contributed by
AV
, 7-Jun-2020)
Ref
Expression
Assertion
halfge0
⊢
0
≤
1
2
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
halfre
⊢
1
2
∈
ℝ
3
halfgt0
⊢
0
<
1
2
4
1
2
3
ltleii
⊢
0
≤
1
2