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	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐹 ↾ 𝑌 ) ) ∈ ℝ )