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