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 49161

Description: Alternate proof of altgsumbc 49160, using Pascal's rule (bcpascm1 49159) instead of the binomial theorem (binom 15889). (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 13556	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
2		bcpascm1 49159	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
3	1, 2	sylan2 604	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
4	3	eqcomd 2769	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))
5	4	oveq2d 7426	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))))
6		ax-1cn 11162	. . . . . . 7 ⊢ 1 ∈ ℂ
7		negcl 11461	. . . . . . . 8 ⊢ (1 ∈ ℂ → -1 ∈ ℂ)
8		elfznn0 13653	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
9		expcl 14120	. . . . . . . 8 ⊢ ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
10	7, 8, 9	syl2an 607	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
11	6, 10	mpan 702	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ)
12	11	adantl 486	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
13		nnm1nn0 12549	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
14		bccl 14363	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℕ₀)
15	14	nn0cnd 12571	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℂ)
16	13, 1, 15	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ)
17		peano2zm 12641	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
18	1, 17	syl 18	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
19		bccl 14363	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
20	19	nn0cnd 12571	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
21	13, 18, 20	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
22	12, 16, 21	adddid 11237	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
23	5, 22	eqtrd 2798	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
24	23	sumeq2dv 15758	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
25		fzfid 14014	. . . 4 ⊢ (𝑁 ∈ ℕ → (0...𝑁) ∈ Fin)
26		neg1cn 12207	. . . . . . 7 ⊢ -1 ∈ ℂ
27	26	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
28	27, 8, 9	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
29	28, 16	mulcld 11233	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ)
30		1z 12628	. . . . . . . 8 ⊢ 1 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ)
32	1, 31	zsubcld 12709	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
33	13, 32, 20	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
34	28, 33	mulcld 11233	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
35	25, 29, 34	fsumadd 15796	. . 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 12607	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℤ)
38		nnz 12616	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
39		oveq2 7418	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1)))
40		oveq2 7418	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1)))
41	39, 40	oveq12d 7428	. . . . . 6 ⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
42	36, 37, 38, 29, 41	fsumshft 15836	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
43		0p1e1 12365	. . . . . . . 8 ⊢ (0 + 1) = 1
44	43	oveq1i 7420	. . . . . . 7 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
45	44	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
46	45	sumeq1d 15756	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
47		elnnuz 12906	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
48	47	biimpi 219	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
49	26	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈ ℂ)
50		elfznn 13586	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
51		nnm1nn0 12549	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ₀)
52	50, 51	syl 18	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ₀)
53	52	adantl 486	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ₀)
54	49, 53	expcld 14187	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ)
55		elfzelz 13556	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
56		elfzel1 13555	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈ ℤ)
57	55, 56	zsubcld 12709	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
58		bccl 14363	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℕ₀)
59	58	nn0cnd 12571	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
60	13, 57, 59	syl2an 607	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
61	54, 60	mulcld 11233	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈ ℂ)
62		oveq1 7417	. . . . . . . . 9 ⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
63	62	oveq2d 7426	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1)))
64	62	oveq2d 7426	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1)))
65	63, 64	oveq12d 7428	. . . . . . 7 ⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))
66	48, 61, 65	fsump1 15812	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))))
67		nncn 12245	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
68		pncan1 11642	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
69	67, 68	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
70		nnnn0 12515	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
71	69, 70	eqeltrd 2863	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℕ₀)
72	71	nn0zd 12620	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℤ)
73		nnre 12244	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
74		ltm1 12061	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁)
75	73, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
76	75, 69	breqtrrd 5139	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) − 1))
77	76	olcd 887	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1)))
78		bcval4 14348	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧ (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1))) → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
79	13, 72, 77, 78	syl3anc 1398	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
80	79	oveq2d 7426	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = ((-1↑((𝑁 + 1) − 1)) · 0))
81	27, 71	expcld 14187	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (-1↑((𝑁 + 1) − 1)) ∈ ℂ)
82	81	mul01d 11413	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · 0) = 0)
83	80, 82	eqtrd 2798	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = 0)
84	83	oveq2d 7426	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0))
85		oveq1 7417	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
86	85	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1)))
87	85	oveq2d 7426	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1)))
88	86, 87	oveq12d 7428	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
89	88	cbvsumv 15752	. . . . . . . . 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 7425	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0))
92		fzfid 14014	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
93	26	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈ ℂ)
94		elfznn 13586	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
95		nnm1nn0 12549	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
96	94, 95	syl 18	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
97	96	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
98	93, 97	expcld 14187	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ)
99		elfzelz 13556	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ)
100		elfzel1 13555	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ)
101	99, 100	zsubcld 12709	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ)
102	13, 101, 19	syl2an 607	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
103	102	nn0cnd 12571	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
104	98, 103	mulcld 11233	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
105	92, 104	fsumcl 15789	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
106	105	addridd 11414	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
107	91, 106	eqtrd 2798	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
108	66, 84, 107	3eqtrd 2802	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
109	42, 46, 108	3eqtrd 2802	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
110		elnn0uz 12907	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
111	70, 110	sylib 221	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘0))
112		oveq2 7418	. . . . . . 7 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
113		oveq1 7417	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
114	113	oveq2d 7426	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1)))
115	112, 114	oveq12d 7428	. . . . . 6 ⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 − 1))))
116	111, 34, 115	fsum1p 15809	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
117	27	exp0d 14181	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (-1↑0) = 1)
118		0z 12606	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
119		zsubcl 12640	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
120	118, 30, 119	mp2an 704	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
121	120	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 − 1) ∈ ℤ)
122		0re 11214	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
123		ltm1 12061	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
124	122, 123	mp1i 14	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (0 − 1) < 0)
125	124	orcd 886	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1)))
126		bcval4 14348	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1))) → ((𝑁 − 1)C(0 − 1)) = 0)
127	13, 121, 125, 126	syl3anc 1398	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) = 0)
128	117, 127	oveq12d 7428	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = (1 · 0))
129	6	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
130	129	mul01d 11413	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (1 · 0) = 0)
131	128, 130	eqtrd 2798	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = 0)
132	43	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 + 1) = 1)
133	132	oveq1d 7425	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...𝑁) = (1...𝑁))
134	99	zcnd 12705	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ)
135		npcan1 11643	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
136	135	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1))
137	134, 136	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1))
138	137	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1))
139	138	oveq2d 7426	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1)))
140		expp1 14109	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℂ ∧ (𝑘 − 1) ∈ ℕ₀) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
141	27, 96, 140	syl2an 607	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
142	139, 141	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1))
143	142	oveq1d 7425	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))))
144	98, 93	mulcomd 11234	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 · (-1↑(𝑘 − 1))))
145	144	oveq1d 7425	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))))
146	93, 98, 103	mulassd 11236	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
147	143, 145, 146	3eqtrd 2802	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
148	133, 147	sumeq12rdv 15763	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
149	92, 27, 104	fsummulc2 15840	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
150	148, 149	eqtr4d 2801	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
151	131, 150	oveq12d 7428	. . . . 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 11233	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈ ℂ)
153	152	addlidd 11415	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0 + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
154	116, 151, 153	3eqtrd 2802	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
155	109, 154	oveq12d 7428	. . 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 2798	. 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 11670	. . . 4 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
158	157	oveq2d 7426	. . 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 11563	. . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = 0)
160	158, 159	eqtrd 2798	. 2 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = 0)
161	24, 156, 160	3eqtrd 2802	1 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 class class class wbr 5109 ‘cfv 6536 (class class class)co 7410 ℂcc 11102 ℝcr 11103 0cc0 11104 1c1 11105 + caddc 11107 · cmul 11109 < clt 11247 − cmin 11445 -cneg 11446 ℕcn 12237 ℕ₀cn0 12508 ℤcz 12595 ℤ_≥cuz 12866 ...cfz 13539 ↑cexp 14102 Ccbc 14343 Σcsu 15742

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-inf2 9606 ax-cnex 11160 ax-resscn 11161 ax-1cn 11162 ax-icn 11163 ax-addcl 11164 ax-addrcl 11165 ax-mulcl 11166 ax-mulrcl 11167 ax-mulcom 11168 ax-addass 11169 ax-mulass 11170 ax-distr 11171 ax-i2m1 11172 ax-1ne0 11173 ax-1rid 11174 ax-rnegex 11175 ax-rrecex 11176 ax-cnre 11177 ax-pre-lttri 11178 ax-pre-lttrn 11179 ax-pre-ltadd 11180 ax-pre-mulgt0 11181 ax-pre-sup 11182

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-se 5615 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-isom 6545 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-sup 9398 df-oi 9468 df-card 9930 df-pnf 11249 df-mnf 11250 df-xr 11251 df-ltxr 11252 df-le 11253 df-sub 11447 df-neg 11448 df-div 11876 df-nn 12238 df-2 12307 df-3 12308 df-n0 12509 df-z 12596 df-uz 12867 df-rp 13021 df-fz 13540 df-fzo 13688 df-seq 14043 df-exp 14103 df-fac 14315 df-bc 14344 df-hash 14372 df-cj 15155 df-re 15156 df-im 15157 df-sqrt 15291 df-abs 15292 df-clim 15544 df-sum 15743

This theorem is used by: (None)

W3C validator