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 ⊢ K ∈ N … N → K = N

Proof

Step Hyp Ref Expression
1 elfzle2 ⊢ K ∈ N … N → K ≤ N
2 elfzle1 ⊢ K ∈ N … N → N ≤ K
3 elfzelz ⊢ K ∈ N … N → K ∈ ℤ
4 elfzel2 ⊢ K ∈ N … N → N ∈ ℤ
5 zre ⊢ K ∈ ℤ → K ∈ ℝ
6 zre ⊢ N ∈ ℤ → N ∈ ℝ
7 letri3 ⊢ K ∈ ℝ ∧ N ∈ ℝ → K = N ↔ K ≤ N ∧ N ≤ K
8 5 6 7 syl2an ⊢ K ∈ ℤ ∧ N ∈ ℤ → K = N ↔ K ≤ N ∧ N ≤ K
9 3 4 8 syl2anc ⊢ K ∈ N … N → K = N ↔ K ≤ N ∧ N ≤ K
10 1 2 9 mpbir2and ⊢ K ∈ N … N → K = N