Theorem eluzfz2b

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

	Ref	Expression
Assertion	eluzfz2b	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow N\in \left(M\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
2		elfzuz	$$⊢N\in \left(M\dots N\right)\to N\in {\mathbb{Z}}_{\ge M}$$
3	1 2	impbii	$$⊢N\in {\mathbb{Z}}_{\ge M}\leftrightarrow N\in \left(M\dots N\right)$$