Theorem fsumadd 6911

Description: The sum of two finite sums.

Assertion

Ref	Expression
fsumadd	|- ((N e. (ZZ>` M) /\ A.k e. (M...N)(A e. CC /\ B e. CC)) -> sum_k e. (M...N)(A + B) = (sum_k e. (M...N)A + sum_k e. (M...N)B))

Distinct variable groups:   k,M   k,N

Proof of Theorem fsumadd

Step	Hyp	Ref	Expression
1		opreq2 3908	. . . . 5 |- (j = M -> (M...j) = (M...M))
2	1	raleq1d 1765	. . . 4 |- (j = M -> (A.k e. (M...j)(A e. CC /\ B e. CC) <-> A.k e. (M...M)(A e. CC /\ B e. CC)))
3	1	sumeq1d 6879	. . . . 5 |- (j = M -> sum_k e. (M...j)(A + B) = sum_k e. (M...M)(A + B))
4	1	sumeq1d 6879	. . . . . 6 |- (j = M -> sum_k e. (M...j)A = sum_k e. (M...M)A)
5	1	sumeq1d 6879	. . . . . 6 |- (j = M -> sum_k e. (M...j)B = sum_k e. (M...M)B)
6	4, 5	opreq12d 3917	. . . . 5 |- (j = M -> (sum_k e. (M...j)A + sum_k e. (M...j)B) = (sum_k e. (M...M)A + sum_k e. (M...M)B))
7	3, 6	eqeq12d 1465	. . . 4 |- (j = M -> (sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B) <-> sum_k e. (M...M)(A + B) = (sum_k e. (M...M)A + sum_k e. (M...M)B)))
8	2, 7	imbi12d 624	. . 3 |- (j = M -> ((A.k e. (M...j)(A e. CC /\ B e. CC) -> sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B)) <-> (A.k e. (M...M)(A e. CC /\ B e. CC) -> sum_k e. (M...M)(A + B) = (sum_k e. (M...M)A + sum_k e. (M...M)B))))
9		opreq2 3908	. . . . 5 |- (j = m -> (M...j) = (M...m))
10	9	raleq1d 1765	. . . 4 |- (j = m -> (A.k e. (M...j)(A e. CC /\ B e. CC) <-> A.k e. (M...m)(A e. CC /\ B e. CC)))
11	9	sumeq1d 6879	. . . . 5 |- (j = m -> sum_k e. (M...j)(A + B) = sum_k e. (M...m)(A + B))
12	9	sumeq1d 6879	. . . . . 6 |- (j = m -> sum_k e. (M...j)A = sum_k e. (M...m)A)
13	9	sumeq1d 6879	. . . . . 6 |- (j = m -> sum_k e. (M...j)B = sum_k e. (M...m)B)
14	12, 13	opreq12d 3917	. . . . 5 |- (j = m -> (sum_k e. (M...j)A + sum_k e. (M...j)B) = (sum_k e. (M...m)A + sum_k e. (M...m)B))
15	11, 14	eqeq12d 1465	. . . 4 |- (j = m -> (sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B) <-> sum_k e. (M...m)(A + B) = (sum_k e. (M...m)A + sum_k e. (M...m)B)))
16	10, 15	imbi12d 624	. . 3 |- (j = m -> ((A.k e. (M...j)(A e. CC /\ B e. CC) -> sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B)) <-> (A.k e. (M...m)(A e. CC /\ B e. CC) -> sum_k e. (M...m)(A + B) = (sum_k e. (M...m)A + sum_k e. (M...m)B))))
17		opreq2 3908	. . . . 5 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
18	17	raleq1d 1765	. . . 4 |- (j = (m + 1) -> (A.k e. (M...j)(A e. CC /\ B e. CC) <-> A.k e. (M...(m + 1))(A e. CC /\ B e. CC)))
19	17	sumeq1d 6879	. . . . 5 |- (j = (m + 1) -> sum_k e. (M...j)(A + B) = sum_k e. (M...(m + 1))(A + B))
20	17	sumeq1d 6879	. . . . . 6 |- (j = (m + 1) -> sum_k e. (M...j)A = sum_k e. (M...(m + 1))A)
21	17	sumeq1d 6879	. . . . . 6 |- (j = (m + 1) -> sum_k e. (M...j)B = sum_k e. (M...(m + 1))B)
22	20, 21	opreq12d 3917	. . . . 5 |- (j = (m + 1) -> (sum_k e. (M...j)A + sum_k e. (M...j)B) = (sum_k e. (M...(m + 1))A + sum_k e. (M...(m + 1))B))
23	19, 22	eqeq12d 1465	. . . 4 |- (j = (m + 1) -> (sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B) <-> sum_k e. (M...(m + 1))(A + B) = (sum_k e. (M...(m + 1))A + sum_k e. (M...(m + 1))B)))
24	18, 23	imbi12d 624	. . 3 |- (j = (m + 1) -> ((A.k e. (M...j)(A e. CC /\ B e. CC) -> sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B)) <-> (A.k e. (M...(m + 1))(A e. CC /\ B e. CC) -> sum_k e. (M...(m + 1))(A + B) = (sum_k e. (M...(m + 1))A + sum_k e. (M...(m + 1))B))))
25		opreq2 3908	. . . . 5 |- (j = N -> (M...j) = (M...N))
26	25	raleq1d 1765	. . . 4 |- (j = N -> (A.k e. (M...j)(A e. CC /\ B e. CC) <-> A.k e. (M...N)(A e. CC /\ B e. CC)))
27	25	sumeq1d 6879	. . . . 5 |- (j = N -> sum_k e. (M...j)(A + B) = sum_k e. (M...N)(A + B))
28	25	sumeq1d 6879	. . . . . 6 |- (j = N -> sum_k e. (M...j)A = sum_k e. (M...N)A)
29	25	sumeq1d 6879	. . . . . 6 |- (j = N -> sum_k e. (M...j)B = sum_k e. (M...N)B)
30	28, 29	opreq12d 3917	. . . . 5 |- (j = N -> (sum_k e. (M...j)A + sum_k e. (M...j)B) = (sum_k e. (M...N)A + sum_k e. (M...N)B))
31	27, 30	eqeq12d 1465	. . . 4 |- (j = N -> (sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B) <-> sum_k e. (M...N)(A + B) = (sum_k e. (M...N)A + sum_k e. (M...N)B)))
32	26, 31	imbi12d 624	. . 3 |- (j = N -> ((A.k e. (M...j)(A e. CC /\ B e. CC) -> sum_k e. (M...j)(A + B) = (sum_k e. (M...j)A + sum_k e. (M...j)B)) <-> (A.k e. (M...N)(A e. CC /\ B e. CC) -> sum_k e. (M...N)(A + B) = (sum_k e. (M...N)A + sum_k e. (M...N)B))))
33		csbopr12g 3926	. . . . . 6 |- (M e. ZZ -> [_M / k]_(A + B) = ([_M / k]_A + [_M / k]_B))
34	33	adantr 389	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. CC /\ B e. CC)) -> [_M / k]_(A + B) = ([_M / k]_A + [_M / k]_B))
35		fsum1s 6898	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A + B) e. CC) -> sum_k e. (M...M)(A + B) = [_M / k]_(A + B))
36		axaddcl 5194	. . . . . . 7 |- ((A e. CC /\ B e. CC) -> (A + B) e. CC)
37	36	r19.20si 1682	. . . . . 6 |- (A.k e. (M...M)(A e. CC /\ B e. CC) -> A.k e. (M...M)(A + B) e. CC)
38	35, 37	sylan2 451	. . . . 5 |- ((M e. ZZ /\ A.k e. (M...M)(A e. CC /\ B e. CC)) -> sum_k e. (M...M)(A + B) = [_M / k]_(A + B))
39		fsum1s 6898	. . . . . . 7 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> sum_k e. (M...M)A = [_M / k]_A)
40		pm3.26 319	. . . . . . . 8 |- ((A e. CC /\ B e. CC) -> A e. CC)
41	40	r19.20si 1682	. . . . . . 7 |- (A.k e. (M...M)(A e. CC /\ B e. CC) -> A.k e. (M...M)A e. CC)
42	39, 41	sylan2 451	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(A e. CC