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

Metamath Proof Explorer

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