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 )