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

Metamath Proof Explorer

Theorem fzval2

Description: An alternative way of expressing a finite set of sequential integers. (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion fzval2 
|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )

Proof

Step Hyp Ref Expression
1 fzval 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = { k e. ZZ | ( M <_ k /\ k <_ N ) } )
2 zssre 
 |-  ZZ C_ RR
3 ressxr 
 |-  RR C_ RR*
4 2 3 sstri 
 |-  ZZ C_ RR*
5 4 sseli 
 |-  ( M e. ZZ -> M e. RR* )
6 4 sseli 
 |-  ( N e. ZZ -> N e. RR* )
7 iccval 
 |-  ( ( M e. RR* /\ N e. RR* ) -> ( M [,] N ) = { k e. RR* | ( M <_ k /\ k <_ N ) } )
8 5 6 7 syl2an 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M [,] N ) = { k e. RR* | ( M <_ k /\ k <_ N ) } )
9 8 ineq1d 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( ( M [,] N ) i^i ZZ ) = ( { k e. RR* | ( M <_ k /\ k <_ N ) } i^i ZZ ) )
10 inrab2 
 |-  ( { k e. RR* | ( M <_ k /\ k <_ N ) } i^i ZZ ) = { k e. ( RR* i^i ZZ ) | ( M <_ k /\ k <_ N ) }
11 sseqin2 
 |-  ( ZZ C_ RR* <-> ( RR* i^i ZZ ) = ZZ )
12 4 11 mpbi 
 |-  ( RR* i^i ZZ ) = ZZ
13 12 rabeqi 
 |-  { k e. ( RR* i^i ZZ ) | ( M <_ k /\ k <_ N ) } = { k e. ZZ | ( M <_ k /\ k <_ N ) }
14 10 13 eqtri 
 |-  ( { k e. RR* | ( M <_ k /\ k <_ N ) } i^i ZZ ) = { k e. ZZ | ( M <_ k /\ k <_ N ) }
15 9 14 eqtr2di 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> { k e. ZZ | ( M <_ k /\ k <_ N ) } = ( ( M [,] N ) i^i ZZ ) )
16 1 15 eqtrd 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M ... N ) = ( ( M [,] N ) i^i ZZ ) )