altgsumbcALT - Mathbox for Alexander van der Vekens

	Mathbox for Alexander van der Vekens		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > altgsumbcALT		Structured version Visualization version GIF version

Theorem altgsumbcALT 47732

Description: Alternate proof of altgsumbc 47731, using Pascal's rule (bcpascm1 47730) instead of the binomial theorem (binom 15834). (Contributed by AV, 8-Sep-2019.) (Proof modification is discouraged.) (New usage is discouraged.)

**Assertion**
Ref	Expression
altgsumbcALT	⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)

Distinct variable group: 𝑘,𝑁

Proof of Theorem altgsumbcALT Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		elfzelz 13555	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
2		bcpascm1 47730	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
3	1, 2	sylan2 591	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
4	3	eqcomd 2732	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))
5	4	oveq2d 7440	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))))
6		ax-1cn 11216	. . . . . . 7 ⊢ 1 ∈ ℂ
7		negcl 11510	. . . . . . . 8 ⊢ (1 ∈ ℂ → -1 ∈ ℂ)
8		elfznn0 13648	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
9		expcl 14099	. . . . . . . 8 ⊢ ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
10	7, 8, 9	syl2an 594	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
11	6, 10	mpan 688	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ)
12	11	adantl 480	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
13		nnm1nn0 12565	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
14		bccl 14339	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℕ₀)
15	14	nn0cnd 12586	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℂ)
16	13, 1, 15	syl2an 594	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ)
17		peano2zm 12657	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
18	1, 17	syl 17	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
19		bccl 14339	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
20	19	nn0cnd 12586	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
21	13, 18, 20	syl2an 594	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
22	12, 16, 21	adddid 11288	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
23	5, 22	eqtrd 2766	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
24	23	sumeq2dv 15707	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
25		fzfid 13993	. . . 4 ⊢ (𝑁 ∈ ℕ → (0...𝑁) ∈ Fin)
26		neg1cn 12378	. . . . . . 7 ⊢ -1 ∈ ℂ
27	26	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
28	27, 8, 9	syl2an 594	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
29	28, 16	mulcld 11284	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ)
30		1z 12644	. . . . . . . 8 ⊢ 1 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ)
32	1, 31	zsubcld 12723	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
33	13, 32, 20	syl2an 594	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
34	28, 33	mulcld 11284	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
35	25, 29, 34	fsumadd 15744	. . 3 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
36	30	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℤ)
37		0zd 12622	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℤ)
38		nnz 12631	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
39		oveq2 7432	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1)))
40		oveq2 7432	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1)))
41	39, 40	oveq12d 7442	. . . . . 6 ⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
42	36, 37, 38, 29, 41	fsumshft 15784	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
43		0p1e1 12386	. . . . . . . 8 ⊢ (0 + 1) = 1
44	43	oveq1i 7434	. . . . . . 7 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
45	44	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
46	45	sumeq1d 15705	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
47		elnnuz 12918	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
48	47	biimpi 215	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
49	26	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈ ℂ)
50		elfznn 13584	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
51		nnm1nn0 12565	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ₀)
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ₀)
53	52	adantl 480	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ₀)
54	49, 53	expcld 14165	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ)
55		elfzelz 13555	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
56		elfzel1 13554	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈ ℤ)
57	55, 56	zsubcld 12723	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
58		bccl 14339	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℕ₀)
59	58	nn0cnd 12586	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
60	13, 57, 59	syl2an 594	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
61	54, 60	mulcld 11284	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈ ℂ)
62		oveq1 7431	. . . . . . . . 9 ⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
63	62	oveq2d 7440	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1)))
64	62	oveq2d 7440	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1)))
65	63, 64	oveq12d 7442	. . . . . . 7 ⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))
66	48, 61, 65	fsump1 15760	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))))
67		nncn 12272	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
68		pncan1 11688	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
70		nnnn0 12531	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
71	69, 70	eqeltrd 2826	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℕ₀)
72	71	nn0zd 12636	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℤ)
73		nnre 12271	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
74		ltm1 12107	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁)
75	73, 74	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
76	75, 69	breqtrrd 5181	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) − 1))
77	76	olcd 872	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1)))
78		bcval4 14324	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧ (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1))) → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
79	13, 72, 77, 78	syl3anc 1368	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
80	79	oveq2d 7440	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = ((-1↑((𝑁 + 1) − 1)) · 0))
81	27, 71	expcld 14165	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (-1↑((𝑁 + 1) − 1)) ∈ ℂ)
82	81	mul01d 11463	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · 0) = 0)
83	80, 82	eqtrd 2766	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = 0)
84	83	oveq2d 7440	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0))
85		oveq1 7431	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
86	85	oveq2d 7440	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1)))
87	85	oveq2d 7440	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1)))
88	86, 87	oveq12d 7442	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
89	88	cbvsumv 15700	. . . . . . . . 9 ⊢ Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))
90	89	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
91	90	oveq1d 7439	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0))
92		fzfid 13993	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
93	26	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈ ℂ)
94		elfznn 13584	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
95		nnm1nn0 12565	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
96	94, 95	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
97	96	adantl 480	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
98	93, 97	expcld 14165	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ)
99		elfzelz 13555	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ)
100		elfzel1 13554	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ)
101	99, 100	zsubcld 12723	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ)
102	13, 101, 19	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
103	102	nn0cnd 12586	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
104	98, 103	mulcld 11284	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
105	92, 104	fsumcl 15737	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
106	105	addridd 11464	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
107	91, 106	eqtrd 2766	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
108	66, 84, 107	3eqtrd 2770	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
109	42, 46, 108	3eqtrd 2770	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
110		elnn0uz 12919	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
111	70, 110	sylib 217	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘0))
112		oveq2 7432	. . . . . . 7 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
113		oveq1 7431	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
114	113	oveq2d 7440	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1)))
115	112, 114	oveq12d 7442	. . . . . 6 ⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 − 1))))
116	111, 34, 115	fsum1p 15757	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
117	27	exp0d 14159	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (-1↑0) = 1)
118		0z 12621	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
119		zsubcl 12656	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
120	118, 30, 119	mp2an 690	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
121	120	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 − 1) ∈ ℤ)
122		0re 11266	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
123		ltm1 12107	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
124	122, 123	mp1i 13	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (0 − 1) < 0)
125	124	orcd 871	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1)))
126		bcval4 14324	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1))) → ((𝑁 − 1)C(0 − 1)) = 0)
127	13, 121, 125, 126	syl3anc 1368	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) = 0)
128	117, 127	oveq12d 7442	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = (1 · 0))
129	6	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
130	129	mul01d 11463	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (1 · 0) = 0)
131	128, 130	eqtrd 2766	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = 0)
132	43	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 + 1) = 1)
133	132	oveq1d 7439	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...𝑁) = (1...𝑁))
134	99	zcnd 12719	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ)
135		npcan1 11689	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
136	135	eqcomd 2732	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1))
137	134, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1))
138	137	adantl 480	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1))
139	138	oveq2d 7440	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1)))
140		expp1 14088	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℂ ∧ (𝑘 − 1) ∈ ℕ₀) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
141	27, 96, 140	syl2an 594	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
142	139, 141	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1))
143	142	oveq1d 7439	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))))
144	98, 93	mulcomd 11285	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 · (-1↑(𝑘 − 1))))
145	144	oveq1d 7439	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))))
146	93, 98, 103	mulassd 11287	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
147	143, 145, 146	3eqtrd 2770	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
148	133, 147	sumeq12rdv 15711	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
149	92, 27, 104	fsummulc2 15788	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
150	148, 149	eqtr4d 2769	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
151	131, 150	oveq12d 7442	. . . . 5 ⊢ (𝑁 ∈ ℕ → (((-1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (0 + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))))
152	27, 105	mulcld 11284	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈ ℂ)
153	152	addlidd 11465	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0 + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
154	116, 151, 153	3eqtrd 2770	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
155	109, 154	oveq12d 7442	. . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))))
156	35, 155	eqtrd 2766	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))))
157	105	mulm1d 11716	. . . 4 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
158	157	oveq2d 7440	. . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
159	105	negidd 11611	. . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = 0)
160	158, 159	eqtrd 2766	. 2 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = 0)
161	24, 156, 160	3eqtrd 2770	1 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∨ wo 845 = wceq 1534 ∈ wcel 2099 class class class wbr 5153 ‘cfv 6554 (class class class)co 7424 ℂcc 11156 ℝcr 11157 0cc0 11158 1c1 11159 + caddc 11161 · cmul 11163 < clt 11298 − cmin 11494 -cneg 11495 ℕcn 12264 ℕ₀cn0 12524 ℤcz 12610 ℤ_≥cuz 12874 ...cfz 13538 ↑cexp 14081 Ccbc 14319 Σcsu 15690

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 ax-inf2 9684 ax-cnex 11214 ax-resscn 11215 ax-1cn 11216 ax-icn 11217 ax-addcl 11218 ax-addrcl 11219 ax-mulcl 11220 ax-mulrcl 11221 ax-mulcom 11222 ax-addass 11223 ax-mulass 11224 ax-distr 11225 ax-i2m1 11226 ax-1ne0 11227 ax-1rid 11228 ax-rnegex 11229 ax-rrecex 11230 ax-cnre 11231 ax-pre-lttri 11232 ax-pre-lttrn 11233 ax-pre-ltadd 11234 ax-pre-mulgt0 11235 ax-pre-sup 11236

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3364 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-se 5638 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-pred 6312 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-isom 6563 df-riota 7380 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7877 df-1st 8003 df-2nd 8004 df-frecs 8296 df-wrecs 8327 df-recs 8401 df-rdg 8440 df-1o 8496 df-er 8734 df-en 8975 df-dom 8976 df-sdom 8977 df-fin 8978 df-sup 9485 df-oi 9553 df-card 9982 df-pnf 11300 df-mnf 11301 df-xr 11302 df-ltxr 11303 df-le 11304 df-sub 11496 df-neg 11497 df-div 11922 df-nn 12265 df-2 12327 df-3 12328 df-n0 12525 df-z 12611 df-uz 12875 df-rp 13029 df-fz 13539 df-fzo 13682 df-seq 14022 df-exp 14082 df-fac 14291 df-bc 14320 df-hash 14348 df-cj 15104 df-re 15105 df-im 15106 df-sqrt 15240 df-abs 15241 df-clim 15490 df-sum 15691

This theorem is referenced by: (None)

W3C validator