Theorem elfz3

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

	Ref	Expression
Assertion	elfz3	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( 𝑁 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		uzid	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) )
2		eluzfz1	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ 𝑁 ) → 𝑁 ∈ ( 𝑁 ... 𝑁 ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ( 𝑁 ... 𝑁 ) )