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

Proof

Step Hyp Ref Expression
1 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
2 elfzuz 
 |-  ( N e. ( M ... N ) -> N e. ( ZZ>= ` M ) )
3 1 2 impbii 
 |-  ( N e. ( ZZ>= ` M ) <-> N e. ( M ... N ) )