Theorem fsumm1

Description: Separate out the last term in a finite sum. (Contributed by Mario Carneiro, 26-Apr-2014)

	Ref	Expression
Hypotheses	fsumm1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
	fsumm1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to A\in ℂ$$
	fsumm1.3	$$⊢k=N\to A=B$$
Assertion	fsumm1	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k=M}^{N-1}A+B$$

Proof

Step	Hyp	Ref	Expression
1		fsumm1.1	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge M}$$
2		fsumm1.2	$$⊢\left(\phi \wedge k\in \left(M\dots N\right)\right)\to A\in ℂ$$
3		fsumm1.3	$$⊢k=N\to A=B$$
4		eluzelz	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \mathbb{Z}$$
5	1 4	syl	$$⊢\phi \to N\in \mathbb{Z}$$
6		fzsn	$$⊢N\in \mathbb{Z}\to \left(N\dots N\right)=\left\{N\right\}$$
7	5 6	syl	$$⊢\phi \to \left(N\dots N\right)=\left\{N\right\}$$
8	7	ineq2d	$$⊢\phi \to \left(M\dots N-1\right)\cap \left(N\dots N\right)=\left(M\dots N-1\right)\cap \left\{N\right\}$$
9	5	zred	$$⊢\phi \to N\in ℝ$$
10	9	ltm1d	$$⊢\phi \to N-1<N$$
11		fzdisj	$$⊢N-1<N\to \left(M\dots N-1\right)\cap \left(N\dots N\right)=\varnothing$$
12	10 11	syl	$$⊢\phi \to \left(M\dots N-1\right)\cap \left(N\dots N\right)=\varnothing$$
13	8 12	eqtr3d	$$⊢\phi \to \left(M\dots N-1\right)\cap \left\{N\right\}=\varnothing$$
14		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
15	1 14	syl	$$⊢\phi \to M\in \mathbb{Z}$$
16		peano2zm	$$⊢M\in \mathbb{Z}\to M-1\in \mathbb{Z}$$
17	15 16	syl	$$⊢\phi \to M-1\in \mathbb{Z}$$
18	15	zcnd	$$⊢\phi \to M\in ℂ$$
19		ax-1cn	$$⊢1\in ℂ$$
20		npcan	$$⊢\left(M\in ℂ\wedge 1\in ℂ\right)\to M-1+1=M$$
21	18 19 20	sylancl	$$⊢\phi \to M-1+1=M$$
22	21	fveq2d	$$⊢\phi \to {\mathbb{Z}}_{\ge \left(M-1+1\right)}={\mathbb{Z}}_{\ge M}$$
23	1 22	eleqtrrd	$$⊢\phi \to N\in {\mathbb{Z}}_{\ge \left(M-1+1\right)}$$
24		eluzp1m1	$$⊢\left(M-1\in \mathbb{Z}\wedge N\in {\mathbb{Z}}_{\ge \left(M-1+1\right)}\right)\to N-1\in {\mathbb{Z}}_{\ge \left(M-1\right)}$$
25	17 23 24	syl2anc	$$⊢\phi \to N-1\in {\mathbb{Z}}_{\ge \left(M-1\right)}$$
26		fzsuc2	$$⊢\left(M\in \mathbb{Z}\wedge N-1\in {\mathbb{Z}}_{\ge \left(M-1\right)}\right)\to \left(M\dots N-1+1\right)=\left(M\dots N-1\right)\cup \left\{N-1+1\right\}$$
27	15 25 26	syl2anc	$$⊢\phi \to \left(M\dots N-1+1\right)=\left(M\dots N-1\right)\cup \left\{N-1+1\right\}$$
28	5	zcnd	$$⊢\phi \to N\in ℂ$$
29		npcan	$$⊢\left(N\in ℂ\wedge 1\in ℂ\right)\to N-1+1=N$$
30	28 19 29	sylancl	$$⊢\phi \to N-1+1=N$$
31	30	oveq2d	$$⊢\phi \to \left(M\dots N-1+1\right)=\left(M\dots N\right)$$
32	27 31	eqtr3d	$$⊢\phi \to \left(M\dots N-1\right)\cup \left\{N-1+1\right\}=\left(M\dots N\right)$$
33	30	sneqd	$$⊢\phi \to \left\{N-1+1\right\}=\left\{N\right\}$$
34	33	uneq2d	$$⊢\phi \to \left(M\dots N-1\right)\cup \left\{N-1+1\right\}=\left(M\dots N-1\right)\cup \left\{N\right\}$$
35	32 34	eqtr3d	$$⊢\phi \to \left(M\dots N\right)=\left(M\dots N-1\right)\cup \left\{N\right\}$$
36		fzfid	$$⊢\phi \to \left(M\dots N\right)\in \mathrm{Fin}$$
37	13 35 36 2	fsumsplit	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k=M}^{N-1}A+\sum _{k\in \left\{N\right\}}A$$
38	3	eleq1d	$$⊢k=N\to \left(A\in ℂ\leftrightarrow B\in ℂ\right)$$
39	2	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N\right)A\in ℂ$$
40		eluzfz2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to N\in \left(M\dots N\right)$$
41	1 40	syl	$$⊢\phi \to N\in \left(M\dots N\right)$$
42	38 39 41	rspcdva	$$⊢\phi \to B\in ℂ$$
43	3	sumsn	$$⊢\left(N\in {\mathbb{Z}}_{\ge M}\wedge B\in ℂ\right)\to \sum _{k\in \left\{N\right\}}A=B$$
44	1 42 43	syl2anc	$$⊢\phi \to \sum _{k\in \left\{N\right\}}A=B$$
45	44	oveq2d	$$⊢\phi \to \sum _{k=M}^{N-1}A+\sum _{k\in \left\{N\right\}}A=\sum _{k=M}^{N-1}A+B$$
46	37 45	eqtrd	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k=M}^{N-1}A+B$$