Theorem esumcvgre

Description: All terms of a converging extended sum shall be finite. (Contributed by Thierry Arnoux, 23-Sep-2019)

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

Proof

Step	Hyp	Ref	Expression
1		esumcvgre.0	$$⊢Ⅎk\phi$$
2		esumcvgre.1	$$⊢\phi \to A\in V$$
3		esumcvgre.2	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		esumcvgre.3	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B\in ℝ$$
5		nfre1	$$⊢Ⅎk\exists k\in AB=\mathrm{+\infty }$$
6	1 5	nfan	$$⊢Ⅎk\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)$$
7	2	adantr	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to A\in V$$
8	3	adantlr	$$⊢\left(\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
9		simpr	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \exists k\in AB=\mathrm{+\infty }$$
10	6 7 8 9	esumpinfval	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$
11		ltpnf	$$⊢\underset{k\in A}{{\sum }^{*}}B\in ℝ\to \underset{k\in A}{{\sum }^{*}}B<\mathrm{+\infty }$$
12	4 11	syl	$$⊢\phi \to \underset{k\in A}{{\sum }^{*}}B<\mathrm{+\infty }$$
13	4 12	gtned	$$⊢\phi \to \mathrm{+\infty }\ne \underset{k\in A}{{\sum }^{*}}B$$
14	13	adantr	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \mathrm{+\infty }\ne \underset{k\in A}{{\sum }^{*}}B$$
15		necom	$$⊢\mathrm{+\infty }\ne \underset{k\in A}{{\sum }^{*}}B\leftrightarrow \underset{k\in A}{{\sum }^{*}}B\ne \mathrm{+\infty }$$
16	15	imbi2i	$$⊢\left(\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \mathrm{+\infty }\ne \underset{k\in A}{{\sum }^{*}}B\right)\leftrightarrow \left(\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \underset{k\in A}{{\sum }^{*}}B\ne \mathrm{+\infty }\right)$$
17	14 16	mpbi	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \underset{k\in A}{{\sum }^{*}}B\ne \mathrm{+\infty }$$
18	17	neneqd	$$⊢\left(\phi \wedge \exists k\in AB=\mathrm{+\infty }\right)\to \neg \underset{k\in A}{{\sum }^{*}}B=\mathrm{+\infty }$$
19	10 18	pm2.65da	$$⊢\phi \to \neg \exists k\in AB=\mathrm{+\infty }$$
20		ralnex	$$⊢\forall k\in A\neg B=\mathrm{+\infty }\leftrightarrow \neg \exists k\in AB=\mathrm{+\infty }$$
21	19 20	sylibr	$$⊢\phi \to \forall k\in A\neg B=\mathrm{+\infty }$$
22	21	r19.21bi	$$⊢\left(\phi \wedge k\in A\right)\to \neg B=\mathrm{+\infty }$$
23		eliccxr	$$⊢B\in \left[0,\mathrm{+\infty }\right]\to B\in {ℝ}^{*}$$
24		xrge0neqmnf	$$⊢B\in \left[0,\mathrm{+\infty }\right]\to B\ne \mathrm{-\infty }$$
25		xrnemnf	$$⊢\left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)\leftrightarrow \left(B\in ℝ\vee B=\mathrm{+\infty }\right)$$
26	25	biimpi	$$⊢\left(B\in {ℝ}^{*}\wedge B\ne \mathrm{-\infty }\right)\to \left(B\in ℝ\vee B=\mathrm{+\infty }\right)$$
27	23 24 26	syl2anc	$$⊢B\in \left[0,\mathrm{+\infty }\right]\to \left(B\in ℝ\vee B=\mathrm{+\infty }\right)$$
28	3 27	syl	$$⊢\left(\phi \wedge k\in A\right)\to \left(B\in ℝ\vee B=\mathrm{+\infty }\right)$$
29	28	orcomd	$$⊢\left(\phi \wedge k\in A\right)\to \left(B=\mathrm{+\infty }\vee B\in ℝ\right)$$
30	29	orcanai	$$⊢\left(\left(\phi \wedge k\in A\right)\wedge \neg B=\mathrm{+\infty }\right)\to B\in ℝ$$
31	22 30	mpdan	$$⊢\left(\phi \wedge k\in A\right)\to B\in ℝ$$