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	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 < 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		eluzp1	⊢ ( 𝑀 ∈ ℤ → ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ↔ ( 𝑁 ∈ ℤ ∧ 𝑀 < 𝑁 ) ) )
2	1	simplbda	⊢ ( ( 𝑀 ∈ ℤ ∧ 𝑁 ∈ ( ℤ≥ ‘ ( 𝑀 + 1 ) ) ) → 𝑀 < 𝑁 )