Theorem sge0isummpt2

Description: If a series of nonnegative reals is convergent, then it agrees with the generalized sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0isummpt2.kph	$$⊢Ⅎk\phi$$
	sge0isummpt2.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in \left[0,\mathrm{+\infty }\right)$$
	sge0isummpt2.m	$$⊢\phi \to M\in \mathbb{Z}$$
	sge0isummpt2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	sge0isummpt2.b	$$⊢\phi \to seqM\left(+,\left(k\in Z⟼A\right)\right)⇝B$$
Assertion	sge0isummpt2	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in Z⟼A\right)\right)=\sum _{k\in Z}A$$

Proof

Step	Hyp	Ref	Expression
1		sge0isummpt2.kph	$$⊢Ⅎk\phi$$
2		sge0isummpt2.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in \left[0,\mathrm{+\infty }\right)$$
3		sge0isummpt2.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		sge0isummpt2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		sge0isummpt2.b	$$⊢\phi \to seqM\left(+,\left(k\in Z⟼A\right)\right)⇝B$$
6		simpr	$$⊢\left(\phi \wedge j\in Z\right)\to j\in Z$$
7		nfv	$$⊢Ⅎkj\in Z$$
8	1 7	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
10	9	nfcsb1	$$⊢\underset{\_}{Ⅎ}k⦋j/k⦌A$$
11	10	nfel1	$$⊢Ⅎk⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)$$
12	8 11	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to ⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)\right)$$
13		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
14	13	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
15		csbeq1a	$$⊢k=j\to A=⦋j/k⦌A$$
16	15	eleq1d	$$⊢k=j\to \left(A\in \left[0,\mathrm{+\infty }\right)\leftrightarrow ⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)\right)$$
17	14 16	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to A\in \left[0,\mathrm{+\infty }\right)\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to ⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)\right)\right)$$
18	12 17 2	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to ⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)$$
19		nfcv	$$⊢\underset{\_}{Ⅎ}iA$$
20		nfcsb1v	$$⊢\underset{\_}{Ⅎ}k⦋i/k⦌A$$
21		csbeq1a	$$⊢k=i\to A=⦋i/k⦌A$$
22	19 20 21	cbvmpt	$$⊢\left(k\in Z⟼A\right)=\left(i\in Z⟼⦋i/k⦌A\right)$$
23	22	eqcomi	$$⊢\left(i\in Z⟼⦋i/k⦌A\right)=\left(k\in Z⟼A\right)$$
24	9 10 15 23	fvmptf	$$⊢\left(j\in Z\wedge ⦋j/k⦌A\in \left[0,\mathrm{+\infty }\right)\right)\to \left(i\in Z⟼⦋i/k⦌A\right)\left(j\right)=⦋j/k⦌A$$
25	6 18 24	syl2anc	$$⊢\left(\phi \wedge j\in Z\right)\to \left(i\in Z⟼⦋i/k⦌A\right)\left(j\right)=⦋j/k⦌A$$
26		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
27		ax-resscn	$$⊢ℝ\subseteq ℂ$$
28	26 27	sstri	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℂ$$
29	28 18	sseldi	$$⊢\left(\phi \wedge j\in Z\right)\to ⦋j/k⦌A\in ℂ$$
30	22	a1i	$$⊢\phi \to \left(k\in Z⟼A\right)=\left(i\in Z⟼⦋i/k⦌A\right)$$
31	30	seqeq3d	$$⊢\phi \to seqM\left(+,\left(k\in Z⟼A\right)\right)=seqM\left(+,\left(i\in Z⟼⦋i/k⦌A\right)\right)$$
32	31	breq1d	$$⊢\phi \to \left(seqM\left(+,\left(k\in Z⟼A\right)\right)⇝B\leftrightarrow seqM\left(+,\left(i\in Z⟼⦋i/k⦌A\right)\right)⇝B\right)$$
33	5 32	mpbid	$$⊢\phi \to seqM\left(+,\left(i\in Z⟼⦋i/k⦌A\right)\right)⇝B$$
34	4 3 25 29 33	isumclim	$$⊢\phi \to \sum _{j\in Z}⦋j/k⦌A=B$$
35		nfcv	$$⊢\underset{\_}{Ⅎ}jZ$$
36		nfcv	$$⊢\underset{\_}{Ⅎ}kZ$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}jA$$
38	15 35 36 37 10	cbvsum	$$⊢\sum _{k\in Z}A=\sum _{j\in Z}⦋j/k⦌A$$
39	38	a1i	$$⊢\phi \to \sum _{k\in Z}A=\sum _{j\in Z}⦋j/k⦌A$$
40	1 2 3 4 5	sge0isummpt	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in Z⟼A\right)\right)=B$$
41	34 39 40	3eqtr4rd	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in Z⟼A\right)\right)=\sum _{k\in Z}A$$