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 ( ℕ0 , ℝ , < ) = 0

Proof

Step Hyp Ref Expression
1 nn0uz 0 = ( ℤ ‘ 0 )
2 1 infeq1i inf ( ℕ0 , ℝ , < ) = inf ( ( ℤ ‘ 0 ) , ℝ , < )
3 0z 0 ∈ ℤ
4 3 uzinfi inf ( ( ℤ ‘ 0 ) , ℝ , < ) = 0
5 2 4 eqtri inf ( ℕ0 , ℝ , < ) = 0