Theorem sge0repnfmpt

Description: The of nonnegative extended reals is a real number if and only if it is not +oo . (Contributed by Glauco Siliprandi, 21-Nov-2020)

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

Proof

Step	Hyp	Ref	Expression
1		sge0repnfmpt.k	$$⊢Ⅎk\phi$$
2		sge0repnfmpt.a	$$⊢\phi \to A\in V$$
3		sge0repnfmpt.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	sge0repnf	$$⊢\phi \to \left(\mathrm{sum^}\left(\left(k\in A⟼B\right)\right)\in ℝ\leftrightarrow \neg \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)=\mathrm{+\infty }\right)$$