Theorem zltlem1d

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

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

Proof

Step	Hyp	Ref	Expression
1		zltlem1d.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		zltlem1d.2	$$⊢\phi \to N\in \mathbb{Z}$$
3		zltlem1	$$⊢\left(M\in \mathbb{Z}\wedge N\in \mathbb{Z}\right)\to \left(M<N\leftrightarrow M\le N-1\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \left(M<N\leftrightarrow M\le N-1\right)$$