Theorem sge0pnfmpt

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, 3-Mar-2021)

	Ref	Expression
Hypotheses	sge0pnfmpt.k	|- F/ k ph
	sge0pnfmpt.a	|- ( ph -> A e. V )
	sge0pnfmpt.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
	sge0pnfmpt.p	|- ( ph -> E. k e. A B = +oo )
Assertion	sge0pnfmpt	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = +oo )

Proof

Step	Hyp	Ref	Expression
1		sge0pnfmpt.k	|- F/ k ph
2		sge0pnfmpt.a	|- ( ph -> A e. V )
3		sge0pnfmpt.b	|- ( ( ph /\ k e. A ) -> B e. ( 0 [,] +oo ) )
4		sge0pnfmpt.p	|- ( ph -> E. k e. A B = +oo )
5		eqid	|- ( k e. A |-> B ) = ( k e. A |-> B )
6	1 3 5	fmptdf	|- ( ph -> ( k e. A |-> B ) : A --> ( 0 [,] +oo ) )
7		eqcom	|- ( B = +oo <-> +oo = B )
8	7	rexbii	|- ( E. k e. A B = +oo <-> E. k e. A +oo = B )
9	4 8	sylib	|- ( ph -> E. k e. A +oo = B )
10		pnfex	|- +oo e. _V
11	10	a1i	|- ( ph -> +oo e. _V )
12	5 9 11	elrnmptd	|- ( ph -> +oo e. ran ( k e. A |-> B ) )
13	2 6 12	sge0pnfval	|- ( ph -> ( sum^ ` ( k e. A |-> B ) ) = +oo )