Theorem nn0ge2m1nn0

Description: If a nonnegative integer is greater than or equal to two, the integer decreased by 1 is also a nonnegative integer. (Contributed by Alexander van der Vekens, 1-Aug-2018)

	Ref	Expression
Assertion	nn0ge2m1nn0	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )

Proof

Step	Hyp	Ref	Expression
1		nn0ge2m1nn	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ )
2	1	nnnn0d	⊢ ( ( 𝑁 ∈ ℕ0 ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ0 )