fsum00

Description: A sum of nonnegative numbers is zero iff all terms are zero. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened 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	fsum00	$⊢ φ \to (\sum_{k \in A} B = 0 \leftrightarrow \forall k \in A B = 0)$

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	1	adantr	$⊢ (φ \land m \in A) \to A \in Fin$
5	2	adantlr	$⊢ ((φ \land m \in A) \land k \in A) \to B \in ℝ$
6	3	adantlr	$⊢ ((φ \land m \in A) \land k \in A) \to 0 \leq B$
7		snssi	$⊢ m \in A \to \{m\} \subseteq A$
8	7	adantl	$⊢ (φ \land m \in A) \to \{m\} \subseteq A$
9	4 5 6 8	fsumless	$⊢ (φ \land m \in A) \to \sum_{k \in \{m\}} B \leq \sum_{k \in A} B$
10	9	adantlr	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to \sum_{k \in \{m\}} B \leq \sum_{k \in A} B$
11		simpr	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to m \in A$
12	2 3	jca	$⊢ (φ \land k \in A) \to (B \in ℝ \land 0 \leq B)$
13	12	ralrimiva	$⊢ φ \to \forall k \in A (B \in ℝ \land 0 \leq B)$
14	13	adantr	$⊢ (φ \land \sum_{k \in A} B = 0) \to \forall k \in A (B \in ℝ \land 0 \leq B)$
15		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ m / k ⦌ B$
16	15	nfel1	$⊢ Ⅎ k ⦋ m / k ⦌ B \in ℝ$
17		nfcv	$⊢ \underline{Ⅎ} k 0$
18		nfcv	$⊢ \underline{Ⅎ} k \leq$
19	17 18 15	nfbr	$⊢ Ⅎ k 0 \leq ⦋ m / k ⦌ B$
20	16 19	nfan	$⊢ Ⅎ k (⦋ m / k ⦌ B \in ℝ \land 0 \leq ⦋ m / k ⦌ B)$
21		csbeq1a	$⊢ k = m \to B = ⦋ m / k ⦌ B$
22	21	eleq1d	$⊢ k = m \to (B \in ℝ \leftrightarrow ⦋ m / k ⦌ B \in ℝ)$
23	21	breq2d	$⊢ k = m \to (0 \leq B \leftrightarrow 0 \leq ⦋ m / k ⦌ B)$
24	22 23	anbi12d	$⊢ k = m \to ((B \in ℝ \land 0 \leq B) \leftrightarrow (⦋ m / k ⦌ B \in ℝ \land 0 \leq ⦋ m / k ⦌ B))$
25	20 24	rspc	$⊢ m \in A \to (\forall k \in A (B \in ℝ \land 0 \leq B) \to (⦋ m / k ⦌ B \in ℝ \land 0 \leq ⦋ m / k ⦌ B))$
26	14 25	mpan9	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to (⦋ m / k ⦌ B \in ℝ \land 0 \leq ⦋ m / k ⦌ B)$
27	26	simpld	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to ⦋ m / k ⦌ B \in ℝ$
28	27	recnd	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to ⦋ m / k ⦌ B \in ℂ$
29		sumsns	$⊢ (m \in A \land ⦋ m / k ⦌ B \in ℂ) \to \sum_{k \in \{m\}} B = ⦋ m / k ⦌ B$
30	11 28 29	syl2anc	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to \sum_{k \in \{m\}} B = ⦋ m / k ⦌ B$
31		simplr	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to \sum_{k \in A} B = 0$
32	10 30 31	3brtr3d	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to ⦋ m / k ⦌ B \leq 0$
33	26	simprd	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to 0 \leq ⦋ m / k ⦌ B$
34		0re	$⊢ 0 \in ℝ$
35		letri3	$⊢ (⦋ m / k ⦌ B \in ℝ \land 0 \in ℝ) \to (⦋ m / k ⦌ B = 0 \leftrightarrow (⦋ m / k ⦌ B \leq 0 \land 0 \leq ⦋ m / k ⦌ B))$
36	27 34 35	sylancl	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to (⦋ m / k ⦌ B = 0 \leftrightarrow (⦋ m / k ⦌ B \leq 0 \land 0 \leq ⦋ m / k ⦌ B))$
37	32 33 36	mpbir2and	$⊢ ((φ \land \sum_{k \in A} B = 0) \land m \in A) \to ⦋ m / k ⦌ B = 0$
38	37	ralrimiva	$⊢ (φ \land \sum_{k \in A} B = 0) \to \forall m \in A ⦋ m / k ⦌ B = 0$
39		nfv	$⊢ Ⅎ m B = 0$
40	15	nfeq1	$⊢ Ⅎ k ⦋ m / k ⦌ B = 0$
41	21	eqeq1d	$⊢ k = m \to (B = 0 \leftrightarrow ⦋ m / k ⦌ B = 0)$
42	39 40 41	cbvralw	$⊢ \forall k \in A B = 0 \leftrightarrow \forall m \in A ⦋ m / k ⦌ B = 0$
43	38 42	sylibr	$⊢ (φ \land \sum_{k \in A} B = 0) \to \forall k \in A B = 0$
44	43	ex	$⊢ φ \to (\sum_{k \in A} B = 0 \to \forall k \in A B = 0)$
45		sumz	$⊢ (A \subseteq ℤ_{\geq 0} \lor A \in Fin) \to \sum_{k \in A} 0 = 0$
46	45	olcs	$⊢ A \in Fin \to \sum_{k \in A} 0 = 0$
47		sumeq2	$⊢ \forall k \in A B = 0 \to \sum_{k \in A} B = \sum_{k \in A} 0$
48	47	eqeq1d	$⊢ \forall k \in A B = 0 \to (\sum_{k \in A} B = 0 \leftrightarrow \sum_{k \in A} 0 = 0)$
49	46 48	syl5ibrcom	$⊢ A \in Fin \to (\forall k \in A B = 0 \to \sum_{k \in A} B = 0)$
50	1 49	syl	$⊢ φ \to (\forall k \in A B = 0 \to \sum_{k \in A} B = 0)$
51	44 50	impbid	$⊢ φ \to (\sum_{k \in A} B = 0 \leftrightarrow \forall k \in A B = 0)$

Metamath Proof Explorer

Theorem fsum00

Proof