Metamath Proof Explorer


Theorem sge0nemnf

Description: The generalized sum of nonnegative extended reals is not minus infinity. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses sge0nemnf.1 ( 𝜑𝐴𝑉 )
sge0nemnf.2 ( 𝜑𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
Assertion sge0nemnf ( 𝜑 → ( Σ^𝐹 ) ≠ -∞ )

Proof

Step Hyp Ref Expression
1 sge0nemnf.1 ( 𝜑𝐴𝑉 )
2 sge0nemnf.2 ( 𝜑𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
3 1 2 sge0cl ( 𝜑 → ( Σ^𝐹 ) ∈ ( 0 [,] +∞ ) )
4 xrge0neqmnf ( ( Σ^𝐹 ) ∈ ( 0 [,] +∞ ) → ( Σ^𝐹 ) ≠ -∞ )
5 3 4 syl ( 𝜑 → ( Σ^𝐹 ) ≠ -∞ )