Metamath Proof Explorer

Theorem fsumcvg2

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 fsumsers.1 
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
fsumsers.2 
|- ( ph -> N e. ( ZZ>= ` M ) )
fsumsers.3 
|- ( ( ph /\ k e. A ) -> B e. CC )
fsumsers.4 
|- ( ph -> A C_ ( M ... N ) )
Assertion fsumcvg2 
|- ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 fsumsers.1 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
2 fsumsers.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 fsumsers.3 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
4 fsumsers.4 
 |-  ( ph -> A C_ ( M ... N ) )
5 nfcv 
 |-  F/_ m if ( k e. A , B , 0 )
6 nfv 
 |-  F/ k m e. A
7 nfcsb1v 
 |-  F/_ k [_ m / k ]_ B
8 nfcv 
 |-  F/_ k 0
9 6 7 8 nfif 
 |-  F/_ k if ( m e. A , [_ m / k ]_ B , 0 )
10 eleq1w 
 |-  ( k = m -> ( k e. A <-> m e. A ) )
11 csbeq1a 
 |-  ( k = m -> B = [_ m / k ]_ B )
12 10 11 ifbieq1d 
 |-  ( k = m -> if ( k e. A , B , 0 ) = if ( m e. A , [_ m / k ]_ B , 0 ) )
13 5 9 12 cbvmpt 
 |-  ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( m e. ZZ |-> if ( m e. A , [_ m / k ]_ B , 0 ) )
14 3 ralrimiva 
 |-  ( ph -> A. k e. A B e. CC )
15 7 nfel1 
 |-  F/ k [_ m / k ]_ B e. CC
16 11 eleq1d 
 |-  ( k = m -> ( B e. CC <-> [_ m / k ]_ B e. CC ) )
17 15 16 rspc 
 |-  ( m e. A -> ( A. k e. A B e. CC -> [_ m / k ]_ B e. CC ) )
18 14 17 mpan9 
 |-  ( ( ph /\ m e. A ) -> [_ m / k ]_ B e. CC )
19 13 18 2 4 fsumcvg 
 |-  ( ph -> seq M ( + , ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ) ~~> ( seq M ( + , ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ) ` N ) )
20 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
21 2 20 syl 
 |-  ( ph -> M e. ZZ )
22 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
23 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 0 ) = B )
24 23 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
25 24 3 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
26 25 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
27 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
28 0cn 
 |-  0 e. CC
29 27 28 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
30 26 29 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 0 ) e. CC )
31 eqid 
 |-  ( k e. ZZ |-> if ( k e. A , B , 0 ) ) = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
32 31 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) = if ( k e. A , B , 0 ) )
33 22 30 32 syl2anr 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) = if ( k e. A , B , 0 ) )
34 1 33 eqtr4d 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) )
35 34 ralrimiva 
 |-  ( ph -> A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) )
36 nffvmpt1 
 |-  F/_ k ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n )
37 36 nfeq2 
 |-  F/ k ( F ` n ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n )
38 fveq2 
 |-  ( k = n -> ( F ` k ) = ( F ` n ) )
39 fveq2 
 |-  ( k = n -> ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n ) )
40 38 39 eqeq12d 
 |-  ( k = n -> ( ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) <-> ( F ` n ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n ) ) )
41 37 40 rspc 
 |-  ( n e. ( ZZ>= ` M ) -> ( A. k e. ( ZZ>= ` M ) ( F ` k ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` k ) -> ( F ` n ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n ) ) )
42 35 41 mpan9 
 |-  ( ( ph /\ n e. ( ZZ>= ` M ) ) -> ( F ` n ) = ( ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ` n ) )
43 21 42 seqfeq 
 |-  ( ph -> seq M ( + , F ) = seq M ( + , ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ) )
44 43 fveq1d 
 |-  ( ph -> ( seq M ( + , F ) ` N ) = ( seq M ( + , ( k e. ZZ |-> if ( k e. A , B , 0 ) ) ) ` N ) )
45 19 43 44 3brtr4d 
 |-  ( ph -> seq M ( + , F ) ~~> ( seq M ( + , F ) ` N ) )