This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in ℤ_{\geq M} \leftrightarrow N \in (M \dots N)$

Step	Hyp	Ref	Expression
1		eluzfz2	$⊢ N \in ℤ_{\geq M} \to N \in (M \dots N)$
2		elfzuz	$⊢ N \in (M \dots N) \to N \in ℤ_{\geq M}$
3	1 2	impbii	$⊢ N \in ℤ_{\geq M} \leftrightarrow N \in (M \dots N)$