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