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	$⊢ φ \to A \in Fin$
		fsumge0.2	$⊢ (φ \land k \in A) \to B \in ℝ$
		fsumge0.3	$⊢ (φ \land k \in A) \to 0 \leq B$
	Assertion	fsumge0	$⊢ φ \to 0 \leq \sum_{k \in A} B$

Proof

Step	Hyp	Ref	Expression
1		fsumge0.1	$⊢ φ \to A \in Fin$
2		fsumge0.2	$⊢ (φ \land k \in A) \to B \in ℝ$
3		fsumge0.3	$⊢ (φ \land k \in A) \to 0 \leq B$
4		rge0ssre	$⊢ [0, +∞) \subseteq ℝ$
5		ax-resscn	$⊢ ℝ \subseteq ℂ$
6	4 5	sstri	$⊢ [0, +∞) \subseteq ℂ$
7	6	a1i	$⊢ φ \to [0, +∞) \subseteq ℂ$
8		ge0addcl	$⊢ (x \in [0, +∞) \land y \in [0, +∞)) \to x + y \in [0, +∞)$
9	8	adantl	$⊢ (φ \land (x \in [0, +∞) \land y \in [0, +∞))) \to x + y \in [0, +∞)$
10		elrege0	$⊢ B \in [0, +∞) \leftrightarrow (B \in ℝ \land 0 \leq B)$
11	2 3 10	sylanbrc	$⊢ (φ \land k \in A) \to B \in [0, +∞)$
12		0e0icopnf	$⊢ 0 \in [0, +∞)$
13	12	a1i	$⊢ φ \to 0 \in [0, +∞)$
14	7 9 1 11 13	fsumcllem	$⊢ φ \to \sum_{k \in A} B \in [0, +∞)$
15		elrege0	$⊢ \sum_{k \in A} B \in [0, +∞) \leftrightarrow (\sum_{k \in A} B \in ℝ \land 0 \leq \sum_{k \in A} B)$
16	15	simprbi	$⊢ \sum_{k \in A} B \in [0, +∞) \to 0 \leq \sum_{k \in A} B$
17	14 16	syl	$⊢ φ \to 0 \leq \sum_{k \in A} B$