Metamath Proof Explorer


Theorem nn0inf

Description: The infimum of the set of nonnegative integers is zero. (Contributed by NM, 16-Jun-2005) (Revised by AV, 5-Sep-2020)

Ref Expression
Assertion nn0inf sup0<=0

Proof

Step Hyp Ref Expression
1 nn0uz 0=0
2 1 infeq1i sup0<=sup0<
3 0z 0
4 3 uzinfi sup0<=0
5 2 4 eqtri sup0<=0