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	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	sge0pnfval.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	sge0pnfval.pnf	⊢ ( 𝜑 → +∞ ∈ ran 𝐹 )
Assertion	sge0pnfval	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = +∞ )

Proof

Step	Hyp	Ref	Expression
1		sge0pnfval.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		sge0pnfval.f	⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		sge0pnfval.pnf	⊢ ( 𝜑 → +∞ ∈ ran 𝐹 )
4	1 2	sge0vald	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) )
5	3	iftrued	⊢ ( 𝜑 → if ( +∞ ∈ ran 𝐹 , +∞ , sup ( ran ( 𝑥 ∈ ( 𝒫 𝑋 ∩ Fin ) ↦ Σ 𝑦 ∈ 𝑥 ( 𝐹 ‘ 𝑦 ) ) , ℝ* , < ) ) = +∞ )
6	4 5	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) = +∞ )