Metamath Proof Explorer


Theorem seradd

Description: The sum of two infinite series. (Contributed by NM, 17-Mar-2005) (Revised by Mario Carneiro, 26-May-2014)

Ref Expression
Hypotheses seradd.1
|- ( ph -> N e. ( ZZ>= ` M ) )
seradd.2
|- ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
seradd.3
|- ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
seradd.4
|- ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )
Assertion seradd
|- ( ph -> ( seq M ( + , H ) ` N ) = ( ( seq M ( + , F ) ` N ) + ( seq M ( + , G ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seradd.1
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 seradd.2
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3 seradd.3
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
4 seradd.4
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( H ` k ) = ( ( F ` k ) + ( G ` k ) ) )
5 addcl
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) e. CC )
6 5 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) e. CC )
7 addcom
 |-  ( ( x e. CC /\ y e. CC ) -> ( x + y ) = ( y + x ) )
8 7 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x + y ) = ( y + x ) )
9 addass
 |-  ( ( x e. CC /\ y e. CC /\ z e. CC ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
10 9 adantl
 |-  ( ( ph /\ ( x e. CC /\ y e. CC /\ z e. CC ) ) -> ( ( x + y ) + z ) = ( x + ( y + z ) ) )
11 6 8 10 1 2 3 4 seqcaopr
 |-  ( ph -> ( seq M ( + , H ) ` N ) = ( ( seq M ( + , F ) ` N ) + ( seq M ( + , G ) ` N ) ) )