This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumge0cl

Description: The finite sum of nonnegative reals is a nonnegative real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses fsumge0cl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumge0cl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
Assertion fsumge0cl ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) )

Proof

Step Hyp Ref Expression
1 fsumge0cl.a ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumge0cl.b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
3 0xr ⊢ 0 ∈ ℝ*
4 3 a1i ⊢ ( 𝜑 → 0 ∈ ℝ* )
5 pnfxr ⊢ +∞ ∈ ℝ*
6 5 a1i ⊢ ( 𝜑 → +∞ ∈ ℝ* )
7 rge0ssre ⊢ ( 0 [,) +∞ ) ⊆ ℝ
8 7 2 sselid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 𝐵 ∈ ℝ )
9 1 8 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ )
10 9 rexrd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ℝ* )
11 3 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ∈ ℝ* )
12 5 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → +∞ ∈ ℝ* )
13 icogelb ⊢ ( ( 0 ∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 𝐵 ∈ ( 0 [,) +∞ ) ) → 0 ≤ 𝐵 )
14 11 12 2 13 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐴 ) → 0 ≤ 𝐵 )
15 1 8 14 fsumge0 ⊢ ( 𝜑 → 0 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )
16 9 ltpnfd ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 < +∞ )
17 4 6 10 15 16 elicod ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐴 𝐵 ∈ ( 0 [,) +∞ ) )