Theorem esumpinfval

Description: The value of the extended sum of nonnegative terms, with at least one infinite term. (Contributed by Thierry Arnoux, 19-Jun-2017)

	Ref	Expression
Hypotheses	esumpinfval.0	$$⊢Ⅎk\phi$$
	esumpinfval.1	$$⊢\phi \to A\in V$$
	esumpinfval.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	esumpinfval.3	$$⊢\phi \to \exists k\in AB=\mathrm{+\infty }$$
Assertion	esumpinfval	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		esumpinfval.0	$$⊢Ⅎk\phi$$
2		esumpinfval.1	$$⊢\phi \to A\in V$$
3		esumpinfval.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		esumpinfval.3	$$⊢\phi \to \exists k\in AB=\mathrm{+\infty }$$
5		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
6	3	ex	$$⊢\phi \to \left(k\in A\to B\in \left[0,\mathrm{+\infty }\right]\right)$$
7	1 6	ralrimi	$$⊢\phi \to \forall k\in AB\in \left[0,\mathrm{+\infty }\right]$$
8		nfcv	$$⊢\underset{\_}{Ⅎ}kA$$
9	8	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]$$
10	2 7 9	syl2anc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in \left[0,\mathrm{+\infty }\right]$$
11	5 10	sselid	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in {ℝ}^{*}$$
12		nfrab1	$$⊢\underset{\_}{Ⅎ}k\left\{k\in A|B=\mathrm{+\infty }\right\}$$
13		ssrab2	$$⊢\left\{k\in A|B=\mathrm{+\infty }\right\}\subseteq A$$
14	13	a1i	$$⊢\phi \to \left\{k\in A|B=\mathrm{+\infty }\right\}\subseteq A$$
15		0xr	$$⊢0\in {ℝ}^{*}$$
16		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
17		0lepnf	$$⊢0\le \mathrm{+\infty }$$
18		ubicc2	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge 0\le \mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$
19	15 16 17 18	mp3an	$$⊢\mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$
20	19	a1i	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge B=\mathrm{+\infty }\right)\to \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]$$
21		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
22	21	a1i	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge \neg B=\mathrm{+\infty }\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
23	20 22	ifclda	$$⊢\left(\phi \wedge k\in A\right)\to if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\in \left[0,\mathrm{+\infty }\right]$$
24		eldif	$$⊢k\in \left(A\setminus \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\leftrightarrow \left(k\in A\wedge \neg k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\right)$$
25		rabid	$$⊢k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\leftrightarrow \left(k\in A\wedge B=\mathrm{+\infty }\right)$$
26	25	simplbi2	$$⊢k\in A\to \left(B=\mathrm{+\infty }\to k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\right)$$
27	26	con3dimp	$$⊢\left(k\in A\wedge \neg k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\to \neg B=\mathrm{+\infty }$$
28	24 27	sylbi	$$⊢k\in \left(A\setminus \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\to \neg B=\mathrm{+\infty }$$
29	28	adantl	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\right)\to \neg B=\mathrm{+\infty }$$
30	29	iffalsed	$$⊢\left(\phi \wedge k\in \left(A\setminus \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\right)\to if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=0$$
31	1 12 8 14 2 23 30	esumss	$$⊢\phi \to \underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\underset{k\in A}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)$$
32		eqidd	$$⊢\phi \to \left\{k\in A|B=\mathrm{+\infty }\right\}=\left\{k\in A|B=\mathrm{+\infty }\right\}$$
33	25	simprbi	$$⊢k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\to B=\mathrm{+\infty }$$
34	33	iftrued	$$⊢k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\to if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\mathrm{+\infty }$$
35	34	adantl	$$⊢\left(\phi \wedge k\in \left\{k\in A|B=\mathrm{+\infty }\right\}\right)\to if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\mathrm{+\infty }$$
36	1 32 35	esumeq12dvaf	$$⊢\phi \to \underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}\mathrm{+\infty }$$
37	2 14	ssexd	$$⊢\phi \to \left\{k\in A|B=\mathrm{+\infty }\right\}\in \mathrm{V}$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}k\mathrm{+\infty }$$
39	12 38	esumcst	$$⊢\left(\left\{k\in A|B=\mathrm{+\infty }\right\}\in \mathrm{V}\wedge \mathrm{+\infty }\in \left[0,\mathrm{+\infty }\right]\right)\to \underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}\mathrm{+\infty }=\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|{\cdot }_{𝑒}\mathrm{+\infty }$$
40	37 19 39	sylancl	$$⊢\phi \to \underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}\mathrm{+\infty }=\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|{\cdot }_{𝑒}\mathrm{+\infty }$$
41		hashxrcl	$$⊢\left\{k\in A|B=\mathrm{+\infty }\right\}\in \mathrm{V}\to \left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|\in {ℝ}^{*}$$
42	37 41	syl	$$⊢\phi \to \left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|\in {ℝ}^{*}$$
43		rabn0	$$⊢\left\{k\in A|B=\mathrm{+\infty }\right\}\ne \varnothing \leftrightarrow \exists k\in AB=\mathrm{+\infty }$$
44	4 43	sylibr	$$⊢\phi \to \left\{k\in A|B=\mathrm{+\infty }\right\}\ne \varnothing$$
45		hashgt0	$$⊢\left(\left\{k\in A|B=\mathrm{+\infty }\right\}\in \mathrm{V}\wedge \left\{k\in A|B=\mathrm{+\infty }\right\}\ne \varnothing \right)\to 0<\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|$$
46	37 44 45	syl2anc	$$⊢\phi \to 0<\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|$$
47		xmulpnf1	$$⊢\left(\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|\in {ℝ}^{*}\wedge 0<\left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|\right)\to \left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|{\cdot }_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
48	42 46 47	syl2anc	$$⊢\phi \to \left|\left\{k\in A|B=\mathrm{+\infty }\right\}\right|{\cdot }_{𝑒}\mathrm{+\infty }=\mathrm{+\infty }$$
49	36 40 48	3eqtrd	$$⊢\phi \to \underset{k\in \left\{k\in A|B=\mathrm{+\infty }\right\}}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\mathrm{+\infty }$$
50	31 49	eqtr3d	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)=\mathrm{+\infty }$$
51		breq1	$$⊢\mathrm{+\infty }=if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\to \left(\mathrm{+\infty }\le B\leftrightarrow if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\le B\right)$$
52		breq1	$$⊢0=if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\to \left(0\le B\leftrightarrow if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\le B\right)$$
53		pnfge	$$⊢\mathrm{+\infty }\in {ℝ}^{*}\to \mathrm{+\infty }\le \mathrm{+\infty }$$
54	16 53	ax-mp	$$⊢\mathrm{+\infty }\le \mathrm{+\infty }$$
55		breq2	$$⊢B=\mathrm{+\infty }\to \left(\mathrm{+\infty }\le B\leftrightarrow \mathrm{+\infty }\le \mathrm{+\infty }\right)$$
56	54 55	mpbiri	$$⊢B=\mathrm{+\infty }\to \mathrm{+\infty }\le B$$
57	56	adantl	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge B=\mathrm{+\infty }\right)\to \mathrm{+\infty }\le B$$
58	3	adantr	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge \neg B=\mathrm{+\infty }\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
59		iccgelb	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\wedge B\in \left[0,\mathrm{+\infty }\right]\right)\to 0\le B$$
60	15 16 59	mp3an12	$$⊢B\in \left[0,\mathrm{+\infty }\right]\to 0\le B$$
61	58 60	syl	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge \neg B=\mathrm{+\infty }\right)\to 0\le B$$
62	51 52 57 61	ifbothda	$$⊢\left(\phi \wedge k\in A\right)\to if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\le B$$
63	1 8 2 23 3 62	esumlef	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}if\left(B=\mathrm{+\infty },\mathrm{+\infty },0\right)\le \underset{k\in A}{{\sum }^{*}}B$$
64	50 63	eqbrtrrd	$$⊢\phi \to \mathrm{+\infty }\le \underset{k\in A}{{\sum }^{*}}B$$
65		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)$$
66	65	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)$$
67	11 64 66	sylc	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$