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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 0 → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = ( ( 𝐴 + 𝐵 ) ↑ 0 ) )
2		oveq2	⊢ ( 𝑥 = 0 → ( 0 ... 𝑥 ) = ( 0 ... 0 ) )
3		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 C 𝑘 ) = ( 0 C 𝑘 ) )
4		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 − 𝑘 ) = ( 0 − 𝑘 ) )
5	4	oveq2d	⊢ ( 𝑥 = 0 → ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) = ( 𝐴 ↑ ( 0 − 𝑘 ) ) )
6	5	oveq1d	⊢ ( 𝑥 = 0 → ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
7	3 6	oveq12d	⊢ ( 𝑥 = 0 → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
8	7	adantr	⊢ ( ( 𝑥 = 0 ∧ 𝑘 ∈ ( 0 ... 𝑥 ) ) → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
9	2 8	sumeq12dv	⊢ ( 𝑥 = 0 → Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
10	1 9	eqeq12d	⊢ ( 𝑥 = 0 → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ↔ ( ( 𝐴 + 𝐵 ) ↑ 0 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
11	10	imbi2d	⊢ ( 𝑥 = 0 → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 0 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
12		oveq2	⊢ ( 𝑥 = 𝑛 → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) )
13		oveq2	⊢ ( 𝑥 = 𝑛 → ( 0 ... 𝑥 ) = ( 0 ... 𝑛 ) )
14		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 C 𝑘 ) = ( 𝑛 C 𝑘 ) )
15		oveq1	⊢ ( 𝑥 = 𝑛 → ( 𝑥 − 𝑘 ) = ( 𝑛 − 𝑘 ) )
16	15	oveq2d	⊢ ( 𝑥 = 𝑛 → ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) = ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) )
17	16	oveq1d	⊢ ( 𝑥 = 𝑛 → ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
18	14 17	oveq12d	⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
19	18	adantr	⊢ ( ( 𝑥 = 𝑛 ∧ 𝑘 ∈ ( 0 ... 𝑥 ) ) → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
20	13 19	sumeq12dv	⊢ ( 𝑥 = 𝑛 → Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
21	12 20	eqeq12d	⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ↔ ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
22	21	imbi2d	⊢ ( 𝑥 = 𝑛 → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
23		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) )
24		oveq2	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 0 ... 𝑥 ) = ( 0 ... ( 𝑛 + 1 ) ) )
25		oveq1	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 C 𝑘 ) = ( ( 𝑛 + 1 ) C 𝑘 ) )
26		oveq1	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝑥 − 𝑘 ) = ( ( 𝑛 + 1 ) − 𝑘 ) )
27	26	oveq2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) = ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) )
28	27	oveq1d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
29	25 28	oveq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
30	29	adantr	⊢ ( ( 𝑥 = ( 𝑛 + 1 ) ∧ 𝑘 ∈ ( 0 ... 𝑥 ) ) → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
31	24 30	sumeq12dv	⊢ ( 𝑥 = ( 𝑛 + 1 ) → Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
32	23 31	eqeq12d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ↔ ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
33	32	imbi2d	⊢ ( 𝑥 = ( 𝑛 + 1 ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
34		oveq2	⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) )
35		oveq2	⊢ ( 𝑥 = 𝑁 → ( 0 ... 𝑥 ) = ( 0 ... 𝑁 ) )
36		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 C 𝑘 ) = ( 𝑁 C 𝑘 ) )
37		oveq1	⊢ ( 𝑥 = 𝑁 → ( 𝑥 − 𝑘 ) = ( 𝑁 − 𝑘 ) )
38	37	oveq2d	⊢ ( 𝑥 = 𝑁 → ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) = ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) )
39	38	oveq1d	⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) )
40	36 39	oveq12d	⊢ ( 𝑥 = 𝑁 → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
41	40	adantr	⊢ ( ( 𝑥 = 𝑁 ∧ 𝑘 ∈ ( 0 ... 𝑥 ) ) → ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
42	35 41	sumeq12dv	⊢ ( 𝑥 = 𝑁 → Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
43	34 42	eqeq12d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ↔ ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
44	43	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑥 ) = Σ 𝑘 ∈ ( 0 ... 𝑥 ) ( ( 𝑥 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑥 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
45		exp0	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 ↑ 0 ) = 1 )
46		exp0	⊢ ( 𝐵 ∈ ℂ → ( 𝐵 ↑ 0 ) = 1 )
47	45 46	oveqan12d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) = ( 1 · 1 ) )
48		1t1e1	⊢ ( 1 · 1 ) = 1
49	47 48	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) = 1 )
50	49	oveq2d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) = ( 1 · 1 ) )
51	50 48	eqtrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) = 1 )
52		0z	⊢ 0 ∈ ℤ
53		ax-1cn	⊢ 1 ∈ ℂ
54	51 53	eqeltrdi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) ∈ ℂ )
55		oveq2	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = ( 0 C 0 ) )
56		0nn0	⊢ 0 ∈ ℕ₀
57		bcn0	⊢ ( 0 ∈ ℕ₀ → ( 0 C 0 ) = 1 )
58	56 57	ax-mp	⊢ ( 0 C 0 ) = 1
59	55 58	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 C 𝑘 ) = 1 )
60		oveq2	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = ( 0 − 0 ) )
61		0m0e0	⊢ ( 0 − 0 ) = 0
62	60 61	eqtrdi	⊢ ( 𝑘 = 0 → ( 0 − 𝑘 ) = 0 )
63	62	oveq2d	⊢ ( 𝑘 = 0 → ( 𝐴 ↑ ( 0 − 𝑘 ) ) = ( 𝐴 ↑ 0 ) )
64		oveq2	⊢ ( 𝑘 = 0 → ( 𝐵 ↑ 𝑘 ) = ( 𝐵 ↑ 0 ) )
65	63 64	oveq12d	⊢ ( 𝑘 = 0 → ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) = ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) )
66	59 65	oveq12d	⊢ ( 𝑘 = 0 → ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) )
67	66	fsum1	⊢ ( ( 0 ∈ ℤ ∧ ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) )
68	52 54 67	sylancr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) = ( 1 · ( ( 𝐴 ↑ 0 ) · ( 𝐵 ↑ 0 ) ) ) )
69		addcl	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( 𝐴 + 𝐵 ) ∈ ℂ )
70	69	exp0d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 0 ) = 1 )
71	51 68 70	3eqtr4rd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 0 ) = Σ 𝑘 ∈ ( 0 ... 0 ) ( ( 0 C 𝑘 ) · ( ( 𝐴 ↑ ( 0 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
72		simprl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝐴 ∈ ℂ )
73		simprr	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝐵 ∈ ℂ )
74		simpl	⊢ ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) → 𝑛 ∈ ℕ₀ )
75		id	⊢ ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
76	72 73 74 75	binomlem	⊢ ( ( ( 𝑛 ∈ ℕ₀ ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ) ∧ ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
77	76	exp31	⊢ ( 𝑛 ∈ ℕ₀ → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
78	77	a2d	⊢ ( 𝑛 ∈ ℕ₀ → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑛 ) = Σ 𝑘 ∈ ( 0 ... 𝑛 ) ( ( 𝑛 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑛 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ ( 𝑛 + 1 ) ) = Σ 𝑘 ∈ ( 0 ... ( 𝑛 + 1 ) ) ( ( ( 𝑛 + 1 ) C 𝑘 ) · ( ( 𝐴 ↑ ( ( 𝑛 + 1 ) − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) ) )
79	11 22 33 44 71 78	nn0ind	⊢ ( 𝑁 ∈ ℕ₀ → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) ) )
80	79	impcom	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ) ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )
81	80	3impa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀ ) → ( ( 𝐴 + 𝐵 ) ↑ 𝑁 ) = Σ 𝑘 ∈ ( 0 ... 𝑁 ) ( ( 𝑁 C 𝑘 ) · ( ( 𝐴 ↑ ( 𝑁 − 𝑘 ) ) · ( 𝐵 ↑ 𝑘 ) ) ) )

Metamath Proof Explorer

Theorem binom

Proof