# 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 ( 𝜑𝐴 ∈ Fin )
fsumge0.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℝ )
fsumge0.3 ( ( 𝜑𝑘𝐴 ) → 0 ≤ 𝐵 )
Assertion fsumge0 ( 𝜑 → 0 ≤ Σ 𝑘𝐴 𝐵 )

### Proof

Step Hyp Ref Expression
1 fsumge0.1 ( 𝜑𝐴 ∈ Fin )
2 fsumge0.2 ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ℝ )
3 fsumge0.3 ( ( 𝜑𝑘𝐴 ) → 0 ≤ 𝐵 )
4 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
5 ax-resscn ℝ ⊆ ℂ
6 4 5 sstri ( 0 [,) +∞ ) ⊆ ℂ
7 6 a1i ( 𝜑 → ( 0 [,) +∞ ) ⊆ ℂ )
8 ge0addcl ( ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
9 8 adantl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,) +∞ ) ∧ 𝑦 ∈ ( 0 [,) +∞ ) ) ) → ( 𝑥 + 𝑦 ) ∈ ( 0 [,) +∞ ) )
10 elrege0 ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
11 2 3 10 sylanbrc ( ( 𝜑𝑘𝐴 ) → 𝐵 ∈ ( 0 [,) +∞ ) )
12 0e0icopnf 0 ∈ ( 0 [,) +∞ )
13 12 a1i ( 𝜑 → 0 ∈ ( 0 [,) +∞ ) )
14 7 9 1 11 13 fsumcllem ( 𝜑 → Σ 𝑘𝐴 𝐵 ∈ ( 0 [,) +∞ ) )
15 elrege0 ( Σ 𝑘𝐴 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( Σ 𝑘𝐴 𝐵 ∈ ℝ ∧ 0 ≤ Σ 𝑘𝐴 𝐵 ) )
16 15 simprbi ( Σ 𝑘𝐴 𝐵 ∈ ( 0 [,) +∞ ) → 0 ≤ Σ 𝑘𝐴 𝐵 )
17 14 16 syl ( 𝜑 → 0 ≤ Σ 𝑘𝐴 𝐵 )