Theorem fsump1i

Description: Optimized version of fsump1 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsump1i.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	fsump1i.2	$$⊢N=K+1$$
	fsump1i.3	$$⊢k=N\to A=B$$
	fsump1i.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
	fsump1i.5	$$⊢\phi \to \left(K\in Z\wedge \sum _{k=M}^{K}A=S\right)$$
	fsump1i.6	$$⊢\phi \to S+B=T$$
Assertion	fsump1i	$$⊢\phi \to \left(N\in Z\wedge \sum _{k=M}^{N}A=T\right)$$

Proof

Step	Hyp	Ref	Expression
1		fsump1i.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		fsump1i.2	$$⊢N=K+1$$
3		fsump1i.3	$$⊢k=N\to A=B$$
4		fsump1i.4	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℂ$$
5		fsump1i.5	$$⊢\phi \to \left(K\in Z\wedge \sum _{k=M}^{K}A=S\right)$$
6		fsump1i.6	$$⊢\phi \to S+B=T$$
7	5	simpld	$$⊢\phi \to K\in Z$$
8	7 1	eleqtrdi	$$⊢\phi \to K\in {\mathbb{Z}}_{\ge M}$$
9		peano2uz	$$⊢K\in {\mathbb{Z}}_{\ge M}\to K+1\in {\mathbb{Z}}_{\ge M}$$
10	9 1	eleqtrrdi	$$⊢K\in {\mathbb{Z}}_{\ge M}\to K+1\in Z$$
11	8 10	syl	$$⊢\phi \to K+1\in Z$$
12	2 11	eqeltrid	$$⊢\phi \to N\in Z$$
13	2	oveq2i	$$⊢\left(M\dots N\right)=\left(M\dots K+1\right)$$
14	13	sumeq1i	$$⊢\sum _{k=M}^{N}A=\sum _{k=M}^{K+1}A$$
15		elfzuz	$$⊢k\in \left(M\dots K+1\right)\to k\in {\mathbb{Z}}_{\ge M}$$
16	15 1	eleqtrrdi	$$⊢k\in \left(M\dots K+1\right)\to k\in Z$$
17	16 4	sylan2	$$⊢\left(\phi \wedge k\in \left(M\dots K+1\right)\right)\to A\in ℂ$$
18	2	eqeq2i	$$⊢k=N\leftrightarrow k=K+1$$
19	18 3	sylbir	$$⊢k=K+1\to A=B$$
20	8 17 19	fsump1	$$⊢\phi \to \sum _{k=M}^{K+1}A=\sum _{k=M}^{K}A+B$$
21	14 20	eqtrid	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k=M}^{K}A+B$$
22	5	simprd	$$⊢\phi \to \sum _{k=M}^{K}A=S$$
23	22	oveq1d	$$⊢\phi \to \sum _{k=M}^{K}A+B=S+B$$
24	21 23 6	3eqtrd	$$⊢\phi \to \sum _{k=M}^{N}A=T$$
25	12 24	jca	$$⊢\phi \to \left(N\in Z\wedge \sum _{k=M}^{N}A=T\right)$$