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 sup 0 < = 0

Proof

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