Theorem sge0ge0mpt

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

	Ref	Expression
Hypotheses	sge0ge0mpt.k	$$⊢Ⅎk\phi$$
	sge0ge0mpt.a	$$⊢\phi \to A\in V$$
	sge0ge0mpt.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	sge0ge0mpt	$$⊢\phi \to 0\le \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0ge0mpt.k	$$⊢Ⅎk\phi$$
2		sge0ge0mpt.a	$$⊢\phi \to A\in V$$
3		sge0ge0mpt.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
5	1 3 4	fmptdf	$$⊢\phi \to \left(k\in A⟼B\right):A⟶\left[0,\mathrm{+\infty }\right]$$
6	2 5	sge0ge0	$$⊢\phi \to 0\le \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)$$