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	|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		nn0ge2m1nn	|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN )
2	1	nnnn0d	|- ( ( N e. NN0 /\ 2 <_ N ) -> ( N - 1 ) e. NN0 )