Theorem ser0

Description: The value of the partial sums in a zero-valued infinite series. (Contributed by Mario Carneiro, 31-Aug-2013) (Revised by Mario Carneiro, 15-Dec-2014)

	Ref	Expression
Hypothesis	ser0.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
Assertion	ser0	$$⊢N\in Z\to seqM\left(+,\left(Z\times \left\{0\right\}\right)\right)\left(N\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		ser0.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		00id	$$⊢0+0=0$$
3	2	a1i	$$⊢N\in Z\to 0+0=0$$
4	1	eleq2i	$$⊢N\in Z\leftrightarrow N\in {\mathbb{Z}}_{\ge M}$$
5	4	biimpi	$$⊢N\in Z\to N\in {\mathbb{Z}}_{\ge M}$$
6		0cn	$$⊢0\in ℂ$$
7		elfzuz	$$⊢k\in \left(M\dots N\right)\to k\in {\mathbb{Z}}_{\ge M}$$
8	7 1	eleqtrrdi	$$⊢k\in \left(M\dots N\right)\to k\in Z$$
9	8	adantl	$$⊢\left(N\in Z\wedge k\in \left(M\dots N\right)\right)\to k\in Z$$
10		fvconst2g	$$⊢\left(0\in ℂ\wedge k\in Z\right)\to \left(Z\times \left\{0\right\}\right)\left(k\right)=0$$
11	6 9 10	sylancr	$$⊢\left(N\in Z\wedge k\in \left(M\dots N\right)\right)\to \left(Z\times \left\{0\right\}\right)\left(k\right)=0$$
12	3 5 11	seqid3	$$⊢N\in Z\to seqM\left(+,\left(Z\times \left\{0\right\}\right)\right)\left(N\right)=0$$