Metamath Proof Explorer


Theorem esumel

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 kφ
esumel.2 _kA
esumel.3 φAV
esumel.4 φkAB0+∞
Assertion esumel φ*kAB𝑠*𝑠0+∞tsumskAB

Proof

Step Hyp Ref Expression
1 esumel.1 kφ
2 esumel.2 _kA
3 esumel.3 φAV
4 esumel.4 φkAB0+∞
5 4 ex φkAB0+∞
6 1 5 ralrimi φkAB0+∞
7 2 esumcl AVkAB0+∞*kAB0+∞
8 3 6 7 syl2anc φ*kAB0+∞
9 snidg *kAB0+∞*kAB*kAB
10 8 9 syl φ*kAB*kAB
11 eqid 𝑠*𝑠0+∞=𝑠*𝑠0+∞
12 nfcv _k0+∞
13 eqid kAB=kAB
14 1 2 12 4 13 fmptdF φkAB:A0+∞
15 inss1 𝒫AFin𝒫A
16 simpr φx𝒫AFinx𝒫AFin
17 15 16 sselid φx𝒫AFinx𝒫A
18 17 elpwid φx𝒫AFinxA
19 nfcv _kx
20 2 19 resmptf xAkABx=kxB
21 18 20 syl φx𝒫AFinkABx=kxB
22 21 eqcomd φx𝒫AFinkxB=kABx
23 22 oveq2d φx𝒫AFin𝑠*𝑠0+∞kxB=𝑠*𝑠0+∞kABx
24 1 2 3 4 23 esumval φ*kAB=supranx𝒫AFin𝑠*𝑠0+∞kABx*<
25 11 3 14 24 xrge0tsmsd φ𝑠*𝑠0+∞tsumskAB=*kAB
26 10 25 eleqtrrd φ*kAB𝑠*𝑠0+∞tsumskAB