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\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$

Proof

Step	Hyp	Ref	Expression
1		nn1m1nn	$$⊢N\in \mathbb{N}\to \left(N=1\vee N-1\in \mathbb{N}\right)$$
2		oveq1	$$⊢N=1\to N-1=1-1$$
3		1m1e0	$$⊢1-1=0$$
4	2 3	eqtrdi	$$⊢N=1\to N-1=0$$
5	4	orim1i	$$⊢\left(N=1\vee N-1\in \mathbb{N}\right)\to \left(N-1=0\vee N-1\in \mathbb{N}\right)$$
6	1 5	syl	$$⊢N\in \mathbb{N}\to \left(N-1=0\vee N-1\in \mathbb{N}\right)$$
7	6	orcomd	$$⊢N\in \mathbb{N}\to \left(N-1\in \mathbb{N}\vee N-1=0\right)$$
8		elnn0	$$⊢N-1\in {\mathbb{N}}_0\leftrightarrow \left(N-1\in \mathbb{N}\vee N-1=0\right)$$
9	7 8	sylibr	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$