Metamath Proof Explorer

Theorem fsumrev

Description: Reversal of a finite sum. (Contributed by NM, 26-Nov-2005) (Revised by Mario Carneiro, 24-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 fsumrev.1 
 |-  ( ph -> K e. ZZ )
2 fsumrev.2 
 |-  ( ph -> M e. ZZ )
3 fsumrev.3 
 |-  ( ph -> N e. ZZ )
4 fsumrev.4 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
5 fsumrev.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 ovexd 
 |-  ( ( ph /\ j e. ( ( K - N ) ... ( K - M ) ) ) -> ( K - j ) e. _V )
9 ovexd 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( K - k ) e. _V )
10 simprr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k = ( K - j ) )
11 simprl 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) )
12 2 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> M e. ZZ )
13 3 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> N e. ZZ )
14 1 adantr 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> K e. ZZ )
15 elfzelz 
 |-  ( j e. ( ( K - N ) ... ( K - M ) ) -> j e. ZZ )
16 11 15 syl 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j e. ZZ )
17 fzrev 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ j e. ZZ ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) )
18 12 13 14 16 17 syl22anc 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) <-> ( K - j ) e. ( M ... N ) ) )
19 11 18 mpbid 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - j ) e. ( M ... N ) )
20 10 19 eqeltrd 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> k e. ( M ... N ) )
21 10 oveq2d 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - k ) = ( K - ( K - j ) ) )
22 zcn 
 |-  ( K e. ZZ -> K e. CC )
23 zcn 
 |-  ( j e. ZZ -> j e. CC )
24 nncan 
 |-  ( ( K e. CC /\ j e. CC ) -> ( K - ( K - j ) ) = j )
25 22 23 24 syl2an 
 |-  ( ( K e. ZZ /\ j e. ZZ ) -> ( K - ( K - j ) ) = j )
26 1 16 25 syl2an2r 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( K - ( K - j ) ) = j )
27 21 26 eqtr2d 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> j = ( K - k ) )
28 20 27 jca 
 |-  ( ( ph /\ ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) ) -> ( k e. ( M ... N ) /\ j = ( K - k ) ) )
29 simprr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j = ( K - k ) )
30 simprl 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ( M ... N ) )
31 2 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> M e. ZZ )
32 3 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> N e. ZZ )
33 1 adantr 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> K e. ZZ )
34 elfzelz 
 |-  ( k e. ( M ... N ) -> k e. ZZ )
35 30 34 syl 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k e. ZZ )
36 fzrev2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ ) /\ ( K e. ZZ /\ k e. ZZ ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) )
37 31 32 33 35 36 syl22anc 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( k e. ( M ... N ) <-> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) ) )
38 30 37 mpbid 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - k ) e. ( ( K - N ) ... ( K - M ) ) )
39 29 38 eqeltrd 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> j e. ( ( K - N ) ... ( K - M ) ) )
40 29 oveq2d 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - j ) = ( K - ( K - k ) ) )
41 zcn 
 |-  ( k e. ZZ -> k e. CC )
42 nncan 
 |-  ( ( K e. CC /\ k e. CC ) -> ( K - ( K - k ) ) = k )
43 22 41 42 syl2an 
 |-  ( ( K e. ZZ /\ k e. ZZ ) -> ( K - ( K - k ) ) = k )
44 1 35 43 syl2an2r 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( K - ( K - k ) ) = k )
45 40 44 eqtr2d 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> k = ( K - j ) )
46 39 45 jca 
 |-  ( ( ph /\ ( k e. ( M ... N ) /\ j = ( K - k ) ) ) -> ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) )
47 28 46 impbida 
 |-  ( ph -> ( ( j e. ( ( K - N ) ... ( K - M ) ) /\ k = ( K - j ) ) <-> ( k e. ( M ... N ) /\ j = ( K - k ) ) ) )
48 7 8 9 47 f1od 
 |-  ( ph -> ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) : ( ( K - N ) ... ( K - M ) ) -1-1-onto-> ( M ... N ) )
49 oveq2 
 |-  ( j = k -> ( K - j ) = ( K - k ) )
50 ovex 
 |-  ( K - k ) e. _V
51 49 7 50 fvmpt 
 |-  ( k e. ( ( K - N ) ... ( K - M ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) )
52 51 adantl 
 |-  ( ( ph /\ k e. ( ( K - N ) ... ( K - M ) ) ) -> ( ( j e. ( ( K - N ) ... ( K - M ) ) |-> ( K - j ) ) ` k ) = ( K - k ) )
53 5 6 48 52 4 fsumf1o 
 |-  ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( K - N ) ... ( K - M ) ) B )