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 
|- inf ( NN0 , RR , < ) = 0

Proof

Step Hyp Ref Expression
1 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
2 1 infeq1i 
 |-  inf ( NN0 , RR , < ) = inf ( ( ZZ>= ` 0 ) , RR , < )
3 0z 
 |-  0 e. ZZ
4 3 uzinfi 
 |-  inf ( ( ZZ>= ` 0 ) , RR , < ) = 0
5 2 4 eqtri 
 |-  inf ( NN0 , RR , < ) = 0