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
⊢
0
≤
0
Proof
Step
Hyp
Ref
Expression
1
0re
⊢
0
∈
ℝ
2
1
leidi
⊢
0
≤
0