Theorem isum1p

Description: The infinite sum of a converging infinite series equals the first term plus the infinite sum of the rest of it. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isum1p.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	isum1p.3	$$⊢\phi \to M\in \mathbb{Z}$$
	isum1p.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
	isum1p.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
	isum1p.6	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isum1p	$$⊢\phi \to \sum _{k\in Z}A=F\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}A$$

Proof

Step	Hyp	Ref	Expression
1		isum1p.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		isum1p.3	$$⊢\phi \to M\in \mathbb{Z}$$
3		isum1p.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)=A$$
4		isum1p.5	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
5		isum1p.6	$$⊢\phi \to seqM\left(+,F\right)\in \mathrm{dom}⇝$$
6		eqid	$$⊢{\mathbb{Z}}_{\ge \left(M+1\right)}={\mathbb{Z}}_{\ge \left(M+1\right)}$$
7		uzid	$$⊢M\in \mathbb{Z}\to M\in {\mathbb{Z}}_{\ge M}$$
8	2 7	syl	$$⊢\phi \to M\in {\mathbb{Z}}_{\ge M}$$
9		peano2uz	$$⊢M\in {\mathbb{Z}}_{\ge M}\to M+1\in {\mathbb{Z}}_{\ge M}$$
10	8 9	syl	$$⊢\phi \to M+1\in {\mathbb{Z}}_{\ge M}$$
11	10 1	eleqtrrdi	$$⊢\phi \to M+1\in Z$$
12	1 6 11 3 4 5	isumsplit	$$⊢\phi \to \sum _{k\in Z}A=\sum _{k=M}^{M+1-1}A+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}A$$
13	2	zcnd	$$⊢\phi \to M\in ℂ$$
14		ax-1cn	$$⊢1\in ℂ$$
15		pncan	$$⊢\left(M\in ℂ\wedge 1\in ℂ\right)\to M+1-1=M$$
16	13 14 15	sylancl	$$⊢\phi \to M+1-1=M$$
17	16	oveq2d	$$⊢\phi \to \left(M\dots M+1-1\right)=\left(M\dots M\right)$$
18	17	sumeq1d	$$⊢\phi \to \sum _{k=M}^{M+1-1}A=\sum _{k=M}^{M}A$$
19		elfzuz	$$⊢k\in \left(M\dots M\right)\to k\in {\mathbb{Z}}_{\ge M}$$
20	19 1	eleqtrrdi	$$⊢k\in \left(M\dots M\right)\to k\in Z$$
21	20 3	sylan2	$$⊢\left(\phi \wedge k\in \left(M\dots M\right)\right)\to F\left(k\right)=A$$
22	21	sumeq2dv	$$⊢\phi \to \sum _{k=M}^{M}F\left(k\right)=\sum _{k=M}^{M}A$$
23		fveq2	$$⊢k=M\to F\left(k\right)=F\left(M\right)$$
24	23	eleq1d	$$⊢k=M\to \left(F\left(k\right)\in ℂ\leftrightarrow F\left(M\right)\in ℂ\right)$$
25	3 4	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
26	25	ralrimiva	$$⊢\phi \to \forall k\in ZF\left(k\right)\in ℂ$$
27	8 1	eleqtrrdi	$$⊢\phi \to M\in Z$$
28	24 26 27	rspcdva	$$⊢\phi \to F\left(M\right)\in ℂ$$
29	23	fsum1	$$⊢\left(M\in \mathbb{Z}\wedge F\left(M\right)\in ℂ\right)\to \sum _{k=M}^{M}F\left(k\right)=F\left(M\right)$$
30	2 28 29	syl2anc	$$⊢\phi \to \sum _{k=M}^{M}F\left(k\right)=F\left(M\right)$$
31	18 22 30	3eqtr2d	$$⊢\phi \to \sum _{k=M}^{M+1-1}A=F\left(M\right)$$
32	31	oveq1d	$$⊢\phi \to \sum _{k=M}^{M+1-1}A+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}A=F\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}A$$
33	12 32	eqtrd	$$⊢\phi \to \sum _{k\in Z}A=F\left(M\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(M+1\right)}}A$$