Theorem fsummulc1 7156

Description: A finite sum multiplied by a constant.

Assertion

Ref	Expression
fsummulc1	|- ((N e. (ZZ>` M) /\ C e. CC /\ A.k e. (M...N)A e. CC) -> (C x. sum_k e. (M...N)A) = sum_k e. (M...N)(C x. A))

Distinct variable groups:   C,k   k,M   k,N

Proof of Theorem fsummulc1

Step	Hyp	Ref	Expression
1		csbopr2g 4065	. . . . . 6 |- (M e. ZZ -> [_M / k]_(C x. A) = (C x. [_M / k]_A))
2	1	adantr 389	. . . . 5 |- ((M e. ZZ /\ (C e. CC /\ A.k e. (M...M)A e. CC)) -> [_M / k]_(C x. A) = (C x. [_M / k]_A))
3		fsum1s 7132	. . . . . 6 |- ((M e. ZZ /\ A.k e. (M...M)(C x. A) e. CC) -> sum_k e. (M...M)(C x. A) = [_M / k]_(C x. A))
4		r19.28av 1793	. . . . . . 7 |- ((C e. CC /\ A.k e. (M...M)A e. CC) -> A.k e. (M...M)(C e. CC /\ A e. CC))
5		mulcl 5392	. . . . . . . 8 |- ((C e. CC /\ A e. CC) -> (C x. A) e. CC)
6	5	r19.20si 1744	. . . . . . 7 |- (A.k e. (M...M)(C e. CC /\ A e. CC) -> A.k e. (M...M)(C x. A) e. CC)
7	4, 6	syl 10	. . . . . 6 |- ((C e. CC /\ A.k e. (M...M)A e. CC) -> A.k e. (M...M)(C x. A) e. CC)
8	3, 7	sylan2 453	. . . . 5 |- ((M e. ZZ /\ (C e. CC /\ A.k e. (M...M)A e. CC)) -> sum_k e. (M...M)(C x. A) = [_M / k]_(C x. A))
9		fsum1s 7132	. . . . . . 7 |- ((M e. ZZ /\ A.k e. (M...M)A e. CC) -> sum_k e. (M...M)A = [_M / k]_A)
10	9	adantrl 394	. . . . . 6 |- ((M e. ZZ /\ (C e. CC /\ A.k e. (M...M)A e. CC)) -> sum_k e. (M...M)A = [_M / k]_A)
11	10	opreq2d 4052	. . . . 5 |- ((M e. ZZ /\ (C e. CC /\ A.k e. (M...M)A e. CC)) -> (C x. sum_k e. (M...M)A) = (C x. [_M / k]_A))
12	2, 8, 11	3eqtr4rd 1555	. . . 4 |- ((M e. ZZ /\ (C e. CC /\ A.k e. (M...M)A e. CC)) -> (C x. sum_k e. (M...M)A) = sum_k e. (M...M)(C x. A))
13	12	ex 371	. . 3 |- (M e. ZZ -> ((C e. CC /\ A.k e. (M...M)A e. CC) -> (C x. sum_k e. (M...M)A) = sum_k e. (M...M)(C x. A)))
14		fzssp1 6566	. . . . . . . . . 10 |- ((M e. ZZ /\ m e. ZZ) -> (M...m) (_ (M...(m + 1)))
15		eluzel2 6484	. . . . . . . . . 10 |- (m e. (ZZ>` M) -> M e. ZZ)
16		eluzelz 6483	. . . . . . . . . 10 |- (m e. (ZZ>` M) -> m e. ZZ)
17	14, 15, 16	sylanc 473	. . . . . . . . 9 |- (m e. (ZZ>` M) -> (M...m) (_ (M...(m + 1)))
18	17	sseld 2111	. . . . . . . 8 |- (m e. (ZZ>` M) -> (k e. (M...m) -> k e. (M...(m + 1))))
19	18	imim1d 28	. . . . . . 7 |- (m e. (ZZ>` M) -> ((k e. (M...(m + 1)) -> A e. CC) -> (k e. (M...m) -> A e. CC)))
20	19	r19.20dv2 1749	. . . . . 6 |- (m e. (ZZ>` M) -> (A.k e. (M...(m + 1))A e. CC -> A.k e. (M...m)A e. CC))
21	20	anim2d 563	. . . . 5 |- (m e. (ZZ>` M) -> ((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C e. CC /\ A.k e. (M...m)A e. CC)))
22	21	imim1d 28	. . . 4 |- (m e. (ZZ>` M) -> (((C e. CC /\ A.k e. (M...m)A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A)) -> ((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A))))
23		adddi 5398	. . . . . . . . 9 |- ((C e. CC /\ sum_k e. (M...m)A e. CC /\ [_(m + 1) / k]_A e. CC) -> (C x. (sum_k e. (M...m)A + [_(m + 1) / k]_A)) = ((C x. sum_k e. (M...m)A) + (C x. [_(m + 1) / k]_A)))
24		simprl 414	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> C e. CC)
25	20	imp 348	. . . . . . . . . . 11 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. CC) -> A.k e. (M...m)A e. CC)
26		fsumcl 7138	. . . . . . . . . . 11 |- ((m e. (ZZ>` M) /\ A.k e. (M...m)A e. CC) -> sum_k e. (M...m)A e. CC)
27	25, 26	syldan 469	. . . . . . . . . 10 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. CC) -> sum_k e. (M...m)A e. CC)
28	27	adantrl 394	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> sum_k e. (M...m)A e. CC)
29		ra4csbela 2086	. . . . . . . . . . 11 |- (((m + 1) e. (M...(m + 1)) /\ A.k e. (M...(m + 1))A e. CC) -> [_(m + 1) / k]_A e. CC)
30		peano2uz 6507	. . . . . . . . . . . 12 |- (m e. (ZZ>` M) -> (m + 1) e. (ZZ>` M))
31		eluzfz2 6549	. . . . . . . . . . . 12 |- ((m + 1) e. (ZZ>` M) -> (m + 1) e. (M...(m + 1)))
32	30, 31	syl 10	. . . . . . . . . . 11 |- (m e. (ZZ>` M) -> (m + 1) e. (M...(m + 1)))
33	29, 32	sylan 450	. . . . . . . . . 10 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. CC) -> [_(m + 1) / k]_A e. CC)
34	33	adantrl 394	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> [_(m + 1) / k]_A e. CC)
35	23, 24, 28, 34	syl3anc 861	. . . . . . . 8 |- ((m e. (ZZ>` M) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> (C x. (sum_k e. (M...m)A + [_(m + 1) / k]_A)) = ((C x. sum_k e. (M...m)A) + (C x. [_(m + 1) / k]_A)))
36	35	adantlr 393	. . . . . . 7 |- (((m e. (ZZ>` M) /\ ((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A))) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> (C x. (sum_k e. (M...m)A + [_(m + 1) / k]_A)) = ((C x. sum_k e. (M...m)A) + (C x. [_(m + 1) / k]_A)))
37		id 59	. . . . . . . . . 10 |- (((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A)) -> ((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A)))
38	37	imp 348	. . . . . . . . 9 |- ((((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A)) /\ (C e. CC /\ A.k e. (M...(m + 1))A e. CC)) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m)(C x. A))
39		oprex 4059	. . . . . . . . . . . 12 |- (m + 1) e. V
40		csbopr2g 4065	. . . . . . . . . . . 12 |- ((m + 1) e. V -> [_(m + 1) / k]_(C x. A) = (C x. [_(m + 1) / k]_A))
41	39, 40	ax-mp 7	. . . . . . . . . . 11 |- [_(m + 1) / k]_(C x. A) = (C x. [_(m + 1) / k]_A)
42	41	eqcomi 1516	. . . . . . . . . 10 |- (C x. [_(m + 1) / k]_A) = [_(m + 1) / k]_(C x. A)
43	42	a1i 8	. . . . . . . . 9 |- ((((C e. CC /\ A.k e. (M...(m + 1))A e. CC) -> (C x. sum_k e. (M...m)A) = sum_k e. (M...m