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 ⊢M∈ℤ∧N∈ℤ→M…N=k∈ℤ|M≤k∧k≤N

Proof

Step Hyp Ref Expression
1 breq1 ⊢m=M→m≤k↔M≤k
2 1 anbi1d ⊢m=M→m≤k∧k≤n↔M≤k∧k≤n
3 2 rabbidv ⊢m=M→k∈ℤ|m≤k∧k≤n=k∈ℤ|M≤k∧k≤n
4 breq2 ⊢n=N→k≤n↔k≤N
5 4 anbi2d ⊢n=N→M≤k∧k≤n↔M≤k∧k≤N
6 5 rabbidv ⊢n=N→k∈ℤ|M≤k∧k≤n=k∈ℤ|M≤k∧k≤N
7 df-fz ⊢…=m∈ℤ,n∈ℤ⟼k∈ℤ|m≤k∧k≤n
8 zex ⊢ℤ∈V
9 8 rabex ⊢k∈ℤ|M≤k∧k≤N∈V
10 3 6 7 9 ovmpo ⊢M∈ℤ∧N∈ℤ→M…N=k∈ℤ|M≤k∧k≤N