Theorem sn-eluzp1l

Description: Shorter proof of eluzp1l . (Contributed by NM, 12-Sep-2005) (Revised by SN, 5-Jul-2025)

	Ref	Expression
Assertion	sn-eluzp1l	$$⊢\left(M\in \mathbb{Z}\wedge N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to M<N$$

Proof

Step	Hyp	Ref	Expression
1		eluzp1	$$⊢M\in \mathbb{Z}\to \left(N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\leftrightarrow \left(N\in \mathbb{Z}\wedge M<N\right)\right)$$
2	1	simplbda	$$⊢\left(M\in \mathbb{Z}\wedge N\in {\mathbb{Z}}_{\ge \left(M+1\right)}\right)\to M<N$$