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 ) )