Theorem nn0ltp1ne

Description: Nonnegative integer ordering relation. (Contributed by BTernaryTau, 24-Sep-2023)

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

Proof

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