Metamath Proof Explorer

Theorem sersub

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

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

Proof

Step Hyp Ref Expression
1 sersub.1 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
2 sersub.2 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( F ` k ) e. CC )
3 sersub.3 
 |-  ( ( ph /\ k e. ( M ... N ) ) -> ( G ` k ) e. CC )
4 sersub.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 subcl 
 |-  ( ( x e. CC /\ y e. CC ) -> ( x - y ) e. CC )
8 7 adantl 
 |-  ( ( ph /\ ( x e. CC /\ y e. CC ) ) -> ( x - y ) e. CC )
9 addsub4 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( z e. CC /\ w e. CC ) ) -> ( ( x + y ) - ( z + w ) ) = ( ( x - z ) + ( y - w ) ) )
10 9 eqcomd 
 |-  ( ( ( x e. CC /\ y e. CC ) /\ ( z e. CC /\ w e. CC ) ) -> ( ( x - z ) + ( y - w ) ) = ( ( x + y ) - ( z + w ) ) )
11 10 adantl 
 |-  ( ( ph /\ ( ( x e. CC /\ y e. CC ) /\ ( z e. CC /\ w e. CC ) ) ) -> ( ( x - z ) + ( y - w ) ) = ( ( x + y ) - ( z + w ) ) )
12 6 8 11 1 2 3 4 seqcaopr2 
 |-  ( ph -> ( seq M ( + , H ) ` N ) = ( ( seq M ( + , F ) ` N ) - ( seq M ( + , G ) ` N ) ) )