Theorem sge0isummpt

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	sge0isummpt.kph	$$⊢Ⅎk\phi$$
	sge0isummpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in \left[0,\mathrm{+\infty }\right)$$
	sge0isummpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	sge0isummpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	sge0isummpt.b	$$⊢\phi \to seqM\left(+,\left(k\in Z⟼A\right)\right)⇝B$$
Assertion	sge0isummpt	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in Z⟼A\right)\right)=B$$

Proof

Step	Hyp	Ref	Expression
1		sge0isummpt.kph	$$⊢Ⅎk\phi$$
2		sge0isummpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in \left[0,\mathrm{+\infty }\right)$$
3		sge0isummpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		sge0isummpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
5		sge0isummpt.b	$$⊢\phi \to seqM\left(+,\left(k\in Z⟼A\right)\right)⇝B$$
6		eqid	$$⊢\left(k\in Z⟼A\right)=\left(k\in Z⟼A\right)$$
7	1 2 6	fmptdf	$$⊢\phi \to \left(k\in Z⟼A\right):Z⟶\left[0,\mathrm{+\infty }\right)$$
8		eqid	$$⊢seqM\left(+,\left(k\in Z⟼A\right)\right)=seqM\left(+,\left(k\in Z⟼A\right)\right)$$
9	3 4 7 8 5	sge0isum	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in Z⟼A\right)\right)=B$$