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 13682

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 11938	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
2		elfzp12 12987	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
3		nn0uz 12281	. . . . . . 7 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleq2s 2931	. . . . . 6 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
5	1, 4	syl 17	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
6		1p0e1 11762	. . . . . . . 8 ⊢ (1 + 0) = 1
7		bcn0 13671	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C0) = 1)
8		0z 11993	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
9		1z 12013	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
10		zsubcl 12025	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
11	8, 9, 10	mp2an 690	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
12		0re 10643	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
13		ltm1 11482	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
14	12, 13	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 − 1) < 0
15	14	orci 861	. . . . . . . . . 10 ⊢ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))
16		bcval4 13668	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
17	11, 15, 16	mp3an23 1449	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(0 − 1)) = 0)
18	7, 17	oveq12d 7174	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = (1 + 0))
19		bcn0 13671	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
20	1, 19	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
21	6, 18, 20	3eqtr4a 2882	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0))
22		oveq2 7164	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C𝐾) = (𝑁C0))
23		oveq1 7163	. . . . . . . . . 10 ⊢ (𝐾 = 0 → (𝐾 − 1) = (0 − 1))
24	23	oveq2d 7172	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C(𝐾 − 1)) = (𝑁C(0 − 1)))
25	22, 24	oveq12d 7174	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁C0) + (𝑁C(0 − 1))))
26		oveq2 7164	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C0))
27	25, 26	eqeq12d 2837	. . . . . . 7 ⊢ (𝐾 = 0 → (((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾) ↔ ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0)))
28	21, 27	syl5ibrcom 249	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
29		simpr 487	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))
30		0p1e1 11760	. . . . . . . . . 10 ⊢ (0 + 1) = 1
31	30	oveq1i 7166	. . . . . . . . 9 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
32	29, 31	eleqtrdi 2923	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ (1...(𝑁 + 1)))
33		nn0p1nn 11937	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
34		nnuz 12282	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
35	33, 34	eleqtrdi 2923	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘1))
36		fzm1 12988	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))))
37	36	biimpa 479	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
38	35, 37	sylan 582	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
39		nn0cn 11908	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
40		ax-1cn 10595	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
41		pncan 10892	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
42	39, 40, 41	sylancl 588	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) − 1) = 𝑁)
43	42	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (1...((𝑁 + 1) − 1)) = (1...𝑁))
44	43	eleq2d 2898	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ↔ 𝐾 ∈ (1...𝑁)))
45	44	biimpa 479	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → 𝐾 ∈ (1...𝑁))
46		fz1ssfz0 13004	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
47	46	sseli 3963	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁))
48		bcp1n 13677	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
49	47, 48	syl 17	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
50		bcrpcl 13669	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
51	47, 50	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
52	51	rpcnd 12434	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℂ)
53		elfzuz2 12913	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘1))
54	53, 34	eleqtrrdi 2924	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ)
55	54	peano2nnd 11655	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℕ)
56	55	nncnd 11654	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℂ)
57	54	nncnd 11654	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ)
58		1cnd 10636	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ)
59		elfzelz 12909	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
60	59	zcnd 12089	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ)
61	57, 58, 60	addsubd 11018	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1))
62		fznn0sub 12940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
63		nn0p1nn 11937	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
65	61, 64	eqeltrd 2913	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ)
66	65	nncnd 11654	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ)
67	65	nnne0d 11688	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0)
68	52, 56, 66, 67	div12d 11452	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))))
69	65	nnrpd 12430	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ⁺)
70	51, 69	rpdivcld 12449	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℝ⁺)
71	70	rpcnd 12434	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℂ)
72	56, 71	mulcomd 10662	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
73	68, 72	eqtrd 2856	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
74	56, 60	npcand 11001	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) + 𝐾) = (𝑁 + 1))
75	74	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
76	71, 66, 60	adddid 10665	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
77	73, 75, 76	3eqtr2d 2862	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
78	52, 66, 67	divcan1d 11417	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) = (𝑁C𝐾))
79		elfznn 12937	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
80	79	nnne0d 11688	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0)
81	52, 66, 60, 67, 80	divdiv2d 11448	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)))
82		bcm1k 13676	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)))
83	57, 60, 58	subsub3d 11027	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 + 1) − 𝐾))
84	83	oveq1d 7171	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 + 1) − 𝐾) / 𝐾))
85	84	oveq2d 7172	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
86	82, 85	eqtrd 2856	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
87		fzelp1 12960	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (1...(𝑁 + 1)))
88	55	nnzd 12087	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℤ)
89		elfzm1b 12986	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
90	59, 88, 89	syl2anc 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
91	87, 90	mpbid 234	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)))
92	57, 40, 41	sylancl 588	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 1) = 𝑁)
93	92	oveq2d 7172	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
94	91, 93	eleqtrd 2915	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁))
95		bcrpcl 13669	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
97	96	rpcnd 12434	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℂ)
98	79	nnrpd 12430	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℝ⁺)
99	69, 98	rpdivcld 12449	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℝ⁺)
100	99	rpcnd 12434	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℂ)
101	99	rpne0d 12437	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ≠ 0)
102	52, 97, 100, 101	divmul3d 11450	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)) ↔ (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾))))
103	86, 102	mpbird 259	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)))
104	52, 60, 66, 67	div23d 11453	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾))
105	81, 103, 104	3eqtr3rd 2865	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾) = (𝑁C(𝐾 − 1)))
106	78, 105	oveq12d 7174	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)) = ((𝑁C𝐾) + (𝑁C(𝐾 − 1))))
107	49, 77, 106	3eqtrrd 2861	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
108	45, 107	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
109		oveq2 7164	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑁 + 1) → (𝑁C𝐾) = (𝑁C(𝑁 + 1)))
110	33	nnzd 12087	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
111		nn0re 11907	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
112	111	ltp1d 11570	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 < (𝑁 + 1))
113	112	olcd 870	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1)))
114		bcval4 13668	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℤ ∧ ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0)
115	110, 113, 114	mpd3an23 1459	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(𝑁 + 1)) = 0)
116	109, 115	sylan9eqr 2878	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝐾) = 0)
117		oveq1 7163	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = (𝑁 + 1) → (𝐾 − 1) = ((𝑁 + 1) − 1))
118	117, 42	sylan9eqr 2878	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝐾 − 1) = 𝑁)
119	118	oveq2d 7172	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = (𝑁C𝑁))
120		bcnn 13673	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C𝑁) = 1)
121	120	adantr 483	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝑁) = 1)
122	119, 121	eqtrd 2856	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = 1)
123	116, 122	oveq12d 7174	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 1))
124		oveq2 7164	. . . . . . . . . . . 12 ⊢ (𝐾 = (𝑁 + 1) → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C(𝑁 + 1)))
125		bcnn 13673	. . . . . . . . . . . . 13 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
126	1, 125	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
127	124, 126	sylan9eqr 2878	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁 + 1)C𝐾) = 1)
128	30, 123, 127	3eqtr4a 2882	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
129	108, 128	jaodan 954	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
130	38, 129	syldan 593	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
131	32, 130	syldan 593	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
132	131	ex 415	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
133	28, 132	jaod 855	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ((𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
134	5, 133	sylbid 242	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
135	134	imp 409	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
136	135	adantlr 713	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
137		00id 10815	. . 3 ⊢ (0 + 0) = 0
138		fzelp1 12960	. . . . . 6 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1)))
139	138	con3i 157	. . . . 5 ⊢ (¬ 𝐾 ∈ (0...(𝑁 + 1)) → ¬ 𝐾 ∈ (0...𝑁))
140		bcval3 13667	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
141	140	3expa 1114	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
142	139, 141	sylan2 594	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C𝐾) = 0)
143		simpll 765	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℕ₀)
144		simplr 767	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝐾 ∈ ℤ)
145		peano2zm 12026	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
146	144, 145	syl 17	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝐾 − 1) ∈ ℤ)
147	39	adantr 483	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℂ)
148	147, 40, 41	sylancl 588	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁 + 1) − 1) = 𝑁)
149	148	oveq2d 7172	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
150	149	eleq2d 2898	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) ↔ (𝐾 − 1) ∈ (0...𝑁)))
151		id 22	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℤ)
152	1	nn0zd 12086	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
153	151, 152, 89	syl2anr 598	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
154		fz1ssfz0 13004	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
155	154	sseli 3963	. . . . . . . 8 ⊢ (𝐾 ∈ (1...(𝑁 + 1)) → 𝐾 ∈ (0...(𝑁 + 1)))
156	153, 155	syl6bir 256	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) → 𝐾 ∈ (0...(𝑁 + 1))))
157	150, 156	sylbird 262	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1))))
158	157	con3dimp 411	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ (𝐾 − 1) ∈ (0...𝑁))
159		bcval3 13667	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 − 1) ∈ ℤ ∧ ¬ (𝐾 − 1) ∈ (0...𝑁)) → (𝑁C(𝐾 − 1)) = 0)
160	143, 146, 158, 159	syl3anc 1367	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C(𝐾 − 1)) = 0)
161	142, 160	oveq12d 7174	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 0))
162	143, 1	syl 17	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁 + 1) ∈ ℕ₀)
163		simpr 487	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ 𝐾 ∈ (0...(𝑁 + 1)))
164		bcval3 13667	. . . 4 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
165	162, 144, 163, 164	syl3anc 1367	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
166	137, 161, 165	3eqtr4a 2882	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
167	136, 166	pm2.61dan 811	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 class class class wbr 5066 ‘cfv 6355 (class class class)co 7156 ℂcc 10535 ℝcr 10536 0cc0 10537 1c1 10538 + caddc 10540 · cmul 10542 < clt 10675 − cmin 10870 / cdiv 11297 ℕcn 11638 ℕ₀cn0 11898 ℤcz 11982 ℤ_≥cuz 12244 ℝ⁺crp 12390 ...cfz 12893 Ccbc 13663

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 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 ax-sep 5203 ax-nul 5210 ax-pow 5266 ax-pr 5330 ax-un 7461 ax-cnex 10593 ax-resscn 10594 ax-1cn 10595 ax-icn 10596 ax-addcl 10597 ax-addrcl 10598 ax-mulcl 10599 ax-mulrcl 10600 ax-mulcom 10601 ax-addass 10602 ax-mulass 10603 ax-distr 10604 ax-i2m1 10605 ax-1ne0 10606 ax-1rid 10607 ax-rnegex 10608 ax-rrecex 10609 ax-cnre 10610 ax-pre-lttri 10611 ax-pre-lttrn 10612 ax-pre-ltadd 10613 ax-pre-mulgt0 10614

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1084 df-3an 1085 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-ne 3017 df-nel 3124 df-ral 3143 df-rex 3144 df-reu 3145 df-rmo 3146 df-rab 3147 df-v 3496 df-sbc 3773 df-csb 3884 df-dif 3939 df-un 3941 df-in 3943 df-ss 3952 df-pss 3954 df-nul 4292 df-if 4468 df-pw 4541 df-sn 4568 df-pr 4570 df-tp 4572 df-op 4574 df-uni 4839 df-iun 4921 df-br 5067 df-opab 5129 df-mpt 5147 df-tr 5173 df-id 5460 df-eprel 5465 df-po 5474 df-so 5475 df-fr 5514 df-we 5516 df-xp 5561 df-rel 5562 df-cnv 5563 df-co 5564 df-dm 5565 df-rn 5566 df-res 5567 df-ima 5568 df-pred 6148 df-ord 6194 df-on 6195 df-lim 6196 df-suc 6197 df-iota 6314 df-fun 6357 df-fn 6358 df-f 6359 df-f1 6360 df-fo 6361 df-f1o 6362 df-fv 6363 df-riota 7114 df-ov 7159 df-oprab 7160 df-mpo 7161 df-om 7581 df-1st 7689 df-2nd 7690 df-wrecs 7947 df-recs 8008 df-rdg 8046 df-er 8289 df-en 8510 df-dom 8511 df-sdom 8512 df-pnf 10677 df-mnf 10678 df-xr 10679 df-ltxr 10680 df-le 10681 df-sub 10872 df-neg 10873 df-div 11298 df-nn 11639 df-n0 11899 df-z 11983 df-uz 12245 df-rp 12391 df-fz 12894 df-seq 13371 df-fac 13635 df-bc 13664

This theorem is referenced by: bccl 13683 bcn2m1 13685 bcn2p1 13686 hashbclem 13811 binomlem 15184 bcxmas 15190 binomfallfaclem2 15394 srgbinomlem 19294 bcp1ctr 25855 ex-bc 28231 bccolsum 32971 fwddifnp1 33626 dvnmul 42248 bcpascm1 44419

W3C validator