# Metamath Proof Explorer

## Theorem fzval

Description: The value of a finite set of sequential integers. E.g., 2 ... 5 means the set { 2 , 3 , 4 , 5 } . A special case of this definition (starting at 1) appears as Definition 11-2.1 of Gleason p. 141, where NN_k means our 1 ... k ; he calls these setssegments of the integers. (Contributed by NM, 6-Sep-2005) (Revised by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion fzval ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\dots {N}\right)=\left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {N}\right)\right\}$

### Proof

Step Hyp Ref Expression
1 breq1 ${⊢}{m}={M}\to \left({m}\le {k}↔{M}\le {k}\right)$
2 1 anbi1d ${⊢}{m}={M}\to \left(\left({m}\le {k}\wedge {k}\le {n}\right)↔\left({M}\le {k}\wedge {k}\le {n}\right)\right)$
3 2 rabbidv ${⊢}{m}={M}\to \left\{{k}\in ℤ|\left({m}\le {k}\wedge {k}\le {n}\right)\right\}=\left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {n}\right)\right\}$
4 breq2 ${⊢}{n}={N}\to \left({k}\le {n}↔{k}\le {N}\right)$
5 4 anbi2d ${⊢}{n}={N}\to \left(\left({M}\le {k}\wedge {k}\le {n}\right)↔\left({M}\le {k}\wedge {k}\le {N}\right)\right)$
6 5 rabbidv ${⊢}{n}={N}\to \left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {n}\right)\right\}=\left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {N}\right)\right\}$
7 df-fz ${⊢}\dots =\left({m}\in ℤ,{n}\in ℤ⟼\left\{{k}\in ℤ|\left({m}\le {k}\wedge {k}\le {n}\right)\right\}\right)$
8 zex ${⊢}ℤ\in \mathrm{V}$
9 8 rabex ${⊢}\left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {N}\right)\right\}\in \mathrm{V}$
10 3 6 7 9 ovmpo ${⊢}\left({M}\in ℤ\wedge {N}\in ℤ\right)\to \left({M}\dots {N}\right)=\left\{{k}\in ℤ|\left({M}\le {k}\wedge {k}\le {N}\right)\right\}$