Theorem fsum1p

Description: Separate out the first term in a finite sum. (Contributed by NM, 3-Jan-2006) (Revised by Mario Carneiro, 23-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 ℂ$$
	fsum1p.3	$$⊢k=M\to A=B$$
Assertion	fsum1p	$$⊢\phi \to \sum _{k=M}^{N}A=B+\sum _{k=M+1}^{N}A$$

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		fsum1p.3	$$⊢k=M\to A=B$$
4		eluzel2	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \mathbb{Z}$$
5	1 4	syl	$$⊢\phi \to M\in \mathbb{Z}$$
6		fzsn	$$⊢M\in \mathbb{Z}\to \left(M\dots M\right)=\left\{M\right\}$$
7	5 6	syl	$$⊢\phi \to \left(M\dots M\right)=\left\{M\right\}$$
8	7	ineq1d	$$⊢\phi \to \left(M\dots M\right)\cap \left(M+1\dots N\right)=\left\{M\right\}\cap \left(M+1\dots N\right)$$
9	5	zred	$$⊢\phi \to M\in ℝ$$
10	9	ltp1d	$$⊢\phi \to M<M+1$$
11		fzdisj	$$⊢M<M+1\to \left(M\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
12	10 11	syl	$$⊢\phi \to \left(M\dots M\right)\cap \left(M+1\dots N\right)=\varnothing$$
13	8 12	eqtr3d	$$⊢\phi \to \left\{M\right\}\cap \left(M+1\dots N\right)=\varnothing$$
14		eluzfz1	$$⊢N\in {\mathbb{Z}}_{\ge M}\to M\in \left(M\dots N\right)$$
15	1 14	syl	$$⊢\phi \to M\in \left(M\dots N\right)$$
16		fzsplit	$$⊢M\in \left(M\dots N\right)\to \left(M\dots N\right)=\left(M\dots M\right)\cup \left(M+1\dots N\right)$$
17	15 16	syl	$$⊢\phi \to \left(M\dots N\right)=\left(M\dots M\right)\cup \left(M+1\dots N\right)$$
18	7	uneq1d	$$⊢\phi \to \left(M\dots M\right)\cup \left(M+1\dots N\right)=\left\{M\right\}\cup \left(M+1\dots N\right)$$
19	17 18	eqtrd	$$⊢\phi \to \left(M\dots N\right)=\left\{M\right\}\cup \left(M+1\dots N\right)$$
20		fzfid	$$⊢\phi \to \left(M\dots N\right)\in \mathrm{Fin}$$
21	13 19 20 2	fsumsplit	$$⊢\phi \to \sum _{k=M}^{N}A=\sum _{k\in \left\{M\right\}}A+\sum _{k=M+1}^{N}A$$
22	3	eleq1d	$$⊢k=M\to \left(A\in ℂ\leftrightarrow B\in ℂ\right)$$
23	2	ralrimiva	$$⊢\phi \to \forall k\in \left(M\dots N\right)A\in ℂ$$
24	22 23 15	rspcdva	$$⊢\phi \to B\in ℂ$$
25	3	sumsn	$$⊢\left(M\in \mathbb{Z}\wedge B\in ℂ\right)\to \sum _{k\in \left\{M\right\}}A=B$$
26	5 24 25	syl2anc	$$⊢\phi \to \sum _{k\in \left\{M\right\}}A=B$$
27	26	oveq1d	$$⊢\phi \to \sum _{k\in \left\{M\right\}}A+\sum _{k=M+1}^{N}A=B+\sum _{k=M+1}^{N}A$$
28	21 27	eqtrd	$$⊢\phi \to \sum _{k=M}^{N}A=B+\sum _{k=M+1}^{N}A$$