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 ∈ ℝ
2 1 leidi ⊢ 0 ≤ 0