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	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\le N\right)\to N-1\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nn0ge2m1nn	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\le N\right)\to N-1\in \mathbb{N}$$
2	1	nnnn0d	$$⊢\left(N\in {\mathbb{N}}_0\wedge 2\le N\right)\to N-1\in {\mathbb{N}}_0$$