Description: Membership in a finite set of sequential integers containing one integer. (Contributed by NM, 19-Sep-2005)
Ref | Expression | ||
---|---|---|---|
Assertion | elfz1eq | ⊢ ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 ) |
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 | ⊢ ( 𝐾 ∈ ( 𝑁 ... 𝑁 ) → 𝐾 = 𝑁 ) |