Theorem binomlem6 7071

Description: Lemma for binom 7072 (binomial theorem). Do the final induction.

Hypotheses

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

Assertion

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

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

Proof of Theorem binomlem6

Step	Hyp	Ref	Expression
1		opreq2 3975	. . 3 |- (x = 1 -> ((A + B)^x) = ((A + B)^1))
2		opreq2 3975	. . . 4 |- (x = 1 -> (0...x) = (0...1))
3		opreq1 3974	. . . . . 6 |- (x = 1 -> (x C. k) = (1 C. k))
4		opreq1 3974	. . . . . . . 8 |- (x = 1 -> (x - k) = (1 - k))
5	4	opreq2d 3982	. . . . . . 7 |- (x = 1 -> (A^(x - k)) = (A^(1 - k)))
6	5	opreq1d 3981	. . . . . 6 |- (x = 1 -> ((A^(x - k)) x. (B^k)) = ((A^(1 - k)) x. (B^k)))
7	3, 6	opreq12d 3984	. . . . 5 |- (x = 1 -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((1 C. k) x. ((A^(1 - k)) x. (B^k))))
8	7	adantr 391	. . . 4 |- ((x = 1 /\ k e. (0...1)) -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((1 C. k) x. ((A^(1 - k)) x. (B^k))))
9	2, 8	sumeq12rdv 6996	. . 3 |- (x = 1 -> sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) = sum_k e. (0...1)((1 C. k) x. ((A^(1 - k)) x. (B^k))))
10	1, 9	eqeq12d 1492	. 2 |- (x = 1 -> (((A + B)^x) = sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) <-> ((A + B)^1) = sum_k e. (0...1)((1 C. k) x. ((A^(1 - k)) x. (B^k)))))
11		opreq2 3975	. . 3 |- (x = j -> ((A + B)^x) = ((A + B)^j))
12		opreq2 3975	. . . 4 |- (x = j -> (0...x) = (0...j))
13		opreq1 3974	. . . . . 6 |- (x = j -> (x C. k) = (j C. k))
14		opreq1 3974	. . . . . . . 8 |- (x = j -> (x - k) = (j - k))
15	14	opreq2d 3982	. . . . . . 7 |- (x = j -> (A^(x - k)) = (A^(j - k)))
16	15	opreq1d 3981	. . . . . 6 |- (x = j -> ((A^(x - k)) x. (B^k)) = ((A^(j - k)) x. (B^k)))
17	13, 16	opreq12d 3984	. . . . 5 |- (x = j -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((j C. k) x. ((A^(j - k)) x. (B^k))))
18	17	adantr 391	. . . 4 |- ((x = j /\ k e. (0...j)) -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((j C. k) x. ((A^(j - k)) x. (B^k))))
19	12, 18	sumeq12rdv 6996	. . 3 |- (x = j -> sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) = sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k))))
20	11, 19	eqeq12d 1492	. 2 |- (x = j -> (((A + B)^x) = sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) <-> ((A + B)^j) = sum_k e. (0...j)((j C. k) x. ((A^(j - k)) x. (B^k)))))
21		opreq2 3975	. . 3 |- (x = (j + 1) -> ((A + B)^x) = ((A + B)^(j + 1)))
22		opreq2 3975	. . . 4 |- (x = (j + 1) -> (0...x) = (0...(j + 1)))
23		opreq1 3974	. . . . . 6 |- (x = (j + 1) -> (x C. k) = ((j + 1) C. k))
24		opreq1 3974	. . . . . . . 8 |- (x = (j + 1) -> (x - k) = ((j + 1) - k))
25	24	opreq2d 3982	. . . . . . 7 |- (x = (j + 1) -> (A^(x - k)) = (A^((j + 1) - k)))
26	25	opreq1d 3981	. . . . . 6 |- (x = (j + 1) -> ((A^(x - k)) x. (B^k)) = ((A^((j + 1) - k)) x. (B^k)))
27	23, 26	opreq12d 3984	. . . . 5 |- (x = (j + 1) -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = (((j + 1) C. k) x. ((A^((j + 1) - k)) x. (B^k))))
28	27	adantr 391	. . . 4 |- ((x = (j + 1) /\ k e. (0...(j + 1))) -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = (((j + 1) C. k) x. ((A^((j + 1) - k)) x. (B^k))))
29	22, 28	sumeq12rdv 6996	. . 3 |- (x = (j + 1) -> sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) = sum_k e. (0...(j + 1))(((j + 1) C. k) x. ((A^((j + 1) - k)) x. (B^k))))
30	21, 29	eqeq12d 1492	. 2 |- (x = (j + 1) -> (((A + B)^x) = sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) <-> ((A + B)^(j + 1)) = sum_k e. (0...(j + 1))(((j + 1) C. k) x. ((A^((j + 1) - k)) x. (B^k)))))
31		opreq2 3975	. . 3 |- (x = N -> ((A + B)^x) = ((A + B)^N))
32		opreq2 3975	. . . 4 |- (x = N -> (0...x) = (0...N))
33		opreq1 3974	. . . . . 6 |- (x = N -> (x C. k) = (N C. k))
34		opreq1 3974	. . . . . . . 8 |- (x = N -> (x - k) = (N - k))
35	34	opreq2d 3982	. . . . . . 7 |- (x = N -> (A^(x - k)) = (A^(N - k)))
36	35	opreq1d 3981	. . . . . 6 |- (x = N -> ((A^(x - k)) x. (B^k)) = ((A^(N - k)) x. (B^k)))
37	33, 36	opreq12d 3984	. . . . 5 |- (x = N -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((N C. k) x. ((A^(N - k)) x. (B^k))))
38	37	adantr 391	. . . 4 |- ((x = N /\ k e. (0...N)) -> ((x C. k) x. ((A^(x - k)) x. (B^k))) = ((N C. k) x. ((A^(N - k)) x. (B^k))))
39	32, 38	sumeq12rdv 6996	. . 3 |- (x = N -> sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) = sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))))
40	31, 39	eqeq12d 1492	. 2 |- (x = N -> (((A + B)^x) = sum_k e. (0...x)((x C. k) x. ((A^(x - k)) x. (B^k))) <-> ((A + B)^N) = sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k)))))
41		binomlem.1	. . . . 5 |- A e. CC
42		binomlem.2	. . . . 5 |- B e. CC
43	41, 42	addcl 5332	. . . 4 |- (A + B) e. CC
44		exp1t 6574	. . . 4 |- ((A + B) e. CC -> ((A + B)^1) = (A + B))
45	43, 44	ax-mp 7	. . 3 |- ((A + B)^1) = (A + B)
46		0z 6148	. . . . . 6 |- 0 e. ZZ
47		uzidt 6428	. . . . . 6 |- (0 e. ZZ -> 0 e. (ZZ>` 0))
48	46, 47	ax-mp 7	. . . . 5 |- 0 e. (ZZ>` 0)
49		oprex 3989	. . . . . 6 |- ((1 C. k) x. ((A^(1 - k)) x. (B^k))) e. V
50	42	elisseti 1821	. . . . . 6 |- B e. V
51		ax1cn 5281	. . . . . . . . 9 |- 1 e. CC
52	51	addid2 5343	. . . . . . . 8 |- (0 + 1) = 1
53	52	eqeq2i 1488	. . . . . . 7<