Metamath Proof Explorer

Theorem elfz

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

Ref Expression
Assertion elfz ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N ↔ M ≤ K ∧ K ≤ N

Proof

Step Hyp Ref Expression
1 elfz1 ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
2 3anass ⊢ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
3 2 baib ⊢ K ∈ ℤ → K ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ M ≤ K ∧ K ≤ N
4 1 3 sylan9bb ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → K ∈ M … N ↔ M ≤ K ∧ K ≤ N
5 4 3impa ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ → K ∈ M … N ↔ M ≤ K ∧ K ≤ N
6 5 3comr ⊢ K ∈ ℤ ∧ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N ↔ M ≤ K ∧ K ≤ N