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 ) )