# 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}\in \left({M}\dots {N}\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)$

### Proof

Step Hyp Ref Expression
1 df-3an ${⊢}\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)↔\left(\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
2 an6 ${⊢}\left(\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\wedge {K}\le {N}\right)\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
3 df-3an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)$
4 anandir ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)$
5 an43 ${⊢}\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({N}\in ℤ\wedge {K}\in ℤ\right)\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\right)$
6 3 4 5 3bitri ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\right)$
7 6 anbi1i ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)↔\left(\left(\left({M}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\right)\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
8 1 2 7 3bitr4ri ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\wedge {K}\le {N}\right)\right)$
9 elfz2 ${⊢}{K}\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
10 eluz2 ${⊢}{K}\in {ℤ}_{\ge {M}}↔\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)$
11 eluz2 ${⊢}{N}\in {ℤ}_{\ge {K}}↔\left({K}\in ℤ\wedge {N}\in ℤ\wedge {K}\le {N}\right)$
12 10 11 anbi12i ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)↔\left(\left({M}\in ℤ\wedge {K}\in ℤ\wedge {M}\le {K}\right)\wedge \left({K}\in ℤ\wedge {N}\in ℤ\wedge {K}\le {N}\right)\right)$
13 8 9 12 3bitr4i ${⊢}{K}\in \left({M}\dots {N}\right)↔\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in {ℤ}_{\ge {K}}\right)$