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