Metamath Proof Explorer

Theorem sge0ssrempt

Description: If a sum of nonnegative extended reals is real, than any subsum is real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses sge0ssrempt.xph ⊢ Ⅎ x φ
sge0ssrempt.a ⊢ φ → A ∈ V
sge0ssrempt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
sge0ssrempt.re ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ∈ ℝ
sge0ssrempt.c ⊢ φ → C ⊆ A
Assertion sge0ssrempt ⊢ φ → sum^ ⁡ x ∈ C ⟼ B ∈ ℝ

Proof

Step Hyp Ref Expression
1 sge0ssrempt.xph ⊢ Ⅎ x φ
2 sge0ssrempt.a ⊢ φ → A ∈ V
3 sge0ssrempt.b ⊢ φ ∧ x ∈ A → B ∈ 0 +∞
4 sge0ssrempt.re ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ∈ ℝ
5 sge0ssrempt.c ⊢ φ → C ⊆ A
6 5 resmptd ⊢ φ → x ∈ A ⟼ B ↾ C = x ∈ C ⟼ B
7 6 fveq2d ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ↾ C = sum^ ⁡ x ∈ C ⟼ B
8 7 eqcomd ⊢ φ → sum^ ⁡ x ∈ C ⟼ B = sum^ ⁡ x ∈ A ⟼ B ↾ C
9 eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
10 1 3 9 fmptdf ⊢ φ → x ∈ A ⟼ B : A ⟶ 0 +∞
11 2 10 4 sge0ssre ⊢ φ → sum^ ⁡ x ∈ A ⟼ B ↾ C ∈ ℝ
12 8 11 eqeltrd ⊢ φ → sum^ ⁡ x ∈ C ⟼ B ∈ ℝ