Metamath Proof Explorer

Theorem nninf

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

Ref Expression
Assertion nninf 
|- inf ( NN , RR , < ) = 1

Proof

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