# Metamath Proof Explorer

## Theorem elfz2

Description: Membership in a finite set of sequential integers. We use the fact that an operation's value is empty outside of its domain to show M e. ZZ and N e. ZZ . (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 28-Apr-2015)

Ref Expression
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 anass ${⊢}\left(\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)$
2 df-3an ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\wedge {K}\in ℤ\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge {K}\in ℤ\right)$
3 2 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 {N}\in ℤ\right)\wedge {K}\in ℤ\right)\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)$
4 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)$
5 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)$
6 ibar ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\right)$
7 5 6 syl5bb ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left(\left({K}\in ℤ\wedge {M}\le {K}\wedge {K}\le {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\right)$
8 4 7 bitrd ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\right)$
9 fzf ${⊢}\dots :ℤ×ℤ⟶𝒫ℤ$
10 9 fdmi ${⊢}\mathrm{dom}\dots =ℤ×ℤ$
11 10 ndmov ${⊢}¬\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\dots {N}\right)=\varnothing$
12 11 eleq2d ${⊢}¬\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔{K}\in \varnothing \right)$
13 noel ${⊢}¬{K}\in \varnothing$
14 13 pm2.21i ${⊢}{K}\in \varnothing \to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
15 simpl ${⊢}\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\to \left({M}\in ℤ\wedge {N}\in ℤ\right)$
16 14 15 pm5.21ni ${⊢}¬\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \varnothing ↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\right)$
17 12 16 bitrd ${⊢}¬\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({K}\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)\right)$
18 8 17 pm2.61i ${⊢}{K}\in \left({M}\dots {N}\right)↔\left(\left({M}\in ℤ\wedge {N}\in ℤ\right)\wedge \left({K}\in ℤ\wedge \left({M}\le {K}\wedge {K}\le {N}\right)\right)\right)$
19 1 3 18 3bitr4ri ${⊢}{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)$