bcpasc - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > bcpasc		Structured version Visualization version GIF version

Theorem bcpasc 14357

Description: Pascal's rule for the binomial coefficient, generalized to all integers 𝐾. Equation 2 of [Gleason] p. 295. (Contributed by NM, 13-Jul-2005.) (Revised by Mario Carneiro, 10-Mar-2014.)

**Assertion**
Ref	Expression
bcpasc	⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))

**Proof of Theorem bcpasc**
Step	Hyp	Ref	Expression
1		peano2nn0 12544	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
2		elfzp12 13631	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
3		nn0uz 12900	. . . . . . 7 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleq2s 2887	. . . . . 6 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
5	1, 4	syl 18	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
6		1p0e1 12363	. . . . . . . 8 ⊢ (1 + 0) = 1
7		bcn0 14346	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C0) = 1)
8		0z 12602	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
9		1z 12624	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
10		zsubcl 12636	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
11	8, 9, 10	mp2an 704	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
12		0re 11210	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
13		ltm1 12057	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
14	12, 13	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 − 1) < 0
15	14	orci 878	. . . . . . . . . 10 ⊢ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))
16		bcval4 14343	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
17	11, 15, 16	mp3an23 1479	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(0 − 1)) = 0)
18	7, 17	oveq12d 7429	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = (1 + 0))
19		bcn0 14346	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
20	1, 19	syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
21	6, 18, 20	3eqtr4a 2830	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0))
22		oveq2 7419	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C𝐾) = (𝑁C0))
23		oveq1 7418	. . . . . . . . . 10 ⊢ (𝐾 = 0 → (𝐾 − 1) = (0 − 1))
24	23	oveq2d 7427	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C(𝐾 − 1)) = (𝑁C(0 − 1)))
25	22, 24	oveq12d 7429	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁C0) + (𝑁C(0 − 1))))
26		oveq2 7419	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C0))
27	25, 26	eqeq12d 2785	. . . . . . 7 ⊢ (𝐾 = 0 → (((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾) ↔ ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0)))
28	21, 27	syl5ibrcom 250	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
29		simpr 489	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))
30		0p1e1 12361	. . . . . . . . . 10 ⊢ (0 + 1) = 1
31	30	oveq1i 7421	. . . . . . . . 9 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
32	29, 31	eleqtrdi 2879	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ (1...(𝑁 + 1)))
33		nn0p1nn 12543	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
34		nnuz 12901	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
35	33, 34	eleqtrdi 2879	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘1))
36		fzm1 13635	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))))
37	36	biimpa 481	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
38	35, 37	sylan 591	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
39		nn0cn 12514	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
40		ax-1cn 11158	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
41		pncan 11463	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
42	39, 40, 41	sylancl 597	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) − 1) = 𝑁)
43	42	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (1...((𝑁 + 1) − 1)) = (1...𝑁))
44	43	eleq2d 2855	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ↔ 𝐾 ∈ (1...𝑁)))
45	44	biimpa 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → 𝐾 ∈ (1...𝑁))
46		fz1ssfz0 13651	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
47	46	sseli 3941	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁))
48		bcp1n 14352	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
49	47, 48	syl 18	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
50		bcrpcl 14344	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
51	47, 50	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
52	51	rpcnd 13062	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℂ)
53		elfzuz2 13557	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘1))
54	53, 34	eleqtrrdi 2880	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ)
55	54	peano2nnd 12250	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℕ)
56	55	nncnd 12249	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℂ)
57	54	nncnd 12249	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ)
58		1cnd 11202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ)
59		elfzelz 13552	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
60	59	zcnd 12701	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ)
61	57, 58, 60	addsubd 11590	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1))
62		fznn0sub 13584	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
63		nn0p1nn 12543	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
64	62, 63	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
65	61, 64	eqeltrd 2869	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ)
66	65	nncnd 12249	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ)
67	65	nnne0d 12286	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0)
68	52, 56, 66, 67	div12d 12027	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))))
69	65	nnrpd 13058	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ⁺)
70	51, 69	rpdivcld 13077	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℝ⁺)
71	70	rpcnd 13062	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℂ)
72	56, 71	mulcomd 11230	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
73	68, 72	eqtrd 2804	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
74	56, 60	npcand 11573	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) + 𝐾) = (𝑁 + 1))
75	74	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
76	71, 66, 60	adddid 11233	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
77	73, 75, 76	3eqtr2d 2810	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
78	52, 66, 67	divcan1d 11992	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) = (𝑁C𝐾))
79		elfznn 13581	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
80	79	nnne0d 12286	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0)
81	52, 66, 60, 67, 80	divdiv2d 12023	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)))
82		bcm1k 14351	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)))
83	57, 60, 58	subsub3d 11599	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 + 1) − 𝐾))
84	83	oveq1d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 + 1) − 𝐾) / 𝐾))
85	84	oveq2d 7427	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
86	82, 85	eqtrd 2804	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
87		fzelp1 13604	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (1...(𝑁 + 1)))
88	55	nnzd 12617	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℤ)
89		elfzm1b 13630	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
90	59, 88, 89	syl2anc 595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
91	87, 90	mpbid 235	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)))
92	57, 40, 41	sylancl 597	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 1) = 𝑁)
93	92	oveq2d 7427	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
94	91, 93	eleqtrd 2871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁))
95		bcrpcl 14344	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
96	94, 95	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
97	96	rpcnd 13062	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℂ)
98	79	nnrpd 13058	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℝ⁺)
99	69, 98	rpdivcld 13077	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℝ⁺)
100	99	rpcnd 13062	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℂ)
101	99	rpne0d 13065	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ≠ 0)
102	52, 97, 100, 101	divmul3d 12025	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)) ↔ (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾))))
103	86, 102	mpbird 260	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)))
104	52, 60, 66, 67	div23d 12028	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾))
105	81, 103, 104	3eqtr3rd 2813	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾) = (𝑁C(𝐾 − 1)))
106	78, 105	oveq12d 7429	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)) = ((𝑁C𝐾) + (𝑁C(𝐾 − 1))))
107	49, 77, 106	3eqtrrd 2809	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
108	45, 107	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
109		oveq2 7419	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑁 + 1) → (𝑁C𝐾) = (𝑁C(𝑁 + 1)))
110	33	nnzd 12617	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
111		nn0re 12513	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
112	111	ltp1d 12145	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 < (𝑁 + 1))
113	112	olcd 887	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1)))
114		bcval4 14343	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℤ ∧ ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0)
115	110, 113, 114	mpd3an23 1489	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(𝑁 + 1)) = 0)
116	109, 115	sylan9eqr 2826	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝐾) = 0)
117		oveq1 7418	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = (𝑁 + 1) → (𝐾 − 1) = ((𝑁 + 1) − 1))
118	117, 42	sylan9eqr 2826	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝐾 − 1) = 𝑁)
119	118	oveq2d 7427	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = (𝑁C𝑁))
120		bcnn 14348	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C𝑁) = 1)
121	120	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝑁) = 1)
122	119, 121	eqtrd 2804	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = 1)
123	116, 122	oveq12d 7429	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 1))
124		oveq2 7419	. . . . . . . . . . . 12 ⊢ (𝐾 = (𝑁 + 1) → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C(𝑁 + 1)))
125		bcnn 14348	. . . . . . . . . . . . 13 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
126	1, 125	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
127	124, 126	sylan9eqr 2826	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁 + 1)C𝐾) = 1)
128	30, 123, 127	3eqtr4a 2830	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
129	108, 128	jaodan 972	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
130	38, 129	syldan 602	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
131	32, 130	syldan 602	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
132	131	ex 417	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
133	28, 132	jaod 872	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ((𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
134	5, 133	sylbid 243	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
135	134	imp 411	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
136	135	adantlr 727	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
137		00id 11385	. . 3 ⊢ (0 + 0) = 0
138		fzelp1 13604	. . . . . 6 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1)))
139	138	con3i 155	. . . . 5 ⊢ (¬ 𝐾 ∈ (0...(𝑁 + 1)) → ¬ 𝐾 ∈ (0...𝑁))
140		bcval3 14342	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
141	140	3expa 1134	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
142	139, 141	sylan2 604	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C𝐾) = 0)
143		simpll 778	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℕ₀)
144		simplr 780	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝐾 ∈ ℤ)
145		peano2zm 12637	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
146	144, 145	syl 18	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝐾 − 1) ∈ ℤ)
147	39	adantr 485	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℂ)
148	147, 40, 41	sylancl 597	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁 + 1) − 1) = 𝑁)
149	148	oveq2d 7427	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
150	149	eleq2d 2855	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) ↔ (𝐾 − 1) ∈ (0...𝑁)))
151		id 23	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℤ)
152	1	nn0zd 12616	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
153	151, 152, 89	syl2anr 608	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
154		fz1ssfz0 13651	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
155	154	sseli 3941	. . . . . . . 8 ⊢ (𝐾 ∈ (1...(𝑁 + 1)) → 𝐾 ∈ (0...(𝑁 + 1)))
156	153, 155	biimtrrdi 257	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) → 𝐾 ∈ (0...(𝑁 + 1))))
157	150, 156	sylbird 263	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1))))
158	157	con3dimp 413	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ (𝐾 − 1) ∈ (0...𝑁))
159		bcval3 14342	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 − 1) ∈ ℤ ∧ ¬ (𝐾 − 1) ∈ (0...𝑁)) → (𝑁C(𝐾 − 1)) = 0)
160	143, 146, 158, 159	syl3anc 1396	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C(𝐾 − 1)) = 0)
161	142, 160	oveq12d 7429	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 0))
162	143, 1	syl 18	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁 + 1) ∈ ℕ₀)
163		simpr 489	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ 𝐾 ∈ (0...(𝑁 + 1)))
164		bcval3 14342	. . . 4 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
165	162, 144, 163, 164	syl3anc 1396	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
166	137, 161, 165	3eqtr4a 2830	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
167	136, 166	pm2.61dan 824	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 = wceq 1567 ∈ wcel 2149 class class class wbr 5113 ‘cfv 6537 (class class class)co 7411 ℂcc 11098 ℝcr 11099 0cc0 11100 1c1 11101 + caddc 11103 · cmul 11105 < clt 11243 − cmin 11441 / cdiv 11871 ℕcn 12233 ℕ₀cn0 12504 ℤcz 12591 ℤ_≥cuz 12862 ℝ⁺crp 13016 ...cfz 13535 Ccbc 14338

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4877 df-iun 4962 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-om 7863 df-1st 7986 df-2nd 7987 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-er 8694 df-en 8944 df-dom 8945 df-sdom 8946 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-div 11872 df-nn 12234 df-n0 12505 df-z 12592 df-uz 12863 df-rp 13017 df-fz 13536 df-seq 14038 df-fac 14310 df-bc 14339

This theorem is referenced by: bccl 14358 bcn2m1 14360 bcn2p1 14361 hashbclem 14489 binomlem 15883 bcxmas 15889 binomfallfaclem2 16094 srgbinomlem 20312 bcp1ctr 27409 ex-bc 30744 bccolsum 36130 fwddifnp1 36556 5bc2eq10 42799 sticksstones22 42825 dvnmul 46549 bcpascm1 49016

W3C validator