# Metamath Proof Explorer

## Theorem 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 ${⊢}\left({A}\subseteq {ℤ}_{\ge {M}}\vee {A}\in \mathrm{Fin}\right)\to \sum _{{k}\in {A}}0=0$

### Proof

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