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 ( 𝜑𝑋𝑉 )
sge0less.f ( 𝜑𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
sge0ssre.re ( 𝜑 → ( Σ^𝐹 ) ∈ ℝ )
Assertion sge0ssre ( 𝜑 → ( Σ^ ‘ ( 𝐹𝑌 ) ) ∈ ℝ )

Proof

Step Hyp Ref Expression
1 sge0less.x ( 𝜑𝑋𝑉 )
2 sge0less.f ( 𝜑𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3 sge0ssre.re ( 𝜑 → ( Σ^𝐹 ) ∈ ℝ )
4 inex1g ( 𝑋𝑉 → ( 𝑋𝑌 ) ∈ V )
5 1 4 syl ( 𝜑 → ( 𝑋𝑌 ) ∈ V )
6 fresin ( 𝐹 : 𝑋 ⟶ ( 0 [,] +∞ ) → ( 𝐹𝑌 ) : ( 𝑋𝑌 ) ⟶ ( 0 [,] +∞ ) )
7 2 6 syl ( 𝜑 → ( 𝐹𝑌 ) : ( 𝑋𝑌 ) ⟶ ( 0 [,] +∞ ) )
8 5 7 sge0xrcl ( 𝜑 → ( Σ^ ‘ ( 𝐹𝑌 ) ) ∈ ℝ* )
9 mnfxr -∞ ∈ ℝ*
10 9 a1i ( 𝜑 → -∞ ∈ ℝ* )
11 0xr 0 ∈ ℝ*
12 11 a1i ( 𝜑 → 0 ∈ ℝ* )
13 mnflt0 -∞ < 0
14 13 a1i ( 𝜑 → -∞ < 0 )
15 5 7 sge0ge0 ( 𝜑 → 0 ≤ ( Σ^ ‘ ( 𝐹𝑌 ) ) )
16 10 12 8 14 15 xrltletrd ( 𝜑 → -∞ < ( Σ^ ‘ ( 𝐹𝑌 ) ) )
17 1 2 sge0less ( 𝜑 → ( Σ^ ‘ ( 𝐹𝑌 ) ) ≤ ( Σ^𝐹 ) )
18 xrre ( ( ( ( Σ^ ‘ ( 𝐹𝑌 ) ) ∈ ℝ* ∧ ( Σ^𝐹 ) ∈ ℝ ) ∧ ( -∞ < ( Σ^ ‘ ( 𝐹𝑌 ) ) ∧ ( Σ^ ‘ ( 𝐹𝑌 ) ) ≤ ( Σ^𝐹 ) ) ) → ( Σ^ ‘ ( 𝐹𝑌 ) ) ∈ ℝ )
19 8 3 16 17 18 syl22anc ( 𝜑 → ( Σ^ ‘ ( 𝐹𝑌 ) ) ∈ ℝ )