Theorem sge0repnf

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

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

Proof

Step	Hyp	Ref	Expression
1		sge0repnf.x	$$⊢\phi \to X\in V$$
2		sge0repnf.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		renepnf	$$⊢\mathrm{sum^}\left(F\right)\in ℝ\to \mathrm{sum^}\left(F\right)\ne \mathrm{+\infty }$$
4	3	neneqd	$$⊢\mathrm{sum^}\left(F\right)\in ℝ\to \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$
5	4	a1i	$$⊢\phi \to \left(\mathrm{sum^}\left(F\right)\in ℝ\to \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)$$
6		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
7		0xr	$$⊢0\in {ℝ}^{*}$$
8	7	a1i	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to 0\in {ℝ}^{*}$$
9		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
10	9	a1i	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \mathrm{+\infty }\in {ℝ}^{*}$$
11	1 2	sge0xrcl	$$⊢\phi \to \mathrm{sum^}\left(F\right)\in {ℝ}^{*}$$
12	11	adantr	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \mathrm{sum^}\left(F\right)\in {ℝ}^{*}$$
13	1 2	sge0ge0	$$⊢\phi \to 0\le \mathrm{sum^}\left(F\right)$$
14	13	adantr	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to 0\le \mathrm{sum^}\left(F\right)$$
15		simpr	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }$$
16		nltpnft	$$⊢\mathrm{sum^}\left(F\right)\in {ℝ}^{*}\to \left(\mathrm{sum^}\left(F\right)=\mathrm{+\infty }\leftrightarrow \neg \mathrm{sum^}\left(F\right)<\mathrm{+\infty }\right)$$
17	11 16	syl	$$⊢\phi \to \left(\mathrm{sum^}\left(F\right)=\mathrm{+\infty }\leftrightarrow \neg \mathrm{sum^}\left(F\right)<\mathrm{+\infty }\right)$$
18	17	adantr	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \left(\mathrm{sum^}\left(F\right)=\mathrm{+\infty }\leftrightarrow \neg \mathrm{sum^}\left(F\right)<\mathrm{+\infty }\right)$$
19	15 18	mtbid	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \neg \neg \mathrm{sum^}\left(F\right)<\mathrm{+\infty }$$
20	19	notnotrd	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \mathrm{sum^}\left(F\right)<\mathrm{+\infty }$$
21	8 10 12 14 20	elicod	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \mathrm{sum^}\left(F\right)\in \left[0,\mathrm{+\infty }\right)$$
22	6 21	sseldi	$$⊢\left(\phi \wedge \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)\to \mathrm{sum^}\left(F\right)\in ℝ$$
23	22	ex	$$⊢\phi \to \left(\neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\to \mathrm{sum^}\left(F\right)\in ℝ\right)$$
24	5 23	impbid	$$⊢\phi \to \left(\mathrm{sum^}\left(F\right)\in ℝ\leftrightarrow \neg \mathrm{sum^}\left(F\right)=\mathrm{+\infty }\right)$$