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 49668

Description: Alternate proof of altgsumbc 49667, using Pascal's rule (bcpascm1 49666) instead of the binomial theorem (binom 16025). (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 13680	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℤ)
2		bcpascm1 49666	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℤ) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
3	1, 2	sylan2 605	. . . . . 6 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))) = (𝑁C𝑘))
4	3	eqcomd 2769	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (𝑁C𝑘) = (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1))))
5	4	oveq2d 7456	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (( -1↑𝑘) · (𝑁C𝑘)) = (( -1↑𝑘) · (((𝑁 − 1)C𝑘) + ((𝑁 − 1)C(𝑘 − 1)))))
6		ax-1cn 11282	. . . . . . 7 ⊢ 1 ∈ ℂ
7		negcl 11581	. . . . . . . 8 ⊢ (1 ∈ ℂ → -1 ∈ ℂ)
8		elfznn0 13778	. . . . . . . 8 ⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ₀)
9		expcl 14246	. . . . . . . 8 ⊢ (( -1 ∈ ℂ ∧ 𝑘 ∈ ℕ₀) → ( -1↑𝑘) ∈ ℂ)
10	7, 8, 9	syl2an 608	. . . . . . 7 ⊢ ((1 ∈ ℂ ∧ 𝑘 ∈ (0...𝑁)) → ( -1↑𝑘) ∈ ℂ)
11	6, 10	mpan 703	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → ( -1↑𝑘) ∈ ℂ)
12	11	adantl 487	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ( -1↑𝑘) ∈ ℂ)
13		nnm1nn0 12671	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) ∈ ℕ₀)
14		bccl 14490	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℕ₀)
15	14	nn0cnd 12693	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ 𝑘 ∈ ℤ) → ((𝑁 − 1)C𝑘) ∈ ℂ)
16	13, 1, 15	syl2an 608	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C𝑘) ∈ ℂ)
17		peano2zm 12763	. . . . . . 7 ⊢ (𝑘 ∈ ℤ → (𝑘 − 1) ∈ ℤ)
18	1, 17	syl 18	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
19		bccl 14490	. . . . . . 7 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
20	19	nn0cnd 12693	. . . . . 6 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑘 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
21	13, 18, 20	syl2an 608	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
22	12, 16, 21	adddid 11357	. . . 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 15895	. 2 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) · (𝑁C𝑘)) = Σ𝑘 ∈ (0...𝑁)((( -1↑𝑘) · ((𝑁 − 1)C𝑘)) + (( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
25		fzfid 14140	. . . 4 ⊢ (𝑁 ∈ ℕ → (0...𝑁) ∈ Fin)
26		neg1cn 12329	. . . . . . 7 ⊢ -1 ∈ ℂ
27	26	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → -1 ∈ ℂ)
28	27, 8, 9	syl2an 608	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ( -1↑𝑘) ∈ ℂ)
29	28, 16	mulcld 11353	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (( -1↑𝑘) · ((𝑁 − 1)C𝑘)) ∈ ℂ)
30		1z 12750	. . . . . . . 8 ⊢ 1 ∈ ℤ
31	30	a1i 11	. . . . . . 7 ⊢ (𝑘 ∈ (0...𝑁) → 1 ∈ ℤ)
32	1, 31	zsubcld 12832	. . . . . 6 ⊢ (𝑘 ∈ (0...𝑁) → (𝑘 − 1) ∈ ℤ)
33	13, 32, 20	syl2an 608	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
34	28, 33	mulcld 11353	. . . 4 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (0...𝑁)) → (( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
35	25, 29, 34	fsumadd 15932	. . 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 12729	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 0 ∈ ℤ)
38		nnz 12738	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℤ)
39		oveq2 7448	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ( -1↑𝑘) = ( -1↑(𝑗 − 1)))
40		oveq2 7448	. . . . . . 7 ⊢ (𝑘 = (𝑗 − 1) → ((𝑁 − 1)C𝑘) = ((𝑁 − 1)C(𝑗 − 1)))
41	39, 40	oveq12d 7458	. . . . . 6 ⊢ (𝑘 = (𝑗 − 1) → (( -1↑𝑘) · ((𝑁 − 1)C𝑘)) = (( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
42	36, 37, 38, 29, 41	fsumshft 15972	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) · ((𝑁 − 1)C𝑘)) = Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
43		0p1e1 12487	. . . . . . . 8 ⊢ (0 + 1) = 1
44	43	oveq1i 7450	. . . . . . 7 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
45	44	a1i 11	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1)))
46	45	sumeq1d 15893	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ ((0 + 1)...(𝑁 + 1))(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = Σ𝑗 ∈ (1...(𝑁 + 1))(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))))
47		elnnuz 13029	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ ↔ 𝑁 ∈ (ℤ_≥‘1))
48	47	biimpi 219	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘1))
49	26	a1i 11	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → -1 ∈ ℂ)
50		elfznn 13711	. . . . . . . . . . 11 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℕ)
51		nnm1nn0 12671	. . . . . . . . . . 11 ⊢ (𝑗 ∈ ℕ → (𝑗 − 1) ∈ ℕ₀)
52	50, 51	syl 18	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℕ₀)
53	52	adantl 487	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (𝑗 − 1) ∈ ℕ₀)
54	49, 53	expcld 14313	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ( -1↑(𝑗 − 1)) ∈ ℂ)
55		elfzelz 13680	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 𝑗 ∈ ℤ)
56		elfzel1 13679	. . . . . . . . . 10 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → 1 ∈ ℤ)
57	55, 56	zsubcld 12832	. . . . . . . . 9 ⊢ (𝑗 ∈ (1...(𝑁 + 1)) → (𝑗 − 1) ∈ ℤ)
58		bccl 14490	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℕ₀)
59	58	nn0cnd 12693	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (𝑗 − 1) ∈ ℤ) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
60	13, 57, 59	syl2an 608	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → ((𝑁 − 1)C(𝑗 − 1)) ∈ ℂ)
61	54, 60	mulcld 11353	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ ∧ 𝑗 ∈ (1...(𝑁 + 1))) → (( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) ∈ ℂ)
62		oveq1 7447	. . . . . . . . 9 ⊢ (𝑗 = (𝑁 + 1) → (𝑗 − 1) = ((𝑁 + 1) − 1))
63	62	oveq2d 7456	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ( -1↑(𝑗 − 1)) = ( -1↑((𝑁 + 1) − 1)))
64	62	oveq2d 7456	. . . . . . . 8 ⊢ (𝑗 = (𝑁 + 1) → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C((𝑁 + 1) − 1)))
65	63, 64	oveq12d 7458	. . . . . . 7 ⊢ (𝑗 = (𝑁 + 1) → (( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (( -1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))))
66	48, 61, 65	fsump1 15948	. . . . . 6 ⊢ (𝑁 ∈ ℕ → Σ𝑗 ∈ (1...(𝑁 + 1))(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (Σ𝑗 ∈ (1...𝑁)(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + (( -1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))))
67		nncn 12367	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℂ)
68		pncan1 11764	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℂ → ((𝑁 + 1) − 1) = 𝑁)
69	67, 68	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) = 𝑁)
70		nnnn0 12637	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℕ₀)
71	69, 70	eqeltrd 2864	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℕ₀)
72	71	nn0zd 12742	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → ((𝑁 + 1) − 1) ∈ ℤ)
73		nnre 12366	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ ℝ)
74		ltm1 12183	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℝ → (𝑁 − 1) < 𝑁)
75	73, 74	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < 𝑁)
76	75, 69	breqtrrd 5136	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ → (𝑁 − 1) < ((𝑁 + 1) − 1))
77	76	olcd 888	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1)))
78		bcval4 14475	. . . . . . . . . 10 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ ((𝑁 + 1) − 1) ∈ ℤ ∧ (((𝑁 + 1) − 1) < 0 ∨ (𝑁 − 1) < ((𝑁 + 1) − 1))) → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
79	13, 72, 77, 78	syl3anc 1399	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C((𝑁 + 1) − 1)) = 0)
80	79	oveq2d 7456	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (( -1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = (( -1↑((𝑁 + 1) − 1)) · 0))
81	27, 71	expcld 14313	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ( -1↑((𝑁 + 1) − 1)) ∈ ℂ)
82	81	mul01d 11533	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → (( -1↑((𝑁 + 1) − 1)) · 0) = 0)
83	80, 82	eqtrd 2798	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (( -1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1))) = 0)
84	83	oveq2d 7456	. . . . . 6 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + (( -1↑((𝑁 + 1) − 1)) · ((𝑁 − 1)C((𝑁 + 1) − 1)))) = (Σ𝑗 ∈ (1...𝑁)(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0))
85		oveq1 7447	. . . . . . . . . . . 12 ⊢ (𝑗 = 𝑘 → (𝑗 − 1) = (𝑘 − 1))
86	85	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ( -1↑(𝑗 − 1)) = ( -1↑(𝑘 − 1)))
87	85	oveq2d 7456	. . . . . . . . . . 11 ⊢ (𝑗 = 𝑘 → ((𝑁 − 1)C(𝑗 − 1)) = ((𝑁 − 1)C(𝑘 − 1)))
88	86, 87	oveq12d 7458	. . . . . . . . . 10 ⊢ (𝑗 = 𝑘 → (( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) = (( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
89	88	cbvsumv 15889	. . . . . . . . 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 7455	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (Σ𝑗 ∈ (1...𝑁)(( -1↑(𝑗 − 1)) · ((𝑁 − 1)C(𝑗 − 1))) + 0) = (Σ𝑘 ∈ (1...𝑁)(( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) + 0))
92		fzfid 14140	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (1...𝑁) ∈ Fin)
93	26	a1i 11	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → -1 ∈ ℂ)
94		elfznn 13711	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℕ)
95		nnm1nn0 12671	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ ℕ → (𝑘 − 1) ∈ ℕ₀)
96	94, 95	syl 18	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℕ₀)
97	96	adantl 487	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (𝑘 − 1) ∈ ℕ₀)
98	93, 97	expcld 14313	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ( -1↑(𝑘 − 1)) ∈ ℂ)
99		elfzelz 13680	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℤ)
100		elfzel1 13679	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 1 ∈ ℤ)
101	99, 100	zsubcld 12832	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ (1...𝑁) → (𝑘 − 1) ∈ ℤ)
102	13, 101, 19	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℕ₀)
103	102	nn0cnd 12693	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((𝑁 − 1)C(𝑘 − 1)) ∈ ℂ)
104	98, 103	mulcld 11353	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
105	92, 104	fsumcl 15925	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (1...𝑁)(( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))) ∈ ℂ)
106	105	addridd 11534	. . . . . . 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 13030	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ ↔ 𝑁 ∈ (ℤ_≥‘0))
111	70, 110	sylib 221	. . . . . 6 ⊢ (𝑁 ∈ ℕ → 𝑁 ∈ (ℤ_≥‘0))
112		oveq2 7448	. . . . . . 7 ⊢ (𝑘 = 0 → ( -1↑𝑘) = ( -1↑0))
113		oveq1 7447	. . . . . . . 8 ⊢ (𝑘 = 0 → (𝑘 − 1) = (0 − 1))
114	113	oveq2d 7456	. . . . . . 7 ⊢ (𝑘 = 0 → ((𝑁 − 1)C(𝑘 − 1)) = ((𝑁 − 1)C(0 − 1)))
115	112, 114	oveq12d 7458	. . . . . 6 ⊢ (𝑘 = 0 → (( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = (( -1↑0) · ((𝑁 − 1)C(0 − 1))))
116	111, 34, 115	fsum1p 15945	. . . . 5 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ (0...𝑁)(( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((( -1↑0) · ((𝑁 − 1)C(0 − 1))) + Σ𝑘 ∈ ((0 + 1)...𝑁)(( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1)))))
117	27	exp0d 14307	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ( -1↑0) = 1)
118		0z 12728	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
119		zsubcl 12762	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
120	118, 30, 119	mp2an 705	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
121	120	a1i 11	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → (0 − 1) ∈ ℤ)
122		0re 11334	. . . . . . . . . . 11 ⊢ 0 ∈ ℝ
123		ltm1 12183	. . . . . . . . . . 11 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
124	122, 123	mp1i 14	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ → (0 − 1) < 0)
125	124	orcd 887	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ → ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1)))
126		bcval4 14475	. . . . . . . . 9 ⊢ (((𝑁 − 1) ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ (𝑁 − 1) < (0 − 1))) → ((𝑁 − 1)C(0 − 1)) = 0)
127	13, 121, 125, 126	syl3anc 1399	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((𝑁 − 1)C(0 − 1)) = 0)
128	117, 127	oveq12d 7458	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → (( -1↑0) · ((𝑁 − 1)C(0 − 1))) = (1 · 0))
129	6	a1i 11	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → 1 ∈ ℂ)
130	129	mul01d 11533	. . . . . . 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 7455	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ → ((0 + 1)...𝑁) = (1...𝑁))
134	99	zcnd 12828	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 ∈ ℂ)
135		npcan1 11765	. . . . . . . . . . . . . . 15 ⊢ (𝑘 ∈ ℂ → ((𝑘 − 1) + 1) = 𝑘)
136	135	eqcomd 2769	. . . . . . . . . . . . . 14 ⊢ (𝑘 ∈ ℂ → 𝑘 = ((𝑘 − 1) + 1))
137	134, 136	syl 18	. . . . . . . . . . . . 13 ⊢ (𝑘 ∈ (1...𝑁) → 𝑘 = ((𝑘 − 1) + 1))
138	137	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → 𝑘 = ((𝑘 − 1) + 1))
139	138	oveq2d 7456	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ( -1↑𝑘) = ( -1↑((𝑘 − 1) + 1)))
140		expp1 14235	. . . . . . . . . . . 12 ⊢ (( -1 ∈ ℂ ∧ (𝑘 − 1) ∈ ℕ₀) → ( -1↑((𝑘 − 1) + 1)) = (( -1↑(𝑘 − 1)) · -1))
141	27, 96, 140	syl2an 608	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ( -1↑((𝑘 − 1) + 1)) = (( -1↑(𝑘 − 1)) · -1))
142	139, 141	eqtrd 2798	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ( -1↑𝑘) = (( -1↑(𝑘 − 1)) · -1))
143	142	oveq1d 7455	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = ((( -1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))))
144	98, 93	mulcomd 11354	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → (( -1↑(𝑘 − 1)) · -1) = ( -1 · ( -1↑(𝑘 − 1))))
145	144	oveq1d 7455	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ (1...𝑁)) → ((( -1↑(𝑘 − 1)) · -1) · ((𝑁 − 1)C(𝑘 − 1))) = (( -1 · ( -1↑(𝑘 − 1))) · ((𝑁 − 1)C(𝑘 − 1))))
146	93, 98, 103	mulassd 11356	. . . . . . . . 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 15899	. . . . . . 7 ⊢ (𝑁 ∈ ℕ → Σ𝑘 ∈ ((0 + 1)...𝑁)(( -1↑𝑘) · ((𝑁 − 1)C(𝑘 − 1))) = Σ𝑘 ∈ (1...𝑁)( -1 · (( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))))
149	92, 27, 104	fsummulc2 15976	. . . . . . 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 7458	. . . . 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 11353	. . . . . 6 ⊢ (𝑁 ∈ ℕ → ( -1 · Σ𝑘 ∈ (1...𝑁)(( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) ∈ ℂ)
153	152	addlidd 11535	. . . . 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 7458	. . 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 11792	. . . 4 ⊢ (𝑁 ∈ ℕ → ( -1 · Σ𝑘 ∈ (1...𝑁)(( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1)))) = -Σ𝑘 ∈ (1...𝑁)(( -1↑(𝑘 − 1)) · ((𝑁 − 1)C(𝑘 − 1))))
158	157	oveq2d 7456	. . 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 11683	. . 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 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 class class class wbr 5106 ‘cfv 6555 (class class class)co 7440 ℂcc 11222 ℝcr 11223 0cc0 11224 1c1 11225 + caddc 11227 · cmul 11229 < clt 11367 − cmin 11565 -cneg 11566 ℕcn 12359 ℕ₀cn0 12630 ℤcz 12717 ℤ_≥cuz 12989 ...cfz 13663 ↑cexp 14228 Ccbc 14470 Σcsu 15879

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7772 ax-inf2 9666 ax-cnex 11280 ax-resscn 11281 ax-1cn 11282 ax-icn 11283 ax-addcl 11284 ax-addrcl 11285 ax-mulcl 11286 ax-mulrcl 11287 ax-mulcom 11288 ax-addass 11289 ax-mulass 11290 ax-distr 11291 ax-i2m1 11292 ax-1ne0 11293 ax-1rid 11294 ax-rnegex 11295 ax-rrecex 11296 ax-cnre 11297 ax-pre-lttri 11298 ax-pre-lttrn 11299 ax-pre-ltadd 11300 ax-pre-mulgt0 11301 ax-pre-sup 11302

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6319 df-ord 6380 df-on 6381 df-lim 6382 df-suc 6383 df-iota 6509 df-fun 6557 df-fn 6558 df-f 6559 df-f1 6560 df-fo 6561 df-f1o 6562 df-fv 6563 df-isom 6564 df-riota 7397 df-ov 7443 df-oprab 7444 df-mpo 7445 df-om 7899 df-1st 8022 df-2nd 8023 df-frecs 8324 df-wrecs 8355 df-recs 8404 df-rdg 8443 df-1o 8501 df-er 8742 df-en 8999 df-dom 9000 df-sdom 9001 df-fin 9002 df-sup 9458 df-oi 9528 df-card 10044 df-pnf 11369 df-mnf 11370 df-xr 11371 df-ltxr 11372 df-le 11373 df-sub 11567 df-neg 11568 df-div 11998 df-nn 12360 df-2 12429 df-3 12430 df-n0 12631 df-z 12718 df-uz 12990 df-rp 13145 df-fz 13664 df-fzo 13813 df-seq 14169 df-exp 14229 df-fac 14442 df-bc 14471 df-hash 14499 df-cj 15292 df-re 15293 df-im 15294 df-sqrt 15428 df-abs 15429 df-clim 15681 df-sum 15880

This theorem is used by: (None)

W3C validator