Metamath Proof Explorer

Theorem 0le0

Description: Zero is nonnegative. (Contributed by David A. Wheeler, 7-Jul-2016)

Ref Expression
Assertion 0le0 
|- 0 <_ 0

Proof

Step Hyp Ref Expression
1 0re 
 |-  0 e. RR
2 1 leidi 
 |-  0 <_ 0