Metamath Proof Explorer

Theorem fzoshftral

Description: Shift the scanning order inside of a universal quantification restricted to a half-open integer range, analogous to fzshftral . (Contributed by Alexander van der Vekens, 23-Sep-2018)

Ref Expression
Assertion fzoshftral 
|- ( ( 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 fzoval 
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
2 1 3ad2ant2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
3 2 raleqdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ..^ N ) ph <-> A. j e. ( M ... ( N - 1 ) ) ph ) )
4 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
5 fzshftral 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... ( N - 1 ) ) ph <-> A. k e. ( ( M + K ) ... ( ( N - 1 ) + K ) ) [. ( k - K ) / j ]. ph ) )
6 4 5 syl3an2 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... ( N - 1 ) ) ph <-> A. k e. ( ( M + K ) ... ( ( N - 1 ) + K ) ) [. ( k - K ) / j ]. ph ) )
7 zaddcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ )
8 7 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( N + K ) e. ZZ )
9 fzoval 
 |-  ( ( N + K ) e. ZZ -> ( ( M + K ) ..^ ( N + K ) ) = ( ( M + K ) ... ( ( N + K ) - 1 ) ) )
10 8 9 syl 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( M + K ) ..^ ( N + K ) ) = ( ( M + K ) ... ( ( N + K ) - 1 ) ) )
11 zcn 
 |-  ( N e. ZZ -> N e. CC )
12 11 adantr 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> N e. CC )
13 zcn 
 |-  ( K e. ZZ -> K e. CC )
14 13 adantl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> K e. CC )
15 1cnd 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> 1 e. CC )
16 12 14 15 addsubd 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( ( N + K ) - 1 ) = ( ( N - 1 ) + K ) )
17 16 3adant1 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( N + K ) - 1 ) = ( ( N - 1 ) + K ) )
18 17 oveq2d 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( M + K ) ... ( ( N + K ) - 1 ) ) = ( ( M + K ) ... ( ( N - 1 ) + K ) ) )
19 10 18 eqtr2d 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( ( M + K ) ... ( ( N - 1 ) + K ) ) = ( ( M + K ) ..^ ( N + K ) ) )
20 19 raleqdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( M + K ) ... ( ( N - 1 ) + K ) ) [. ( k - K ) / j ]. ph <-> A. k e. ( ( M + K ) ..^ ( N + K ) ) [. ( k - K ) / j ]. ph ) )
21 3 6 20 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 ) )