Metamath Proof Explorer


Theorem eluzfz2b

Description: Membership in a finite set of sequential integers - special case. (Contributed by NM, 14-Sep-2005)

Ref Expression
Assertion eluzfz2b N M N M N

Proof

Step Hyp Ref Expression
1 eluzfz2 N M N M N
2 elfzuz N M N N M
3 1 2 impbii N M N M N