Metamath Proof Explorer

Theorem elfzuzb

Description: Membership in a finite set of sequential integers in terms of sets of upper integers. (Contributed by NM, 18-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion elfzuzb ⊢ K ∈ M … N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ≥ K

Proof

Step Hyp Ref Expression
1 df-3an ⊢ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K ≤ N
2 an6 ⊢ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ K ≤ N ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K ≤ N
3 df-3an ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ
4 anandir ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ
5 an43 ⊢ M ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ
6 3 4 5 3bitri ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ
7 6 anbi1i ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ M ≤ K ∧ K ≤ N
8 1 2 7 3bitr4ri ⊢ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ K ≤ N
9 elfz2 ⊢ K ∈ M … N ↔ M ∈ ℤ ∧ N ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ≤ N
10 eluz2 ⊢ K ∈ ℤ ≥ M ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K
11 eluz2 ⊢ N ∈ ℤ ≥ K ↔ K ∈ ℤ ∧ N ∈ ℤ ∧ K ≤ N
12 10 11 anbi12i ⊢ K ∈ ℤ ≥ M ∧ N ∈ ℤ ≥ K ↔ M ∈ ℤ ∧ K ∈ ℤ ∧ M ≤ K ∧ K ∈ ℤ ∧ N ∈ ℤ ∧ K ≤ N
13 8 9 12 3bitr4i ⊢ K ∈ M … N ↔ K ∈ ℤ ≥ M ∧ N ∈ ℤ ≥ K