Theorem sge0pnfval

Description: If a term in the sum of nonnegative extended reals is +oo , then the value of the sum is +oo . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0pnfval.x	$$⊢\phi \to X\in V$$
	sge0pnfval.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
	sge0pnfval.pnf	$$⊢\phi \to \mathrm{+\infty }\in \mathrm{ran}F$$
Assertion	sge0pnfval	$$⊢\phi \to \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		sge0pnfval.x	$$⊢\phi \to X\in V$$
2		sge0pnfval.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		sge0pnfval.pnf	$$⊢\phi \to \mathrm{+\infty }\in \mathrm{ran}F$$
4	1 2	sge0vald	$$⊢\phi \to \mathrm{sum^}\left(F\right)=if\left(\mathrm{+\infty }\in \mathrm{ran}F,\mathrm{+\infty },sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)\right)$$
5	3	iftrued	$$⊢\phi \to if\left(\mathrm{+\infty }\in \mathrm{ran}F,\mathrm{+\infty },sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)\right)=\mathrm{+\infty }$$
6	4 5	eqtrd	$$⊢\phi \to \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$