Theorem fzrevral3

Description: Reversal of scanning order inside of a universal quantification restricted to a finite set of sequential integers. (Contributed by NM, 20-Nov-2005)

	Ref	Expression
Assertion	fzrevral3	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( M ... N ) [. ( ( M + N ) - k ) / j ]. ph ) )

Proof

Step	Hyp	Ref	Expression
1		zaddcl	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( M + N ) e. ZZ )
2		fzrevral	|- ( ( M e. ZZ /\ N e. ZZ /\ ( M + N ) e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) [. ( ( M + N ) - k ) / j ]. ph ) )
3	1 2	mpd3an3	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) [. ( ( M + N ) - k ) / j ]. ph ) )
4		zcn	|- ( M e. ZZ -> M e. CC )
5		zcn	|- ( N e. ZZ -> N e. CC )
6		pncan	|- ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - N ) = M )
7		pncan2	|- ( ( M e. CC /\ N e. CC ) -> ( ( M + N ) - M ) = N )
8	6 7	oveq12d	|- ( ( M e. CC /\ N e. CC ) -> ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) = ( M ... N ) )
9	4 5 8	syl2an	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) = ( M ... N ) )
10	9	raleqdv	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. k e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) [. ( ( M + N ) - k ) / j ]. ph <-> A. k e. ( M ... N ) [. ( ( M + N ) - k ) / j ]. ph ) )
11	3 10	bitrd	|- ( ( M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( M ... N ) [. ( ( M + N ) - k ) / j ]. ph ) )