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 15891). (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 13558	. . . . . . 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 2768	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))
5	4	oveq2d 7428	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))))
6		ax-1cn 11164	. . . . . . 7 ⊢ 1 ∈ ℂ
7		negcl 11463	. . . . . . . 8 ⊢ (1 ∈ ℂ → -1 ∈ ℂ)
8		elfznn0 13655	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
9		expcl 14122	. . . . . . . 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 12551	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
14		bccl 14365	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℕ₀)
15	14	nn0cnd 12573	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℂ)
16	13, 1, 15	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ)
17		peano2zm 12643	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
18	1, 17	syl 18	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
19		bccl 14365	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
20	19	nn0cnd 12573	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
21	13, 18, 20	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
22	12, 16, 21	adddid 11239	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
23	5, 22	eqtrd 2797	. . 3 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = (((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
24	23	sumeq2dv 15760	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
25		fzfid 14016	. . . 4 ⊢ (𝑁 ∈ ℕ → (0...𝑁) ∈ Fin)
26		neg1cn 12209	. . . . . . 7 ⊢ -1 ∈ ℂ
27	26	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
28	27, 8, 9	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
29	28, 16	mulcld 11235	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ)
30		1z 12630	. . . . . . . 8 ⊢ 1 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ)
32	1, 31	zsubcld 12711	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
33	13, 32, 20	syl2an 607	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
34	28, 33	mulcld 11235	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
35	25, 29, 34	fsumadd 15798	. . 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 12609	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℤ)
38		nnz 12618	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
39		oveq2 7420	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1)))
40		oveq2 7420	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1)))
41	39, 40	oveq12d 7430	. . . . . 6 ⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
42	36, 37, 38, 29, 41	fsumshft 15838	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
43		0p1e1 12367	. . . . . . . 8 ⊢ (0 + 1) = 1
44	43	oveq1i 7422	. . . . . . 7 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
45	44	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
46	45	sumeq1d 15758	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
47		elnnuz 12908	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
48	47	biimpi 219	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
49	26	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈ ℂ)
50		elfznn 13588	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
51		nnm1nn0 12551	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ₀)
52	50, 51	syl 18	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ₀)
53	52	adantl 486	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ₀)
54	49, 53	expcld 14189	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ)
55		elfzelz 13558	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
56		elfzel1 13557	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈ ℤ)
57	55, 56	zsubcld 12711	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
58		bccl 14365	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℕ₀)
59	58	nn0cnd 12573	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
60	13, 57, 59	syl2an 607	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
61	54, 60	mulcld 11235	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈ ℂ)
62		oveq1 7419	. . . . . . . . 9 ⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
63	62	oveq2d 7428	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1)))
64	62	oveq2d 7428	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1)))
65	63, 64	oveq12d 7430	. . . . . . 7 ⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))
66	48, 61, 65	fsump1 15814	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))))
67		nncn 12247	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
68		pncan1 11644	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
69	67, 68	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
70		nnnn0 12517	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
71	69, 70	eqeltrd 2862	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℕ₀)
72	71	nn0zd 12622	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℤ)
73		nnre 12246	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
74		ltm1 12063	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁)
75	73, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
76	75, 69	breqtrrd 5138	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) − 1))
77	76	olcd 887	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1)))
78		bcval4 14350	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧ (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1))) → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
79	13, 72, 77, 78	syl3anc 1397	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
80	79	oveq2d 7428	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = ((-1↑((𝑁 + 1) − 1)) · 0))
81	27, 71	expcld 14189	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (-1↑((𝑁 + 1) − 1)) ∈ ℂ)
82	81	mul01d 11415	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · 0) = 0)
83	80, 82	eqtrd 2797	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = 0)
84	83	oveq2d 7428	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0))
85		oveq1 7419	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
86	85	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1)))
87	85	oveq2d 7428	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1)))
88	86, 87	oveq12d 7430	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
89	88	cbvsumv 15754	. . . . . . . . 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 7427	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0))
92		fzfid 14016	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
93	26	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈ ℂ)
94		elfznn 13588	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
95		nnm1nn0 12551	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
96	94, 95	syl 18	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
97	96	adantl 486	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
98	93, 97	expcld 14189	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ)
99		elfzelz 13558	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ)
100		elfzel1 13557	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ)
101	99, 100	zsubcld 12711	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ)
102	13, 101, 19	syl2an 607	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
103	102	nn0cnd 12573	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
104	98, 103	mulcld 11235	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
105	92, 104	fsumcl 15791	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
106	105	addridd 11416	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
107	91, 106	eqtrd 2797	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
108	66, 84, 107	3eqtrd 2801	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
109	42, 46, 108	3eqtrd 2801	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
110		elnn0uz 12909	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
111	70, 110	sylib 221	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘0))
112		oveq2 7420	. . . . . . 7 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
113		oveq1 7419	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
114	113	oveq2d 7428	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1)))
115	112, 114	oveq12d 7430	. . . . . 6 ⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 − 1))))
116	111, 34, 115	fsum1p 15811	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
117	27	exp0d 14183	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (-1↑0) = 1)
118		0z 12608	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
119		zsubcl 12642	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
120	118, 30, 119	mp2an 704	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
121	120	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 − 1) ∈ ℤ)
122		0re 11216	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
123		ltm1 12063	. . . . . . . . . . 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 14350	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1))) → ((𝑁 − 1)C(0 − 1)) = 0)
127	13, 121, 125, 126	syl3anc 1397	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) = 0)
128	117, 127	oveq12d 7430	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = (1 · 0))
129	6	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
130	129	mul01d 11415	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (1 · 0) = 0)
131	128, 130	eqtrd 2797	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = 0)
132	43	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 + 1) = 1)
133	132	oveq1d 7427	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...𝑁) = (1...𝑁))
134	99	zcnd 12707	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ)
135		npcan1 11645	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
136	135	eqcomd 2768	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1))
137	134, 136	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1))
138	137	adantl 486	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1))
139	138	oveq2d 7428	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1)))
140		expp1 14111	. . . . . . . . . . . 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 2797	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1))
143	142	oveq1d 7427	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))))
144	98, 93	mulcomd 11236	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 · (-1↑(𝑘 − 1))))
145	144	oveq1d 7427	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))))
146	93, 98, 103	mulassd 11238	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
147	143, 145, 146	3eqtrd 2801	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
148	133, 147	sumeq12rdv 15765	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
149	92, 27, 104	fsummulc2 15842	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
150	148, 149	eqtr4d 2800	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
151	131, 150	oveq12d 7430	. . . . 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 11235	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈ ℂ)
153	152	addlidd 11417	. . . . 5 ⊢ (𝑁 ∈ ℕ → (0 + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
154	116, 151, 153	3eqtrd 2801	. . . 4 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
155	109, 154	oveq12d 7430	. . 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 2797	. 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 11672	. . . 4 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
158	157	oveq2d 7428	. . 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 11565	. . 3 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = 0)
160	158, 159	eqtrd 2797	. 2 ⊢ (𝑁 ∈ ℕ → (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))) = 0)
161	24, 156, 160	3eqtrd 2801	1 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = 0)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1569 ∈ wcel 2142 class class class wbr 5108 ‘cfv 6536 (class class class)co 7412 ℂcc 11104 ℝcr 11105 0cc0 11106 1c1 11107 + caddc 11109 · cmul 11111 < clt 11249 − cmin 11447 -cneg 11448 ℕcn 12239 ℕ₀cn0 12510 ℤcz 12597 ℤ_≥cuz 12868 ...cfz 13541 ↑cexp 14104 Ccbc 14345 Σcsu 15744

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1824 ax-4 1838 ax-5 1939 ax-6 1996 ax-7 2037 ax-8 2144 ax-9 2152 ax-10 2175 ax-11 2191 ax-12 2212 ax-ext 2734 ax-rep 5237 ax-sep 5256 ax-nul 5268 ax-pow 5335 ax-pr 5403 ax-un 7734 ax-inf2 9608 ax-cnex 11162 ax-resscn 11163 ax-1cn 11164 ax-icn 11165 ax-addcl 11166 ax-addrcl 11167 ax-mulcl 11168 ax-mulrcl 11169 ax-mulcom 11170 ax-addass 11171 ax-mulass 11172 ax-distr 11173 ax-i2m1 11174 ax-1ne0 11175 ax-1rid 11176 ax-rnegex 11177 ax-rrecex 11178 ax-cnre 11179 ax-pre-lttri 11180 ax-pre-lttrn 11181 ax-pre-ltadd 11182 ax-pre-mulgt0 11183 ax-pre-sup 11184

This proof depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1103 df-3an 1104 df-tru 1572 df-fal 1582 df-ex 1809 df-nf 1813 df-sb 2096 df-mo 2566 df-eu 2596 df-clab 2741 df-cleq 2754 df-clel 2837 df-nfc 2911 df-ne 2958 df-nel 3064 df-ral 3079 df-rex 3089 df-rmo 3368 df-reu 3369 df-rab 3416 df-v 3456 df-sbc 3744 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4487 df-pw 4563 df-sn 4589 df-pr 4591 df-op 4595 df-uni 4872 df-int 4912 df-iun 4957 df-br 5109 df-opab 5173 df-mpt 5192 df-tr 5218 df-id 5555 df-eprel 5560 df-po 5568 df-so 5569 df-fr 5613 df-se 5614 df-we 5615 df-xp 5666 df-rel 5667 df-cnv 5668 df-co 5669 df-dm 5670 df-rn 5671 df-res 5672 df-ima 5673 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 7369 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7861 df-1st 7984 df-2nd 7985 df-frecs 8276 df-wrecs 8307 df-recs 8356 df-rdg 8395 df-1o 8451 df-er 8692 df-en 8942 df-dom 8943 df-sdom 8944 df-fin 8945 df-sup 9400 df-oi 9470 df-card 9932 df-pnf 11251 df-mnf 11252 df-xr 11253 df-ltxr 11254 df-le 11255 df-sub 11449 df-neg 11450 df-div 11878 df-nn 12240 df-2 12309 df-3 12310 df-n0 12511 df-z 12598 df-uz 12869 df-rp 13023 df-fz 13542 df-fzo 13690 df-seq 14045 df-exp 14105 df-fac 14317 df-bc 14346 df-hash 14374 df-cj 15157 df-re 15158 df-im 15159 df-sqrt 15293 df-abs 15294 df-clim 15546 df-sum 15745

This theorem is used by: (None)

W3C validator