Theorem sge0pnfval

Description: If a term in the sum of nonnegative extended reals is +oo , then the value of the sum is +oo . (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0pnfval.x	|- ( ph -> X e. V )
	sge0pnfval.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
	sge0pnfval.pnf	|- ( ph -> +oo e. ran F )
Assertion	sge0pnfval	|- ( ph -> ( sum^ ` F ) = +oo )

Proof

Step	Hyp	Ref	Expression
1		sge0pnfval.x	|- ( ph -> X e. V )
2		sge0pnfval.f	|- ( ph -> F : X --> ( 0 [,] +oo ) )
3		sge0pnfval.pnf	|- ( ph -> +oo e. ran F )
4	1 2	sge0vald	|- ( ph -> ( sum^ ` F ) = if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) )
5	3	iftrued	|- ( ph -> if ( +oo e. ran F , +oo , sup ( ran ( x e. ( ~P X i^i Fin ) |-> sum_ y e. x ( F ` y ) ) , RR* , < ) ) = +oo )
6	4 5	eqtrd	|- ( ph -> ( sum^ ` F ) = +oo )