This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M < N

Proof

Step Hyp Ref Expression
1 eluzp1 ⊢ M ∈ ℤ → N ∈ ℤ ≥ M + 1 ↔ N ∈ ℤ ∧ M < N
2 1 simplbda ⊢ M ∈ ℤ ∧ N ∈ ℤ ≥ M + 1 → M < N