Metamath Proof Explorer


Theorem halfge0

Description: One-half is not negative. (Contributed by AV, 7-Jun-2020)

Ref Expression
Assertion halfge0 012

Proof

Step Hyp Ref Expression
1 0re 0
2 halfre 12
3 halfgt0 0<12
4 1 2 3 ltleii 012