Theorem nn0lem1lt

Description: Nonnegative integer ordering relation. (Contributed by NM, 21-Jun-2005)

	Ref	Expression
Assertion	nn0lem1lt	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$

Proof

Step	Hyp	Ref	Expression
1		nn0z	$$⊢M\in {\mathbb{N}}_0\to M\in \mathbb{Z}$$
2		nn0z	$$⊢N\in {\mathbb{N}}_0\to N\in \mathbb{Z}$$
3		zlem1lt	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$
4	1 2 3	syl2an	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M-1<N\right)$$