Metamath Proof Explorer

Theorem fsumrev2

Description: Reversal of a finite sum. (Contributed by NM, 27-Nov-2005) (Revised by Mario Carneiro, 13-Apr-2016)

Ref Expression
Hypotheses fsumrev2.1 
|- ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
fsumrev2.2 
|- ( j = ( ( M + N ) - k ) -> A = B )
Assertion fsumrev2 
|- ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )

Proof

Step Hyp Ref Expression
1 fsumrev2.1 
 |-  ( ( ph /\ j e. ( M ... N ) ) -> A e. CC )
2 fsumrev2.2 
 |-  ( j = ( ( M + N ) - k ) -> A = B )
3 sum0 
 |-  sum_ j e. (/) A = 0
4 sum0 
 |-  sum_ k e. (/) B = 0
5 3 4 eqtr4i 
 |-  sum_ j e. (/) A = sum_ k e. (/) B
6 sumeq1 
 |-  ( ( M ... N ) = (/) -> sum_ j e. ( M ... N ) A = sum_ j e. (/) A )
7 sumeq1 
 |-  ( ( M ... N ) = (/) -> sum_ k e. ( M ... N ) B = sum_ k e. (/) B )
8 5 6 7 3eqtr4a 
 |-  ( ( M ... N ) = (/) -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )
9 8 adantl 
 |-  ( ( ph /\ ( M ... N ) = (/) ) -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )
10 fzn0 
 |-  ( ( M ... N ) =/= (/) <-> N e. ( ZZ>= ` M ) )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 11 adantl 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> M e. ZZ )
13 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
14 13 adantl 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. ZZ )
15 12 14 zaddcld 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( M + N ) e. ZZ )
16 1 adantlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` M ) ) /\ j e. ( M ... N ) ) -> A e. CC )
17 15 12 14 16 2 fsumrev 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> sum_ j e. ( M ... N ) A = sum_ k e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) B )
18 12 zcnd 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> M e. CC )
19 14 zcnd 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> N e. CC )
20 18 19 pncand 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( M + N ) - N ) = M )
21 18 19 pncan2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( M + N ) - M ) = N )
22 20 21 oveq12d 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) = ( M ... N ) )
23 22 sumeq1d 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> sum_ k e. ( ( ( M + N ) - N ) ... ( ( M + N ) - M ) ) B = sum_ k e. ( M ... N ) B )
24 17 23 eqtrd 
 |-  ( ( ph /\ N e. ( ZZ>= ` M ) ) -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )
25 10 24 sylan2b 
 |-  ( ( ph /\ ( M ... N ) =/= (/) ) -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )
26 9 25 pm2.61dane 
 |-  ( ph -> sum_ j e. ( M ... N ) A = sum_ k e. ( M ... N ) B )