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 ) ) ) )