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 e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> M < N )

Proof

Step Hyp Ref Expression
1 eluzp1 
 |-  ( M e. ZZ -> ( N e. ( ZZ>= ` ( M + 1 ) ) <-> ( N e. ZZ /\ M < N ) ) )
2 1 simplbda 
 |-  ( ( M e. ZZ /\ N e. ( ZZ>= ` ( M + 1 ) ) ) -> M < N )