bcpasc - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > bcpasc		GIF version

Theorem bcpasc 10644

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 9131	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
2		elfzp12 10002	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
3		nn0uz 9474	. . . . . . 7 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleq2s 2252	. . . . . 6 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
5	1, 4	syl 14	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
6		1p0e1 8950	. . . . . . . 8 ⊢ (1 + 0) = 1
7		bcn0 10633	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C0) = 1)
8		0z 9179	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
9		1z 9194	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
10		zsubcl 9209	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
11	8, 9, 10	mp2an 423	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
12		0re 7879	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
13		ltm1 8718	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
14	12, 13	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 − 1) < 0
15	14	orci 721	. . . . . . . . . 10 ⊢ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))
16		bcval4 10630	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
17	11, 15, 16	mp3an23 1311	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(0 − 1)) = 0)
18	7, 17	oveq12d 5843	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = (1 + 0))
19		bcn0 10633	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
20	1, 19	syl 14	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
21	6, 18, 20	3eqtr4a 2216	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0))
22		oveq2 5833	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C𝐾) = (𝑁C0))
23		oveq1 5832	. . . . . . . . . 10 ⊢ (𝐾 = 0 → (𝐾 − 1) = (0 − 1))
24	23	oveq2d 5841	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C(𝐾 − 1)) = (𝑁C(0 − 1)))
25	22, 24	oveq12d 5843	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁C0) + (𝑁C(0 − 1))))
26		oveq2 5833	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C0))
27	25, 26	eqeq12d 2172	. . . . . . 7 ⊢ (𝐾 = 0 → (((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾) ↔ ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0)))
28	21, 27	syl5ibrcom 156	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
29		simpr 109	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))
30		0p1e1 8948	. . . . . . . . . 10 ⊢ (0 + 1) = 1
31	30	oveq1i 5835	. . . . . . . . 9 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
32	29, 31	eleqtrdi 2250	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ (1...(𝑁 + 1)))
33		nn0p1nn 9130	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
34		nnuz 9475	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
35	33, 34	eleqtrdi 2250	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘1))
36		fzm1 10003	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))))
37	36	biimpa 294	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
38	35, 37	sylan 281	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
39		nn0cn 9101	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
40		ax-1cn 7826	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
41		pncan 8082	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
42	39, 40, 41	sylancl 410	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) − 1) = 𝑁)
43	42	oveq2d 5841	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (1...((𝑁 + 1) − 1)) = (1...𝑁))
44	43	eleq2d 2227	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ↔ 𝐾 ∈ (1...𝑁)))
45	44	biimpa 294	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → 𝐾 ∈ (1...𝑁))
46		1eluzge0 9486	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ (ℤ_≥‘0)
47		fzss1 9966	. . . . . . . . . . . . . . 15 ⊢ (1 ∈ (ℤ_≥‘0) → (1...𝑁) ⊆ (0...𝑁))
48	46, 47	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
49	48	sseli 3124	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁))
50		bcp1n 10639	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
51	49, 50	syl 14	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
52		bcrpcl 10631	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
53	49, 52	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
54	53	rpcnd 9606	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℂ)
55		elfzuz2 9932	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘1))
56	55, 34	eleqtrrdi 2251	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ)
57	56	peano2nnd 8849	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℕ)
58	57	nncnd 8848	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℂ)
59	56	nncnd 8848	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ)
60		1cnd 7895	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ)
61		elfzelz 9929	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
62	61	zcnd 9288	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ)
63	59, 60, 62	addsubd 8208	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1))
64		fznn0sub 9960	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
65		nn0p1nn 9130	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
66	64, 65	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
67	63, 66	eqeltrd 2234	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ)
68	67	nncnd 8848	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ)
69	67	nnap0d 8880	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) # 0)
70	54, 58, 68, 69	div12apd 8701	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))))
71	67	nnrpd 9602	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ⁺)
72	53, 71	rpdivcld 9622	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℝ⁺)
73	72	rpcnd 9606	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℂ)
74	58, 73	mulcomd 7900	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
75	70, 74	eqtrd 2190	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
76	58, 62	npcand 8191	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) + 𝐾) = (𝑁 + 1))
77	76	oveq2d 5841	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
78	73, 68, 62	adddid 7903	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
79	75, 77, 78	3eqtr2d 2196	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
80	54, 68, 69	divcanap1d 8665	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) = (𝑁C𝐾))
81		elfznn 9957	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
82	81	nnap0d 8880	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 # 0)
83	54, 68, 62, 69, 82	divdivap2d 8697	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)))
84		bcm1k 10638	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)))
85	59, 62, 60	subsub3d 8217	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 + 1) − 𝐾))
86	85	oveq1d 5840	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 + 1) − 𝐾) / 𝐾))
87	86	oveq2d 5841	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
88	84, 87	eqtrd 2190	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
89		fzelp1 9977	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (1...(𝑁 + 1)))
90	57	nnzd 9286	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℤ)
91		elfzm1b 10001	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
92	61, 90, 91	syl2anc 409	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
93	89, 92	mpbid 146	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)))
94	59, 40, 41	sylancl 410	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 1) = 𝑁)
95	94	oveq2d 5841	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
96	93, 95	eleqtrd 2236	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁))
97		bcrpcl 10631	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
98	96, 97	syl 14	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
99	98	rpcnd 9606	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℂ)
100	81	nnrpd 9602	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℝ⁺)
101	71, 100	rpdivcld 9622	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℝ⁺)
102	101	rpcnd 9606	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℂ)
103	68, 62, 69, 82	divap0d 8680	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) # 0)
104	54, 99, 102, 103	divmulap3d 8699	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)) ↔ (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾))))
105	88, 104	mpbird 166	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)))
106	54, 62, 68, 69	div23apd 8702	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾))
107	83, 105, 106	3eqtr3rd 2199	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾) = (𝑁C(𝐾 − 1)))
108	80, 107	oveq12d 5843	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)) = ((𝑁C𝐾) + (𝑁C(𝐾 − 1))))
109	51, 79, 108	3eqtrrd 2195	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
110	45, 109	syl 14	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
111		oveq2 5833	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑁 + 1) → (𝑁C𝐾) = (𝑁C(𝑁 + 1)))
112	33	nnzd 9286	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
113		nn0re 9100	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
114	113	ltp1d 8802	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 < (𝑁 + 1))
115	114	olcd 724	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1)))
116		bcval4 10630	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℤ ∧ ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0)
117	112, 115, 116	mpd3an23 1321	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(𝑁 + 1)) = 0)
118	111, 117	sylan9eqr 2212	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝐾) = 0)
119		oveq1 5832	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = (𝑁 + 1) → (𝐾 − 1) = ((𝑁 + 1) − 1))
120	119, 42	sylan9eqr 2212	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝐾 − 1) = 𝑁)
121	120	oveq2d 5841	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = (𝑁C𝑁))
122		bcnn 10635	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C𝑁) = 1)
123	122	adantr 274	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝑁) = 1)
124	121, 123	eqtrd 2190	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = 1)
125	118, 124	oveq12d 5843	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 1))
126		oveq2 5833	. . . . . . . . . . . 12 ⊢ (𝐾 = (𝑁 + 1) → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C(𝑁 + 1)))
127		bcnn 10635	. . . . . . . . . . . . 13 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
128	1, 127	syl 14	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
129	126, 128	sylan9eqr 2212	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁 + 1)C𝐾) = 1)
130	30, 125, 129	3eqtr4a 2216	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
131	110, 130	jaodan 787	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
132	38, 131	syldan 280	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
133	32, 132	syldan 280	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
134	133	ex 114	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
135	28, 134	jaod 707	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ((𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
136	5, 135	sylbid 149	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
137	136	imp 123	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
138	137	adantlr 469	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
139		00id 8017	. . 3 ⊢ (0 + 0) = 0
140		fzelp1 9977	. . . . . 6 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1)))
141	140	con3i 622	. . . . 5 ⊢ (¬ 𝐾 ∈ (0...(𝑁 + 1)) → ¬ 𝐾 ∈ (0...𝑁))
142		bcval3 10629	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
143	142	3expa 1185	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
144	141, 143	sylan2 284	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C𝐾) = 0)
145		simpll 519	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℕ₀)
146		simplr 520	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝐾 ∈ ℤ)
147		peano2zm 9206	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
148	146, 147	syl 14	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝐾 − 1) ∈ ℤ)
149	39	adantr 274	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℂ)
150	149, 40, 41	sylancl 410	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁 + 1) − 1) = 𝑁)
151	150	oveq2d 5841	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
152	151	eleq2d 2227	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) ↔ (𝐾 − 1) ∈ (0...𝑁)))
153		id 19	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℤ)
154	1	nn0zd 9285	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
155	153, 154, 91	syl2anr 288	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
156		fzp1ss 9976	. . . . . . . . . . 11 ⊢ (0 ∈ ℤ → ((0 + 1)...(𝑁 + 1)) ⊆ (0...(𝑁 + 1)))
157	8, 156	ax-mp 5	. . . . . . . . . 10 ⊢ ((0 + 1)...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
158	31, 157	eqsstrri 3161	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
159	158	sseli 3124	. . . . . . . 8 ⊢ (𝐾 ∈ (1...(𝑁 + 1)) → 𝐾 ∈ (0...(𝑁 + 1)))
160	155, 159	syl6bir 163	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) → 𝐾 ∈ (0...(𝑁 + 1))))
161	152, 160	sylbird 169	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1))))
162	161	con3dimp 625	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ (𝐾 − 1) ∈ (0...𝑁))
163		bcval3 10629	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 − 1) ∈ ℤ ∧ ¬ (𝐾 − 1) ∈ (0...𝑁)) → (𝑁C(𝐾 − 1)) = 0)
164	145, 148, 162, 163	syl3anc 1220	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C(𝐾 − 1)) = 0)
165	144, 164	oveq12d 5843	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 0))
166	145, 1	syl 14	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁 + 1) ∈ ℕ₀)
167		simpr 109	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ 𝐾 ∈ (0...(𝑁 + 1)))
168		bcval3 10629	. . . 4 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
169	166, 146, 167, 168	syl3anc 1220	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
170	139, 165, 169	3eqtr4a 2216	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
171		simpr 109	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 𝐾 ∈ ℤ)
172		0zd 9180	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 0 ∈ ℤ)
173	112	adantr 274	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝑁 + 1) ∈ ℤ)
174		fzdcel 9943	. . . 4 ⊢ ((𝐾 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → DECID 𝐾 ∈ (0...(𝑁 + 1)))
175		exmiddc 822	. . . 4 ⊢ (DECID 𝐾 ∈ (0...(𝑁 + 1)) → (𝐾 ∈ (0...(𝑁 + 1)) ∨ ¬ 𝐾 ∈ (0...(𝑁 + 1))))
176	174, 175	syl 14	. . 3 ⊢ ((𝐾 ∈ ℤ ∧ 0 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐾 ∈ (0...(𝑁 + 1)) ∨ ¬ 𝐾 ∈ (0...(𝑁 + 1))))
177	171, 172, 173, 176	syl3anc 1220	. 2 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (0...(𝑁 + 1)) ∨ ¬ 𝐾 ∈ (0...(𝑁 + 1))))
178	138, 170, 177	mpjaodan 788	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))

Colors of variables: wff set class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 103 ↔ wb 104 ∨ wo 698 DECID wdc 820 ∧ w3a 963 = wceq 1335 ∈ wcel 2128 ⊆ wss 3102 class class class wbr 3966 ‘cfv 5171 (class class class)co 5825 ℂcc 7731 ℝcr 7732 0cc0 7733 1c1 7734 + caddc 7736 · cmul 7738 < clt 7913 − cmin 8047 / cdiv 8546 ℕcn 8834 ℕ₀cn0 9091 ℤcz 9168 ℤ_≥cuz 9440 ℝ⁺crp 9561 ...cfz 9913 Ccbc 10625

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 604 ax-in2 605 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-13 2130 ax-14 2131 ax-ext 2139 ax-coll 4080 ax-sep 4083 ax-nul 4091 ax-pow 4136 ax-pr 4170 ax-un 4394 ax-setind 4497 ax-iinf 4548 ax-cnex 7824 ax-resscn 7825 ax-1cn 7826 ax-1re 7827 ax-icn 7828 ax-addcl 7829 ax-addrcl 7830 ax-mulcl 7831 ax-mulrcl 7832 ax-addcom 7833 ax-mulcom 7834 ax-addass 7835 ax-mulass 7836 ax-distr 7837 ax-i2m1 7838 ax-0lt1 7839 ax-1rid 7840 ax-0id 7841 ax-rnegex 7842 ax-precex 7843 ax-cnre 7844 ax-pre-ltirr 7845 ax-pre-ltwlin 7846 ax-pre-lttrn 7847 ax-pre-apti 7848 ax-pre-ltadd 7849 ax-pre-mulgt0 7850 ax-pre-mulext 7851

This theorem depends on definitions: df-bi 116 df-dc 821 df-3or 964 df-3an 965 df-tru 1338 df-fal 1341 df-nf 1441 df-sb 1743 df-eu 2009 df-mo 2010 df-clab 2144 df-cleq 2150 df-clel 2153 df-nfc 2288 df-ne 2328 df-nel 2423 df-ral 2440 df-rex 2441 df-reu 2442 df-rmo 2443 df-rab 2444 df-v 2714 df-sbc 2938 df-csb 3032 df-dif 3104 df-un 3106 df-in 3108 df-ss 3115 df-nul 3395 df-if 3506 df-pw 3545 df-sn 3566 df-pr 3567 df-op 3569 df-uni 3774 df-int 3809 df-iun 3852 df-br 3967 df-opab 4027 df-mpt 4028 df-tr 4064 df-id 4254 df-po 4257 df-iso 4258 df-iord 4327 df-on 4329 df-ilim 4330 df-suc 4332 df-iom 4551 df-xp 4593 df-rel 4594 df-cnv 4595 df-co 4596 df-dm 4597 df-rn 4598 df-res 4599 df-ima 4600 df-iota 5136 df-fun 5173 df-fn 5174 df-f 5175 df-f1 5176 df-fo 5177 df-f1o 5178 df-fv 5179 df-riota 5781 df-ov 5828 df-oprab 5829 df-mpo 5830 df-1st 6089 df-2nd 6090 df-recs 6253 df-frec 6339 df-pnf 7915 df-mnf 7916 df-xr 7917 df-ltxr 7918 df-le 7919 df-sub 8049 df-neg 8050 df-reap 8451 df-ap 8458 df-div 8547 df-inn 8835 df-n0 9092 df-z 9169 df-uz 9441 df-q 9530 df-rp 9562 df-fz 9914 df-seqfrec 10349 df-fac 10604 df-bc 10626

This theorem is referenced by: bccl 10645 bcn2m1 10647 bcn2p1 10648 binomlem 11384 bcxmas 11390 ex-bc 13347

W3C validator