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	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	fsump1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
	fsump1.3	$$⊢k=N+1\to A=B$$
Assertion	fsump1	$$⊢\phi \to \sum _{k=M}^{N+1}A=\sum _{k=M}^{N}A+B$$

Proof

Step	Hyp	Ref	Expression
1		fsump1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fsump1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N+1\right)\right)\to A\in ℂ$$
3		fsump1.3	$$⊢k=N+1\to A=B$$
4		peano2uz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N+1\in {\mathbb{Z}}_{\ge M}$$
5	1 4	syl	$$⊢\phi \to N+1\in {\mathbb{Z}}_{\ge M}$$
6	5 2 3	fsumm1	$$⊢\phi \to \sum _{k=M}^{N+1}A=\sum _{k=M}^{N+1-1}A+B$$
7		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
8	1 7	syl	$$⊢\phi \to N\in \mathbb{Z}$$
9	8	zcnd	$$⊢\phi \to N\in ℂ$$
10		ax-1cn	$$⊢1\in ℂ$$
11		pncan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N+1-1=N$$
12	9 10 11	sylancl	$$⊢\phi \to N+1-1=N$$
13	12	oveq2d	$$⊢\phi \to \left(M\dots N+1-1\right)=\left(M\dots N\right)$$
14	13	sumeq1d	$$⊢\phi \to \sum _{k=M}^{N+1-1}A=\sum _{k=M}^{N}A$$
15	14	oveq1d	$$⊢\phi \to \sum _{k=M}^{N+1-1}A+B=\sum _{k=M}^{N}A+B$$
16	6 15	eqtrd	$$⊢\phi \to \sum _{k=M}^{N+1}A=\sum _{k=M}^{N}A+B$$