Theorem isumnn0nn

Description: Sum from 0 to infinity in terms of sum from 1 to infinity. (Contributed by NM, 2-Jan-2006) (Revised by Mario Carneiro, 24-Apr-2014)

	Ref	Expression
Hypotheses	isumnn0nn.1	$$⊢k=0\to A=B$$
	isumnn0nn.2	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=A$$
	isumnn0nn.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
	isumnn0nn.4	$$⊢\phi \to seq0\left(+,F\right)\in \mathrm{dom}⇝$$
Assertion	isumnn0nn	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}A=B+\sum _{k\in \mathbb{N}}A$$

Proof

Step	Hyp	Ref	Expression
1		isumnn0nn.1	$$⊢k=0\to A=B$$
2		isumnn0nn.2	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to F\left(k\right)=A$$
3		isumnn0nn.3	$$⊢\left(\phi \wedge k\in {\mathbb{N}}_0\right)\to A\in ℂ$$
4		isumnn0nn.4	$$⊢\phi \to seq0\left(+,F\right)\in \mathrm{dom}⇝$$
5		nn0uz	$$⊢{\mathbb{N}}_0={\mathbb{Z}}_{\ge 0}$$
6		0zd	$$⊢\phi \to 0\in \mathbb{Z}$$
7	5 6 2 3 4	isum1p	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}A=F\left(0\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(0+1\right)}}A$$
8		fveq2	$$⊢k=0\to F\left(k\right)=F\left(0\right)$$
9	8 1	eqeq12d	$$⊢k=0\to \left(F\left(k\right)=A\leftrightarrow F\left(0\right)=B\right)$$
10	2	ralrimiva	$$⊢\phi \to \forall k\in {\mathbb{N}}_{0}F\left(k\right)=A$$
11		0nn0	$$⊢0\in {\mathbb{N}}_0$$
12	11	a1i	$$⊢\phi \to 0\in {\mathbb{N}}_0$$
13	9 10 12	rspcdva	$$⊢\phi \to F\left(0\right)=B$$
14		0p1e1	$$⊢0+1=1$$
15	14	fveq2i	$$⊢{\mathbb{Z}}_{\ge \left(0+1\right)}={\mathbb{Z}}_{\ge 1}$$
16		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
17	15 16	eqtr4i	$$⊢{\mathbb{Z}}_{\ge \left(0+1\right)}=\mathbb{N}$$
18	17	sumeq1i	$$⊢\sum _{k\in {\mathbb{Z}}_{\ge \left(0+1\right)}}A=\sum _{k\in \mathbb{N}}A$$
19	18	a1i	$$⊢\phi \to \sum _{k\in {\mathbb{Z}}_{\ge \left(0+1\right)}}A=\sum _{k\in \mathbb{N}}A$$
20	13 19	oveq12d	$$⊢\phi \to F\left(0\right)+\sum _{k\in {\mathbb{Z}}_{\ge \left(0+1\right)}}A=B+\sum _{k\in \mathbb{N}}A$$
21	7 20	eqtrd	$$⊢\phi \to \sum _{k\in {\mathbb{N}}_0}A=B+\sum _{k\in \mathbb{N}}A$$