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

Metamath Proof Explorer

Theorem elfz3

Description: Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 21-Jul-2005)

		Ref	Expression
	Assertion	elfz3	$⊢ N \in ℤ \to N \in (N \dots N)$

Step	Hyp	Ref	Expression
1		uzid	$⊢ N \in ℤ \to N \in ℤ_{\geq N}$
2		eluzfz1	$⊢ N \in ℤ_{\geq N} \to N \in (N \dots N)$
3	1 2	syl	$⊢ N \in ℤ \to N \in (N \dots N)$