Theorem sge0xrcl

Description: The arbitrary sum of nonnegative extended reals is an extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		sge0xrcl.x	$$⊢\phi \to X\in V$$
2		sge0xrcl.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
4	1 2	sge0cl	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right]$$
5	3 4	sseldi	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in {ℝ}^{*}$$