Theorem sge0reval

Description: Value of the sum of nonnegative extended reals, when all terms in the sum are reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0reval.x	$$⊢\phi \to X\in V$$
	sge0reval.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right)$$
Assertion	sge0reval	$$⊢\phi \to \mathrm{sum^}\left(F\right)=sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0reval.x	$$⊢\phi \to X\in V$$
2		sge0reval.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right)$$
3	2	fge0icoicc	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
4	1 3	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	2	fge0npnf	$$⊢\phi \to \neg \mathrm{+\infty }\in \mathrm{ran}F$$
6	5	iffalsed	$$⊢\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)=sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)$$
7	4 6	eqtrd	$$⊢\phi \to \mathrm{sum^}\left(F\right)=sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)$$