Theorem binomlem4 7069

Description: Lemma for binom 7072 (binomial theorem). Break out the first term of the summation used by the induction hypothesis.

Hypotheses

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

Assertion

Ref	Expression
binomlem4	|- (N e. NN0 -> sum_k e. (0...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) = ((A^(N + 1)) + sum_k e. (1...(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 binomlem4

Step	Hyp	Ref	Expression
1		fsum1ps 7018	. . 3 |- (((N + 1) e. (ZZ>` 0) /\ 0 < (N + 1) /\ A.k e. (0...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC) -> sum_k e. (0...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) = ([_0 / k]_(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) + sum_k e. ((0 + 1)...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k)))))
2		peano2nn0 6126	. . . 4 |- (N e. NN0 -> (N + 1) e. NN0)
3		nn0uz 6439	. . . 4 |- NN0 = (ZZ>` 0)
4	2, 3	syl6eleq 1561	. . 3 |- (N e. NN0 -> (N + 1) e. (ZZ>` 0))
5		nn0p1nnt 6177	. . . 4 |- (N e. NN0 -> (N + 1) e. NN)
6		nngt0t 5948	. . . 4 |- ((N + 1) e. NN -> 0 < (N + 1))
7	5, 6	syl 10	. . 3 |- (N e. NN0 -> 0 < (N + 1))
8		axmulcl 5285	. . . . 5 |- ((((N + 1) C. k) e. CC /\ ((A^((N + 1) - k)) x. (B^k)) e. CC) -> (((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
9		bcclt 6972	. . . . . . 7 |- (((N + 1) e. NN0 /\ k e. ZZ) -> ((N + 1) C. k) e. NN0)
10		nn0cnt 6111	. . . . . . 7 |- (((N + 1) C. k) e. NN0 -> ((N + 1) C. k) e. CC)
11	9, 10	syl 10	. . . . . 6 |- (((N + 1) e. NN0 /\ k e. ZZ) -> ((N + 1) C. k) e. CC)
12		elfzelz 6483	. . . . . 6 |- (k e. (0...(N + 1)) -> k e. ZZ)
13	11, 2, 12	syl2an 456	. . . . 5 |- ((N e. NN0 /\ k e. (0...(N + 1))) -> ((N + 1) C. k) e. CC)
14		axmulcl 5285	. . . . . 6 |- (((A^((N + 1) - k)) e. CC /\ (B^k) e. CC) -> ((A^((N + 1) - k)) x. (B^k)) e. CC)
15		oprex 3989	. . . . . . . . 9 |- (N + 1) e. V
16		fznn0subt 6499	. . . . . . . . 9 |- (((N + 1) e. V /\ k e. (0...(N + 1))) -> ((N + 1) - k) e. NN0)
17	15, 16	mpan 697	. . . . . . . 8 |- (k e. (0...(N + 1)) -> ((N + 1) - k) e. NN0)
18		binomlem.1	. . . . . . . . 9 |- A e. CC
19		expclt 6582	. . . . . . . . 9 |- ((A e. CC /\ ((N + 1) - k) e. NN0) -> (A^((N + 1) - k)) e. CC)
20	18, 19	mpan 697	. . . . . . . 8 |- (((N + 1) - k) e. NN0 -> (A^((N + 1) - k)) e. CC)
21	17, 20	syl 10	. . . . . . 7 |- (k e. (0...(N + 1)) -> (A^((N + 1) - k)) e. CC)
22	21	adantl 390	. . . . . 6 |- ((N e. NN0 /\ k e. (0...(N + 1))) -> (A^((N + 1) - k)) e. CC)
23		elfznn0t 6497	. . . . . . . 8 |- (k e. (0...(N + 1)) -> k e. NN0)
24		binomlem.2	. . . . . . . . 9 |- B e. CC
25		expclt 6582	. . . . . . . . 9 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
26	24, 25	mpan 697	. . . . . . . 8 |- (k e. NN0 -> (B^k) e. CC)
27	23, 26	syl 10	. . . . . . 7 |- (k e. (0...(N + 1)) -> (B^k) e. CC)
28	27	adantl 390	. . . . . 6 |- ((N e. NN0 /\ k e. (0...(N + 1))) -> (B^k) e. CC)
29	14, 22, 28	sylanc 473	. . . . 5 |- ((N e. NN0 /\ k e. (0...(N + 1))) -> ((A^((N + 1) - k)) x. (B^k)) e. CC)
30	8, 13, 29	sylanc 473	. . . 4 |- ((N e. NN0 /\ k e. (0...(N + 1))) -> (((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
31	30	r19.21aiva 1717	. . 3 |- (N e. NN0 -> A.k e. (0...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) e. CC)
32	1, 4, 7, 31	syl3anc 860	. 2 |- (N e. NN0 -> sum_k e. (0...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) = ([_0 / k]_(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k))) + sum_k e. ((0 + 1)...(N + 1))(((N + 1) C. k) x. ((A^((N + 1) - k)) x. (B^k)))))
33		bcn0t 6963	. . . . . . 7 |- ((N + 1) e. NN0 -> ((N + 1) C. 0) = 1)
34	2, 33	syl 10	. . . . . 6 |- (N e. NN0 -> ((N + 1) C. 0) = 1)
35		nn0cnt 6111	. . . . . . . . . 10 |- ((N + 1) e. NN0 -> (N + 1) e. CC)
36		subid1t 5408	. . . . . . . . . 10 |- ((N + 1) e. CC -> ((N + 1) - 0) = (N + 1))
37	2, 35, 36	3syl 20	. . . . . . . . 9 |- (N e. NN0 -> ((N + 1) - 0) = (N + 1))
38	37	opreq2d 3982	. . . . . . . 8 |- (N e. NN0 -> (A^((N + 1) - 0)) = (A^(N + 1)))
39	38	opreq1d 3981	. . . . . . 7 |- (N e. NN0 -> ((A^((N + 1) - 0)) x. 1) = ((A^(N + 1)) x. 1))
40		expclt 6582	. . . . . . . . 9 |- ((A e. CC /\ (N + 1) e. NN0) -> (A^(N + 1)) e. CC)
41	18, 40	mpan 697	. . . . . . . 8 |- ((N + 1) e. NN0 -> (A^(N + 1)) e. CC)
42		ax1id 5294	. . . . . . . 8 |- ((A^(N + 1)) e. CC -> ((A^(N + 1)) x. 1) = (A^(N + 1)))
43	2, 41, 42	3syl 20	. . . . . . 7 |- (N e. NN0 -> ((A^(N + 1)) x. 1) = (A^(N + 1)))
44	39, 43	eqtrd 1510	. . . . . 6 |- (N e. NN0 -> ((A^((N + 1) - 0)) x. 1) = (A^(N + 1)))
45	34, 44	opreq12d 3984	. . . . 5 |- (N e. NN0 -> (((N + 1) C. 0) x. ((A^((N + 1) - 0)) x. 1)) = (1 x. (A^(N + 1))))
46		mulid2t 5429	. . . . . 6 |- ((A^(N + 1)) e. CC -> (1 x. (A^(N + 1))) = (A^(N + 1)))
47	2, 41, 46	3syl 20	. . . . 5 |- (N e. NN0 -> (1 x. (A^(N + 1))) = (A^(N + 1)))
48	45, 47	eqtrd 1510	. . . 4 |- (N e. NN0 -> (((N + 1) C. 0) x. ((A^((N + 1) - 0)) x. 1)) = (A^(N + 1)))
49		0cn 5340	. . . . . 6 |- 0 e. CC
50	49	elisseti 1821	. . . . 5 |- 0 e. V
51		ax-17 973	. . . . 5 |- (x e. (((N + 1) C. 0) x. ((A^((N + 1) - 0)) x. 1)) -> A.k x e. (((N + 1) C. 0) x. ((A^((N + 1) - 0)) x. 1)))
52		opreq2 3975	. . . . . 6 |- (k = 0 -> ((N + 1) C. k) = ((N + 1) C. 0))
53		opreq2 3975	. . . . . . . 8 |- (k = 0 -> ((N + 1) - k) = ((N + 1) - 0))
54	53	opreq2d 3982	. . . . . . 7 |- (k = 0 -> (A^((N + 1) - k)) = (A^((N + 1) - 0)))
55		opreq2 3975	. . . . . . . 8 |- (k = 0 -> (B^k) = (B^0))
56		exp0t 6572	. . . . . . . . 9 |- (B e. CC -> (B^0) = 1)
57	24, 56	ax-mp 7	. . . . . . . 8 |- (B^0) = 1
58	55, 57	syl6eq 1526	. . . . . . 7 |- (k = 0 -> (B^k) = 1)
59	54, 58	opreq12d 3984	. . . . . 6 |- (k = 0 -> ((A^((N + 1) - k)) x. (B^k)) = ((A^((N + 1) - 0))