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\phi$$
	esumpinfsum.a	$$⊢\underset{\_}{Ⅎ}kA$$
	esumpinfsum.1	$$⊢\phi \to A\in V$$
	esumpinfsum.2	$$⊢\phi \to \neg A\in \mathrm{Fin}$$
	esumpinfsum.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	esumpinfsum.4	$$⊢\left(\phi \wedge k\in A\right)\to M\le B$$
	esumpinfsum.5	$$⊢\phi \to M\in {ℝ}^{*}$$
	esumpinfsum.6	$$⊢\phi \to 0<M$$
Assertion	esumpinfsum	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		esumpinfsum.p	$$⊢Ⅎk\phi$$
2		esumpinfsum.a	$$⊢\underset{\_}{Ⅎ}kA$$
3		esumpinfsum.1	$$⊢\phi \to A\in V$$
4		esumpinfsum.2	$$⊢\phi \to \neg A\in \mathrm{Fin}$$
5		esumpinfsum.3	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
6		esumpinfsum.4	$$⊢\left(\phi \wedge k\in A\right)\to M\le B$$
7		esumpinfsum.5	$$⊢\phi \to M\in {ℝ}^{*}$$
8		esumpinfsum.6	$$⊢\phi \to 0<M$$
9		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
10	5	ex	$$⊢\phi \to \left(k\in A\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
11	1 10	ralrimi	$$⊢\phi \to \forall k\in AB\in \left[0,\mathrm{+\infty }\right]$$
12	2	esumcl	$$⊢\left(A\in V\wedge \forall k\in AB\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
13	3 11 12	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
14	9 13	sseldi	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}$$
15		0xr	$$⊢0\in {ℝ}^{*}$$
16		xrltle	$$⊢\left(0\in {ℝ}^{*}\wedge M\in {ℝ}^{*}\right)\to \left(0<M\to 0\le M\right)$$
17	15 7 16	sylancr	$$⊢\phi \to \left(0<M\to 0\le M\right)$$
18	8 17	mpd	$$⊢\phi \to 0\le M$$
19		pnfge	$$⊢M\in {ℝ}^{*}\to M\le \mathrm{+\infty }$$
20	7 19	syl	$$⊢\phi \to M\le \mathrm{+\infty }$$
21		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
22		elicc1	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(M\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(M\in {ℝ}^{*}\wedge 0\le M\wedge M\le \mathrm{+\infty }\right)\right)$$
23	15 21 22	mp2an	$$⊢M\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(M\in {ℝ}^{*}\wedge 0\le M\wedge M\le \mathrm{+\infty }\right)$$
24	7 18 20 23	syl3anbrc	$$⊢\phi \to M\in \left[0,\mathrm{+\infty }\right]$$
25		nfcv	$$⊢\underset{\_}{Ⅎ}kM$$
26	2 25	esumcst	$$⊢\left(A\in V\wedge M\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in A}{{\sum }^{*}}M=\left|A\right|{\cdot }_{𝑒}M$$
27	3 24 26	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}M=\left|A\right|{\cdot }_{𝑒}M$$
28		hashinf	$$⊢\left(A\in V\wedge \neg A\in \mathrm{Fin}\right)\to \left|A\right|=\mathrm{+\infty }$$
29	3 4 28	syl2anc	$$⊢\phi \to \left|A\right|=\mathrm{+\infty }$$
30	29	oveq1d	$$⊢\phi \to \left|A\right|{\cdot }_{𝑒}M=\mathrm{+\infty }{\cdot }_{𝑒}M$$
31		xmulpnf2	$$⊢\left(M\in {ℝ}^{*}\wedge 0<M\right)\to \mathrm{+\infty }{\cdot }_{𝑒}M=\mathrm{+\infty }$$
32	7 8 31	syl2anc	$$⊢\phi \to \mathrm{+\infty }{\cdot }_{𝑒}M=\mathrm{+\infty }$$
33	27 30 32	3eqtrd	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}M=\mathrm{+\infty }$$
34	24	adantr	$$⊢\left(\phi \wedge k\in A\right)\to M\in \left[0,\mathrm{+\infty }\right]$$
35	1 2 3 34 5 6	esumlef	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}M\le \underset{k\in A}{{\sum }^{*}}B$$
36	33 35	eqbrtrrd	$$⊢\phi \to \mathrm{+\infty }\le \underset{k\in A}{{\sum }^{*}}B$$
37		xgepnf	$$⊢\underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le \underset{k\in A}{{\sum }^{*}}B\leftrightarrow \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }\right)$$
38	37	biimpd	$$⊢\underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}\to \left(\mathrm{+\infty }\le \underset{k\in A}{{\sum }^{*}}B\to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }\right)$$
39	14 36 38	sylc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$