# Metamath Proof Explorer

## Theorem elfz1

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

Ref Expression
Assertion elfz1 ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 fzval ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\dots {N}\right)=\left\{{j}\in ℤ|\left({M}\le {j}\wedge {j}\le {N}\right)\right\}$
2 1 eleq2d ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔{K}\in \left\{{j}\in ℤ|\left({M}\le {j}\wedge {j}\le {N}\right)\right\}\right)$
3 breq2 ${⊢}{j}={K}\to \left({M}\le {j}↔{M}\le {K}\right)$
4 breq1 ${⊢}{j}={K}\to \left({j}\le {N}↔{K}\le {N}\right)$
5 3 4 anbi12d ${⊢}{j}={K}\to \left(\left({M}\le {j}\wedge {j}\le {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
6 5 elrab ${⊢}{K}\in \left\{{j}\in ℤ|\left({M}\le {j}\wedge {j}\le {N}\right)\right\}↔\left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
7 3anass ${⊢}\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)↔\left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
8 6 7 bitr4i ${⊢}{K}\in \left\{{j}\in ℤ|\left({M}\le {j}\wedge {j}\le {N}\right)\right\}↔\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)$
9 2 8 syl6bb ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)\right)$