Metamath Proof Explorer


Theorem esumpinfsum

Description: The value of the extended sum of infinitely many terms greater than one. (Contributed by Thierry Arnoux, 29-Jun-2017)

Ref Expression
Hypotheses esumpinfsum.p k φ
esumpinfsum.a _ k A
esumpinfsum.1 φ A V
esumpinfsum.2 φ ¬ A Fin
esumpinfsum.3 φ k A B 0 +∞
esumpinfsum.4 φ k A M B
esumpinfsum.5 φ M *
esumpinfsum.6 φ 0 < M
Assertion esumpinfsum φ * k A B = +∞

Proof

Step Hyp Ref Expression
1 esumpinfsum.p k φ
2 esumpinfsum.a _ k A
3 esumpinfsum.1 φ A V
4 esumpinfsum.2 φ ¬ A Fin
5 esumpinfsum.3 φ k A B 0 +∞
6 esumpinfsum.4 φ k A M B
7 esumpinfsum.5 φ M *
8 esumpinfsum.6 φ 0 < M
9 iccssxr 0 +∞ *
10 5 ex φ k A B 0 +∞
11 1 10 ralrimi φ k A B 0 +∞
12 2 esumcl A V k A B 0 +∞ * k A B 0 +∞
13 3 11 12 syl2anc φ * k A B 0 +∞
14 9 13 sseldi φ * k A B *
15 0xr 0 *
16 xrltle 0 * M * 0 < M 0 M
17 15 7 16 sylancr φ 0 < M 0 M
18 8 17 mpd φ 0 M
19 pnfge M * M +∞
20 7 19 syl φ M +∞
21 pnfxr +∞ *
22 elicc1 0 * +∞ * M 0 +∞ M * 0 M M +∞
23 15 21 22 mp2an M 0 +∞ M * 0 M M +∞
24 7 18 20 23 syl3anbrc φ M 0 +∞
25 nfcv _ k M
26 2 25 esumcst A V M 0 +∞ * k A M = A 𝑒 M
27 3 24 26 syl2anc φ * k A M = A 𝑒 M
28 hashinf A V ¬ A Fin A = +∞
29 3 4 28 syl2anc φ A = +∞
30 29 oveq1d φ A 𝑒 M = +∞ 𝑒 M
31 xmulpnf2 M * 0 < M +∞ 𝑒 M = +∞
32 7 8 31 syl2anc φ +∞ 𝑒 M = +∞
33 27 30 32 3eqtrd φ * k A M = +∞
34 24 adantr φ k A M 0 +∞
35 1 2 3 34 5 6 esumlef φ * k A M * k A B
36 33 35 eqbrtrrd φ +∞ * k A B
37 xgepnf * k A B * +∞ * k A B * k A B = +∞
38 37 biimpd * k A B * +∞ * k A B * k A B = +∞
39 14 36 38 sylc φ * k A B = +∞