Description: Addition of infinite sums. (Contributed by Thierry Arnoux, 22-Jun-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | esumaddf.0 | |
|
esumaddf.a | |
||
esumaddf.1 | |
||
esumaddf.2 | |
||
esumaddf.3 | |
||
Assertion | esumaddf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | esumaddf.0 | |
|
2 | esumaddf.a | |
|
3 | esumaddf.1 | |
|
4 | esumaddf.2 | |
|
5 | esumaddf.3 | |
|
6 | ge0xaddcl | |
|
7 | 4 5 6 | syl2anc | |
8 | xrge0base | |
|
9 | xrge0plusg | |
|
10 | xrge0cmn | |
|
11 | 10 | a1i | |
12 | xrge0tmd | |
|
13 | 12 | a1i | |
14 | nfcv | |
|
15 | eqid | |
|
16 | 1 2 14 4 15 | fmptdF | |
17 | eqid | |
|
18 | 1 2 14 5 17 | fmptdF | |
19 | 1 2 3 4 | esumel | |
20 | 1 2 3 5 | esumel | |
21 | 8 9 11 13 3 16 18 19 20 | tsmsadd | |
22 | eqidd | |
|
23 | eqidd | |
|
24 | 1 2 3 4 5 22 23 | offval2f | |
25 | 24 | oveq2d | |
26 | 21 25 | eleqtrd | |
27 | 1 2 3 7 26 | esumid | |