binomlem - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > binomlem		GIF version

Theorem binomlem 11446

Description: Lemma for binom 11447 (binomial theorem). Inductive step. (Contributed by NM, 6-Dec-2005.) (Revised by Mario Carneiro, 24-Apr-2014.)

**Hypotheses**
Ref	Expression
binomlem.1	⊢ (𝜑 → 𝐴 ∈ ℂ)
binomlem.2	⊢ (𝜑 → 𝐵 ∈ ℂ)
binomlem.3	⊢ (𝜑 → 𝑁 ∈ ℕ₀)
binomlem.4	⊢ (𝜓 → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))))

**Assertion**
Ref	Expression
binomlem	⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑(𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))

Distinct variable groups: 𝐴,𝑘 𝐵,𝑘 𝑘,𝑁 𝜑,𝑘 Allowed substitution hint: 𝜓(𝑘)

Proof of Theorem binomlem Dummy variables 𝑗 𝑛 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		binomlem.4	. . . . . 6 ⊢ (𝜓 → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))))
2	1	adantl 275	. . . . 5 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑𝑁) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))))
3	2	oveq1d 5868	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + 𝐵)↑𝑁) · 𝐴) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴))
4		0zd 9224	. . . . . . . 8 ⊢ (𝜑 → 0 ∈ ℤ)
5		binomlem.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑁 ∈ ℕ₀)
6	5	nn0zd 9332	. . . . . . . 8 ⊢ (𝜑 → 𝑁 ∈ ℤ)
7	4, 6	fzfigd 10387	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ∈ Fin)
8		binomlem.1	. . . . . . 7 ⊢ (𝜑 → 𝐴 ∈ ℂ)
9		fzelp1 10030	. . . . . . . . 9 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ (0...(𝑁 + 1)))
10		elfzelz 9981	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℤ)
11		bccl 10701	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → (𝑁C𝑘) ∈ ℕ₀)
12	5, 10, 11	syl2an 287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℕ₀)
13	12	nn0cnd 9190	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C𝑘) ∈ ℂ)
14	9, 13	sylan2 284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) ∈ ℂ)
15		fznn0sub 10013	. . . . . . . . . 10 ⊢ (𝑘 ∈ (0...𝑁) → (𝑁 − 𝑘) ∈ ℕ₀)
16		expcl 10494	. . . . . . . . . 10 ⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ₀) → (𝐴↑(𝑁 − 𝑘)) ∈ ℂ)
17	8, 15, 16	syl2an 287	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑(𝑁 − 𝑘)) ∈ ℂ)
18		binomlem.2	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐵 ∈ ℂ)
19		elfznn0 10070	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(𝑁 + 1)) → 𝑘 ∈ ℕ₀)
20		expcl 10494	. . . . . . . . . . 11 ⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (𝐵↑𝑘) ∈ ℂ)
21	18, 19, 20	syl2an 287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐵↑𝑘) ∈ ℂ)
22	9, 21	sylan2 284	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐵↑𝑘) ∈ ℂ)
23	17, 22	mulcld 7940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) ∈ ℂ)
24	14, 23	mulcld 7940	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ)
25	7, 8, 24	fsummulc1 11412	. . . . . 6 ⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴))
26	8	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐴 ∈ ℂ)
27	14, 23, 26	mulassd 7943	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = ((𝑁C𝑘) · (((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) · 𝐴)))
28	5	nn0cnd 9190	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑁 ∈ ℂ)
29	28	adantr 274	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑁 ∈ ℂ)
30		1cnd 7936	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 1 ∈ ℂ)
31		elfzelz 9981	. . . . . . . . . . . . . . . 16 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
32	31	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℤ)
33	32	zcnd 9335	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝑘 ∈ ℂ)
34	29, 30, 33	addsubd 8251	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 + 1) − 𝑘) = ((𝑁 − 𝑘) + 1))
35	34	oveq2d 5869	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑((𝑁 + 1) − 𝑘)) = (𝐴↑((𝑁 − 𝑘) + 1)))
36		expp1 10483	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∈ ℂ ∧ (𝑁 − 𝑘) ∈ ℕ₀) → (𝐴↑((𝑁 − 𝑘) + 1)) = ((𝐴↑(𝑁 − 𝑘)) · 𝐴))
37	8, 15, 36	syl2an 287	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑((𝑁 − 𝑘) + 1)) = ((𝐴↑(𝑁 − 𝑘)) · 𝐴))
38	35, 37	eqtrd 2203	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (𝐴↑((𝑁 + 1) − 𝑘)) = ((𝐴↑(𝑁 − 𝑘)) · 𝐴))
39	38	oveq1d 5868	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)) = (((𝐴↑(𝑁 − 𝑘)) · 𝐴) · (𝐵↑𝑘)))
40	17, 26, 22	mul32d 8072	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝐴↑(𝑁 − 𝑘)) · 𝐴) · (𝐵↑𝑘)) = (((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) · 𝐴))
41	39, 40	eqtrd 2203	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)) = (((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) · 𝐴))
42	41	oveq2d 5869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = ((𝑁C𝑘) · (((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) · 𝐴)))
43	27, 42	eqtr4d 2206	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
44	43	sumeq2dv 11331	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
45		fzssp1 10023	. . . . . . . 8 ⊢ (0...𝑁) ⊆ (0...(𝑁 + 1))
46	45	a1i 9	. . . . . . 7 ⊢ (𝜑 → (0...𝑁) ⊆ (0...(𝑁 + 1)))
47		fznn0sub 10013	. . . . . . . . . . 11 ⊢ (𝑘 ∈ (0...(𝑁 + 1)) → ((𝑁 + 1) − 𝑘) ∈ ℕ₀)
48		expcl 10494	. . . . . . . . . . 11 ⊢ ((𝐴 ∈ ℂ ∧ ((𝑁 + 1) − 𝑘) ∈ ℕ₀) → (𝐴↑((𝑁 + 1) − 𝑘)) ∈ ℂ)
49	8, 47, 48	syl2an 287	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝐴↑((𝑁 + 1) − 𝑘)) ∈ ℂ)
50	49, 21	mulcld 7940	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)) ∈ ℂ)
51	13, 50	mulcld 7940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ)
52	9, 51	sylan2 284	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ)
53	5	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → 𝑁 ∈ ℕ₀)
54		eldifi 3249	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁)) → 𝑘 ∈ (0...(𝑁 + 1)))
55	54, 10	syl 14	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁)) → 𝑘 ∈ ℤ)
56	55	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → 𝑘 ∈ ℤ)
57		eldifn 3250	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁)) → ¬ 𝑘 ∈ (0...𝑁))
58	57	adantl 275	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → ¬ 𝑘 ∈ (0...𝑁))
59		bcval3 10685	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ ∧ ¬ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = 0)
60	53, 56, 58, 59	syl3anc 1233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → (𝑁C𝑘) = 0)
61	60	oveq1d 5868	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (0 · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
62	50	mul02d 8311	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (0 · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = 0)
63	54, 62	sylan2 284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → (0 · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = 0)
64	61, 63	eqtrd 2203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ (0...𝑁))) → ((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = 0)
65		eluzelz 9496	. . . . . . . . . 10 ⊢ (𝑛 ∈ (ℤ_≥‘0) → 𝑛 ∈ ℤ)
66	65	adantl 275	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → 𝑛 ∈ ℤ)
67		0zd 9224	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → 0 ∈ ℤ)
68	6	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → 𝑁 ∈ ℤ)
69		fzdcel 9996	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 0 ∈ ℤ ∧ 𝑁 ∈ ℤ) → DECID 𝑛 ∈ (0...𝑁))
70	66, 67, 68, 69	syl3anc 1233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → DECID 𝑛 ∈ (0...𝑁))
71	70	ralrimiva 2543	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘0)DECID 𝑛 ∈ (0...𝑁))
72		fzssuz 10021	. . . . . . . 8 ⊢ (0...(𝑁 + 1)) ⊆ (ℤ_≥‘0)
73	72	a1i 9	. . . . . . 7 ⊢ (𝜑 → (0...(𝑁 + 1)) ⊆ (ℤ_≥‘0))
74	68	peano2zd 9337	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → (𝑁 + 1) ∈ ℤ)
75		fzdcel 9996	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → DECID 𝑛 ∈ (0...(𝑁 + 1)))
76	66, 67, 74, 75	syl3anc 1233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → DECID 𝑛 ∈ (0...(𝑁 + 1)))
77	76	ralrimiva 2543	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘0)DECID 𝑛 ∈ (0...(𝑁 + 1)))
78	46, 52, 64, 71, 4, 73, 77	isumss 11354	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
79	25, 44, 78	3eqtrd 2207	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
80	79	adantr 274	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐴) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
81	3, 80	eqtrd 2203	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + 𝐵)↑𝑁) · 𝐴) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
82	1	oveq1d 5868	. . . 4 ⊢ (𝜓 → (((𝐴 + 𝐵)↑𝑁) · 𝐵) = (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵))
83	7, 18, 24	fsummulc1 11412	. . . . 5 ⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵))
84		1zzd 9239	. . . . . . . 8 ⊢ (𝜑 → 1 ∈ ℤ)
85	18	adantr 274	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → 𝐵 ∈ ℂ)
86	24, 85	mulcld 7940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) ∈ ℂ)
87		oveq2 5861	. . . . . . . . . 10 ⊢ (𝑘 = (𝑗 − 1) → (𝑁C𝑘) = (𝑁C(𝑗 − 1)))
88		oveq2 5861	. . . . . . . . . . . 12 ⊢ (𝑘 = (𝑗 − 1) → (𝑁 − 𝑘) = (𝑁 − (𝑗 − 1)))
89	88	oveq2d 5869	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 − 1) → (𝐴↑(𝑁 − 𝑘)) = (𝐴↑(𝑁 − (𝑗 − 1))))
90		oveq2 5861	. . . . . . . . . . 11 ⊢ (𝑘 = (𝑗 − 1) → (𝐵↑𝑘) = (𝐵↑(𝑗 − 1)))
91	89, 90	oveq12d 5871	. . . . . . . . . 10 ⊢ (𝑘 = (𝑗 − 1) → ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘)) = ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1))))
92	87, 91	oveq12d 5871	. . . . . . . . 9 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) = ((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))))
93	92	oveq1d 5868	. . . . . . . 8 ⊢ (𝑘 = (𝑗 − 1) → (((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = (((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))) · 𝐵))
94	84, 4, 6, 86, 93	fsumshft 11407	. . . . . . 7 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))(((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))) · 𝐵))
95		oveq1 5860	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
96	95	oveq2d 5869	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (𝑁C(𝑗 − 1)) = (𝑁C(𝑘 − 1)))
97	95	oveq2d 5869	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑁 − (𝑗 − 1)) = (𝑁 − (𝑘 − 1)))
98	97	oveq2d 5869	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐴↑(𝑁 − (𝑗 − 1))) = (𝐴↑(𝑁 − (𝑘 − 1))))
99	95	oveq2d 5869	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (𝐵↑(𝑗 − 1)) = (𝐵↑(𝑘 − 1)))
100	98, 99	oveq12d 5871	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1))) = ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1))))
101	96, 100	oveq12d 5871	. . . . . . . . 9 ⊢ (𝑗 = 𝑘 → ((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))))
102	101	oveq1d 5868	. . . . . . . 8 ⊢ (𝑗 = 𝑘 → (((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))) · 𝐵) = (((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵))
103	102	cbvsumv 11324	. . . . . . 7 ⊢ Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))(((𝑁C(𝑗 − 1)) · ((𝐴↑(𝑁 − (𝑗 − 1))) · (𝐵↑(𝑗 − 1)))) · 𝐵) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵)
104	94, 103	eqtrdi 2219	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵))
105	28	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑁 ∈ ℂ)
106		elfzelz 9981	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℤ)
107	106	adantl 275	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℤ)
108	107	zcnd 9335	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℂ)
109		1cnd 7936	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 1 ∈ ℂ)
110	105, 108, 109	subsub3d 8260	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁 − (𝑘 − 1)) = ((𝑁 + 1) − 𝑘))
111	110	oveq2d 5869	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐴↑(𝑁 − (𝑘 − 1))) = (𝐴↑((𝑁 + 1) − 𝑘)))
112	111	oveq1d 5868	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1))) = ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))))
113	112	oveq2d 5869	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) = ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1)))))
114	113	oveq1d 5868	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵) = (((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1)))) · 𝐵))
115		0z 9223	. . . . . . . . . . . 12 ⊢ 0 ∈ ℤ
116		fzp1ss 10029	. . . . . . . . . . . 12 ⊢ (0 ∈ ℤ → ((0 + 1)...(𝑁 + 1)) ⊆ (0...(𝑁 + 1)))
117	115, 116	ax-mp 5	. . . . . . . . . . 11 ⊢ ((0 + 1)...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
118	117	sseli 3143	. . . . . . . . . 10 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ (0...(𝑁 + 1)))
119	10	adantl 275	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → 𝑘 ∈ ℤ)
120		peano2zm 9250	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
121	119, 120	syl 14	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑘 − 1) ∈ ℤ)
122		bccl 10701	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → (𝑁C(𝑘 − 1)) ∈ ℕ₀)
123	5, 121, 122	syl2an2r 590	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℕ₀)
124	123	nn0cnd 9190	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ)
125	118, 124	sylan2 284	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑁C(𝑘 − 1)) ∈ ℂ)
126	118, 49	sylan2 284	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐴↑((𝑁 + 1) − 𝑘)) ∈ ℂ)
127	18	adantr 274	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐵 ∈ ℂ)
128		elfznn 10010	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...(𝑁 + 1)) → 𝑘 ∈ ℕ)
129		0p1e1 8992	. . . . . . . . . . . . . . 15 ⊢ (0 + 1) = 1
130	129	oveq1i 5863	. . . . . . . . . . . . . 14 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
131	128, 130	eleq2s 2265	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((0 + 1)...(𝑁 + 1)) → 𝑘 ∈ ℕ)
132	131	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ ℕ)
133		nnm1nn0 9176	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
134	132, 133	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝑘 − 1) ∈ ℕ₀)
135	127, 134	expcld 10609	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐵↑(𝑘 − 1)) ∈ ℂ)
136	126, 135	mulcld 7940	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))) ∈ ℂ)
137	125, 136, 127	mulassd 7943	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1)))) · 𝐵) = ((𝑁C(𝑘 − 1)) · (((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))) · 𝐵)))
138	126, 135, 127	mulassd 7943	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))) · 𝐵) = ((𝐴↑((𝑁 + 1) − 𝑘)) · ((𝐵↑(𝑘 − 1)) · 𝐵)))
139		expm1t 10504	. . . . . . . . . . . 12 ⊢ ((𝐵 ∈ ℂ ∧ 𝑘 ∈ ℕ) → (𝐵↑𝑘) = ((𝐵↑(𝑘 − 1)) · 𝐵))
140	18, 131, 139	syl2an 287	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (𝐵↑𝑘) = ((𝐵↑(𝑘 − 1)) · 𝐵))
141	140	oveq2d 5869	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)) = ((𝐴↑((𝑁 + 1) − 𝑘)) · ((𝐵↑(𝑘 − 1)) · 𝐵)))
142	138, 141	eqtr4d 2206	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))) · 𝐵) = ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))
143	142	oveq2d 5869	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · (((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑(𝑘 − 1))) · 𝐵)) = ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
144	114, 137, 143	3eqtrd 2207	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → (((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵) = ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
145	144	sumeq2dv 11331	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))(((𝑁C(𝑘 − 1)) · ((𝐴↑(𝑁 − (𝑘 − 1))) · (𝐵↑(𝑘 − 1)))) · 𝐵) = Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
146	117	a1i 9	. . . . . . 7 ⊢ (𝜑 → ((0 + 1)...(𝑁 + 1)) ⊆ (0...(𝑁 + 1)))
147	124, 50	mulcld 7940	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ)
148	118, 147	sylan2 284	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) ∈ ℂ)
149	5	adantr 274	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 𝑁 ∈ ℕ₀)
150		eldifi 3249	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1))) → 𝑘 ∈ (0...(𝑁 + 1)))
151	150	adantl 275	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 𝑘 ∈ (0...(𝑁 + 1)))
152	151, 10	syl 14	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 𝑘 ∈ ℤ)
153	152, 120	syl 14	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → (𝑘 − 1) ∈ ℤ)
154		eldifn 3250	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1))) → ¬ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))
155	154	adantl 275	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ¬ 𝑘 ∈ ((0 + 1)...(𝑁 + 1)))
156		0zd 9224	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 0 ∈ ℤ)
157	149	nn0zd 9332	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 𝑁 ∈ ℤ)
158		1zzd 9239	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 1 ∈ ℤ)
159		fzaddel 10015	. . . . . . . . . . . . 13 ⊢ (((0 ∈ ℤ ∧ 𝑁 ∈ ℤ) ∧ ((𝑘 − 1) ∈ ℤ ∧ 1 ∈ ℤ)) → ((𝑘 − 1) ∈ (0...𝑁) ↔ ((𝑘 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
160	156, 157, 153, 158, 159	syl22anc 1234	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ((𝑘 − 1) ∈ (0...𝑁) ↔ ((𝑘 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1))))
161	152	zcnd 9335	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → 𝑘 ∈ ℂ)
162		ax-1cn 7867	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
163		npcan 8128	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑘 − 1) + 1) = 𝑘)
164	161, 162, 163	sylancl 411	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ((𝑘 − 1) + 1) = 𝑘)
165	164	eleq1d 2239	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → (((𝑘 − 1) + 1) ∈ ((0 + 1)...(𝑁 + 1)) ↔ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))
166	160, 165	bitrd 187	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ((𝑘 − 1) ∈ (0...𝑁) ↔ 𝑘 ∈ ((0 + 1)...(𝑁 + 1))))
167	155, 166	mtbird 668	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ¬ (𝑘 − 1) ∈ (0...𝑁))
168		bcval3 10685	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ ∧ ¬ (𝑘 − 1) ∈ (0...𝑁)) → (𝑁C(𝑘 − 1)) = 0)
169	149, 153, 167, 168	syl3anc 1233	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → (𝑁C(𝑘 − 1)) = 0)
170	169	oveq1d 5868	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (0 · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
171	150, 62	sylan2 284	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → (0 · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = 0)
172	170, 171	eqtrd 2203	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ((0...(𝑁 + 1)) ∖ ((0 + 1)...(𝑁 + 1)))) → ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = 0)
173	67	peano2zd 9337	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → (0 + 1) ∈ ℤ)
174		fzdcel 9996	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ (0 + 1) ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → DECID 𝑛 ∈ ((0 + 1)...(𝑁 + 1)))
175	66, 173, 74, 174	syl3anc 1233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑛 ∈ (ℤ_≥‘0)) → DECID 𝑛 ∈ ((0 + 1)...(𝑁 + 1)))
176	175	ralrimiva 2543	. . . . . . 7 ⊢ (𝜑 → ∀𝑛 ∈ (ℤ_≥‘0)DECID 𝑛 ∈ ((0 + 1)...(𝑁 + 1)))
177	146, 148, 172, 176, 4, 73, 77	isumss 11354	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ ((0 + 1)...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
178	104, 145, 177	3eqtrd 2207	. . . . 5 ⊢ (𝜑 → Σ𝑘 ∈ (0...𝑁)(((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
179	83, 178	eqtrd 2203	. . . 4 ⊢ (𝜑 → (Σ𝑘 ∈ (0...𝑁)((𝑁C𝑘) · ((𝐴↑(𝑁 − 𝑘)) · (𝐵↑𝑘))) · 𝐵) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
180	82, 179	sylan9eqr 2225	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (((𝐴 + 𝐵)↑𝑁) · 𝐵) = Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
181	81, 180	oveq12d 5871	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((((𝐴 + 𝐵)↑𝑁) · 𝐴) + (((𝐴 + 𝐵)↑𝑁) · 𝐵)) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
182	8, 18	addcld 7939	. . . . 5 ⊢ (𝜑 → (𝐴 + 𝐵) ∈ ℂ)
183	182, 5	expp1d 10610	. . . 4 ⊢ (𝜑 → ((𝐴 + 𝐵)↑(𝑁 + 1)) = (((𝐴 + 𝐵)↑𝑁) · (𝐴 + 𝐵)))
184	182, 5	expcld 10609	. . . . 5 ⊢ (𝜑 → ((𝐴 + 𝐵)↑𝑁) ∈ ℂ)
185	184, 8, 18	adddid 7944	. . . 4 ⊢ (𝜑 → (((𝐴 + 𝐵)↑𝑁) · (𝐴 + 𝐵)) = ((((𝐴 + 𝐵)↑𝑁) · 𝐴) + (((𝐴 + 𝐵)↑𝑁) · 𝐵)))
186	183, 185	eqtrd 2203	. . 3 ⊢ (𝜑 → ((𝐴 + 𝐵)↑(𝑁 + 1)) = ((((𝐴 + 𝐵)↑𝑁) · 𝐴) + (((𝐴 + 𝐵)↑𝑁) · 𝐵)))
187	186	adantr 274	. 2 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑(𝑁 + 1)) = ((((𝐴 + 𝐵)↑𝑁) · 𝐴) + (((𝐴 + 𝐵)↑𝑁) · 𝐵)))
188		bcpasc 10700	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘))
189	5, 10, 188	syl2an 287	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → ((𝑁C𝑘) + (𝑁C(𝑘 − 1))) = ((𝑁 + 1)C𝑘))
190	189	oveq1d 5868	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))
191	13, 124, 50	adddird 7945	. . . . . 6 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁C𝑘) + (𝑁C(𝑘 − 1))) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
192	190, 191	eqtr3d 2205	. . . . 5 ⊢ ((𝜑 ∧ 𝑘 ∈ (0...(𝑁 + 1))) → (((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
193	192	sumeq2dv 11331	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
194	6	peano2zd 9337	. . . . . 6 ⊢ (𝜑 → (𝑁 + 1) ∈ ℤ)
195	4, 194	fzfigd 10387	. . . . 5 ⊢ (𝜑 → (0...(𝑁 + 1)) ∈ Fin)
196	195, 51, 147	fsumadd 11369	. . . 4 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + ((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
197	193, 196	eqtrd 2203	. . 3 ⊢ (𝜑 → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
198	197	adantr 274	. 2 ⊢ ((𝜑 ∧ 𝜓) → Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) = (Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))) + Σ𝑘 ∈ (0...(𝑁 + 1))((𝑁C(𝑘 − 1)) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘)))))
199	181, 187, 198	3eqtr4d 2213	1 ⊢ ((𝜑 ∧ 𝜓) → ((𝐴 + 𝐵)↑(𝑁 + 1)) = Σ𝑘 ∈ (0...(𝑁 + 1))(((𝑁 + 1)C𝑘) · ((𝐴↑((𝑁 + 1) − 𝑘)) · (𝐵↑𝑘))))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 DECID wdc 829 = wceq 1348 ∈ wcel 2141 ∖ cdif 3118 ⊆ wss 3121 ‘cfv 5198 (class class class)co 5853 ℂcc 7772 0cc0 7774 1c1 7775 + caddc 7777 · cmul 7779 − cmin 8090 ℕcn 8878 ℕ₀cn0 9135 ℤcz 9212 ℤ_≥cuz 9487 ...cfz 9965 ↑cexp 10475 Ccbc 10681 Σcsu 11316

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4104 ax-sep 4107 ax-nul 4115 ax-pow 4160 ax-pr 4194 ax-un 4418 ax-setind 4521 ax-iinf 4572 ax-cnex 7865 ax-resscn 7866 ax-1cn 7867 ax-1re 7868 ax-icn 7869 ax-addcl 7870 ax-addrcl 7871 ax-mulcl 7872 ax-mulrcl 7873 ax-addcom 7874 ax-mulcom 7875 ax-addass 7876 ax-mulass 7877 ax-distr 7878 ax-i2m1 7879 ax-0lt1 7880 ax-1rid 7881 ax-0id 7882 ax-rnegex 7883 ax-precex 7884 ax-cnre 7885 ax-pre-ltirr 7886 ax-pre-ltwlin 7887 ax-pre-lttrn 7888 ax-pre-apti 7889 ax-pre-ltadd 7890 ax-pre-mulgt0 7891 ax-pre-mulext 7892 ax-arch 7893 ax-caucvg 7894

This theorem depends on definitions: df-bi 116 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3527 df-pw 3568 df-sn 3589 df-pr 3590 df-op 3592 df-uni 3797 df-int 3832 df-iun 3875 df-br 3990 df-opab 4051 df-mpt 4052 df-tr 4088 df-id 4278 df-po 4281 df-iso 4282 df-iord 4351 df-on 4353 df-ilim 4354 df-suc 4356 df-iom 4575 df-xp 4617 df-rel 4618 df-cnv 4619 df-co 4620 df-dm 4621 df-rn 4622 df-res 4623 df-ima 4624 df-iota 5160 df-fun 5200 df-fn 5201 df-f 5202 df-f1 5203 df-fo 5204 df-f1o 5205 df-fv 5206 df-isom 5207 df-riota 5809 df-ov 5856 df-oprab 5857 df-mpo 5858 df-1st 6119 df-2nd 6120 df-recs 6284 df-irdg 6349 df-frec 6370 df-1o 6395 df-oadd 6399 df-er 6513 df-en 6719 df-dom 6720 df-fin 6721 df-pnf 7956 df-mnf 7957 df-xr 7958 df-ltxr 7959 df-le 7960 df-sub 8092 df-neg 8093 df-reap 8494 df-ap 8501 df-div 8590 df-inn 8879 df-2 8937 df-3 8938 df-4 8939 df-n0 9136 df-z 9213 df-uz 9488 df-q 9579 df-rp 9611 df-fz 9966 df-fzo 10099 df-seqfrec 10402 df-exp 10476 df-fac 10660 df-bc 10682 df-ihash 10710 df-cj 10806 df-re 10807 df-im 10808 df-rsqrt 10962 df-abs 10963 df-clim 11242 df-sumdc 11317

This theorem is referenced by: binom 11447

W3C validator