HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem binomlem2 7005
Description: Lemma for binom 7010 (binomial theorem). Shift up the summation index with fsumshft 6969, 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
StepHypRef Expression
1 nnnn0t 6053 . . 3 |- (N e. NN -> N e. NN0)
2 binomlem.2 . . . . . . 7 |- B e. CC
3 fsummulc2 6972 . . . . . . 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))
42, 3mp3an2 901 . . . . . 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 6373 . . . . . . 7 |- (N e. NN0 <-> N e. (ZZ>` 0))
65biimp 151 . . . . . 6 |- (N e. NN0 -> N e. (ZZ>` 0))
7 axmulcl 5245 . . . . . . . 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 6910 . . . . . . . . . 10 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. NN0)
9 nn0cnt 6056 . . . . . . . . . 10 |- ((N C. k) e. NN0 -> (N C. k) e. CC)
108, 9syl 10 . . . . . . . . 9 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. CC)
11 elfzelz 6414 . . . . . . . . 9 |- (k e. (0...N) -> k e. ZZ)
1210, 11sylan2 451 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (N C. k) e. CC)
13 axmulcl 5245 . . . . . . . . 9 |- (((A^(N - k)) e. CC /\ (B^k) e. CC) -> ((A^(N - k)) x. (B^k)) e. CC)
14 fznn0subt 6430 . . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (N - k) e. NN0)
15 binomlem.1 . . . . . . . . . . 11 |- A e. CC
16 expclt 6513 . . . . . . . . . . 11 |- ((A e. CC /\ (N - k) e. NN0) -> (A^(N - k)) e. CC)
1715, 16mpan 693 . . . . . . . . . 10 |- ((N - k) e. NN0 -> (A^(N - k)) e. CC)
1814, 17syl 10 . . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (A^(N - k)) e. CC)
19 elfznn0t 6428 . . . . . . . . . . 11 |- (k e. (0...N) -> k e. NN0)
20 expclt 6513 . . . . . . . . . . . 12 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
212, 20mpan 693 . . . . . . . . . . 11 |- (k e. NN0 -> (B^k) e. CC)
2219, 21syl 10 . . . . . . . . . 10 |- (k e. (0...N) -> (B^k) e. CC)
2322adantl 388 . . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (B^k) e. CC)
2413, 18, 23sylanc 471 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^(N - k)) x. (B^k)) e. CC)
257, 12, 24sylanc 471 . . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> ((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
2625r19.21aiva 1706 . . . . . 6 |- (N e. NN0 -> A.k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
274, 6, 26sylanc 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 5250 . . . . . . . . 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)))
292, 28mp3an3 902 . . . . . . . 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)))
3029, 12, 24sylanc 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 5250 . . . . . . . . . . 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)))
322, 31mp3an3 902 . . . . . . . . . 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)))
3332, 18, 23sylanc 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 6506 . . . . . . . . . . . . 13 |- ((B e. CC /\ k e. NN0) -> (B^(k + 1)) = ((B^k) x. B))
352, 34mpan 693 . . . . . . . . . . . 12 |- (k e. NN0 -> (B^(k + 1)) = ((B^k) x. B))
3619, 35syl 10 . . . . . . . . . . 11 |- (k e. (0...N) -> (B^(k + 1)) = ((B^k) x. B))
3736adantl 388 . . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (B^(k + 1)) = ((B^k) x. B))
3837opreq2d 3961 . . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^(N - k)) x. (B^(k + 1))) = ((A^(N - k)) x. ((B^k) x. B)))
3933, 38eqtr4d 1502 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (((A^(N - k)) x. (B^k)) x. B) = ((A^(N - k)) x. (B^(k + 1))))
4039opreq2d 3961 . . . . . . 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)))))
4130, 40eqtrd 1499 . . . . . 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)))))
4241sumeq2dv 6930 . . . . 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)))))
4327, 42eqtrd 1499 . . . 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 6106 . . . . . . 7 |- 1 e. ZZ
45 fsumshft 6969 . . . . . . 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. CC