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 φNM
seradd.2 φkMNFk
seradd.3 φkMNGk
seradd.4 φkMNHk=Fk+Gk
Assertion seradd φseqM+HN=seqM+FN+seqM+GN

Proof

Step Hyp Ref Expression
1 seradd.1 φNM
2 seradd.2 φkMNFk
3 seradd.3 φkMNGk
4 seradd.4 φkMNHk=Fk+Gk
5 addcl xyx+y
6 5 adantl φxyx+y
7 addcom xyx+y=y+x
8 7 adantl φxyx+y=y+x
9 addass xyzx+y+z=x+y+z
10 9 adantl φxyzx+y+z=x+y+z
11 6 8 10 1 2 3 4 seqcaopr φseqM+HN=seqM+FN+seqM+GN