# Metamath Proof Explorer

## Theorem elfz

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

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

### Proof

Step Hyp Ref Expression
1 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)$
2 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)$
3 2 baib ${⊢}{K}\in ℤ\to \left(\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
4 1 3 sylan9bb ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
5 4 3impa ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
6 5 3comr ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$