Metamath Proof Explorer

Theorem isumadd

Description: Addition of infinite sums. (Contributed by Mario Carneiro, 18-Aug-2013) (Revised by Mario Carneiro, 23-Apr-2014)

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

Proof

Step Hyp Ref Expression
1 isumadd.1 
 |-  Z = ( ZZ>= ` M )
2 isumadd.2 
 |-  ( ph -> M e. ZZ )
3 isumadd.3 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) = A )
4 isumadd.4 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
5 isumadd.5 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = B )
6 isumadd.6 
 |-  ( ( ph /\ k e. Z ) -> B e. CC )
7 isumadd.7 
 |-  ( ph -> seq M ( + , F ) e. dom ~~> )
8 isumadd.8 
 |-  ( ph -> seq M ( + , G ) e. dom ~~> )
9 fveq2 
 |-  ( m = k -> ( F ` m ) = ( F ` k ) )
10 fveq2 
 |-  ( m = k -> ( G ` m ) = ( G ` k ) )
11 9 10 oveq12d 
 |-  ( m = k -> ( ( F ` m ) + ( G ` m ) ) = ( ( F ` k ) + ( G ` k ) ) )
12 eqid 
 |-  ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) = ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) )
13 ovex 
 |-  ( ( F ` k ) + ( G ` k ) ) e. _V
14 11 12 13 fvmpt 
 |-  ( k e. Z -> ( ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ` k ) = ( ( F ` k ) + ( G ` k ) ) )
15 14 adantl 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ` k ) = ( ( F ` k ) + ( G ` k ) ) )
16 3 5 oveq12d 
 |-  ( ( ph /\ k e. Z ) -> ( ( F ` k ) + ( G ` k ) ) = ( A + B ) )
17 15 16 eqtrd 
 |-  ( ( ph /\ k e. Z ) -> ( ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ` k ) = ( A + B ) )
18 4 6 addcld 
 |-  ( ( ph /\ k e. Z ) -> ( A + B ) e. CC )
19 1 2 3 4 7 isumclim2 
 |-  ( ph -> seq M ( + , F ) ~~> sum_ k e. Z A )
20 seqex 
 |-  seq M ( + , ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ) e. _V
21 20 a1i 
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ) e. _V )
22 1 2 5 6 8 isumclim2 
 |-  ( ph -> seq M ( + , G ) ~~> sum_ k e. Z B )
23 3 4 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
24 1 2 23 serf 
 |-  ( ph -> seq M ( + , F ) : Z --> CC )
25 24 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , F ) ` j ) e. CC )
26 5 6 eqeltrd 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) e. CC )
27 1 2 26 serf 
 |-  ( ph -> seq M ( + , G ) : Z --> CC )
28 27 ffvelcdmda 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , G ) ` j ) e. CC )
29 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
30 29 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
31 simpll 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ph )
32 elfzuz 
 |-  ( k e. ( M ... j ) -> k e. ( ZZ>= ` M ) )
33 32 1 eleqtrrdi 
 |-  ( k e. ( M ... j ) -> k e. Z )
34 33 adantl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> k e. Z )
35 31 34 23 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( F ` k ) e. CC )
36 31 34 26 syl2anc 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( G ` k ) e. CC )
37 34 14 syl 
 |-  ( ( ( ph /\ j e. Z ) /\ k e. ( M ... j ) ) -> ( ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ` k ) = ( ( F ` k ) + ( G ` k ) ) )
38 30 35 36 37 seradd 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( + , ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ) ` j ) = ( ( seq M ( + , F ) ` j ) + ( seq M ( + , G ) ` j ) ) )
39 1 2 19 21 22 25 28 38 climadd 
 |-  ( ph -> seq M ( + , ( m e. Z |-> ( ( F ` m ) + ( G ` m ) ) ) ) ~~> ( sum_ k e. Z A + sum_ k e. Z B ) )
40 1 2 17 18 39 isumclim 
 |-  ( ph -> sum_ k e. Z ( A + B ) = ( sum_ k e. Z A + sum_ k e. Z B ) )