Metamath Proof Explorer

Theorem fsumge0

Description: If all of the terms of a finite sum are nonnegative, so is the sum. (Contributed by NM, 26-Dec-2005) (Revised by Mario Carneiro, 24-Apr-2014)

Ref Expression
Hypotheses fsumge0.1 ⊢ φ → A ∈ Fin
fsumge0.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
fsumge0.3 ⊢ φ ∧ k ∈ A → 0 ≤ B
Assertion fsumge0 ⊢ φ → 0 ≤ ∑ k ∈ A B

Proof

Step Hyp Ref Expression
1 fsumge0.1 ⊢ φ → A ∈ Fin
2 fsumge0.2 ⊢ φ ∧ k ∈ A → B ∈ ℝ
3 fsumge0.3 ⊢ φ ∧ k ∈ A → 0 ≤ B
4 rge0ssre ⊢ 0 +∞ ⊆ ℝ
5 ax-resscn ⊢ ℝ ⊆ ℂ
6 4 5 sstri ⊢ 0 +∞ ⊆ ℂ
7 6 a1i ⊢ φ → 0 +∞ ⊆ ℂ
8 ge0addcl ⊢ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
9 8 adantl ⊢ φ ∧ x ∈ 0 +∞ ∧ y ∈ 0 +∞ → x + y ∈ 0 +∞
10 elrege0 ⊢ B ∈ 0 +∞ ↔ B ∈ ℝ ∧ 0 ≤ B
11 2 3 10 sylanbrc ⊢ φ ∧ k ∈ A → B ∈ 0 +∞
12 0e0icopnf ⊢ 0 ∈ 0 +∞
13 12 a1i ⊢ φ → 0 ∈ 0 +∞
14 7 9 1 11 13 fsumcllem ⊢ φ → ∑ k ∈ A B ∈ 0 +∞
15 elrege0 ⊢ ∑ k ∈ A B ∈ 0 +∞ ↔ ∑ k ∈ A B ∈ ℝ ∧ 0 ≤ ∑ k ∈ A B
16 15 simprbi ⊢ ∑ k ∈ A B ∈ 0 +∞ → 0 ≤ ∑ k ∈ A B
17 14 16 syl ⊢ φ → 0 ≤ ∑ k ∈ A B