Theorem fsump1i

Description: Optimized version of fsump1 for making sums of a concrete number of terms. (Contributed by Mario Carneiro, 23-Apr-2014)

	Ref	Expression
Hypotheses	fsump1i.1	|- Z = ( ZZ>= ` M )
	fsump1i.2	|- N = ( K + 1 )
	fsump1i.3	|- ( k = N -> A = B )
	fsump1i.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
	fsump1i.5	|- ( ph -> ( K e. Z /\ sum_ k e. ( M ... K ) A = S ) )
	fsump1i.6	|- ( ph -> ( S + B ) = T )
Assertion	fsump1i	|- ( ph -> ( N e. Z /\ sum_ k e. ( M ... N ) A = T ) )

Proof

Step	Hyp	Ref	Expression
1		fsump1i.1	|- Z = ( ZZ>= ` M )
2		fsump1i.2	|- N = ( K + 1 )
3		fsump1i.3	|- ( k = N -> A = B )
4		fsump1i.4	|- ( ( ph /\ k e. Z ) -> A e. CC )
5		fsump1i.5	|- ( ph -> ( K e. Z /\ sum_ k e. ( M ... K ) A = S ) )
6		fsump1i.6	|- ( ph -> ( S + B ) = T )
7	5	simpld	|- ( ph -> K e. Z )
8	7 1	eleqtrdi	|- ( ph -> K e. ( ZZ>= ` M ) )
9		peano2uz	|- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. ( ZZ>= ` M ) )
10	9 1	eleqtrrdi	|- ( K e. ( ZZ>= ` M ) -> ( K + 1 ) e. Z )
11	8 10	syl	|- ( ph -> ( K + 1 ) e. Z )
12	2 11	eqeltrid	|- ( ph -> N e. Z )
13	2	oveq2i	|- ( M ... N ) = ( M ... ( K + 1 ) )
14	13	sumeq1i	|- sum_ k e. ( M ... N ) A = sum_ k e. ( M ... ( K + 1 ) ) A
15		elfzuz	|- ( k e. ( M ... ( K + 1 ) ) -> k e. ( ZZ>= ` M ) )
16	15 1	eleqtrrdi	|- ( k e. ( M ... ( K + 1 ) ) -> k e. Z )
17	16 4	sylan2	|- ( ( ph /\ k e. ( M ... ( K + 1 ) ) ) -> A e. CC )
18	2	eqeq2i	|- ( k = N <-> k = ( K + 1 ) )
19	18 3	sylbir	|- ( k = ( K + 1 ) -> A = B )
20	8 17 19	fsump1	|- ( ph -> sum_ k e. ( M ... ( K + 1 ) ) A = ( sum_ k e. ( M ... K ) A + B ) )
21	14 20	eqtrid	|- ( ph -> sum_ k e. ( M ... N ) A = ( sum_ k e. ( M ... K ) A + B ) )
22	5	simprd	|- ( ph -> sum_ k e. ( M ... K ) A = S )
23	22	oveq1d	|- ( ph -> ( sum_ k e. ( M ... K ) A + B ) = ( S + B ) )
24	21 23 6	3eqtrd	|- ( ph -> sum_ k e. ( M ... N ) A = T )
25	12 24	jca	|- ( ph -> ( N e. Z /\ sum_ k e. ( M ... N ) A = T ) )