sumz

Description: Any sum of zero over a summable set is zero. (Contributed by Mario Carneiro, 12-Aug-2013) (Revised by Mario Carneiro, 20-Apr-2014)

		Ref	Expression
	Assertion	sumz	$⊢ (A \subseteq ℤ_{\geq M} \lor A \in Fin) \to \sum_{k \in A} 0 = 0$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ℤ_{\geq M} = ℤ_{\geq M}$
2		simpr	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to M \in ℤ$
3		simpl	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to A \subseteq ℤ_{\geq M}$
4		c0ex	$⊢ 0 \in V$
5	4	fvconst2	$⊢ k \in ℤ_{\geq M} \to (ℤ_{\geq M} \times \{0\}) (k) = 0$
6		ifid	$⊢ if (k \in A, 0, 0) = 0$
7	5 6	eqtr4di	$⊢ k \in ℤ_{\geq M} \to (ℤ_{\geq M} \times \{0\}) (k) = if (k \in A, 0, 0)$
8	7	adantl	$⊢ ((A \subseteq ℤ_{\geq M} \land M \in ℤ) \land k \in ℤ_{\geq M}) \to (ℤ_{\geq M} \times \{0\}) (k) = if (k \in A, 0, 0)$
9		0cnd	$⊢ ((A \subseteq ℤ_{\geq M} \land M \in ℤ) \land k \in A) \to 0 \in ℂ$
10	1 2 3 8 9	zsum	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to \sum_{k \in A} 0 = ⇝ (seq M (+ (ℤ_{\geq M} \times \{0\})))$
11		fclim	$⊢ ⇝ : dom ⇝ ⟶ ℂ$
12		ffun	$⊢ ⇝ : dom ⇝ ⟶ ℂ \to Fun ⇝$
13	11 12	ax-mp	$⊢ Fun ⇝$
14		serclim0	$⊢ M \in ℤ \to seq M (+ (ℤ_{\geq M} \times \{0\})) ⇝ 0$
15	14	adantl	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to seq M (+ (ℤ_{\geq M} \times \{0\})) ⇝ 0$
16		funbrfv	$⊢ Fun ⇝ \to (seq M (+ (ℤ_{\geq M} \times \{0\})) ⇝ 0 \to ⇝ (seq M (+ (ℤ_{\geq M} \times \{0\}))) = 0)$
17	13 15 16	mpsyl	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to ⇝ (seq M (+ (ℤ_{\geq M} \times \{0\}))) = 0$
18	10 17	eqtrd	$⊢ (A \subseteq ℤ_{\geq M} \land M \in ℤ) \to \sum_{k \in A} 0 = 0$
19		uzf	$⊢ ℤ_{\geq} : ℤ ⟶ 𝒫 ℤ$
20	19	fdmi	$⊢ dom ℤ_{\geq} = ℤ$
21	20	eleq2i	$⊢ M \in dom ℤ_{\geq} \leftrightarrow M \in ℤ$
22		ndmfv	$⊢ \neg M \in dom ℤ_{\geq} \to ℤ_{\geq M} = \emptyset$
23	21 22	sylnbir	$⊢ \neg M \in ℤ \to ℤ_{\geq M} = \emptyset$
24	23	sseq2d	$⊢ \neg M \in ℤ \to (A \subseteq ℤ_{\geq M} \leftrightarrow A \subseteq \emptyset)$
25	24	biimpac	$⊢ (A \subseteq ℤ_{\geq M} \land \neg M \in ℤ) \to A \subseteq \emptyset$
26		ss0	$⊢ A \subseteq \emptyset \to A = \emptyset$
27		sumeq1	$⊢ A = \emptyset \to \sum_{k \in A} 0 = \sum_{k \in \emptyset} 0$
28		sum0	$⊢ \sum_{k \in \emptyset} 0 = 0$
29	27 28	eqtrdi	$⊢ A = \emptyset \to \sum_{k \in A} 0 = 0$
30	25 26 29	3syl	$⊢ (A \subseteq ℤ_{\geq M} \land \neg M \in ℤ) \to \sum_{k \in A} 0 = 0$
31	18 30	pm2.61dan	$⊢ A \subseteq ℤ_{\geq M} \to \sum_{k \in A} 0 = 0$
32		fz1f1o	$⊢ A \in Fin \to (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A))$
33		eqidd	$⊢ k = f (n) \to 0 = 0$
34		simpl	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \|A\| \in ℕ$
35		simpr	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A$
36		0cnd	$⊢ ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land k \in A) \to 0 \in ℂ$
37		elfznn	$⊢ n \in (1 \dots \|A\|) \to n \in ℕ$
38	4	fvconst2	$⊢ n \in ℕ \to (ℕ \times \{0\}) (n) = 0$
39	37 38	syl	$⊢ n \in (1 \dots \|A\|) \to (ℕ \times \{0\}) (n) = 0$
40	39	adantl	$⊢ ((\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \land n \in (1 \dots \|A\|)) \to (ℕ \times \{0\}) (n) = 0$
41	33 34 35 36 40	fsum	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \sum_{k \in A} 0 = seq 1 (+ (ℕ \times \{0\})) (\|A\|)$
42		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
43	42	ser0	$⊢ \|A\| \in ℕ \to seq 1 (+ (ℕ \times \{0\})) (\|A\|) = 0$
44	43	adantr	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to seq 1 (+ (ℕ \times \{0\})) (\|A\|) = 0$
45	41 44	eqtrd	$⊢ (\|A\| \in ℕ \land f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \sum_{k \in A} 0 = 0$
46	45	ex	$⊢ \|A\| \in ℕ \to (f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} 0 = 0)$
47	46	exlimdv	$⊢ \|A\| \in ℕ \to (\exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A \to \sum_{k \in A} 0 = 0)$
48	47	imp	$⊢ (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A) \to \sum_{k \in A} 0 = 0$
49	29 48	jaoi	$⊢ (A = \emptyset \lor (\|A\| \in ℕ \land \exists f f : (1 \dots \|A\|) \underset{1-1 onto}{⟶} A)) \to \sum_{k \in A} 0 = 0$
50	32 49	syl	$⊢ A \in Fin \to \sum_{k \in A} 0 = 0$
51	31 50	jaoi	$⊢ (A \subseteq ℤ_{\geq M} \lor A \in Fin) \to \sum_{k \in A} 0 = 0$

Metamath Proof Explorer

Theorem sumz

Proof