Metamath Proof Explorer

Theorem isum1p

Description: The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses isum1p.1 
|- Z = ( ZZ>= ` M )
isum1p.3 
|- ( ph -> M e. ZZ )
isum1p.4 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
isum1p.5 
|- ( ( ph /\ k e. Z ) -> A e. CC )
isum1p.6 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion isum1p 
|- ( ph -> sum_ k e. Z A = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )

Proof

Step Hyp Ref Expression
1 isum1p.1 
 |-  Z = ( ZZ>= ` M )
2 isum1p.3 
 |-  ( ph -> M e. ZZ )
3 isum1p.4 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isum1p.5 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 isum1p.6 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
6 eqid 
 |-  ( ZZ>= ` ( M + 1 ) ) = ( ZZ>= ` ( M + 1 ) )
7 uzid 
 |-  ( M e. ZZ -> M e. ( ZZ>= ` M ) )
8 2 7 syl 
 |-  ( ph -> M e. ( ZZ>= ` M ) )
9 peano2uz 
 |-  ( M e. ( ZZ>= ` M ) -> ( M + 1 ) e. ( ZZ>= ` M ) )
10 8 9 syl 
 |-  ( ph -> ( M + 1 ) e. ( ZZ>= ` M ) )
11 10 1 eleqtrrdi 
 |-  ( ph -> ( M + 1 ) e. Z )
12 1 6 11 3 4 5 isumsplit 
 |-  ( ph -> sum_ k e. Z A = ( sum_ k e. ( M ... ( ( M + 1 ) - 1 ) ) A + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )
13 2 zcnd 
 |-  ( ph -> M e. CC )
14 ax-1cn 
 |-  1 e. CC
15 pncan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M + 1 ) - 1 ) = M )
16 13 14 15 sylancl 
 |-  ( ph -> ( ( M + 1 ) - 1 ) = M )
17 16 oveq2d 
 |-  ( ph -> ( M ... ( ( M + 1 ) - 1 ) ) = ( M ... M ) )
18 17 sumeq1d 
 |-  ( ph -> sum_ k e. ( M ... ( ( M + 1 ) - 1 ) ) A = sum_ k e. ( M ... M ) A )
19 elfzuz 
 |-  ( k e. ( M ... M ) -> k e. ( ZZ>= ` M ) )
20 19 1 eleqtrrdi 
 |-  ( k e. ( M ... M ) -> k e. Z )
21 20 3 sylan2 
 |-  ( ( ph /\ k e. ( M ... M ) ) -> ( F ` k ) = A )
22 21 sumeq2dv 
 |-  ( ph -> sum_ k e. ( M ... M ) ( F ` k ) = sum_ k e. ( M ... M ) A )
23 fveq2 
 |-  ( k = M -> ( F ` k ) = ( F ` M ) )
24 23 eleq1d 
 |-  ( k = M -> ( ( F ` k ) e. CC <-> ( F ` M ) e. CC ) )
25 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
26 25 ralrimiva 
 |-  ( ph -> A. k e. Z ( F ` k ) e. CC )
27 8 1 eleqtrrdi 
 |-  ( ph -> M e. Z )
28 24 26 27 rspcdva 
 |-  ( ph -> ( F ` M ) e. CC )
29 23 fsum1 
 |-  ( ( M e. ZZ /\ ( F ` M ) e. CC ) -> sum_ k e. ( M ... M ) ( F ` k ) = ( F ` M ) )
30 2 28 29 syl2anc 
 |-  ( ph -> sum_ k e. ( M ... M ) ( F ` k ) = ( F ` M ) )
31 18 22 30 3eqtr2d 
 |-  ( ph -> sum_ k e. ( M ... ( ( M + 1 ) - 1 ) ) A = ( F ` M ) )
32 31 oveq1d 
 |-  ( ph -> ( sum_ k e. ( M ... ( ( M + 1 ) - 1 ) ) A + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )
33 12 32 eqtrd 
 |-  ( ph -> sum_ k e. Z A = ( ( F ` M ) + sum_ k e. ( ZZ>= ` ( M + 1 ) ) A ) )