Metamath Proof Explorer

Theorem fsumcvg

Description: The sequence of partial sums of a finite sum converges to the whole sum. (Contributed by Mario Carneiro, 20-Apr-2014)

Ref Expression
Hypotheses summo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
sumrb.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
fsumcvg.4 
|- ( ph -> A C_ ( M ... N ) )
Assertion fsumcvg 
|- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 summo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2 summo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 sumrb.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 fsumcvg.4 
 |-  ( ph -> A C_ ( M ... N ) )
5 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
6 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
7 3 6 syl 
 |-  ( ph -> N e. ZZ )
8 seqex 
 |-  seq M ( + , F ) e. _V
9 8 a1i 
 |-  ( ph -> seq M ( + , F ) e. _V )
10 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 3 11 syl 
 |-  ( ph -> M e. ZZ )
13 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
14 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 0 ) = B )
15 14 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
16 15 2 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
17 16 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
18 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
19 0cn 
 |-  0 e. CC
20 18 19 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
21 17 20 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 0 ) e. CC )
22 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
23 13 21 22 syl2anr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
24 21 adantr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> if ( k e. A , B , 0 ) e. CC )
25 23 24 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
26 10 12 25 serf 
 |-  ( ph -> seq M ( + , F ) : ( ZZ>= ` M ) --> CC )
27 26 3 ffvelrnd 
 |-  ( ph -> ( seq M ( + , F ) ` N ) e. CC )
28 addid1 
 |-  ( m e. CC -> ( m + 0 ) = m )
29 28 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. CC ) -> ( m + 0 ) = m )
30 3 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )
31 simpr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ( ZZ>= ` N ) )
32 27 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( + , F ) ` N ) e. CC )
33 elfzuz 
 |-  ( m e. ( ( N + 1 ) ... n ) -> m e. ( ZZ>= ` ( N + 1 ) ) )
34 eluzelz 
 |-  ( m e. ( ZZ>= ` ( N + 1 ) ) -> m e. ZZ )
35 34 adantl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> m e. ZZ )
36 4 sseld 
 |-  ( ph -> ( m e. A -> m e. ( M ... N ) ) )
37 fznuz 
 |-  ( m e. ( M ... N ) -> -. m e. ( ZZ>= ` ( N + 1 ) ) )
38 36 37 syl6 
 |-  ( ph -> ( m e. A -> -. m e. ( ZZ>= ` ( N + 1 ) ) ) )
39 38 con2d 
 |-  ( ph -> ( m e. ( ZZ>= ` ( N + 1 ) ) -> -. m e. A ) )
40 39 imp 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> -. m e. A )
41 35 40 eldifd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> m e. ( ZZ \ A ) )
42 fveqeq2 
 |-  ( k = m -> ( ( F ` k ) = 0 <-> ( F ` m ) = 0 ) )
43 eldifi 
 |-  ( k e. ( ZZ \ A ) -> k e. ZZ )
44 eldifn 
 |-  ( k e. ( ZZ \ A ) -> -. k e. A )
45 44 18 syl 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 0 ) = 0 )
46 45 19 eqeltrdi 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 0 ) e. CC )
47 43 46 22 syl2anc 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
48 47 45 eqtrd 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = 0 )
49 42 48 vtoclga 
 |-  ( m e. ( ZZ \ A ) -> ( F ` m ) = 0 )
50 41 49 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` m ) = 0 )
51 33 50 sylan2 
 |-  ( ( ph /\ m e. ( ( N + 1 ) ... n ) ) -> ( F ` m ) = 0 )
52 51 adantlr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( F ` m ) = 0 )
53 29 30 31 32 52 seqid2 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( + , F ) ` N ) = ( seq M ( + , F ) ` n ) )
54 53 eqcomd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( + , F ) ` n ) = ( seq M ( + , F ) ` N ) )
55 5 7 9 27 54 climconst 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )