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 -> A = B )
	isumnn0nn.2	|- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )
	isumnn0nn.3	|- ( ( ph /\ k e. NN0 ) -> A e. CC )
	isumnn0nn.4	|- ( ph -> seq 0 ( + , F ) e. dom ~~> )
Assertion	isumnn0nn	|- ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )

Proof

Step	Hyp	Ref	Expression
1		isumnn0nn.1	|- ( k = 0 -> A = B )
2		isumnn0nn.2	|- ( ( ph /\ k e. NN0 ) -> ( F ` k ) = A )
3		isumnn0nn.3	|- ( ( ph /\ k e. NN0 ) -> A e. CC )
4		isumnn0nn.4	|- ( ph -> seq 0 ( + , F ) e. dom ~~> )
5		nn0uz	|- NN0 = ( ZZ>= ` 0 )
6		0zd	|- ( ph -> 0 e. ZZ )
7	5 6 2 3 4	isum1p	|- ( ph -> sum_ k e. NN0 A = ( ( F ` 0 ) + sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A ) )
8		fveq2	|- ( k = 0 -> ( F ` k ) = ( F ` 0 ) )
9	8 1	eqeq12d	|- ( k = 0 -> ( ( F ` k ) = A <-> ( F ` 0 ) = B ) )
10	2	ralrimiva	|- ( ph -> A. k e. NN0 ( F ` k ) = A )
11		0nn0	|- 0 e. NN0
12	11	a1i	|- ( ph -> 0 e. NN0 )
13	9 10 12	rspcdva	|- ( ph -> ( F ` 0 ) = B )
14		0p1e1	|- ( 0 + 1 ) = 1
15	14	fveq2i	|- ( ZZ>= ` ( 0 + 1 ) ) = ( ZZ>= ` 1 )
16		nnuz	|- NN = ( ZZ>= ` 1 )
17	15 16	eqtr4i	|- ( ZZ>= ` ( 0 + 1 ) ) = NN
18	17	sumeq1i	|- sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A = sum_ k e. NN A
19	18	a1i	|- ( ph -> sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A = sum_ k e. NN A )
20	13 19	oveq12d	|- ( ph -> ( ( F ` 0 ) + sum_ k e. ( ZZ>= ` ( 0 + 1 ) ) A ) = ( B + sum_ k e. NN A ) )
21	7 20	eqtrd	|- ( ph -> sum_ k e. NN0 A = ( B + sum_ k e. NN A ) )