# 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
`|- ( ph -> N e. ( ZZ>= ` M ) )`
fsumm1.2
`|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )`
fsum1p.3
`|- ( k = M -> A = B )`
Assertion fsum1p
`|- ( ph -> sum_ k e. ( M ... N ) A = ( B + sum_ k e. ( ( M + 1 ) ... N ) A ) )`

### Proof

Step Hyp Ref Expression
1 fsumm1.1
` |-  ( ph -> N e. ( ZZ>= ` M ) )`
2 fsumm1.2
` |-  ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )`
3 fsum1p.3
` |-  ( k = M -> A = B )`
4 eluzel2
` |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )`
5 1 4 syl
` |-  ( ph -> M e. ZZ )`
6 fzsn
` |-  ( M e. ZZ -> ( M ... M ) = { M } )`
7 5 6 syl
` |-  ( ph -> ( M ... M ) = { M } )`
8 7 ineq1d
` |-  ( ph -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = ( { M } i^i ( ( M + 1 ) ... N ) ) )`
9 5 zred
` |-  ( ph -> M e. RR )`
10 9 ltp1d
` |-  ( ph -> M < ( M + 1 ) )`
11 fzdisj
` |-  ( M < ( M + 1 ) -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )`
12 10 11 syl
` |-  ( ph -> ( ( M ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )`
13 8 12 eqtr3d
` |-  ( ph -> ( { M } i^i ( ( M + 1 ) ... N ) ) = (/) )`
14 eluzfz1
` |-  ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )`
15 1 14 syl
` |-  ( ph -> M e. ( M ... N ) )`
16 fzsplit
` |-  ( M e. ( M ... N ) -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )`
17 15 16 syl
` |-  ( ph -> ( M ... N ) = ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) )`
18 7 uneq1d
` |-  ( ph -> ( ( M ... M ) u. ( ( M + 1 ) ... N ) ) = ( { M } u. ( ( M + 1 ) ... N ) ) )`
19 17 18 eqtrd
` |-  ( ph -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )`
20 fzfid
` |-  ( ph -> ( M ... N ) e. Fin )`
21 13 19 20 2 fsumsplit
` |-  ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. { M } A + sum_ k e. ( ( M + 1 ) ... N ) A ) )`
22 3 eleq1d
` |-  ( k = M -> ( A e. CC <-> B e. CC ) )`
23 2 ralrimiva
` |-  ( ph -> A. k e. ( M ... N ) A e. CC )`
24 22 23 15 rspcdva
` |-  ( ph -> B e. CC )`
25 3 sumsn
` |-  ( ( M e. ZZ /\ B e. CC ) -> sum_ k e. { M } A = B )`
26 5 24 25 syl2anc
` |-  ( ph -> sum_ k e. { M } A = B )`
27 26 oveq1d
` |-  ( ph -> ( sum_ k e. { M } A + sum_ k e. ( ( M + 1 ) ... N ) A ) = ( B + sum_ k e. ( ( M + 1 ) ... N ) A ) )`
28 21 27 eqtrd
` |-  ( ph -> sum_ k e. ( M ... N ) A = ( B + sum_ k e. ( ( M + 1 ) ... N ) A ) )`