Theorem nnm1nn0

Description: A positive integer minus 1 is a nonnegative integer. (Contributed by Jason Orendorff, 24-Jan-2007) (Revised by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )

Proof

Step	Hyp	Ref	Expression
1		nn1m1nn	|- ( N e. NN -> ( N = 1 \/ ( N - 1 ) e. NN ) )
2		oveq1	|- ( N = 1 -> ( N - 1 ) = ( 1 - 1 ) )
3		1m1e0	|- ( 1 - 1 ) = 0
4	2 3	eqtrdi	|- ( N = 1 -> ( N - 1 ) = 0 )
5	4	orim1i	|- ( ( N = 1 \/ ( N - 1 ) e. NN ) -> ( ( N - 1 ) = 0 \/ ( N - 1 ) e. NN ) )
6	1 5	syl	|- ( N e. NN -> ( ( N - 1 ) = 0 \/ ( N - 1 ) e. NN ) )
7	6	orcomd	|- ( N e. NN -> ( ( N - 1 ) e. NN \/ ( N - 1 ) = 0 ) )
8		elnn0	|- ( ( N - 1 ) e. NN0 <-> ( ( N - 1 ) e. NN \/ ( N - 1 ) = 0 ) )
9	7 8	sylibr	|- ( N e. NN -> ( N - 1 ) e. NN0 )