Theorem fsumsplit 7143

Description: Split a finite sum into two parts. Warning: The HTML proof page is 0.6 megabyte in size.

Assertion

Ref	Expression
fsumsplit	|- ((N e. ZZ /\ K e. (M...(N - 1)) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...K)A + sum_k e. ((K + 1)...N)A))

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumsplit

Step	Hyp	Ref	Expression
1		breq1 2672	. . . . . . . . 9 |- (j = M -> (j < N <-> M < N))
2	1	anbi2d 618	. . . . . . . 8 |- (j = M -> ((N e. ZZ /\ j < N) <-> (N e. ZZ /\ M < N)))
3	2	anbi1d 619	. . . . . . 7 |- (j = M -> (((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) <-> ((N e. ZZ /\ M < N) /\ A.k e. (M...N)A e. CC)))
4		opreq2 4045	. . . . . . . . . 10 |- (j = M -> (M...j) = (M...M))
5	4	sumeq1d 7113	. . . . . . . . 9 |- (j = M -> sum_k e. (M...j)A = sum_k e. (M...M)A)
6		opreq1 4044	. . . . . . . . . . 11 |- (j = M -> (j + 1) = (M + 1))
7	6	opreq1d 4051	. . . . . . . . . 10 |- (j = M -> ((j + 1)...N) = ((M + 1)...N))
8	7	sumeq1d 7113	. . . . . . . . 9 |- (j = M -> sum_k e. ((j + 1)...N)A = sum_k e. ((M + 1)...N)A)
9	5, 8	opreq12d 4054	. . . . . . . 8 |- (j = M -> (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) = (sum_k e. (M...M)A + sum_k e. ((M + 1)...N)A))
10	9	eqeq2d 1523	. . . . . . 7 |- (j = M -> (sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) <-> sum_k e. (M...N)A = (sum_k e. (M...M)A + sum_k e. ((M + 1)...N)A)))
11	3, 10	imbi12d 628	. . . . . 6 |- (j = M -> ((((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A)) <-> (((N e. ZZ /\ M < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...M)A + sum_k e. ((M + 1)...N)A))))
12		breq1 2672	. . . . . . . . 9 |- (j = m -> (j < N <-> m < N))
13	12	anbi2d 618	. . . . . . . 8 |- (j = m -> ((N e. ZZ /\ j < N) <-> (N e. ZZ /\ m < N)))
14	13	anbi1d 619	. . . . . . 7 |- (j = m -> (((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) <-> ((N e. ZZ /\ m < N) /\ A.k e. (M...N)A e. CC)))
15		opreq2 4045	. . . . . . . . . 10 |- (j = m -> (M...j) = (M...m))
16	15	sumeq1d 7113	. . . . . . . . 9 |- (j = m -> sum_k e. (M...j)A = sum_k e. (M...m)A)
17		opreq1 4044	. . . . . . . . . . 11 |- (j = m -> (j + 1) = (m + 1))
18	17	opreq1d 4051	. . . . . . . . . 10 |- (j = m -> ((j + 1)...N) = ((m + 1)...N))
19	18	sumeq1d 7113	. . . . . . . . 9 |- (j = m -> sum_k e. ((j + 1)...N)A = sum_k e. ((m + 1)...N)A)
20	16, 19	opreq12d 4054	. . . . . . . 8 |- (j = m -> (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) = (sum_k e. (M...m)A + sum_k e. ((m + 1)...N)A))
21	20	eqeq2d 1523	. . . . . . 7 |- (j = m -> (sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) <-> sum_k e. (M...N)A = (sum_k e. (M...m)A + sum_k e. ((m + 1)...N)A)))
22	14, 21	imbi12d 628	. . . . . 6 |- (j = m -> ((((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A)) <-> (((N e. ZZ /\ m < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...m)A + sum_k e. ((m + 1)...N)A))))
23		breq1 2672	. . . . . . . . 9 |- (j = (m + 1) -> (j < N <-> (m + 1) < N))
24	23	anbi2d 618	. . . . . . . 8 |- (j = (m + 1) -> ((N e. ZZ /\ j < N) <-> (N e. ZZ /\ (m + 1) < N)))
25	24	anbi1d 619	. . . . . . 7 |- (j = (m + 1) -> (((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) <-> ((N e. ZZ /\ (m + 1) < N) /\ A.k e. (M...N)A e. CC)))
26		opreq2 4045	. . . . . . . . . 10 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
27	26	sumeq1d 7113	. . . . . . . . 9 |- (j = (m + 1) -> sum_k e. (M...j)A = sum_k e. (M...(m + 1))A)
28		opreq1 4044	. . . . . . . . . . 11 |- (j = (m + 1) -> (j + 1) = ((m + 1) + 1))
29	28	opreq1d 4051	. . . . . . . . . 10 |- (j = (m + 1) -> ((j + 1)...N) = (((m + 1) + 1)...N))
30	29	sumeq1d 7113	. . . . . . . . 9 |- (j = (m + 1) -> sum_k e. ((j + 1)...N)A = sum_k e. (((m + 1) + 1)...N)A)
31	27, 30	opreq12d 4054	. . . . . . . 8 |- (j = (m + 1) -> (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) = (sum_k e. (M...(m + 1))A + sum_k e. (((m + 1) + 1)...N)A))
32	31	eqeq2d 1523	. . . . . . 7 |- (j = (m + 1) -> (sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) <-> sum_k e. (M...N)A = (sum_k e. (M...(m + 1))A + sum_k e. (((m + 1) + 1)...N)A)))
33	25, 32	imbi12d 628	. . . . . 6 |- (j = (m + 1) -> ((((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A)) <-> (((N e. ZZ /\ (m + 1) < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...(m + 1))A + sum_k e. (((m + 1) + 1)...N)A))))
34		breq1 2672	. . . . . . . . 9 |- (j = K -> (j < N <-> K < N))
35	34	anbi2d 618	. . . . . . . 8 |- (j = K -> ((N e. ZZ /\ j < N) <-> (N e. ZZ /\ K < N)))
36	35	anbi1d 619	. . . . . . 7 |- (j = K -> (((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) <-> ((N e. ZZ /\ K < N) /\ A.k e. (M...N)A e. CC)))
37		opreq2 4045	. . . . . . . . . 10 |- (j = K -> (M...j) = (M...K))
38	37	sumeq1d 7113	. . . . . . . . 9 |- (j = K -> sum_k e. (M...j)A = sum_k e. (M...K)A)
39		opreq1 4044	. . . . . . . . . . 11 |- (j = K -> (j + 1) = (K + 1))
40	39	opreq1d 4051	. . . . . . . . . 10 |- (j = K -> ((j + 1)...N) = ((K + 1)...N))
41	40	sumeq1d 7113	. . . . . . . . 9 |- (j = K -> sum_k e. ((j + 1)...N)A = sum_k e. ((K + 1)...N)A)
42	38, 41	opreq12d 4054	. . . . . . . 8 |- (j = K -> (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) = (sum_k e. (M...K)A + sum_k e. ((K + 1)...N)A))
43	42	eqeq2d 1523	. . . . . . 7 |- (j = K -> (sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A) <-> sum_k e. (M...N)A = (sum_k e. (M...K)A + sum_k e. ((K + 1)...N)A)))
44	36, 43	imbi12d 628	. . . . . 6 |- (j = K -> ((((N e. ZZ /\ j < N) /\ A.k e. (M...N)A e. CC) -> sum_k e. (M...N)A = (sum_k e. (M...j)A + sum_k e. ((j + 1)...N)A)) <-> (((N e. ZZ