This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem binom

Description: The binomial theorem: ( A + B ) ^ N is the sum from k = 0 to N of ( N _C k ) x. ( ( A ^ k ) x. ( B ^ ( N - k ) ) . Theorem 15-2.8 of Gleason p. 296. This part of the proof sets up the induction and does the base case, with the bulk of the work (the induction step) in binomlem . This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005) (Proof shortened by Mario Carneiro, 24-Apr-2014)

Ref Expression
Assertion binom 
|- ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = 0 -> ( ( A + B ) ^ x ) = ( ( A + B ) ^ 0 ) )
2 oveq2 
 |-  ( x = 0 -> ( 0 ... x ) = ( 0 ... 0 ) )
3 oveq1 
 |-  ( x = 0 -> ( x _C k ) = ( 0 _C k ) )
4 oveq1 
 |-  ( x = 0 -> ( x - k ) = ( 0 - k ) )
5 4 oveq2d 
 |-  ( x = 0 -> ( A ^ ( x - k ) ) = ( A ^ ( 0 - k ) ) )
6 5 oveq1d 
 |-  ( x = 0 -> ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) )
7 3 6 oveq12d 
 |-  ( x = 0 -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) )
8 7 adantr 
 |-  ( ( x = 0 /\ k e. ( 0 ... x ) ) -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) )
9 2 8 sumeq12dv 
 |-  ( x = 0 -> sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) )
10 1 9 eqeq12d 
 |-  ( x = 0 -> ( ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) <-> ( ( A + B ) ^ 0 ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) ) )
11 10 imbi2d 
 |-  ( x = 0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 0 ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) ) ) )
12 oveq2 
 |-  ( x = n -> ( ( A + B ) ^ x ) = ( ( A + B ) ^ n ) )
13 oveq2 
 |-  ( x = n -> ( 0 ... x ) = ( 0 ... n ) )
14 oveq1 
 |-  ( x = n -> ( x _C k ) = ( n _C k ) )
15 oveq1 
 |-  ( x = n -> ( x - k ) = ( n - k ) )
16 15 oveq2d 
 |-  ( x = n -> ( A ^ ( x - k ) ) = ( A ^ ( n - k ) ) )
17 16 oveq1d 
 |-  ( x = n -> ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) )
18 14 17 oveq12d 
 |-  ( x = n -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) )
19 18 adantr 
 |-  ( ( x = n /\ k e. ( 0 ... x ) ) -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) )
20 13 19 sumeq12dv 
 |-  ( 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 ) ) ) )
21 12 20 eqeq12d 
 |-  ( 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 ) ) ) ) )
22 21 imbi2d 
 |-  ( x = n -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) ) ) )
23 oveq2 
 |-  ( x = ( n + 1 ) -> ( ( A + B ) ^ x ) = ( ( A + B ) ^ ( n + 1 ) ) )
24 oveq2 
 |-  ( x = ( n + 1 ) -> ( 0 ... x ) = ( 0 ... ( n + 1 ) ) )
25 oveq1 
 |-  ( x = ( n + 1 ) -> ( x _C k ) = ( ( n + 1 ) _C k ) )
26 oveq1 
 |-  ( x = ( n + 1 ) -> ( x - k ) = ( ( n + 1 ) - k ) )
27 26 oveq2d 
 |-  ( x = ( n + 1 ) -> ( A ^ ( x - k ) ) = ( A ^ ( ( n + 1 ) - k ) ) )
28 27 oveq1d 
 |-  ( x = ( n + 1 ) -> ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) )
29 25 28 oveq12d 
 |-  ( x = ( n + 1 ) -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) )
30 29 adantr 
 |-  ( ( x = ( n + 1 ) /\ k e. ( 0 ... x ) ) -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) )
31 24 30 sumeq12dv 
 |-  ( x = ( n + 1 ) -> sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) )
32 23 31 eqeq12d 
 |-  ( x = ( n + 1 ) -> ( ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) <-> ( ( A + B ) ^ ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) ) )
33 32 imbi2d 
 |-  ( x = ( n + 1 ) -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) ) ) )
34 oveq2 
 |-  ( x = N -> ( ( A + B ) ^ x ) = ( ( A + B ) ^ N ) )
35 oveq2 
 |-  ( x = N -> ( 0 ... x ) = ( 0 ... N ) )
36 oveq1 
 |-  ( x = N -> ( x _C k ) = ( N _C k ) )
37 oveq1 
 |-  ( x = N -> ( x - k ) = ( N - k ) )
38 37 oveq2d 
 |-  ( x = N -> ( A ^ ( x - k ) ) = ( A ^ ( N - k ) ) )
39 38 oveq1d 
 |-  ( x = N -> ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) = ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) )
40 36 39 oveq12d 
 |-  ( x = N -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
41 40 adantr 
 |-  ( ( x = N /\ k e. ( 0 ... x ) ) -> ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) = ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
42 35 41 sumeq12dv 
 |-  ( 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 ) ) ) )
43 34 42 eqeq12d 
 |-  ( 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 ) ) ) ) )
44 43 imbi2d 
 |-  ( x = N -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ x ) = sum_ k e. ( 0 ... x ) ( ( x _C k ) x. ( ( A ^ ( x - k ) ) x. ( B ^ k ) ) ) ) <-> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) ) ) )
45 exp0 
 |-  ( A e. CC -> ( A ^ 0 ) = 1 )
46 exp0 
 |-  ( B e. CC -> ( B ^ 0 ) = 1 )
47 45 46 oveqan12d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 0 ) x. ( B ^ 0 ) ) = ( 1 x. 1 ) )
48 1t1e1 
 |-  ( 1 x. 1 ) = 1
49 47 48 eqtrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A ^ 0 ) x. ( B ^ 0 ) ) = 1 )
50 49 oveq2d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) = ( 1 x. 1 ) )
51 50 48 eqtrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) = 1 )
52 0z 
 |-  0 e. ZZ
53 ax-1cn 
 |-  1 e. CC
54 51 53 eqeltrdi 
 |-  ( ( A e. CC /\ B e. CC ) -> ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) e. CC )
55 oveq2 
 |-  ( k = 0 -> ( 0 _C k ) = ( 0 _C 0 ) )
56 0nn0 
 |-  0 e. NN0
57 bcn0 
 |-  ( 0 e. NN0 -> ( 0 _C 0 ) = 1 )
58 56 57 ax-mp 
 |-  ( 0 _C 0 ) = 1
59 55 58 eqtrdi 
 |-  ( k = 0 -> ( 0 _C k ) = 1 )
60 oveq2 
 |-  ( k = 0 -> ( 0 - k ) = ( 0 - 0 ) )
61 0m0e0 
 |-  ( 0 - 0 ) = 0
62 60 61 eqtrdi 
 |-  ( k = 0 -> ( 0 - k ) = 0 )
63 62 oveq2d 
 |-  ( k = 0 -> ( A ^ ( 0 - k ) ) = ( A ^ 0 ) )
64 oveq2 
 |-  ( k = 0 -> ( B ^ k ) = ( B ^ 0 ) )
65 63 64 oveq12d 
 |-  ( k = 0 -> ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) = ( ( A ^ 0 ) x. ( B ^ 0 ) ) )
66 59 65 oveq12d 
 |-  ( k = 0 -> ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) = ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) )
67 66 fsum1 
 |-  ( ( 0 e. ZZ /\ ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) = ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) )
68 52 54 67 sylancr 
 |-  ( ( A e. CC /\ B e. CC ) -> sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) = ( 1 x. ( ( A ^ 0 ) x. ( B ^ 0 ) ) ) )
69 addcl 
 |-  ( ( A e. CC /\ B e. CC ) -> ( A + B ) e. CC )
70 69 exp0d 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 0 ) = 1 )
71 51 68 70 3eqtr4rd 
 |-  ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ 0 ) = sum_ k e. ( 0 ... 0 ) ( ( 0 _C k ) x. ( ( A ^ ( 0 - k ) ) x. ( B ^ k ) ) ) )
72 simprl 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> A e. CC )
73 simprr 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> B e. CC )
74 simpl 
 |-  ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) -> n e. NN0 )
75 id 
 |-  ( ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) -> ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) )
76 72 73 74 75 binomlem 
 |-  ( ( ( n e. NN0 /\ ( A e. CC /\ B e. CC ) ) /\ ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) ) -> ( ( A + B ) ^ ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) )
77 76 exp31 
 |-  ( n e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) -> ( ( A + B ) ^ ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) ) ) )
78 77 a2d 
 |-  ( n e. NN0 -> ( ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ n ) = sum_ k e. ( 0 ... n ) ( ( n _C k ) x. ( ( A ^ ( n - k ) ) x. ( B ^ k ) ) ) ) -> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ ( n + 1 ) ) = sum_ k e. ( 0 ... ( n + 1 ) ) ( ( ( n + 1 ) _C k ) x. ( ( A ^ ( ( n + 1 ) - k ) ) x. ( B ^ k ) ) ) ) ) )
79 11 22 33 44 71 78 nn0ind 
 |-  ( N e. NN0 -> ( ( A e. CC /\ B e. CC ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) ) )
80 79 impcom 
 |-  ( ( ( A e. CC /\ B e. CC ) /\ N e. NN0 ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )
81 80 3impa 
 |-  ( ( A e. CC /\ B e. CC /\ N e. NN0 ) -> ( ( A + B ) ^ N ) = sum_ k e. ( 0 ... N ) ( ( N _C k ) x. ( ( A ^ ( N - k ) ) x. ( B ^ k ) ) ) )