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 e. RR
2 halfre 
 |-  ( 1 / 2 ) e. RR
3 halfgt0 
 |-  0 < ( 1 / 2 )
4 1 2 3 ltleii 
 |-  0 <_ ( 1 / 2 )