Theorem binomlem5 7016

Description: Lemma for binom 7018 (binomial theorem). We use Pascal's rule bcpasct 6916 to combine the sum of the summations in binomlem1 7012 and binomlem2 7013 into a single summation.

Hypotheses

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

Assertion

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

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

Proof of Theorem binomlem5

Step	Hyp	Ref	Expression
1		axaddass 5257	. . . 4 |- (((A^(N + 1)) e. CC /\ sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC /\ (sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) + (B^(N + 1))) e. CC) -> (((A^(N + 1)) + sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k)))) + (sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) + (B^(N + 1)))) = ((A^(N + 1)) + (sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) + (sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) + (B^(N + 1))))))
2		peano2nn 5891	. . . . 5 |- (N e. NN -> (N + 1) e. NN)
3		binomlem.1	. . . . . 6 |- A e. CC
4		expclt 6521	. . . . . . 7 |- ((A e. CC /\ (N + 1) e. NN0) -> (A^(N + 1)) e. CC)
5		nnnn0t 6061	. . . . . . 7 |- ((N + 1) e. NN -> (N + 1) e. NN0)
6	4, 5	sylan2 451	. . . . . 6 |- ((A e. CC /\ (N + 1) e. NN) -> (A^(N + 1)) e. CC)
7	3, 6	mpan 694	. . . . 5 |- ((N + 1) e. NN -> (A^(N + 1)) e. CC)
8	2, 7	syl 10	. . . 4 |- (N e. NN -> (A^(N + 1)) e. CC)
9		axmulcl 5253	. . . . . . 7 |- (((N C. k) e. CC /\ ((A^((N + 1) - k)) x. (B^k)) e. CC) -> ((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
10		bcclt 6918	. . . . . . . . 9 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. NN0)
11		nn0cnt 6064	. . . . . . . . 9 |- ((N C. k) e. NN0 -> (N C. k) e. CC)
12	10, 11	syl 10	. . . . . . . 8 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. CC)
13		nnnn0t 6061	. . . . . . . 8 |- (N e. NN -> N e. NN0)
14		elfzelz 6422	. . . . . . . 8 |- (k e. (1...N) -> k e. ZZ)
15	12, 13, 14	syl2an 454	. . . . . . 7 |- ((N e. NN /\ k e. (1...N)) -> (N C. k) e. CC)
16		axmulcl 5253	. . . . . . . 8 |- (((A^((N + 1) - k)) e. CC /\ (B^k) e. CC) -> ((A^((N + 1) - k)) x. (B^k)) e. CC)
17		fzelp1t 6448	. . . . . . . . 9 |- ((N e. NN /\ k e. (1...N)) -> k e. (1...(N + 1)))
18		oprex 3974	. . . . . . . . . 10 |- (N + 1) e. V
19		fznn0subt 6438	. . . . . . . . . 10 |- (((N + 1) e. V /\ k e. (1...(N + 1))) -> ((N + 1) - k) e. NN0)
20	18, 19	mpan 694	. . . . . . . . 9 |- (k e. (1...(N + 1)) -> ((N + 1) - k) e. NN0)
21		expclt 6521	. . . . . . . . . 10 |- ((A e. CC /\ ((N + 1) - k) e. NN0) -> (A^((N + 1) - k)) e. CC)
22	3, 21	mpan 694	. . . . . . . . 9 |- (((N + 1) - k) e. NN0 -> (A^((N + 1) - k)) e. CC)
23	17, 20, 22	3syl 20	. . . . . . . 8 |- ((N e. NN /\ k e. (1...N)) -> (A^((N + 1) - k)) e. CC)
24		elfznnt 6434	. . . . . . . . . 10 |- (k e. (1...N) -> k e. NN)
25		binomlem.2	. . . . . . . . . . 11 |- B e. CC
26		expclt 6521	. . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
27		nnnn0t 6061	. . . . . . . . . . . 12 |- (k e. NN -> k e. NN0)
28	26, 27	sylan2 451	. . . . . . . . . . 11 |- ((B e. CC /\ k e. NN) -> (B^k) e. CC)
29	25, 28	mpan 694	. . . . . . . . . 10 |- (k e. NN -> (B^k) e. CC)
30	24, 29	syl 10	. . . . . . . . 9 |- (k e. (1...N) -> (B^k) e. CC)
31	30	adantl 388	. . . . . . . 8 |- ((N e. NN /\ k e. (1...N)) -> (B^k) e. CC)
32	16, 23, 31	sylanc 471	. . . . . . 7 |- ((N e. NN /\ k e. (1...N)) -> ((A^((N + 1) - k)) x. (B^k)) e. CC)
33	9, 15, 32	sylanc 471	. . . . . 6 |- ((N e. NN /\ k e. (1...N)) -> ((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
34	33	r19.21aiva 1711	. . . . 5 |- (N e. NN -> A.k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
35		fsumclt 6961	. . . . . 6 |- ((N e. (ZZ>` 1) /\ A.k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC) -> sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
36		elnnuz 6380	. . . . . 6 |- (N e. NN <-> N e. (ZZ>` 1))
37	35, 36	sylanb 449	. . . . 5 |- ((N e. NN /\ A.k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC) -> sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
38	34, 37	mpdan 703	. . . 4 |- (N e. NN -> sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
39		axaddcl 5251	. . . . 5 |- ((sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC /\ (B^(N + 1)) e. CC) -> (sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) + (B^(N + 1))) e. CC)
40		axmulcl 5253	. . . . . . . 8 |- (((N C. (k - 1)) e. CC /\ ((A^((N + 1) - k)) x. (B^k)) e. CC) -> ((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
41		bcclt 6918	. . . . . . . . . 10 |- ((N e. NN0 /\ (k - 1) e. ZZ) -> (N C. (k - 1)) e. NN0)
42		nn0cnt 6064	. . . . . . . . . 10 |- ((N C. (k - 1)) e. NN0 -> (N C. (k - 1)) e. CC)
43	41, 42	syl 10	. . . . . . . . 9 |- ((N e. NN0 /\ (k - 1) e. ZZ) -> (N C. (k - 1)) e. CC)
44		peano2zm 6124	. . . . . . . . . 10 |- (k e. ZZ -> (k - 1) e. ZZ)
45	14, 44	syl 10	. . . . . . . . 9 |- (k e. (1...N) -> (k - 1) e. ZZ)
46	43, 13, 45	syl2an 454	. . . . . . . 8 |- ((N e. NN /\ k e. (1...N)) -> (N C. (k - 1)) e. CC)
47	40, 46, 32	sylanc 471	. . . . . . 7 |- ((N e. NN /\ k e. (1...N)) -> ((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
48	47	r19.21aiva 1711	. . . . . 6 |- (N e. NN -> A.k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
49		fsumclt 6961	. . . . . . 7 |- ((N e. (ZZ>` 1) /\ A.k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC) -> sum_k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
50	49, 36	sylanb 449	. . . . . 6 |- ((N e. NN /\ A.k e. (1...N)((N C. (k - 1)) x. ((A^((N + 1) - k)) x. (B