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 48452

Description: Alternate proof of altgsumbc 48451, using Pascal's rule (bcpascm1 48450) instead of the binomial theorem (binom 15737). (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 13424	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
2		bcpascm1 48450	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
3	1, 2	sylan2 593	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
4	3	eqcomd 2737	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))
5	4	oveq2d 7362	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · (𝑁C𝑘)) = ((-1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))))
6		ax-1cn 11064	. . . . . . 7 ⊢ 1 ∈ ℂ
7		negcl 11360	. . . . . . . 8 ⊢ (1 ∈ ℂ → -1 ∈ ℂ)
8		elfznn0 13520	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
9		expcl 13986	. . . . . . . 8 ⊢ ((-1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → (-1↑𝑘) ∈ ℂ)
10	7, 8, 9	syl2an 596	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
11	6, 10	mpan 690	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (-1↑𝑘) ∈ ℂ)
12	11	adantl 481	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
13		nnm1nn0 12422	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
14		bccl 14229	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℕ₀)
15	14	nn0cnd 12444	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℂ)
16	13, 1, 15	syl2an 596	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ)
17		peano2zm 12515	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
18	1, 17	syl 17	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
19		bccl 14229	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
20	19	nn0cnd 12444	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
21	13, 18, 20	syl2an 596	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
22	12, 16, 21	adddid 11136	. . . 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 15609	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)(((-1↑𝑘) · ((𝑁 − 1)C𝑘)) + ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
25		fzfid 13880	. . . 4 ⊢ (𝑁 ∈ ℕ → (0...𝑁) ∈ Fin)
26		neg1cn 12110	. . . . . . 7 ⊢ -1 ∈ ℂ
27	26	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
28	27, 8, 9	syl2an 596	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (-1↑𝑘) ∈ ℂ)
29	28, 16	mulcld 11132	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ)
30		1z 12502	. . . . . . . 8 ⊢ 1 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ)
32	1, 31	zsubcld 12582	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
33	13, 32, 20	syl2an 596	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
34	28, 33	mulcld 11132	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
35	25, 29, 34	fsumadd 15647	. . 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 12480	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℤ)
38		nnz 12489	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
39		oveq2 7354	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → (-1↑𝑘) = (-1↑(𝑗 − 1)))
40		oveq2 7354	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1)))
41	39, 40	oveq12d 7364	. . . . . 6 ⊢ (𝑘 = (𝑗 − 1) → ((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
42	36, 37, 38, 29, 41	fsumshft 15687	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
43		0p1e1 12242	. . . . . . . 8 ⊢ (0 + 1) = 1
44	43	oveq1i 7356	. . . . . . 7 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
45	44	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
46	45	sumeq1d 15607	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
47		elnnuz 12776	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
48	47	biimpi 216	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
49	26	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈ ℂ)
50		elfznn 13453	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
51		nnm1nn0 12422	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ₀)
52	50, 51	syl 17	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ₀)
53	52	adantl 481	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ₀)
54	49, 53	expcld 14053	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (-1↑(𝑗 − 1)) ∈ ℂ)
55		elfzelz 13424	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
56		elfzel1 13423	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈ ℤ)
57	55, 56	zsubcld 12582	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
58		bccl 14229	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℕ₀)
59	58	nn0cnd 12444	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
60	13, 57, 59	syl2an 596	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
61	54, 60	mulcld 11132	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈ ℂ)
62		oveq1 7353	. . . . . . . . 9 ⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
63	62	oveq2d 7362	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → (-1↑(𝑗 − 1)) = (-1↑((𝑁 + 1) − 1)))
64	62	oveq2d 7362	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1)))
65	63, 64	oveq12d 7364	. . . . . . 7 ⊢ (𝑗 = (𝑁 + 1) → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))
66	48, 61, 65	fsump1 15663	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))))
67		nncn 12133	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
68		pncan1 11541	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
69	67, 68	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
70		nnnn0 12388	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
71	69, 70	eqeltrd 2831	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℕ₀)
72	71	nn0zd 12494	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℤ)
73		nnre 12132	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
74		ltm1 11963	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁)
75	73, 74	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
76	75, 69	breqtrrd 5117	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) − 1))
77	76	olcd 874	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1)))
78		bcval4 14214	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧ (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1))) → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
79	13, 72, 77, 78	syl3anc 1373	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
80	79	oveq2d 7362	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = ((-1↑((𝑁 + 1) − 1)) · 0))
81	27, 71	expcld 14053	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (-1↑((𝑁 + 1) − 1)) ∈ ℂ)
82	81	mul01d 11312	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · 0) = 0)
83	80, 82	eqtrd 2766	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = 0)
84	83	oveq2d 7362	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + ((-1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0))
85		oveq1 7353	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
86	85	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → (-1↑(𝑗 − 1)) = (-1↑(𝑘 − 1)))
87	85	oveq2d 7362	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1)))
88	86, 87	oveq12d 7364	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → ((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
89	88	cbvsumv 15603	. . . . . . . . 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 7361	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)((-1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0))
92		fzfid 13880	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
93	26	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈ ℂ)
94		elfznn 13453	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
95		nnm1nn0 12422	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
96	94, 95	syl 17	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
97	96	adantl 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
98	93, 97	expcld 14053	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑(𝑘 − 1)) ∈ ℂ)
99		elfzelz 13424	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ)
100		elfzel1 13423	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ)
101	99, 100	zsubcld 12582	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ)
102	13, 101, 19	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
103	102	nn0cnd 12444	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
104	98, 103	mulcld 11132	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
105	92, 104	fsumcl 15640	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
106	105	addridd 11313	. . . . . . 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 12777	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
111	70, 110	sylib 218	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘0))
112		oveq2 7354	. . . . . . 7 ⊢ (𝑘 = 0 → (-1↑𝑘) = (-1↑0))
113		oveq1 7353	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
114	113	oveq2d 7362	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1)))
115	112, 114	oveq12d 7364	. . . . . 6 ⊢ (𝑘 = 0 → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1↑0) · ((𝑁 − 1)C(0 − 1))))
116	111, 34, 115	fsum1p 15660	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
117	27	exp0d 14047	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (-1↑0) = 1)
118		0z 12479	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
119		zsubcl 12514	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
120	118, 30, 119	mp2an 692	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
121	120	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 − 1) ∈ ℤ)
122		0re 11114	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
123		ltm1 11963	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
124	122, 123	mp1i 13	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (0 − 1) < 0)
125	124	orcd 873	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1)))
126		bcval4 14214	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1))) → ((𝑁 − 1)C(0 − 1)) = 0)
127	13, 121, 125, 126	syl3anc 1373	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) = 0)
128	117, 127	oveq12d 7364	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → ((-1↑0) · ((𝑁 − 1)C(0 − 1))) = (1 · 0))
129	6	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
130	129	mul01d 11312	. . . . . . 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 7361	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...𝑁) = (1...𝑁))
134	99	zcnd 12578	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ)
135		npcan1 11542	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
136	135	eqcomd 2737	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1))
137	134, 136	syl 17	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1))
138	137	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1))
139	138	oveq2d 7362	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = (-1↑((𝑘 − 1) + 1)))
140		expp1 13975	. . . . . . . . . . . 12 ⊢ ((-1 ∈ ℂ ∧ (𝑘 − 1) ∈ ℕ₀) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
141	27, 96, 140	syl2an 596	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑((𝑘 − 1) + 1)) = ((-1↑(𝑘 − 1)) · -1))
142	139, 141	eqtrd 2766	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (-1↑𝑘) = ((-1↑(𝑘 − 1)) · -1))
143	142	oveq1d 7361	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))))
144	98, 93	mulcomd 11133	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((-1↑(𝑘 − 1)) · -1) = (-1 · (-1↑(𝑘 − 1))))
145	144	oveq1d 7361	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (((-1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = ((-1 · (-1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))))
146	93, 98, 103	mulassd 11135	. . . . . . . . 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 15614	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)((-1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)(-1 · ((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
149	92, 27, 104	fsummulc2 15691	. . . . . . 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 7364	. . . . 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 11132	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈ ℂ)
153	152	addlidd 11314	. . . . 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 7364	. . 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 11569	. . . 4 ⊢ (𝑁 ∈ ℕ → (-1 · Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)((-1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
158	157	oveq2d 7362	. . 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 11462	. . 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 395 ∨ wo 847 = wceq 1541 ∈ wcel 2111 class class class wbr 5089 ‘cfv 6481 (class class class)co 7346 ℂcc 11004 ℝcr 11005 0cc0 11006 1c1 11007 + caddc 11009 · cmul 11011 < clt 11146 − cmin 11344 -cneg 11345 ℕcn 12125 ℕ₀cn0 12381 ℤcz 12468 ℤ_≥cuz 12732 ...cfz 13407 ↑cexp 13968 Ccbc 14209 Σcsu 15593

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 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5215 ax-sep 5232 ax-nul 5242 ax-pow 5301 ax-pr 5368 ax-un 7668 ax-inf2 9531 ax-cnex 11062 ax-resscn 11063 ax-1cn 11064 ax-icn 11065 ax-addcl 11066 ax-addrcl 11067 ax-mulcl 11068 ax-mulrcl 11069 ax-mulcom 11070 ax-addass 11071 ax-mulass 11072 ax-distr 11073 ax-i2m1 11074 ax-1ne0 11075 ax-1rid 11076 ax-rnegex 11077 ax-rrecex 11078 ax-cnre 11079 ax-pre-lttri 11080 ax-pre-lttrn 11081 ax-pre-ltadd 11082 ax-pre-mulgt0 11083 ax-pre-sup 11084

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 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4281 df-if 4473 df-pw 4549 df-sn 4574 df-pr 4576 df-op 4580 df-uni 4857 df-int 4896 df-iun 4941 df-br 5090 df-opab 5152 df-mpt 5171 df-tr 5197 df-id 5509 df-eprel 5514 df-po 5522 df-so 5523 df-fr 5567 df-se 5568 df-we 5569 df-xp 5620 df-rel 5621 df-cnv 5622 df-co 5623 df-dm 5624 df-rn 5625 df-res 5626 df-ima 5627 df-pred 6248 df-ord 6309 df-on 6310 df-lim 6311 df-suc 6312 df-iota 6437 df-fun 6483 df-fn 6484 df-f 6485 df-f1 6486 df-fo 6487 df-f1o 6488 df-fv 6489 df-isom 6490 df-riota 7303 df-ov 7349 df-oprab 7350 df-mpo 7351 df-om 7797 df-1st 7921 df-2nd 7922 df-frecs 8211 df-wrecs 8242 df-recs 8291 df-rdg 8329 df-1o 8385 df-er 8622 df-en 8870 df-dom 8871 df-sdom 8872 df-fin 8873 df-sup 9326 df-oi 9396 df-card 9832 df-pnf 11148 df-mnf 11149 df-xr 11150 df-ltxr 11151 df-le 11152 df-sub 11346 df-neg 11347 df-div 11775 df-nn 12126 df-2 12188 df-3 12189 df-n0 12382 df-z 12469 df-uz 12733 df-rp 12891 df-fz 13408 df-fzo 13555 df-seq 13909 df-exp 13969 df-fac 14181 df-bc 14210 df-hash 14238 df-cj 15006 df-re 15007 df-im 15008 df-sqrt 15142 df-abs 15143 df-clim 15395 df-sum 15594

This theorem is referenced by: (None)

W3C validator