Metamath Proof Explorer

Theorem fprodrev

Description: Reversal of a finite product. (Contributed by Scott Fenton, 5-Jan-2018)

Ref Expression
Hypotheses fprodshft.1 
|- ( ph -> K e. ZZ )
fprodshft.2 
|- ( ph -> M e. ZZ )
fprodshft.3 
|- ( ph -> N e. ZZ )
fprodshft.4 
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
fprodrev.5 
|- ( j = ( K - k ) -> A = B )
Assertion fprodrev 
|- ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( K - N ) ... ( K - M ) ) B )

Proof

Step Hyp Ref Expression
1 fprodshft.1 
 |-  ( ph -> K e. ZZ )
2 fprodshft.2 
 |-  ( ph -> M e. ZZ )
3 fprodshft.3 
 |-  ( ph -> N e. ZZ )
4 fprodshft.4 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
5 fprodrev.5 
 |-  ( j = ( K - k ) -> A = B )
6 fzfid 
 |-  ( ph -> ( ( K - N ) ... ( K - M ) ) e. Fin )
7 eqid 
 |-  ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) = ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) )
8 1 adantr 
 |-  ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> K e. ZZ )
9 elfzelz 
 |-  ( j e. ( ( K - N ) ... ( K - M ) ) -> j e. ZZ )
10 9 adantl 
 |-  ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> j e. ZZ )
11 8 10 zsubcld 
 |-  ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> ( K - j ) e. ZZ )
12 1 adantr 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> K e. ZZ )
13 elfzelz 
 |-  ( k e. ( M ... N ) -> k e. ZZ )
14 13 adantl 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> k e. ZZ )
15 12 14 zsubcld 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( K - k ) e. ZZ )
16 simprr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k = ( K - j ) )
17 simprl 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) )
18 2 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> M e. ZZ )
19 3 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> N e. ZZ )
20 1 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> K e. ZZ )
21 9 ad2antrl 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ZZ )
22 fzrev 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ j e. ZZ ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) )
23 18 19 20 21 22 syl22anc 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) )
24 17 23 mpbid 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - j ) e. ( M ... N ) )
25 16 24 eqeltrd 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k e. ( M ... N ) )
26 oveq2 
 |-  ( k = ( K - j ) -> ( K - k ) = ( K - ( K - j ) ) )
27 26 ad2antll 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - k ) = ( K - ( K - j ) ) )
28 1 zcnd 
 |-  ( ph -> K e. CC )
29 28 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> K e. CC )
30 9 zcnd 
 |-  ( j e. ( ( K - N ) ... ( K - M ) ) -> j e. CC )
31 30 ad2antrl 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. CC )
32 29 31 nncand 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - ( K - j ) ) = j )
33 27 32 eqtr2d 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j = ( K - k ) )
34 25 33 jca 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( k e. ( M ... N ) /\ j = ( K - k ) ) )
35 simprr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j = ( K - k ) )
36 simprl 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ( M ... N ) )
37 2 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> M e. ZZ )
38 3 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> N e. ZZ )
39 1 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> K e. ZZ )
40 13 ad2antrl 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ZZ )
41 fzrev2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ k e. ZZ ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) )
42 37 38 39 40 41 syl22anc 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) )
43 36 42 mpbid 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) )
44 35 43 eqeltrd 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) )
45 oveq2 
 |-  ( j = ( K - k ) -> ( K - j ) = ( K - ( K - k ) ) )
46 45 ad2antll 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - j ) = ( K - ( K - k ) ) )
47 28 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> K e. CC )
48 13 zcnd 
 |-  ( k e. ( M ... N ) -> k e. CC )
49 48 ad2antrl 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. CC )
50 47 49 nncand 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - ( K - k ) ) = k )
51 46 50 eqtr2d 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k = ( K - j ) )
52 44 51 jca 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) )
53 34 52 impbida 
 |-  ( ph -> ( ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) <-> ( k e. ( M ... N ) /\ j = ( K - k ) ) ) )
54 7 11 15 53 f1od 
 |-  ( ph -> ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) : ( ( K - N ) ... ( K - M ) ) -1-1-onto-> ( M ... N ) )
55 oveq2 
 |-  ( j = k -> ( K - j ) = ( K - k ) )
56 ovex 
 |-  ( K - k ) e. _V
57 55 7 56 fvmpt 
 |-  ( k e. ( ( K - N ) ... ( K - M ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) )
58 57 adantl 
 |-  ( ( ph /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) )
59 5 6 54 58 4 fprodf1o 
 |-  ( ph -> prod_ j e. ( M ... N ) A = prod_ k e. ( ( K - N ) ... ( K - M ) ) B )