HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem binomlem1 7004
Description: Lemma for binom 7010 (binomial theorem). Break out and simplify the first term of the summation.
Hypotheses
Ref Expression
binomlem.1 |- A e. CC
binomlem.2 |- B e. CC
Assertion
Ref Expression
binomlem1 |- (N e. NN -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = ((A^(N + 1)) + sum_k e. (1...N)((N C. k) x. ((A^((N + 1) - k)) x. (B^k)))))
Distinct variable groups:   A,k   B,k   k,N
Proof of Theorem binomlem1
StepHypRef Expression
1 nnnn0t 6053 . . 3 |- (N e. NN -> N e. NN0)
2 binomlem.1 . . . . . 6 |- A e. CC
3 fsummulc2 6972 . . . . . 6 |- ((N e. (ZZ>` 0) /\ A 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. A) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. A))
42, 3mp3an2 901 . . . . 5 |- ((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. A) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. A))
5 elnn0uz 6373 . . . . . 6 |- (N e. NN0 <-> N e. (ZZ>` 0))
65biimp 151 . . . . 5 |- (N e. NN0 -> N e. (ZZ>` 0))
7 axmulcl 5245 . . . . . . 7 |- (((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 . . . . . . . . 9 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. NN0)
9 nn0cnt 6056 . . . . . . . . 9 |- ((N C. k) e. NN0 -> (N C. k) e. CC)
108, 9syl 10 . . . . . . . 8 |- ((N e. NN0 /\ k e. ZZ) -> (N C. k) e. CC)
11 elfzelz 6414 . . . . . . . 8 |- (k e. (0...N) -> k e. ZZ)
1210, 11sylan2 451 . . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> (N C. k) e. CC)
13 axmulcl 5245 . . . . . . . 8 |- (((A^(N - k)) e. CC /\ (B^k) e. CC) -> ((A^(N - k)) x. (B^k)) e. CC)
14 fznn0subt 6430 . . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (N - k) e. NN0)
15 expclt 6513 . . . . . . . . . 10 |- ((A e. CC /\ (N - k) e. NN0) -> (A^(N - k)) e. CC)
162, 15mpan 693 . . . . . . . . 9 |- ((N - k) e. NN0 -> (A^(N - k)) e. CC)
1714, 16syl 10 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (A^(N - k)) e. CC)
18 elfznn0t 6428 . . . . . . . . . 10 |- (k e. (0...N) -> k e. NN0)
19 binomlem.2 . . . . . . . . . . 11 |- B e. CC
20 expclt 6513 . . . . . . . . . . 11 |- ((B e. CC /\ k e. NN0) -> (B^k) e. CC)
2119, 20mpan 693 . . . . . . . . . 10 |- (k e. NN0 -> (B^k) e. CC)
2218, 21syl 10 . . . . . . . . 9 |- (k e. (0...N) -> (B^k) e. CC)
2322adantl 388 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (B^k) e. CC)
2413, 17, 23sylanc 471 . . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^(N - k)) x. (B^k)) e. CC)
257, 12, 24sylanc 471 . . . . . 6 |- ((N e. NN0 /\ k e. (0...N)) -> ((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
2625r19.21aiva 1706 . . . . 5 |- (N e. NN0 -> A.k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) e. CC)
274, 6, 26sylanc 471 . . . 4 |- (N e. NN0 -> (sum_k e. (0...N)((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = sum_k e. (0...N)(((N C. k) x. ((A^(N - k)) x. (B^k))) x. A))
28 axmulass 5250 . . . . . . . 8 |- (((N C. k) e. CC /\ ((A^(N - k)) x. (B^k)) e. CC /\ A e. CC) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. A)))
292, 28mp3an3 902 . . . . . . 7 |- (((N C. k) e. CC /\ ((A^(N - k)) x. (B^k)) e. CC) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. A)))
3029, 12, 24sylanc 471 . . . . . 6 |- ((N e. NN0 /\ k e. (0...N)) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = ((N C. k) x. (((A^(N - k)) x. (B^k)) x. A)))
31 ax1cn 5241 . . . . . . . . . . . . 13 |- 1 e. CC
32 addsubt 5356 . . . . . . . . . . . . 13 |- ((N e. CC /\ 1 e. CC /\ k e. CC) -> ((N + 1) - k) = ((N - k) + 1))
3331, 32mp3an2 901 . . . . . . . . . . . 12 |- ((N e. CC /\ k e. CC) -> ((N + 1) - k) = ((N - k) + 1))
34 nn0cnt 6056 . . . . . . . . . . . 12 |- (N e. NN0 -> N e. CC)
35 zcnt 6087 . . . . . . . . . . . . 13 |- (k e. ZZ -> k e. CC)
3611, 35syl 10 . . . . . . . . . . . 12 |- (k e. (0...N) -> k e. CC)
3733, 34, 36syl2an 454 . . . . . . . . . . 11 |- ((N e. NN0 /\ k e. (0...N)) -> ((N + 1) - k) = ((N - k) + 1))
3837opreq2d 3961 . . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (A^((N + 1) - k)) = (A^((N - k) + 1)))
39 expp1t 6506 . . . . . . . . . . . 12 |- ((A e. CC /\ (N - k) e. NN0) -> (A^((N - k) + 1)) = ((A^(N - k)) x. A))
402, 39mpan 693 . . . . . . . . . . 11 |- ((N - k) e. NN0 -> (A^((N - k) + 1)) = ((A^(N - k)) x. A))
4114, 40syl 10 . . . . . . . . . 10 |- ((N e. NN0 /\ k e. (0...N)) -> (A^((N - k) + 1)) = ((A^(N - k)) x. A))
4238, 41eqtrd 1499 . . . . . . . . 9 |- ((N e. NN0 /\ k e. (0...N)) -> (A^((N + 1) - k)) = ((A^(N - k)) x. A))
4342opreq1d 3960 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> ((A^((N + 1) - k)) x. (B^k)) = (((A^(N - k)) x. A) x. (B^k)))
44 mul23t 5391 . . . . . . . . . 10 |- (((A^(N - k)) e. CC /\ A e. CC /\ (B^k) e. CC) -> (((A^(N - k)) x. A) x. (B^k)) = (((A^(N - k)) x. (B^k)) x. A))
452, 44mp3an2 901 . . . . . . . . 9 |- (((A^(N - k)) e. CC /\ (B^k) e. CC) -> (((A^(N - k)) x. A) x. (B^k)) = (((A^(N - k)) x. (B^k)) x. A))
4645, 17, 23sylanc 471 . . . . . . . 8 |- ((N e. NN0 /\ k e. (0...N)) -> (((A^(N - k)) x. A) x. (B^k)) = (((A^(N - k)) x. (B^k)) x. A))
4743, 46eqtr2d 1500 . . . . . . 7 |- ((N e. NN0 /\ k e. (0...N)) -> (((A^(N - k)) x. (B^k)) x. A) = ((A^((N + 1) - k)) x. (B^k)))
4847opreq2d 3961 . . . . . 6 |- ((N e. NN0 /\ k e. (0...N)) -> ((N C. k) x. (((A^(N - k)) x. (B^k)) x. A)) = ((N C. k) x. ((A^((N + 1) - k)) x. (B^k))))
4930, 48eqtrd 1499 . . . . 5 |- ((N e. NN0 /\ k e. (0...N)) -> (((N C. k) x. ((A^(N - k)) x. (B^k))) x. A) = ((N C. k) x. (