Theorem nnleltp1

Description: Positive integer ordering relation. (Contributed by NM, 13-Aug-2001) (Proof shortened by Mario Carneiro, 16-May-2014)

	Ref	Expression
Assertion	nnleltp1	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\le B\leftrightarrow A<B+1\right)$$

Proof

Step	Hyp	Ref	Expression
1		nnz	$$⊢A\in \mathbb{N}\to A\in \mathbb{Z}$$
2		nnz	$$⊢B\in \mathbb{N}\to B\in \mathbb{Z}$$
3		zleltp1	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A\le B\leftrightarrow A<B+1\right)$$
4	1 2 3	syl2an	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A\le B\leftrightarrow A<B+1\right)$$