Database
REAL AND COMPLEX NUMBERS
Integer sets
Decimal representation of numbers
0le0
Next ⟩
0le2
Metamath Proof Explorer
Ascii
Unicode
Theorem
0le0
Description:
Zero is nonnegative.
(Contributed by
David A. Wheeler
, 7-Jul-2016)
Ref
Expression
Assertion
0le0
$${\u22a2}0\le 0$$
Proof
Step
Hyp
Ref
Expression
1
0re
$${\u22a2}0\in \mathbb{R}$$
2
1
leidi
$${\u22a2}0\le 0$$