Metamath Proof Explorer

Theorem fzshftral

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

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

Proof

Step Hyp Ref Expression
1 0z 
 |-  0 e. ZZ
2 fzrevral 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ 0 e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph ) )
3 1 2 mp3an3 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph ) )
4 3 3adant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph ) )
5 zsubcl 
 |-  ( ( 0 e. ZZ /\ N e. ZZ ) -> ( 0 - N ) e. ZZ )
6 1 5 mpan 
 |-  ( N e. ZZ -> ( 0 - N ) e. ZZ )
7 zsubcl 
 |-  ( ( 0 e. ZZ /\ M e. ZZ ) -> ( 0 - M ) e. ZZ )
8 1 7 mpan 
 |-  ( M e. ZZ -> ( 0 - M ) e. ZZ )
9 id 
 |-  ( K e. ZZ -> K e. ZZ )
10 fzrevral 
 |-  ( ( ( 0 - N ) e. ZZ /\ ( 0 - M ) e. ZZ /\ K e. ZZ ) -> ( A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph <-> A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph ) )
11 6 8 9 10 syl3an 
 |-  ( ( N e. ZZ /\ M e. ZZ /\ K e. ZZ ) -> ( A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph <-> A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph ) )
12 11 3com12 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. x e. ( ( 0 - N ) ... ( 0 - M ) ) [. ( 0 - x ) / j ]. ph <-> A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph ) )
13 ovex 
 |-  ( K - k ) e. _V
14 oveq2 
 |-  ( x = ( K - k ) -> ( 0 - x ) = ( 0 - ( K - k ) ) )
15 14 sbcco3gw 
 |-  ( ( K - k ) e. _V -> ( [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph <-> [. ( 0 - ( K - k ) ) / j ]. ph ) )
16 13 15 ax-mp 
 |-  ( [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph <-> [. ( 0 - ( K - k ) ) / j ]. ph )
17 16 ralbii 
 |-  ( A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph <-> A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( 0 - ( K - k ) ) / j ]. ph )
18 zcn 
 |-  ( M e. ZZ -> M e. CC )
19 zcn 
 |-  ( N e. ZZ -> N e. CC )
20 zcn 
 |-  ( K e. ZZ -> K e. CC )
21 df-neg 
 |-  -u M = ( 0 - M )
22 21 oveq2i 
 |-  ( K - -u M ) = ( K - ( 0 - M ) )
23 subneg 
 |-  ( ( K e. CC /\ M e. CC ) -> ( K - -u M ) = ( K + M ) )
24 addcom 
 |-  ( ( K e. CC /\ M e. CC ) -> ( K + M ) = ( M + K ) )
25 23 24 eqtrd 
 |-  ( ( K e. CC /\ M e. CC ) -> ( K - -u M ) = ( M + K ) )
26 22 25 eqtr3id 
 |-  ( ( K e. CC /\ M e. CC ) -> ( K - ( 0 - M ) ) = ( M + K ) )
27 26 3adant3 
 |-  ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( K - ( 0 - M ) ) = ( M + K ) )
28 df-neg 
 |-  -u N = ( 0 - N )
29 28 oveq2i 
 |-  ( K - -u N ) = ( K - ( 0 - N ) )
30 subneg 
 |-  ( ( K e. CC /\ N e. CC ) -> ( K - -u N ) = ( K + N ) )
31 addcom 
 |-  ( ( K e. CC /\ N e. CC ) -> ( K + N ) = ( N + K ) )
32 30 31 eqtrd 
 |-  ( ( K e. CC /\ N e. CC ) -> ( K - -u N ) = ( N + K ) )
33 29 32 eqtr3id 
 |-  ( ( K e. CC /\ N e. CC ) -> ( K - ( 0 - N ) ) = ( N + K ) )
34 33 3adant2 
 |-  ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( K - ( 0 - N ) ) = ( N + K ) )
35 27 34 oveq12d 
 |-  ( ( K e. CC /\ M e. CC /\ N e. CC ) -> ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) = ( ( M + K ) ... ( N + K ) ) )
36 35 3coml 
 |-  ( ( M e. CC /\ N e. CC /\ K e. CC ) -> ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) = ( ( M + K ) ... ( N + K ) ) )
37 18 19 20 36 syl3an 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) = ( ( M + K ) ... ( N + K ) ) )
38 37 raleqdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( 0 - ( K - k ) ) / j ]. ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( 0 - ( K - k ) ) / j ]. ph ) )
39 elfzelz 
 |-  ( k e. ( ( M + K ) ... ( N + K ) ) -> k e. ZZ )
40 39 zcnd 
 |-  ( k e. ( ( M + K ) ... ( N + K ) ) -> k e. CC )
41 df-neg 
 |-  -u ( K - k ) = ( 0 - ( K - k ) )
42 negsubdi2 
 |-  ( ( K e. CC /\ k e. CC ) -> -u ( K - k ) = ( k - K ) )
43 41 42 eqtr3id 
 |-  ( ( K e. CC /\ k e. CC ) -> ( 0 - ( K - k ) ) = ( k - K ) )
44 20 40 43 syl2an 
 |-  ( ( K e. ZZ /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( 0 - ( K - k ) ) = ( k - K ) )
45 44 sbceq1d 
 |-  ( ( K e. ZZ /\ k e. ( ( M + K ) ... ( N + K ) ) ) -> ( [. ( 0 - ( K - k ) ) / j ]. ph <-> [. ( k - K ) / j ]. ph ) )
46 45 ralbidva 
 |-  ( K e. ZZ -> ( A. k e. ( ( M + K ) ... ( N + K ) ) [. ( 0 - ( K - k ) ) / j ]. ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) )
47 46 3ad2ant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( M + K ) ... ( N + K ) ) [. ( 0 - ( K - k ) ) / j ]. ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) )
48 38 47 bitrd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( 0 - ( K - k ) ) / j ]. ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) )
49 17 48 syl5bb 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( K - ( 0 - M ) ) ... ( K - ( 0 - N ) ) ) [. ( K - k ) / x ]. [. ( 0 - x ) / j ]. ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) )
50 4 12 49 3bitrd 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( M + K ) ... ( N + K ) ) [. ( k - K ) / j ]. ph ) )