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 \in ℂ \land B \in ℂ \land N \in ℕ_{0}) \to {(A + B)}^{N} = \sum_{k = 0}^{N} (\binom{N}{k}) A^{N - k} B^{k}$

Proof

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

Metamath Proof Explorer

Theorem binom

Proof