Metamath Proof Explorer

Theorem sge0ssre

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 sge0less.x ⊢ φ → X ∈ V
sge0less.f ⊢ φ → F : X ⟶ 0 +∞
sge0ssre.re ⊢ φ → sum^ ⁡ F ∈ ℝ
Assertion sge0ssre ⊢ φ → sum^ ⁡ F ↾ Y ∈ ℝ

Proof

Step Hyp Ref Expression
1 sge0less.x ⊢ φ → X ∈ V
2 sge0less.f ⊢ φ → F : X ⟶ 0 +∞
3 sge0ssre.re ⊢ φ → sum^ ⁡ F ∈ ℝ
4 inex1g ⊢ X ∈ V → X ∩ Y ∈ V
5 1 4 syl ⊢ φ → X ∩ Y ∈ V
6 fresin ⊢ F : X ⟶ 0 +∞ → F ↾ Y : X ∩ Y ⟶ 0 +∞
7 2 6 syl ⊢ φ → F ↾ Y : X ∩ Y ⟶ 0 +∞
8 5 7 sge0xrcl ⊢ φ → sum^ ⁡ F ↾ Y ∈ ℝ *
9 mnfxr ⊢ −∞ ∈ ℝ *
10 9 a1i ⊢ φ → −∞ ∈ ℝ *
11 0xr ⊢ 0 ∈ ℝ *
12 11 a1i ⊢ φ → 0 ∈ ℝ *
13 mnflt0 ⊢ −∞ < 0
14 13 a1i ⊢ φ → −∞ < 0
15 5 7 sge0ge0 ⊢ φ → 0 ≤ sum^ ⁡ F ↾ Y
16 10 12 8 14 15 xrltletrd ⊢ φ → −∞ < sum^ ⁡ F ↾ Y
17 1 2 sge0less ⊢ φ → sum^ ⁡ F ↾ Y ≤ sum^ ⁡ F
18 xrre ⊢ sum^ ⁡ F ↾ Y ∈ ℝ * ∧ sum^ ⁡ F ∈ ℝ ∧ −∞ < sum^ ⁡ F ↾ Y ∧ sum^ ⁡ F ↾ Y ≤ sum^ ⁡ F → sum^ ⁡ F ↾ Y ∈ ℝ
19 8 3 16 17 18 syl22anc ⊢ φ → sum^ ⁡ F ↾ Y ∈ ℝ