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) (Proof shortened by SN, 22-Mar-2025)

	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		1cnd	|- ( ph -> 1 e. CC )
11	9 10	pncand	|- ( ph -> ( ( N + 1 ) - 1 ) = N )
12	11	oveq2d	|- ( ph -> ( M ... ( ( N + 1 ) - 1 ) ) = ( M ... N ) )
13	12	sumeq1d	|- ( ph -> sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A = sum_ k e. ( M ... N ) A )
14	13	oveq1d	|- ( ph -> ( sum_ k e. ( M ... ( ( N + 1 ) - 1 ) ) A + B ) = ( sum_ k e. ( M ... N ) A + B ) )
15	6 14	eqtrd	|- ( ph -> sum_ k e. ( M ... ( N + 1 ) ) A = ( sum_ k e. ( M ... N ) A + B ) )