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

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 ≤ Σ 𝑘 ∈ 𝐴 𝐵 )