Metamath Proof Explorer

Theorem sge0vald

Description: The value of the sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0vald.x ⊢ φ → X ∈ V
sge0vald.f ⊢ φ → F : X ⟶ 0 +∞
Assertion sge0vald ⊢ φ → sum^ ⁡ F = if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ℝ * <

Proof

Step Hyp Ref Expression
1 sge0vald.x ⊢ φ → X ∈ V
2 sge0vald.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0val ⊢ X ∈ V ∧ F : X ⟶ 0 +∞ → sum^ ⁡ F = if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ℝ * <
4 1 2 3 syl2anc ⊢ φ → sum^ ⁡ F = if +∞ ∈ ran ⁡ F +∞ sup ran ⁡ x ∈ 𝒫 X ∩ Fin ⟼ ∑ y ∈ x F ⁡ y ℝ * <