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	$$⊢\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		1cnd	$$⊢\phi \to 1\in ℂ$$
11	9 10	pncand	$$⊢\phi \to N+1-1=N$$
12	11	oveq2d	$$⊢\phi \to \left(M\dots N+1-1\right)=\left(M\dots N\right)$$
13	12	sumeq1d	$$⊢\phi \to \sum _{k=M}^{N+1-1}A=\sum _{k=M}^{N}A$$
14	13	oveq1d	$$⊢\phi \to \sum _{k=M}^{N+1-1}A+B=\sum _{k=M}^{N}A+B$$
15	6 14	eqtrd	$$⊢\phi \to \sum _{k=M}^{N+1}A=\sum _{k=M}^{N}A+B$$