# Metamath Proof Explorer

## Theorem elfz5

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

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

### Proof

Step Hyp Ref Expression
1 eluzelz ${⊢}{K}\in {ℤ}_{\ge {M}}\to {K}\in ℤ$
2 eluzel2 ${⊢}{K}\in {ℤ}_{\ge {M}}\to {M}\in ℤ$
3 1 2 jca ${⊢}{K}\in {ℤ}_{\ge {M}}\to \left({K}\in ℤ\wedge {M}\in ℤ\right)$
4 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)$
5 4 3expa ${⊢}\left(\left({K}\in ℤ\wedge {M}\in ℤ\right)\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
6 3 5 sylan ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
7 eluzle ${⊢}{K}\in {ℤ}_{\ge {M}}\to {M}\le {K}$
8 7 biantrurd ${⊢}{K}\in {ℤ}_{\ge {M}}\to \left({K}\le {N}↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
9 8 adantr ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\right)\to \left({K}\le {N}↔\left({M}\le {K}\wedge {K}\le {N}\right)\right)$
10 6 9 bitr4d ${⊢}\left({K}\in {ℤ}_{\ge {M}}\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔{K}\le {N}\right)$