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 ⊢ φ → A ∈ Fin
fsumge0cl.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
Assertion fsumge0cl ⊢ φ → ∑ k ∈ A B ∈ 0 +∞

Proof

Step Hyp Ref Expression
1 fsumge0cl.a ⊢ φ → A ∈ Fin
2 fsumge0cl.b ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
3 0xr ⊢ 0 ∈ ℝ *
4 3 a1i ⊢ φ → 0 ∈ ℝ *
5 pnfxr ⊢ +∞ ∈ ℝ *
6 5 a1i ⊢ φ → +∞ ∈ ℝ *
7 rge0ssre ⊢ 0 +∞ ⊆ ℝ
8 7 2 sselid ⊢ φ ∧ k ∈ A → B ∈ ℝ
9 1 8 fsumrecl ⊢ φ → ∑ k ∈ A B ∈ ℝ
10 9 rexrd ⊢ φ → ∑ k ∈ A B ∈ ℝ *
11 3 a1i ⊢ φ ∧ k ∈ A → 0 ∈ ℝ *
12 5 a1i ⊢ φ ∧ k ∈ A → +∞ ∈ ℝ *
13 icogelb ⊢ 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ B ∈ 0 +∞ → 0 ≤ B
14 11 12 2 13 syl3anc ⊢ φ ∧ k ∈ A → 0 ≤ B
15 1 8 14 fsumge0 ⊢ φ → 0 ≤ ∑ k ∈ A B
16 9 ltpnfd ⊢ φ → ∑ k ∈ A B < +∞
17 4 6 10 15 16 elicod ⊢ φ → ∑ k ∈ A B ∈ 0 +∞