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	⊢ Ⅎ 𝑘 𝜑
	sge0pnfmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0pnfmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
	sge0pnfmpt.p	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
Assertion	sge0pnfmpt	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		sge0pnfmpt.k	⊢ Ⅎ 𝑘 𝜑
2		sge0pnfmpt.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		sge0pnfmpt.b	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,] +∞ ) )
4		sge0pnfmpt.p	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ )
5		eqid	⊢ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑘 ∈ 𝐴 ↦ 𝐵 )
6	1 3 5	fmptdf	⊢ ( 𝜑 → ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ( 0 [,] +∞ ) )
7		eqcom	⊢ ( 𝐵 = +∞ ↔ +∞ = 𝐵 )
8	7	rexbii	⊢ ( ∃ 𝑘 ∈ 𝐴 𝐵 = +∞ ↔ ∃ 𝑘 ∈ 𝐴 +∞ = 𝐵 )
9	4 8	sylib	⊢ ( 𝜑 → ∃ 𝑘 ∈ 𝐴 +∞ = 𝐵 )
10		pnfex	⊢ +∞ ∈ V
11	10	a1i	⊢ ( 𝜑 → +∞ ∈ V )
12	5 9 11	elrnmptd	⊢ ( 𝜑 → +∞ ∈ ran ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) )
13	2 6 12	sge0pnfval	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑘 ∈ 𝐴 ↦ 𝐵 ) ) = +∞ )