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 \mathbb{Z}\to N\in \left(N\dots N\right)$$

Proof

Step	Hyp	Ref	Expression
1		uzid	$$⊢N\in \mathbb{Z}\to N\in {\mathbb{Z}}_{\ge N}$$
2		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge N}\to N\in \left(N\dots N\right)$$
3	1 2	syl	$$⊢N\in \mathbb{Z}\to N\in \left(N\dots N\right)$$