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

Metamath Proof Explorer

Theorem fzrevral2

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

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

Proof

Step	Hyp	Ref	Expression
1		zsubcl	\|- ( ( K e. ZZ /\ N e. ZZ ) -> ( K - N ) e. ZZ )
2	1	3adant2	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K - N ) e. ZZ )
3		zsubcl	\|- ( ( K e. ZZ /\ M e. ZZ ) -> ( K - M ) e. ZZ )
4	3	3adant3	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( K - M ) e. ZZ )
5		simp1	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> K e. ZZ )
6		fzrevral	\|- ( ( ( K - N ) e. ZZ /\ ( K - M ) e. ZZ /\ K e. ZZ ) -> ( A. j e. ( ( K - N ) ... ( K - M ) ) ph <-> A. k e. ( ( K - ( K - M ) ) ... ( K - ( K - N ) ) ) [. ( K - k ) / j ]. ph ) )
7	2 4 5 6	syl3anc	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( ( K - N ) ... ( K - M ) ) ph <-> A. k e. ( ( K - ( K - M ) ) ... ( K - ( K - N ) ) ) [. ( K - k ) / j ]. ph ) )
8		zcn	\|- ( K e. ZZ -> K e. CC )
9		zcn	\|- ( M e. ZZ -> M e. CC )
10		zcn	\|- ( N e. ZZ -> N e. CC )
11		nncan	\|- ( ( K e. CC /\ M e. CC ) -> ( K - ( K - M ) ) = M )
12	11	3adant3	\|- ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( K - ( K - M ) ) = M )
13		nncan	\|- ( ( K e. CC /\ N e. CC ) -> ( K - ( K - N ) ) = N )
14	13	3adant2	\|- ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( K - ( K - N ) ) = N )
15	12 14	oveq12d	\|- ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( ( K - ( K - M ) ) ... ( K - ( K - N ) ) ) = ( M ... N ) )
16	8 9 10 15	syl3an	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( ( K - ( K - M ) ) ... ( K - ( K - N ) ) ) = ( M ... N ) )
17	16	raleqdv	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( A. k e. ( ( K - ( K - M ) ) ... ( K - ( K - N ) ) ) [. ( K - k ) / j ]. ph <-> A. k e. ( M ... N ) [. ( K - k ) / j ]. ph ) )
18	7 17	bitrd	\|- ( ( K e. ZZ /\ M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( ( K - N ) ... ( K - M ) ) ph <-> A. k e. ( M ... N ) [. ( K - k ) / j ]. ph ) )
19	18	3coml	\|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( ( K - N ) ... ( K - M ) ) ph <-> A. k e. ( M ... N ) [. ( K - k ) / j ]. ph ) )