This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fsumm1

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

Ref Expression
Hypotheses fsumm1.1 
|- ( ph -> N e. ( ZZ>= ` M ) )
fsumm1.2 
|- ( ( ph /\ k e. ( M ... N ) ) -> A e. CC )
fsumm1.3 
|- ( k = N -> A = B )
Assertion fsumm1 
|- ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )

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 fsumm1.3 
 |-  ( k = N -> A = B )
4 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
5 1 4 syl 
 |-  ( ph -> N e. ZZ )
6 fzsn 
 |-  ( N e. ZZ -> ( N ... N ) = { N } )
7 5 6 syl 
 |-  ( ph -> ( N ... N ) = { N } )
8 7 ineq2d 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) i^i ( N ... N ) ) = ( ( M ... ( N - 1 ) ) i^i { N } ) )
9 5 zred 
 |-  ( ph -> N e. RR )
10 9 ltm1d 
 |-  ( ph -> ( N - 1 ) < N )
11 fzdisj 
 |-  ( ( N - 1 ) < N -> ( ( M ... ( N - 1 ) ) i^i ( N ... N ) ) = (/) )
12 10 11 syl 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) i^i ( N ... N ) ) = (/) )
13 8 12 eqtr3d 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) i^i { N } ) = (/) )
14 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
15 1 14 syl 
 |-  ( ph -> M e. ZZ )
16 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
17 15 16 syl 
 |-  ( ph -> ( M - 1 ) e. ZZ )
18 15 zcnd 
 |-  ( ph -> M e. CC )
19 ax-1cn 
 |-  1 e. CC
20 npcan 
 |-  ( ( M e. CC /\ 1 e. CC ) -> ( ( M - 1 ) + 1 ) = M )
21 18 19 20 sylancl 
 |-  ( ph -> ( ( M - 1 ) + 1 ) = M )
22 21 fveq2d 
 |-  ( ph -> ( ZZ>= ` ( ( M - 1 ) + 1 ) ) = ( ZZ>= ` M ) )
23 1 22 eleqtrrd 
 |-  ( ph -> N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) )
24 eluzp1m1 
 |-  ( ( ( M - 1 ) e. ZZ /\ N e. ( ZZ>= ` ( ( M - 1 ) + 1 ) ) ) -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
25 17 23 24 syl2anc 
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
26 fzsuc2 
 |-  ( ( M e. ZZ /\ ( N - 1 ) e. ( ZZ>= ` ( M - 1 ) ) ) -> ( M ... ( ( N - 1 ) + 1 ) ) = ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
27 15 25 26 syl2anc 
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) )
28 5 zcnd 
 |-  ( ph -> N e. CC )
29 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
30 28 19 29 sylancl 
 |-  ( ph -> ( ( N - 1 ) + 1 ) = N )
31 30 oveq2d 
 |-  ( ph -> ( M ... ( ( N - 1 ) + 1 ) ) = ( M ... N ) )
32 27 31 eqtr3d 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) = ( M ... N ) )
33 30 sneqd 
 |-  ( ph -> { ( ( N - 1 ) + 1 ) } = { N } )
34 33 uneq2d 
 |-  ( ph -> ( ( M ... ( N - 1 ) ) u. { ( ( N - 1 ) + 1 ) } ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
35 32 34 eqtr3d 
 |-  ( ph -> ( M ... N ) = ( ( M ... ( N - 1 ) ) u. { N } ) )
36 fzfid 
 |-  ( ph -> ( M ... N ) e. Fin )
37 13 35 36 2 fsumsplit 
 |-  ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. { N } A ) )
38 3 eleq1d 
 |-  ( k = N -> ( A e. CC <-> B e. CC ) )
39 2 ralrimiva 
 |-  ( ph -> A. k e. ( M ... N ) A e. CC )
40 eluzfz2 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ( M ... N ) )
41 1 40 syl 
 |-  ( ph -> N e. ( M ... N ) )
42 38 39 41 rspcdva 
 |-  ( ph -> B e. CC )
43 3 sumsn 
 |-  ( ( N e. ( ZZ>= ` M ) /\ B e. CC ) -> sum_ k e. { N } A = B )
44 1 42 43 syl2anc 
 |-  ( ph -> sum_ k e. { N } A = B )
45 44 oveq2d 
 |-  ( ph -> ( sum_ k e. ( M ... ( N - 1 ) ) A + sum_ k e. { N } A ) = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )
46 37 45 eqtrd 
 |-  ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... ( N - 1 ) ) A + B ) )