Theorem zltp1led

Description: Integer ordering relation, a deduction version. (Contributed by metakunt, 23-May-2024)

	Ref	Expression
Hypotheses	zltp1led.1	$$⊢\phi \to M\in \mathbb{Z}$$
	zltp1led.2	$$⊢\phi \to N\in \mathbb{Z}$$
Assertion	zltp1led	$$⊢\phi \to \left(M<N\leftrightarrow M+1\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		zltp1led.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		zltp1led.2	$$⊢\phi \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	syl2anc	$$⊢\phi \to \left(M<N\leftrightarrow M+1\le N\right)$$