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

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 )