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