This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	⊢ ( ( 𝑁 ∈ ℕ₀ ∧ 2 ≤ 𝑁 ) → ( 𝑁 − 1 ) ∈ ℕ₀ )

Proof

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