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	⊢ ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 )