Metamath Proof Explorer

Theorem fzrevral

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 fzrevral 
|- ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph ) )

Proof

Step Hyp Ref Expression
1 simpr 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> k e. ( ( K - N ) ... ( K - M ) ) )
2 elfzelz 
 |-  ( k e. ( ( K - N ) ... ( K - M ) ) -> k e. ZZ )
3 fzrev 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ k e. ZZ ) ) -> ( k e. ( ( K - N ) ... ( K - M ) ) <-> ( K - k ) e. ( M ... N ) ) )
4 3 anassrs 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ k e. ZZ ) -> ( k e. ( ( K - N ) ... ( K - M ) ) <-> ( K - k ) e. ( M ... N ) ) )
5 2 4 sylan2 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( k e. ( ( K - N ) ... ( K - M ) ) <-> ( K - k ) e. ( M ... N ) ) )
6 1 5 mpbid 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( K - k ) e. ( M ... N ) )
7 rspsbc 
 |-  ( ( K - k ) e. ( M ... N ) -> ( A. j e. ( M ... N ) ph -> [. ( K - k ) / j ]. ph ) )
8 6 7 syl 
 |-  ( ( ( ( M e. ZZ /\ N e. ZZ ) /\ K e. ZZ ) /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( A. j e. ( M ... N ) ph -> [. ( K - k ) / j ]. ph ) )
9 8 ex3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( k e. ( ( K - N ) ... ( K - M ) ) -> ( A. j e. ( M ... N ) ph -> [. ( K - k ) / j ]. ph ) ) )
10 9 com23 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph -> ( k e. ( ( K - N ) ... ( K - M ) ) -> [. ( K - k ) / j ]. ph ) ) )
11 10 ralrimdv 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph -> A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph ) )
12 nfv 
 |-  F/ j K e. ZZ
13 nfcv 
 |-  F/_ j ( ( K - N ) ... ( K - M ) )
14 nfsbc1v 
 |-  F/ j [. ( K - k ) / j ]. ph
15 13 14 nfralw 
 |-  F/ j A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph
16 fzrev2i 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> ( K - j ) e. ( ( K - N ) ... ( K - M ) ) )
17 oveq2 
 |-  ( k = ( K - j ) -> ( K - k ) = ( K - ( K - j ) ) )
18 17 sbceq1d 
 |-  ( k = ( K - j ) -> ( [. ( K - k ) / j ]. ph <-> [. ( K - ( K - j ) ) / j ]. ph ) )
19 18 rspcv 
 |-  ( ( K - j ) e. ( ( K - N ) ... ( K - M ) ) -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> [. ( K - ( K - j ) ) / j ]. ph ) )
20 16 19 syl 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> [. ( K - ( K - j ) ) / j ]. ph ) )
21 zcn 
 |-  ( K e. ZZ -> K e. CC )
22 elfzelz 
 |-  ( j e. ( M ... N ) -> j e. ZZ )
23 22 zcnd 
 |-  ( j e. ( M ... N ) -> j e. CC )
24 nncan 
 |-  ( ( K e. CC /\ j e. CC ) -> ( K - ( K - j ) ) = j )
25 21 23 24 syl2an 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> ( K - ( K - j ) ) = j )
26 25 eqcomd 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> j = ( K - ( K - j ) ) )
27 sbceq1a 
 |-  ( j = ( K - ( K - j ) ) -> ( ph <-> [. ( K - ( K - j ) ) / j ]. ph ) )
28 26 27 syl 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> ( ph <-> [. ( K - ( K - j ) ) / j ]. ph ) )
29 20 28 sylibrd 
 |-  ( ( K e. ZZ /\ j e. ( M ... N ) ) -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> ph ) )
30 29 ex 
 |-  ( K e. ZZ -> ( j e. ( M ... N ) -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> ph ) ) )
31 30 com23 
 |-  ( K e. ZZ -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> ( j e. ( M ... N ) -> ph ) ) )
32 12 15 31 ralrimd 
 |-  ( K e. ZZ -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> A. j e. ( M ... N ) ph ) )
33 32 3ad2ant3 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph -> A. j e. ( M ... N ) ph ) )
34 11 33 impbid 
 |-  ( ( M e. ZZ /\ N e. ZZ /\ K e. ZZ ) -> ( A. j e. ( M ... N ) ph <-> A. k e. ( ( K - N ) ... ( K - M ) ) [. ( K - k ) / j ]. ph ) )