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 | ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≠ -∞ ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sge0nemnf.1 | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
2 | sge0nemnf.2 | ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) ) | |
3 | 1 2 | sge0cl | ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) ) |
4 | xrge0neqmnf | ⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) → ( Σ^ ‘ 𝐹 ) ≠ -∞ ) | |
5 | 3 4 | syl | ⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≠ -∞ ) |