Theorem nn0ltp1le

Description: Nonnegative integer ordering relation. (Contributed by Raph Levien, 10-Dec-2002) (Proof shortened by Mario Carneiro, 16-May-2014)

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