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 ) )