binom - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > binom		Structured version Visualization version GIF version

Theorem binom 15751

Description: The binomial theorem: (𝐴 + 𝐵)↑𝑁 is the sum from 𝑘 = 0 to 𝑁 of (𝑁C𝑘) · ((𝐴↑𝑘) · (𝐵↑(𝑁 − 𝑘)). 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 15750. This is Metamath 100 proof #44. (Contributed by NM, 7-Dec-2005.) (Proof shortened by Mario Carneiro, 24-Apr-2014.)

**Assertion**
Ref	Expression
binom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝑁 ∈ ℕ₀) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝑘,𝑁

Proof of Theorem binom Dummy variables 𝑛 𝑥 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ∈ wcel 2113 (class class class)co 7356 ℂcc 11022 0cc0 11024 1c1 11025 + caddc 11027 · cmul 11029 − cmin 11362 ℕ₀cn0 12399 ℤcz 12486 ...cfz 13421 ↑cexp 13982 Ccbc 14223 Σcsu 15607

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2182 ax-ext 2706 ax-rep 5222 ax-sep 5239 ax-nul 5249 ax-pow 5308 ax-pr 5375 ax-un 7678 ax-inf2 9548 ax-cnex 11080 ax-resscn 11081 ax-1cn 11082 ax-icn 11083 ax-addcl 11084 ax-addrcl 11085 ax-mulcl 11086 ax-mulrcl 11087 ax-mulcom 11088 ax-addass 11089 ax-mulass 11090 ax-distr 11091 ax-i2m1 11092 ax-1ne0 11093 ax-1rid 11094 ax-rnegex 11095 ax-rrecex 11096 ax-cnre 11097 ax-pre-lttri 11098 ax-pre-lttrn 11099 ax-pre-ltadd 11100 ax-pre-mulgt0 11101 ax-pre-sup 11102

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2537 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2809 df-nfc 2883 df-ne 2931 df-nel 3035 df-ral 3050 df-rex 3059 df-rmo 3348 df-reu 3349 df-rab 3398 df-v 3440 df-sbc 3739 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4579 df-pr 4581 df-op 4585 df-uni 4862 df-int 4901 df-iun 4946 df-br 5097 df-opab 5159 df-mpt 5178 df-tr 5204 df-id 5517 df-eprel 5522 df-po 5530 df-so 5531 df-fr 5575 df-se 5576 df-we 5577 df-xp 5628 df-rel 5629 df-cnv 5630 df-co 5631 df-dm 5632 df-rn 5633 df-res 5634 df-ima 5635 df-pred 6257 df-ord 6318 df-on 6319 df-lim 6320 df-suc 6321 df-iota 6446 df-fun 6492 df-fn 6493 df-f 6494 df-f1 6495 df-fo 6496 df-f1o 6497 df-fv 6498 df-isom 6499 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-en 8882 df-dom 8883 df-sdom 8884 df-fin 8885 df-sup 9343 df-oi 9413 df-card 9849 df-pnf 11166 df-mnf 11167 df-xr 11168 df-ltxr 11169 df-le 11170 df-sub 11364 df-neg 11365 df-div 11793 df-nn 12144 df-2 12206 df-3 12207 df-n0 12400 df-z 12487 df-uz 12750 df-rp 12904 df-fz 13422 df-fzo 13569 df-seq 13923 df-exp 13983 df-fac 14195 df-bc 14224 df-hash 14252 df-cj 15020 df-re 15021 df-im 15022 df-sqrt 15156 df-abs 15157 df-clim 15409 df-sum 15608

This theorem is referenced by: binom1p 15752 efaddlem 16014 basellem3 27047 lcmineqlem1 42222 jm2.22 43179 binomcxplemnn0 44532 altgsumbc 48540

W3C validator