Metamath Proof Explorer


Theorem fzosumm1

Description: Separate out the last term in a finite sum. (Contributed by Steven Nguyen, 22-Aug-2023)

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

Proof

Step Hyp Ref Expression
1 fzosumm1.1
 |-  ( ph -> ( N - 1 ) e. ( ZZ>= ` M ) )
2 fzosumm1.2
 |-  ( ( ph /\ k e. ( M ..^ N ) ) -> A e. CC )
3 fzosumm1.3
 |-  ( k = ( N - 1 ) -> A = B )
4 fzosumm1.n
 |-  ( ph -> N e. ZZ )
5 fzoval
 |-  ( N e. ZZ -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
6 4 5 syl
 |-  ( ph -> ( M ..^ N ) = ( M ... ( N - 1 ) ) )
7 6 eqcomd
 |-  ( ph -> ( M ... ( N - 1 ) ) = ( M ..^ N ) )
8 7 eleq2d
 |-  ( ph -> ( k e. ( M ... ( N - 1 ) ) <-> k e. ( M ..^ N ) ) )
9 8 biimpa
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> k e. ( M ..^ N ) )
10 9 2 syldan
 |-  ( ( ph /\ k e. ( M ... ( N - 1 ) ) ) -> A e. CC )
11 1 10 3 fsumm1
 |-  ( ph -> sum_ k e. ( M ... ( N - 1 ) ) A = ( sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A + B ) )
12 6 sumeq1d
 |-  ( ph -> sum_ k e. ( M ..^ N ) A = sum_ k e. ( M ... ( N - 1 ) ) A )
13 eluzelz
 |-  ( ( N - 1 ) e. ( ZZ>= ` M ) -> ( N - 1 ) e. ZZ )
14 fzoval
 |-  ( ( N - 1 ) e. ZZ -> ( M ..^ ( N - 1 ) ) = ( M ... ( ( N - 1 ) - 1 ) ) )
15 1 13 14 3syl
 |-  ( ph -> ( M ..^ ( N - 1 ) ) = ( M ... ( ( N - 1 ) - 1 ) ) )
16 15 sumeq1d
 |-  ( ph -> sum_ k e. ( M ..^ ( N - 1 ) ) A = sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A )
17 16 oveq1d
 |-  ( ph -> ( sum_ k e. ( M ..^ ( N - 1 ) ) A + B ) = ( sum_ k e. ( M ... ( ( N - 1 ) - 1 ) ) A + B ) )
18 11 12 17 3eqtr4d
 |-  ( ph -> sum_ k e. ( M ..^ N ) A = ( sum_ k e. ( M ..^ ( N - 1 ) ) A + B ) )