Theorem nnltp1le

Description: Positive integer ordering relation. (Contributed by NM, 19-Aug-2001)

	Ref	Expression
Assertion	nnltp1le	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A<B\leftrightarrow A+1\le B\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		zltp1le	$$⊢\left(A\in \mathbb{Z}\wedge B\in \mathbb{Z}\right)\to \left(A<B\leftrightarrow A+1\le B\right)$$
4	1 2 3	syl2an	$$⊢\left(A\in \mathbb{N}\wedge B\in \mathbb{N}\right)\to \left(A<B\leftrightarrow A+1\le B\right)$$