Metamath Proof Explorer

Theorem isumclim3

Description: The sequence of partial finite sums of a converging infinite series converges to the infinite sum of the series. Note that j must not occur in A . (Contributed by NM, 9-Jan-2006) (Revised by Mario Carneiro, 23-Apr-2014)

Ref Expression
Hypotheses isumclim3.1 
|- Z = ( ZZ>= ` M )
isumclim3.2 
|- ( ph -> M e. ZZ )
isumclim3.3 
|- ( ph -> F e. dom ~~> )
isumclim3.4 
|- ( ( ph /\ k e. Z ) -> A e. CC )
isumclim3.5 
|- ( ( ph /\ j e. Z ) -> ( F ` j ) = sum_ k e. ( M ... j ) A )
Assertion isumclim3 
|- ( ph -> F ~~> sum_ k e. Z A )

Proof

Step Hyp Ref Expression
1 isumclim3.1 
 |-  Z = ( ZZ>= ` M )
2 isumclim3.2 
 |-  ( ph -> M e. ZZ )
3 isumclim3.3 
 |-  ( ph -> F e. dom ~~> )
4 isumclim3.4 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 isumclim3.5 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = sum_ k e. ( M ... j ) A )
6 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
7 3 6 sylib 
 |-  ( ph -> F ~~> ( ~~> ` F ) )
8 sumfc 
 |-  sum_ m e. Z ( ( k e. Z |-> A ) ` m ) = sum_ k e. Z A
9 eqidd 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
10 4 fmpttd 
 |-  ( ph -> ( k e. Z |-> A ) : Z --> CC )
11 10 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> A ) ` m ) e. CC )
12 1 2 9 11 isum 
 |-  ( ph -> sum_ m e. Z ( ( k e. Z |-> A ) ` m ) = ( ~~> ` seq M ( + , ( k e. Z |-> A ) ) ) )
13 8 12 syl5eqr 
 |-  ( ph -> sum_ k e. Z A = ( ~~> ` seq M ( + , ( k e. Z |-> A ) ) ) )
14 seqex 
 |-  seq M ( + , ( k e. Z |-> A ) ) e. _V
15 14 a1i 
 |-  ( ph -> seq M ( + , ( k e. Z |-> A ) ) e. _V )
16 fzssuz 
 |-  ( M ... j ) C_ ( ZZ>= ` M )
17 16 1 sseqtrri 
 |-  ( M ... j ) C_ Z
18 resmpt 
 |-  ( ( M ... j ) C_ Z -> ( ( k e. Z |-> A ) |` ( M ... j ) ) = ( k e. ( M ... j ) |-> A ) )
19 17 18 ax-mp 
 |-  ( ( k e. Z |-> A ) |` ( M ... j ) ) = ( k e. ( M ... j ) |-> A )
20 19 fveq1i 
 |-  ( ( ( k e. Z |-> A ) |` ( M ... j ) ) ` m ) = ( ( k e. ( M ... j ) |-> A ) ` m )
21 fvres 
 |-  ( m e. ( M ... j ) -> ( ( ( k e. Z |-> A ) |` ( M ... j ) ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
22 20 21 syl5reqr 
 |-  ( m e. ( M ... j ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. ( M ... j ) |-> A ) ` m ) )
23 22 sumeq2i 
 |-  sum_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = sum_ m e. ( M ... j ) ( ( k e. ( M ... j ) |-> A ) ` m )
24 sumfc 
 |-  sum_ m e. ( M ... j ) ( ( k e. ( M ... j ) |-> A ) ` m ) = sum_ k e. ( M ... j ) A
25 23 24 eqtri 
 |-  sum_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = sum_ k e. ( M ... j ) A
26 eqidd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( M ... j ) ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
27 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
28 27 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
29 simpl 
 |-  ( ( ph /\ j e. Z ) -> ph )
30 elfzuz 
 |-  ( m e. ( M ... j ) -> m e. ( ZZ>= ` M ) )
31 30 1 eleqtrrdi 
 |-  ( m e. ( M ... j ) -> m e. Z )
32 29 31 11 syl2an 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( M ... j ) ) -> ( ( k e. Z |-> A ) ` m ) e. CC )
33 26 28 32 fsumser 
 |-  ( ( ph /\ j e. Z ) -> sum_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = ( seq M ( + , ( k e. Z |-> A ) ) ` j ) )
34 25 33 syl5eqr 
 |-  ( ( ph /\ j e. Z ) -> sum_ k e. ( M ... j ) A = ( seq M ( + , ( k e. Z |-> A ) ) ` j ) )
35 5 34 eqtr2d 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , ( k e. Z |-> A ) ) ` j ) = ( F ` j ) )
36 1 15 3 2 35 climeq 
 |-  ( ph -> ( seq M ( + , ( k e. Z |-> A ) ) ~~> x <-> F ~~> x ) )
37 36 iotabidv 
 |-  ( ph -> ( iota x seq M ( + , ( k e. Z |-> A ) ) ~~> x ) = ( iota x F ~~> x ) )
38 df-fv 
 |-  ( ~~> ` seq M ( + , ( k e. Z |-> A ) ) ) = ( iota x seq M ( + , ( k e. Z |-> A ) ) ~~> x )
39 df-fv 
 |-  ( ~~> ` F ) = ( iota x F ~~> x )
40 37 38 39 3eqtr4g 
 |-  ( ph -> ( ~~> ` seq M ( + , ( k e. Z |-> A ) ) ) = ( ~~> ` F ) )
41 13 40 eqtrd 
 |-  ( ph -> sum_ k e. Z A = ( ~~> ` F ) )
42 7 41 breqtrrd 
 |-  ( ph -> F ~~> sum_ k e. Z A )