Theorem nn0leltp1

Description: Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Apr-2004)

	Ref	Expression
Assertion	nn0leltp1	$$⊢\left(M\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(M\le N\leftrightarrow M<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		zleltp1	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M\le N\leftrightarrow M<N+1\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<N+1\right)$$