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 ( 𝑁 ∈ ℤ → 𝑁 ∈ ( 𝑁 ... 𝑁 ) )

Proof

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