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	|- ( ph -> X e. V )
	sge0repnf.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
Assertion	sge0repnf	|- ( ph -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )

Proof

Step	Hyp	Ref	Expression
1		sge0repnf.x	|- ( ph -> X e. V )
2		sge0repnf.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
3		renepnf	|- ( ( sum^ ` F ) e. RR -> ( sum^ ` F ) =/= +oo )
4	3	neneqd	|- ( ( sum^ ` F ) e. RR -> -. ( sum^ ` F ) = +oo )
5	4	a1i	|- ( ph -> ( ( sum^ ` F ) e. RR -> -. ( sum^ ` F ) = +oo ) )
6		rge0ssre	|- ( 0 [,) +oo ) C_ RR
7		0xr	|- 0 e. RR*
8	7	a1i	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> 0 e. RR* )
9		pnfxr	|- +oo e. RR*
10	9	a1i	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> +oo e. RR* )
11	1 2	sge0xrcl	|- ( ph -> ( sum^ ` F ) e. RR* )
12	11	adantr	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. RR* )
13	1 2	sge0ge0	|- ( ph -> 0 <_ ( sum^ ` F ) )
14	13	adantr	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> 0 <_ ( sum^ ` F ) )
15		simpr	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> -. ( sum^ ` F ) = +oo )
16		nltpnft	|- ( ( sum^ ` F ) e. RR* -> ( ( sum^ ` F ) = +oo <-> -. ( sum^ ` F ) < +oo ) )
17	11 16	syl	|- ( ph -> ( ( sum^ ` F ) = +oo <-> -. ( sum^ ` F ) < +oo ) )
18	17	adantr	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( ( sum^ ` F ) = +oo <-> -. ( sum^ ` F ) < +oo ) )
19	15 18	mtbid	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> -. -. ( sum^ ` F ) < +oo )
20	19	notnotrd	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) < +oo )
21	8 10 12 14 20	elicod	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. ( 0 [,) +oo ) )
22	6 21	sseldi	|- ( ( ph /\ -. ( sum^ ` F ) = +oo ) -> ( sum^ ` F ) e. RR )
23	22	ex	|- ( ph -> ( -. ( sum^ ` F ) = +oo -> ( sum^ ` F ) e. RR ) )
24	5 23	impbid	|- ( ph -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )