Theorem binomlem2 7067

Description: Lemma for binom 7072 (binomial theorem). Shift up the summation index with fsumshft 7031, then break out and simplify the last term of the summation.

Hypotheses

Ref	Expression
binomlem.1	|- A e. CC
binomlem.2	|- B e. CC

Assertion

Ref	Expression
binomlem2	|- (N e. NN -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = (sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) + (B^(N + 1))))

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

Proof of Theorem binomlem2

Step	Hyp	Ref	Expression
1		nnnn0t 6106	. . 3 |- (N e. NN -> N e. NN0)
2		binomlem.2	. . . . . . 7 |- B e. CC
3		fsummulc2 7034	. . . . . . 7 |- ((N e. (ZZ>` 0) /\ B e. CC /\ A.k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC) -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. B))
4	2, 3	mp3an2 904	. . . . . 6 |- ((N e. (ZZ>` 0) /\ A.k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC) -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. B))
5		elnn0uz 6441	. . . . . . 7 |- (N e. NN0 <-> N e. (ZZ>` 0))
6	5	biimp 151	. . . . . 6 |- (N e. NN0 -> N e. (ZZ>` 0))
7		axmulcl 5273	. . . . . . . 8 |- (((N C. k) e. CC /\ ((A^(N - k)) x. (B^k)) e. CC) -> ((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
8		bcclt 6972	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. NN0)
9		nn0cnt 6109	. . . . . . . . . 10 |- ((N C. k) e. NN0 -> (N C. k) e. CC)
10	8, 9	syl 10	. . . . . . . . 9 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. CC)
11		elfzelz 6482	. . . . . . . . 9 |- (k e. (0...N) -> k e. ZZ)
12	10, 11	sylan2 451	. . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (N C. k) e. CC)
13		axmulcl 5273	. . . . . . . . 9 |- (((A^(N - k)) e. CC /\ (B^k) e. CC) -> ((A^(N - k)) x. (B^k)) e. CC)
14		fznn0subt 6498	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (N - k) e. NN0)
15		binomlem.1	. . . . . . . . . . 11 |- A e. CC
16		expclt 6581	. . . . . . . . . . 11 |- ((A e. CC /\ (N - k) e. NN0) -> (A^(N - k)) e. CC)
17	15, 16	mpan 695	. . . . . . . . . 10 |- ((N - k) e. NN0 -> (A^(N - k)) e. CC)
18	14, 17	syl 10	. . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (A^(N - k)) e. CC)
19		elfznn0t 6496	. . . . . . . . . . 11 |- (k e. (0...N) -> k e. NN0)
20		expclt 6581	. . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
21	2, 20	mpan 695	. . . . . . . . . . 11 |- (k e. NN0 -> (B^k) e. CC)
22	19, 21	syl 10	. . . . . . . . . 10 |- (k e. (0...N) -> (B^k) e. CC)
23	22	adantl 388	. . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (B^k) e. CC)
24	13, 18, 23	sylanc 471	. . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^(N - k)) x. (B^k)) e. CC)
25	7, 12, 24	sylanc 471	. . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> ((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
26	25	r19.21aiva 1714	. . . . . 6 |- (N e. NN0 -> A.k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
27	4, 6, 26	sylanc 471	. . . . 5 |- (N e. NN0 -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. B))
28		axmulass 5278	. . . . . . . . 9 |- (((N C. k) e. CC /\ ((A^(N - k)) x. (B^k)) e. CC /\ B e. CC) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. B)))
29	2, 28	mp3an3 905	. . . . . . . 8 |- (((N C. k) e. CC /\ ((A^(N - k)) x. (B^k)) e. CC) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. B)))
30	29, 12, 24	sylanc 471	. . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. B)))
31		axmulass 5278	. . . . . . . . . . 11 |- (((A^(N - k)) e. CC /\ (B^k) e. CC /\ B e. CC) -> (((A^(N - k)) x. (B^k)) x. B) = ((A^(N - k)) x. ((B^k) x. B)))
32	2, 31	mp3an3 905	. . . . . . . . . 10 |- (((A^(N - k)) e. CC /\ (B^k) e. CC) -> (((A^(N - k)) x. (B^k)) x. B) = ((A^(N - k)) x. ((B^k) x. B)))
33	32, 18, 23	sylanc 471	. . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (((A^(N - k)) x. (B^k)) x. B) = ((A^(N - k)) x. ((B^k) x. B)))
34		expp1t 6574	. . . . . . . . . . . . 13 |- ((B e. CC /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
35	2, 34	mpan 695	. . . . . . . . . . . 12 |- (k e. NN0 -> (B^(k + 1)) = ((B^k) x. B))
36	19, 35	syl 10	. . . . . . . . . . 11 |- (k e. (0...N) -> (B^(k + 1)) = ((B^k) x. B))
37	36	adantl 388	. . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (B^(k + 1)) = ((B^k) x. B))
38	37	opreq2d 3976	. . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^(N - k)) x. (B^(k + 1))) = ((A^(N - k)) x. ((B^k) x. B)))
39	33, 38	eqtr4d 1510	. . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (((A^(N - k)) x. (B^k)) x. B) = ((A^(N - k)) x. (B^(k + 1))))
40	39	opreq2d 3976	. . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> ((N C. k) x. (((A^(N - k)) x. (B^k)) x. B)) = ((N C. k) x. ((A^(N - k)) x. (B^(k + 1)))))
41	30, 40	eqtrd 1507	. . . . . 6 |- ((N e. NN0 /\ k e. (0...N)) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = ((N C. k) x. ((A^(N - k)) x. (B^(k + 1)))))
42	41	sumeq2dv 6992	. . . . 5 |- (N e. NN0 -> sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^(k + 1)))))
43	27, 42	eqtrd 1507	. . . 4 |- (N e. NN0 -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. B) = sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^(k + 1)))))
44		1z 6159	. . . . . . 7 |- 1 e. ZZ
45		fsumshft 7031	. . . . . . 7 |- ((N e. (ZZ>` 0) /\ 1 e. ZZ /\ A.j e. (0...N)((N C. j) x. ((A^(N - j)) x. (B^(j + 1)))) e.