Theorem fsump1

Description: The addition of the next term in a finite sum of A ( k ) is the current term plus B i.e. A ( N + 1 ) . (Contributed by NM, 4-Nov-2005) (Revised by Mario Carneiro, 21-Apr-2014)

	Ref	Expression
Hypotheses	fsump1.1	|- ( ph -> N e. ( ZZ>= ` M ) )
	fsump1.2	|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
	fsump1.3	|- ( k = ( N + 1 ) -> A = B )
Assertion	fsump1	|- ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... N ) A + B ) )

Proof

Step	Hyp	Ref	Expression
1		fsump1.1	|- ( ph -> N e. ( ZZ>= ` M ) )
2		fsump1.2	|- ( ( ph /\ k e. ( M ... ( N + 1 ) ) ) -> A e. CC )
3		fsump1.3	|- ( k = ( N + 1 ) -> A = B )
4		peano2uz	|- ( N e. ( ZZ>= ` M ) -> ( N + 1 ) e. ( ZZ>= ` M ) )
5	1 4	syl	|- ( ph -> ( N + 1 ) e. ( ZZ>= ` M ) )
6	5 2 3	fsumm1	|- ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A + B ) )
7		eluzelz	|- ( N e. ( ZZ>= ` M ) -> N e. ZZ )
8	1 7	syl	|- ( ph -> N e. ZZ )
9	8	zcnd	|- ( ph -> N e. CC )
10		ax-1cn	|- 1 e. CC
11		pncan	|- ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
12	9 10 11	sylancl	|- ( ph -> ( ( N + 1 ) - 1 ) = N )
13	12	oveq2d	|- ( ph -> ( M ... ( ( N + 1 ) - 1 ) ) = ( M ... N ) )
14	13	sumeq1d	|- ( ph -> sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A = sum_ k e. ( M ... N ) A )
15	14	oveq1d	|- ( ph -> ( sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A + B ) = ( sum_ k e. ( M ... N ) A + B ) )
16	6 15	eqtrd	|- ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... N ) A + B ) )