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

Proof

Step	Hyp	Ref	Expression
1		sge0rern.x	|- ( ph -> X e. V )
2		sge0rern.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
3		sge0rern.re	|- ( ph -> ( sum^ ` F ) e. RR )
4	1	adantr	|- ( ( ph /\ +oo e. ran F ) -> X e. V )
5	2	adantr	|- ( ( ph /\ +oo e. ran F ) -> F : X --> ( 0 [,] +oo ) )
6		simpr	|- ( ( ph /\ +oo e. ran F ) -> +oo e. ran F )
7	4 5 6	sge0pnfval	|- ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) = +oo )
8	3	adantr	|- ( ( ph /\ +oo e. ran F ) -> ( sum^ ` F ) e. RR )
9	4 5	sge0repnf	|- ( ( ph /\ +oo e. ran F ) -> ( ( sum^ ` F ) e. RR <-> -. ( sum^ ` F ) = +oo ) )
10	8 9	mpbid	|- ( ( ph /\ +oo e. ran F ) -> -. ( sum^ ` F ) = +oo )
11	7 10	pm2.65da	|- ( ph -> -. +oo e. ran F )