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