# Metamath Proof Explorer

## Theorem sum0

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

Ref Expression
Assertion sum0 ${⊢}\sum _{{k}\in \varnothing }{A}=0$

### Proof

Step Hyp Ref Expression
1 nnuz ${⊢}ℕ={ℤ}_{\ge 1}$
2 1z ${⊢}1\in ℤ$
3 2 a1i ${⊢}\top \to 1\in ℤ$
4 0ss ${⊢}\varnothing \subseteq ℕ$
5 4 a1i ${⊢}\top \to \varnothing \subseteq ℕ$
6 simpr ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}\in ℕ$
7 6 1 eleqtrdi ${⊢}\left(\top \wedge {k}\in ℕ\right)\to {k}\in {ℤ}_{\ge 1}$
8 c0ex ${⊢}0\in \mathrm{V}$
9 8 fvconst2 ${⊢}{k}\in {ℤ}_{\ge 1}\to \left({ℤ}_{\ge 1}×\left\{0\right\}\right)\left({k}\right)=0$
10 7 9 syl ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left({ℤ}_{\ge 1}×\left\{0\right\}\right)\left({k}\right)=0$
11 noel ${⊢}¬{k}\in \varnothing$
12 11 iffalsei ${⊢}if\left({k}\in \varnothing ,{A},0\right)=0$
13 10 12 syl6eqr ${⊢}\left(\top \wedge {k}\in ℕ\right)\to \left({ℤ}_{\ge 1}×\left\{0\right\}\right)\left({k}\right)=if\left({k}\in \varnothing ,{A},0\right)$
14 11 pm2.21i ${⊢}{k}\in \varnothing \to {A}\in ℂ$
15 14 adantl ${⊢}\left(\top \wedge {k}\in \varnothing \right)\to {A}\in ℂ$
16 1 3 5 13 15 zsum ${⊢}\top \to \sum _{{k}\in \varnothing }{A}=⇝\left(seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)\right)$
17 16 mptru ${⊢}\sum _{{k}\in \varnothing }{A}=⇝\left(seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)\right)$
18 fclim ${⊢}⇝:\mathrm{dom}⇝⟶ℂ$
19 ffun ${⊢}⇝:\mathrm{dom}⇝⟶ℂ\to \mathrm{Fun}⇝$
20 18 19 ax-mp ${⊢}\mathrm{Fun}⇝$
21 serclim0 ${⊢}1\in ℤ\to seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)⇝0$
22 2 21 ax-mp ${⊢}seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)⇝0$
23 funbrfv ${⊢}\mathrm{Fun}⇝\to \left(seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)⇝0\to ⇝\left(seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)\right)=0\right)$
24 20 22 23 mp2 ${⊢}⇝\left(seq1\left(+,\left({ℤ}_{\ge 1}×\left\{0\right\}\right)\right)\right)=0$
25 17 24 eqtri ${⊢}\sum _{{k}\in \varnothing }{A}=0$