Description: The extended sum is a limit point of the corresponding infinite group sum. (Contributed by Thierry Arnoux, 24-Mar-2017)
Ref | Expression | ||
---|---|---|---|
Hypotheses | esumel.1 | |
|
esumel.2 | |
||
esumel.3 | |
||
esumel.4 | |
||
Assertion | esumel | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | esumel.1 | |
|
2 | esumel.2 | |
|
3 | esumel.3 | |
|
4 | esumel.4 | |
|
5 | 4 | ex | |
6 | 1 5 | ralrimi | |
7 | 2 | esumcl | |
8 | 3 6 7 | syl2anc | |
9 | snidg | |
|
10 | 8 9 | syl | |
11 | eqid | |
|
12 | nfcv | |
|
13 | eqid | |
|
14 | 1 2 12 4 13 | fmptdF | |
15 | inss1 | |
|
16 | simpr | |
|
17 | 15 16 | sselid | |
18 | 17 | elpwid | |
19 | nfcv | |
|
20 | 2 19 | resmptf | |
21 | 18 20 | syl | |
22 | 21 | eqcomd | |
23 | 22 | oveq2d | |
24 | 1 2 3 4 23 | esumval | |
25 | 11 3 14 24 | xrge0tsmsd | |
26 | 10 25 | eleqtrrd | |