Theorem fz1sump1

Description: Add one more term to a sum. Special case of fsump1 generalized to N e. NN0 . (Contributed by SN, 22-Mar-2025)

	Ref	Expression
Hypotheses	fz1sump1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	fz1sump1.a	$$⊢\left(\phi \wedge k\in \left(1\dots N+1\right)\right)\to A\in ℂ$$
	fz1sump1.s	$$⊢k=N+1\to A=B$$
Assertion	fz1sump1	$$⊢\phi \to \sum _{k=1}^{N+1}A=\sum _{k=1}^{N}A+B$$

Proof

Step	Hyp	Ref	Expression
1		fz1sump1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
2		fz1sump1.a	$$⊢\left(\phi \wedge k\in \left(1\dots N+1\right)\right)\to A\in ℂ$$
3		fz1sump1.s	$$⊢k=N+1\to A=B$$
4		nn0p1nn	$$⊢N\in {\mathbb{N}}_0\to N+1\in \mathbb{N}$$
5	1 4	syl	$$⊢\phi \to N+1\in \mathbb{N}$$
6		nnuz	$$⊢\mathbb{N}={\mathbb{Z}}_{\ge 1}$$
7	5 6	eleqtrdi	$$⊢\phi \to N+1\in {\mathbb{Z}}_{\ge 1}$$
8	7 2 3	fsumm1	$$⊢\phi \to \sum _{k=1}^{N+1}A=\sum _{k=1}^{N+1-1}A+B$$
9	1	nn0cnd	$$⊢\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(1\dots N+1-1\right)=\left(1\dots N\right)$$
13	12	sumeq1d	$$⊢\phi \to \sum _{k=1}^{N+1-1}A=\sum _{k=1}^{N}A$$
14	13	oveq1d	$$⊢\phi \to \sum _{k=1}^{N+1-1}A+B=\sum _{k=1}^{N}A+B$$
15	8 14	eqtrd	$$⊢\phi \to \sum _{k=1}^{N+1}A=\sum _{k=1}^{N}A+B$$