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	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
2		1z	$$⊢1\in \mathbb{Z}$$
3	2	a1i	$$⊢\top \to 1\in \mathbb{Z}$$
4		0ss	$$⊢\varnothing \subseteq \mathbb{N}$$
5	4	a1i	$$⊢\top \to \varnothing \subseteq \mathbb{N}$$
6		simpr	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to k\in \mathbb{N}$$
7	6 1	eleqtrdi	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to k\in {\mathbb{Z}}_{\ge 1}$$
8		c0ex	$$⊢0\in \mathrm{V}$$
9	8	fvconst2	$$⊢k\in {\mathbb{Z}}_{\ge 1}\to \left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\left(k\right)=0$$
10	7 9	syl	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to \left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\left(k\right)=0$$
11		noel	$$⊢\neg k\in \varnothing$$
12	11	iffalsei	$$⊢if\left(k\in \varnothing ,A,0\right)=0$$
13	10 12	eqtr4di	$$⊢\left(\top \wedge k\in \mathbb{N}\right)\to \left({\mathbb{Z}}_{\ge 1}\times \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({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)\right)$$
17	16	mptru	$$⊢\sum _{k\in \varnothing }A=⇝\left(seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \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 \mathbb{Z}\to seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0$$
22	2 21	ax-mp	$$⊢seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0$$
23		funbrfv	$$⊢\mathrm{Fun}⇝\to \left(seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)⇝0\to ⇝\left(seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)\right)=0\right)$$
24	20 22 23	mp2	$$⊢⇝\left(seq1\left(+,\left({\mathbb{Z}}_{\ge 1}\times \left\{0\right\}\right)\right)\right)=0$$
25	17 24	eqtri	$$⊢\sum _{k\in \varnothing }A=0$$