Metamath Proof Explorer


Theorem nnm1ge0

Description: A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018)

Ref Expression
Assertion nnm1ge0 ( 𝑁 ∈ ℕ → 0 ≤ ( 𝑁 − 1 ) )

Proof

Step Hyp Ref Expression
1 nngt0 ( 𝑁 ∈ ℕ → 0 < 𝑁 )
2 0z 0 ∈ ℤ
3 nnz ( 𝑁 ∈ ℕ → 𝑁 ∈ ℤ )
4 zltlem1 ( ( 0 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 0 < 𝑁 ↔ 0 ≤ ( 𝑁 − 1 ) ) )
5 2 3 4 sylancr ( 𝑁 ∈ ℕ → ( 0 < 𝑁 ↔ 0 ≤ ( 𝑁 − 1 ) ) )
6 1 5 mpbid ( 𝑁 ∈ ℕ → 0 ≤ ( 𝑁 − 1 ) )