Theorem sge0rern

Description: If the sum of nonnegative extended reals is not +oo then no terms is +oo . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step	Hyp	Ref	Expression
1		sge0rern.x	$$⊢\phi \to X\in V$$
2		sge0rern.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		sge0rern.re	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in ℝ$$
4	1	adantr	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to X\in V$$
5	2	adantr	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to F:X⟶\left[0,\mathrm{+\infty }\right]$$
6		simpr	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to \mathrm{+\infty }\in \mathrm{ran}F$$
7	4 5 6	sge0pnfval	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$
8	3	adantr	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to \mathrm{sum^}\left(F\right)\in ℝ$$
9	4 5	sge0repnf	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to \left(\mathrm{sum^}\left(F\right)\in ℝ\leftrightarrow \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)$$
10	8 9	mpbid	$$⊢\left(\phi \wedge \mathrm{+\infty }\in \mathrm{ran}F\right)\to \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$
11	7 10	pm2.65da	$$⊢\phi \to \neg \mathrm{+\infty }\in \mathrm{ran}F$$