# Metamath Proof Explorer

## 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 {ℤ}_{\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 {ℤ}_{\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 {ℤ}_{\ge {M}}\to {M}\in ℤ$
5 1 4 syl ${⊢}{\phi }\to {M}\in ℤ$
6 fzsn ${⊢}{M}\in ℤ\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 {ℤ}_{\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 ℂ↔{B}\in ℂ\right)$
23 2 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left({M}\dots {N}\right)\phantom{\rule{.4em}{0ex}}{A}\in ℂ$
24 22 23 15 rspcdva ${⊢}{\phi }\to {B}\in ℂ$
25 3 sumsn ${⊢}\left({M}\in ℤ\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}$