Theorem fsumconst 6976

Description: The sum of constant terms (k is not free in A).

Assertion

Ref	Expression
fsumconst	|- ((N e. (ZZ>` M) /\ A e. CC) -> sum_k e. (M...N)A = (((N - M) + 1) x. A))

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

Proof of Theorem fsumconst

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . . 6 |- (j = M -> (M...j) = (M...M))
2	1	sumeq1d 6928	. . . . 5 |- (j = M -> sum_k e. (M...j)A = sum_k e. (M...M)A)
3		opreq1 3953	. . . . . . 7 |- (j = M -> (j - M) = (M - M))
4	3	opreq1d 3960	. . . . . 6 |- (j = M -> ((j - M) + 1) = ((M - M) + 1))
5	4	opreq1d 3960	. . . . 5 |- (j = M -> (((j - M) + 1) x. A) = (((M - M) + 1) x. A))
6	2, 5	eqeq12d 1481	. . . 4 |- (j = M -> (sum_k e. (M...j)A = (((j - M) + 1) x. A) <-> sum_k e. (M...M)A = (((M - M) + 1) x. A)))
7	6	imbi2d 610	. . 3 |- (j = M -> ((A e. CC -> sum_k e. (M...j)A = (((j - M) + 1) x. A)) <-> (A e. CC -> sum_k e. (M...M)A = (((M - M) + 1) x. A))))
8		opreq2 3954	. . . . . 6 |- (j = m -> (M...j) = (M...m))
9	8	sumeq1d 6928	. . . . 5 |- (j = m -> sum_k e. (M...j)A = sum_k e. (M...m)A)
10		opreq1 3953	. . . . . . 7 |- (j = m -> (j - M) = (m - M))
11	10	opreq1d 3960	. . . . . 6 |- (j = m -> ((j - M) + 1) = ((m - M) + 1))
12	11	opreq1d 3960	. . . . 5 |- (j = m -> (((j - M) + 1) x. A) = (((m - M) + 1) x. A))
13	9, 12	eqeq12d 1481	. . . 4 |- (j = m -> (sum_k e. (M...j)A = (((j - M) + 1) x. A) <-> sum_k e. (M...m)A = (((m - M) + 1) x. A)))
14	13	imbi2d 610	. . 3 |- (j = m -> ((A e. CC -> sum_k e. (M...j)A = (((j - M) + 1) x. A)) <-> (A e. CC -> sum_k e. (M...m)A = (((m - M) + 1) x. A))))
15		opreq2 3954	. . . . . 6 |- (j = (m + 1) -> (M...j) = (M...(m + 1)))
16	15	sumeq1d 6928	. . . . 5 |- (j = (m + 1) -> sum_k e. (M...j)A = sum_k e. (M...(m + 1))A)
17		opreq1 3953	. . . . . . 7 |- (j = (m + 1) -> (j - M) = ((m + 1) - M))
18	17	opreq1d 3960	. . . . . 6 |- (j = (m + 1) -> ((j - M) + 1) = (((m + 1) - M) + 1))
19	18	opreq1d 3960	. . . . 5 |- (j = (m + 1) -> (((j - M) + 1) x. A) = ((((m + 1) - M) + 1) x. A))
20	16, 19	eqeq12d 1481	. . . 4 |- (j = (m + 1) -> (sum_k e. (M...j)A = (((j - M) + 1) x. A) <-> sum_k e. (M...(m + 1))A = ((((m + 1) - M) + 1) x. A)))
21	20	imbi2d 610	. . 3 |- (j = (m + 1) -> ((A e. CC -> sum_k e. (M...j)A = (((j - M) + 1) x. A)) <-> (A e. CC -> sum_k e. (M...(m + 1))A = ((((m + 1) - M) + 1) x. A))))
22		opreq2 3954	. . . . . 6 |- (j = N -> (M...j) = (M...N))
23	22	sumeq1d 6928	. . . . 5 |- (j = N -> sum_k e. (M...j)A = sum_k e. (M...N)A)
24		opreq1 3953	. . . . . . 7 |- (j = N -> (j - M) = (N - M))
25	24	opreq1d 3960	. . . . . 6 |- (j = N -> ((j - M) + 1) = ((N - M) + 1))
26	25	opreq1d 3960	. . . . 5 |- (j = N -> (((j - M) + 1) x. A) = (((N - M) + 1) x. A))
27	23, 26	eqeq12d 1481	. . . 4 |- (j = N -> (sum_k e. (M...j)A = (((j - M) + 1) x. A) <-> sum_k e. (M...N)A = (((N - M) + 1) x. A)))
28	27	imbi2d 610	. . 3 |- (j = N -> ((A e. CC -> sum_k e. (M...j)A = (((j - M) + 1) x. A)) <-> (A e. CC -> sum_k e. (M...N)A = (((N - M) + 1) x. A))))
29		eqid 1468	. . . . . . . 8 |- A = A
30	29	a1i 8	. . . . . . 7 |- (k = M -> A = A)
31	30	fsum1 6943	. . . . . 6 |- ((A e. CC /\ M e. ZZ) -> sum_k e. (M...M)A = A)
32	31	ancoms 436	. . . . 5 |- ((M e. ZZ /\ A e. CC) -> sum_k e. (M...M)A = A)
33		subidt 5367	. . . . . . . . . 10 |- (M e. CC -> (M - M) = 0)
34	33	opreq1d 3960	. . . . . . . . 9 |- (M e. CC -> ((M - M) + 1) = (0 + 1))
35		ax1cn 5241	. . . . . . . . . 10 |- 1 e. CC
36	35	addid2 5303	. . . . . . . . 9 |- (0 + 1) = 1
37	34, 36	syl6eq 1515	. . . . . . . 8 |- (M e. CC -> ((M - M) + 1) = 1)
38	37	opreq1d 3960	. . . . . . 7 |- (M e. CC -> (((M - M) + 1) x. A) = (1 x. A))
39		mulid2t 5389	. . . . . . 7 |- (A e. CC -> (1 x. A) = A)
40	38, 39	sylan9eq 1519	. . . . . 6 |- ((M e. CC /\ A e. CC) -> (((M - M) + 1) x. A) = A)
41		zcnt 6087	. . . . . 6 |- (M e. ZZ -> M e. CC)
42	40, 41	sylan 448	. . . . 5 |- ((M e. ZZ /\ A e. CC) -> (((M - M) + 1) x. A) = A)
43	32, 42	eqtr4d 1502	. . . 4 |- ((M e. ZZ /\ A e. CC) -> sum_k e. (M...M)A = (((M - M) + 1) x. A))
44	43	ex 373	. . 3 |- (M e. ZZ -> (A e. CC -> sum_k e. (M...M)A = (((M - M) + 1) x. A)))
45		fsump1s 6951	. . . . . . . . 9 |- ((m e. (ZZ>` M) /\ A.k e. (M...(m + 1))A e. CC) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
46		ax-1 4	. . . . . . . . . 10 |- (A e. CC -> (k e. (M...(m + 1)) -> A e. CC))
47	46	r19.21aiv 1705	. . . . . . . . 9 |- (A e. CC -> A.k e. (M...(m + 1))A e. CC)
48	45, 47	sylan2 451	. . . . . . . 8 |- ((m e. (ZZ>` M) /\ A e. CC) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + [_(m + 1) / k]_A))
49		oprex 3968	. . . . . . . . . 10 |- (m + 1) e. V
50		ax-17 968	. . . . . . . . . . 11 |- (j e. A -> A.k j e. A)
51	50	csbconstgf 2000	. . . . . . . . . 10 |- ((m + 1) e. V -> [_(m + 1) / k]_A = A)
52	49, 51	ax-mp 7	. . . . . . . . 9 |- [_(m + 1) / k]_A = A
53	52	opreq2i 3957	. . . . . . . 8 |- (sum_k e. (M...m)A + [_(m + 1) / k]_A) = (sum_k e. (M...m)A + A)
54	48, 53	syl6eq 1515	. . . . . . 7 |- ((m e. (ZZ>` M) /\ A e. CC) -> sum_k e. (M...(m + 1))A = (sum_k e. (M...m)A + A))
55		opreq1 3953	. . . . . . 7 |- (sum_k e. (M...m)A = (((m - M) + 1) x. A) -> (sum_k e. (M...m)A + A) = ((((m - M) + 1) x. A) + A))
56	54, 55	sylan9eq 1519	. . . . . 6 |- (((m e. (ZZ>` M) /\ A e. CC) /\ sum_k e. (M...m)A = (((m - M) + 1) x. A)) -> sum_k e. (M...(m + 1))A = ((((m - M) + 1) x. A) + A))
57		addsubt 5356	. . . . . . . . . . . . 13 |- ((m e. CC /\ 1 e. CC /\ M e. CC) -> ((m + 1) - M) = ((m - M) + 1))
58	35, 57	mp3an2 901	. . . . . . . . . . . 12 |- ((m e. CC /\ M e. CC) -> ((m + 1) - M) = ((m - M) + 1))
59	58	adantr 389	. . . . . . . . . . 11 |- (((m e. CC /\ M e. CC) /\ A e. CC) -> ((m + 1) - M) = ((m - M) + 1))
60	59	opreq1d 3960	. . . . . . . . . 10 |- (((m e. CC /\ M e. CC) /\ A e. CC) -> (((m + 1) - M) + 1) = (((m - M) + 1) + 1))
61	60	opreq1d 3960	. . . . . . . . 9 |- (((m e. CC /\ M e. CC) /\ A e. CC) -> ((((m + 1) - M) + 1) x. A) =