# Metamath Proof Explorer

## Theorem elfzo

Description: Membership in a half-open finite set of integers. (Contributed by Stefan O'Rear, 15-Aug-2015)

Ref Expression
Assertion elfzo ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}..^{N}\right)↔\left({M}\le {K}\wedge {K}<{N}\right)\right)$

### Proof

Step Hyp Ref Expression
1 peano2zm ${⊢}{N}\in ℤ\to {N}-1\in ℤ$
2 elfz ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}-1\in ℤ\right)\to \left({K}\in \left({M}\dots {N}-1\right)↔\left({M}\le {K}\wedge {K}\le {N}-1\right)\right)$
3 1 2 syl3an3 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}-1\right)↔\left({M}\le {K}\wedge {K}\le {N}-1\right)\right)$
4 fzoval ${⊢}{N}\in ℤ\to \left({M}..^{N}\right)=\left({M}\dots {N}-1\right)$
5 4 eleq2d ${⊢}{N}\in ℤ\to \left({K}\in \left({M}..^{N}\right)↔{K}\in \left({M}\dots {N}-1\right)\right)$
6 5 3ad2ant3 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}..^{N}\right)↔{K}\in \left({M}\dots {N}-1\right)\right)$
7 zltlem1 ${⊢}\left({K}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}<{N}↔{K}\le {N}-1\right)$
8 7 3adant2 ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}<{N}↔{K}\le {N}-1\right)$
9 8 anbi2d ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({M}\le {K}\wedge {K}<{N}\right)↔\left({M}\le {K}\wedge {K}\le {N}-1\right)\right)$
10 3 6 9 3bitr4d ${⊢}\left({K}\in ℤ\wedge {M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}..^{N}\right)↔\left({M}\le {K}\wedge {K}<{N}\right)\right)$