Metamath Proof Explorer


Theorem eluzfz2

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 13-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion eluzfz2 N M N M N

Proof

Step Hyp Ref Expression
1 eluzelz N M N
2 uzid N N N
3 1 2 syl N M N N
4 eluzfz N M N N N M N
5 3 4 mpdan N M N M N