This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( 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 e. ZZ | ( m <_ k /\ k <_ n ) } = { k e. ZZ | ( 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 e. ZZ | ( M <_ k /\ k <_ n ) } = { k e. ZZ | ( M <_ k /\ k <_ N ) } )
7 df-fz 
 |-  ... = ( m e. ZZ , n e. ZZ |-> { k e. ZZ | ( m <_ k /\ k <_ n ) } )
8 zex 
 |-  ZZ e. _V
9 8 rabex 
 |-  { k e. ZZ | ( M <_ k /\ k <_ N ) } e. _V
10 3 6 7 9 ovmpo 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( M <_ k /\ k <_ N ) } )