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 | |
|
seradd.2 | |
||
seradd.3 | |
||
seradd.4 | |
||
Assertion | seradd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | seradd.1 | |
|
2 | seradd.2 | |
|
3 | seradd.3 | |
|
4 | seradd.4 | |
|
5 | addcl | |
|
6 | 5 | adantl | |
7 | addcom | |
|
8 | 7 | adantl | |
9 | addass | |
|
10 | 9 | adantl | |
11 | 6 8 10 1 2 3 4 | seqcaopr | |