Metamath Proof Explorer


Theorem telfsumo2

Description: Sum of a telescoping series. (Contributed by Mario Carneiro, 2-May-2016)

Ref Expression
Hypotheses telfsumo.1
|- ( k = j -> A = B )
telfsumo.2
|- ( k = ( j + 1 ) -> A = C )
telfsumo.3
|- ( k = M -> A = D )
telfsumo.4
|- ( k = N -> A = E )
telfsumo.5
|- ( ph -> N e. ( ZZ>= ` M ) )
telfsumo.6
|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
Assertion telfsumo2
|- ( ph -> sum_ j e. ( M ..^ N ) ( C - B ) = ( E - D ) )

Proof

Step Hyp Ref Expression
1 telfsumo.1
 |-  ( k = j -> A = B )
2 telfsumo.2
 |-  ( k = ( j + 1 ) -> A = C )
3 telfsumo.3
 |-  ( k = M -> A = D )
4 telfsumo.4
 |-  ( k = N -> A = E )
5 telfsumo.5
 |-  ( ph -> N e. ( ZZ>= ` M ) )
6 telfsumo.6
 |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
7 1 negeqd
 |-  ( k = j -> -u A = -u B )
8 2 negeqd
 |-  ( k = ( j + 1 ) -> -u A = -u C )
9 3 negeqd
 |-  ( k = M -> -u A = -u D )
10 4 negeqd
 |-  ( k = N -> -u A = -u E )
11 6 negcld
 |-  ( ( ph /\ k e. ( M ... N ) ) -> -u A e. CC )
12 7 8 9 10 5 11 telfsumo
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( -u B - -u C ) = ( -u D - -u E ) )
13 6 ralrimiva
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
14 elfzofz
 |-  ( j e. ( M ..^ N ) -> j e. ( M ... N ) )
15 1 eleq1d
 |-  ( k = j -> ( A e. CC <-> B e. CC ) )
16 15 rspccva
 |-  ( ( A. k e. ( M ... N ) A e. CC /\ j e. ( M ... N ) ) -> B e. CC )
17 13 14 16 syl2an
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> B e. CC )
18 fzofzp1
 |-  ( j e. ( M ..^ N ) -> ( j + 1 ) e. ( M ... N ) )
19 2 eleq1d
 |-  ( k = ( j + 1 ) -> ( A e. CC <-> C e. CC ) )
20 19 rspccva
 |-  ( ( A. k e. ( M ... N ) A e. CC /\ ( j + 1 ) e. ( M ... N ) ) -> C e. CC )
21 13 18 20 syl2an
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> C e. CC )
22 17 21 neg2subd
 |-  ( ( ph /\ j e. ( M ..^ N ) ) -> ( -u B - -u C ) = ( C - B ) )
23 22 sumeq2dv
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( -u B - -u C ) = sum_ j e. ( M ..^ N ) ( C - B ) )
24 3 eleq1d
 |-  ( k = M -> ( A e. CC <-> D e. CC ) )
25 eluzfz1
 |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
26 5 25 syl
 |-  ( ph -> M e. ( M ... N ) )
27 24 13 26 rspcdva
 |-  ( ph -> D e. CC )
28 4 eleq1d
 |-  ( k = N -> ( A e. CC <-> E e. CC ) )
29 eluzfz2
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
30 5 29 syl
 |-  ( ph -> N e. ( M ... N ) )
31 28 13 30 rspcdva
 |-  ( ph -> E e. CC )
32 27 31 neg2subd
 |-  ( ph -> ( -u D - -u E ) = ( E - D ) )
33 12 23 32 3eqtr3d
 |-  ( ph -> sum_ j e. ( M ..^ N ) ( C - B ) = ( E - D ) )