Theorem nn0ltlem1

Description: Nonnegative integer ordering relation. (Contributed by NM, 10-May-2004) (Proof shortened by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nn0ltlem1	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M<N\leftrightarrow M\le N-1\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		zltlem1	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M<N\leftrightarrow M\le N-1\right)$$
4	1 2 3	syl2an	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M<N\leftrightarrow M\le N-1\right)$$