Metamath Proof Explorer

Theorem elfz1

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

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

Proof

Step Hyp Ref Expression
1 fzval ⊢ M ∈ ℤ ∧ N ∈ ℤ → M … N = j ∈ ℤ | M ≤ j ∧ j ≤ N
2 1 eleq2d ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N ↔ K ∈ j ∈ ℤ | M ≤ j ∧ j ≤ N
3 breq2 ⊢ j = K → M ≤ j ↔ M ≤ K
4 breq1 ⊢ j = K → j ≤ N ↔ K ≤ N
5 3 4 anbi12d ⊢ j = K → M ≤ j ∧ j ≤ N ↔ M ≤ K ∧ K ≤ N
6 5 elrab ⊢ K ∈ j ∈ ℤ | M ≤ j ∧ j ≤ N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
7 3anass ⊢ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
8 6 7 bitr4i ⊢ K ∈ j ∈ ℤ | M ≤ j ∧ j ≤ N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
9 2 8 bitrdi ⊢ M ∈ ℤ ∧ N ∈ ℤ → K ∈ M … N ↔ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N