Metamath Proof Explorer


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 )