Theorem nnm1ge0

Description: A positive integer decreased by 1 is greater than or equal to 0. (Contributed by AV, 30-Oct-2018)

	Ref	Expression
Assertion	nnm1ge0	$$⊢N\in \mathbb{N}\to 0\le N-1$$

Proof

Step	Hyp	Ref	Expression
1		nngt0	$$⊢N\in \mathbb{N}\to 0<N$$
2		0z	$$⊢0\in \mathbb{Z}$$
3		nnz	$$⊢N\in \mathbb{N}\to N\in \mathbb{Z}$$
4		zltlem1	$$⊢\left(0\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(0<N\leftrightarrow 0\le N-1\right)$$
5	2 3 4	sylancr	$$⊢N\in \mathbb{N}\to \left(0<N\leftrightarrow 0\le N-1\right)$$
6	1 5	mpbid	$$⊢N\in \mathbb{N}\to 0\le N-1$$