Metamath Proof Explorer


Theorem elfz1eq

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

Ref Expression
Assertion elfz1eq ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 )

Proof

Step Hyp Ref Expression
1 elfzle2 ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾𝑁 )
2 elfzle1 ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝑁𝐾 )
3 elfzelz ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 ∈ ℤ )
4 elfzel2 ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝑁 ∈ ℤ )
5 zre ( 𝐾 ∈ ℤ → 𝐾 ∈ ℝ )
6 zre ( 𝑁 ∈ ℤ → 𝑁 ∈ ℝ )
7 letri3 ( ( 𝐾 ∈ ℝ ∧ 𝑁 ∈ ℝ ) → ( 𝐾 = 𝑁 ↔ ( 𝐾𝑁𝑁𝐾 ) ) )
8 5 6 7 syl2an ( ( 𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ ) → ( 𝐾 = 𝑁 ↔ ( 𝐾𝑁𝑁𝐾 ) ) )
9 3 4 8 syl2anc ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → ( 𝐾 = 𝑁 ↔ ( 𝐾𝑁𝑁𝐾 ) ) )
10 1 2 9 mpbir2and ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 )