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 14286

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 12482	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
2		elfzp12 13564	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
3		nn0uz 12835	. . . . . . 7 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleq2s 2846	. . . . . 6 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
5	1, 4	syl 17	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
6		1p0e1 12305	. . . . . . . 8 ⊢ (1 + 0) = 1
7		bcn0 14275	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C0) = 1)
8		0z 12540	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
9		1z 12563	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
10		zsubcl 12575	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
11	8, 9, 10	mp2an 692	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
12		0re 11176	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
13		ltm1 12024	. . . . . . . . . . . 12 ⊢ (0 ∈ ℝ → (0 − 1) < 0)
14	12, 13	ax-mp 5	. . . . . . . . . . 11 ⊢ (0 − 1) < 0
15	14	orci 865	. . . . . . . . . 10 ⊢ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))
16		bcval4 14272	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
17	11, 15, 16	mp3an23 1455	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(0 − 1)) = 0)
18	7, 17	oveq12d 7405	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = (1 + 0))
19		bcn0 14275	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
20	1, 19	syl 17	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
21	6, 18, 20	3eqtr4a 2790	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0))
22		oveq2 7395	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C𝐾) = (𝑁C0))
23		oveq1 7394	. . . . . . . . . 10 ⊢ (𝐾 = 0 → (𝐾 − 1) = (0 − 1))
24	23	oveq2d 7403	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C(𝐾 − 1)) = (𝑁C(0 − 1)))
25	22, 24	oveq12d 7405	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁C0) + (𝑁C(0 − 1))))
26		oveq2 7395	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C0))
27	25, 26	eqeq12d 2745	. . . . . . 7 ⊢ (𝐾 = 0 → (((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾) ↔ ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0)))
28	21, 27	syl5ibrcom 247	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
29		simpr 484	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))
30		0p1e1 12303	. . . . . . . . . 10 ⊢ (0 + 1) = 1
31	30	oveq1i 7397	. . . . . . . . 9 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
32	29, 31	eleqtrdi 2838	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ (1...(𝑁 + 1)))
33		nn0p1nn 12481	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
34		nnuz 12836	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
35	33, 34	eleqtrdi 2838	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘1))
36		fzm1 13568	. . . . . . . . . . 11 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘1) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))))
37	36	biimpa 476	. . . . . . . . . 10 ⊢ (((𝑁 + 1) ∈ (ℤ_≥‘1) ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
38	35, 37	sylan 580	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1)))
39		nn0cn 12452	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
40		ax-1cn 11126	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
41		pncan 11427	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
42	39, 40, 41	sylancl 586	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) − 1) = 𝑁)
43	42	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (1...((𝑁 + 1) − 1)) = (1...𝑁))
44	43	eleq2d 2814	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ↔ 𝐾 ∈ (1...𝑁)))
45	44	biimpa 476	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → 𝐾 ∈ (1...𝑁))
46		fz1ssfz0 13584	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
47	46	sseli 3942	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁))
48		bcp1n 14281	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
49	47, 48	syl 17	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
50		bcrpcl 14273	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
51	47, 50	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
52	51	rpcnd 12997	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℂ)
53		elfzuz2 13490	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘1))
54	53, 34	eleqtrrdi 2839	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ)
55	54	peano2nnd 12203	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℕ)
56	55	nncnd 12202	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℂ)
57	54	nncnd 12202	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ)
58		1cnd 11169	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ)
59		elfzelz 13485	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
60	59	zcnd 12639	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ)
61	57, 58, 60	addsubd 11554	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1))
62		fznn0sub 13517	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
63		nn0p1nn 12481	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
65	61, 64	eqeltrd 2828	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ)
66	65	nncnd 12202	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ)
67	65	nnne0d 12236	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0)
68	52, 56, 66, 67	div12d 11994	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))))
69	65	nnrpd 12993	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ⁺)
70	51, 69	rpdivcld 13012	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℝ⁺)
71	70	rpcnd 12997	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℂ)
72	56, 71	mulcomd 11195	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
73	68, 72	eqtrd 2764	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
74	56, 60	npcand 11537	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) + 𝐾) = (𝑁 + 1))
75	74	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
76	71, 66, 60	adddid 11198	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
77	73, 75, 76	3eqtr2d 2770	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
78	52, 66, 67	divcan1d 11959	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) = (𝑁C𝐾))
79		elfznn 13514	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
80	79	nnne0d 12236	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0)
81	52, 66, 60, 67, 80	divdiv2d 11990	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)))
82		bcm1k 14280	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)))
83	57, 60, 58	subsub3d 11563	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 + 1) − 𝐾))
84	83	oveq1d 7402	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 + 1) − 𝐾) / 𝐾))
85	84	oveq2d 7403	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
86	82, 85	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
87		fzelp1 13537	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (1...(𝑁 + 1)))
88	55	nnzd 12556	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℤ)
89		elfzm1b 13563	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ ℤ ∧ (𝑁 + 1) ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
90	59, 88, 89	syl2anc 584	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
91	87, 90	mpbid 232	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)))
92	57, 40, 41	sylancl 586	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 1) = 𝑁)
93	92	oveq2d 7403	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
94	91, 93	eleqtrd 2830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁))
95		bcrpcl 14273	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
96	94, 95	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
97	96	rpcnd 12997	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℂ)
98	79	nnrpd 12993	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℝ⁺)
99	69, 98	rpdivcld 13012	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℝ⁺)
100	99	rpcnd 12997	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℂ)
101	99	rpne0d 13000	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ≠ 0)
102	52, 97, 100, 101	divmul3d 11992	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)) ↔ (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾))))
103	86, 102	mpbird 257	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (𝑁C(𝐾 − 1)))
104	52, 60, 66, 67	div23d 11995	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾))
105	81, 103, 104	3eqtr3rd 2773	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾) = (𝑁C(𝐾 − 1)))
106	78, 105	oveq12d 7405	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)) = ((𝑁C𝐾) + (𝑁C(𝐾 − 1))))
107	49, 77, 106	3eqtrrd 2769	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
108	45, 107	syl 17	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
109		oveq2 7395	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑁 + 1) → (𝑁C𝐾) = (𝑁C(𝑁 + 1)))
110	33	nnzd 12556	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
111		nn0re 12451	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
112	111	ltp1d 12113	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 < (𝑁 + 1))
113	112	olcd 874	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1)))
114		bcval4 14272	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℤ ∧ ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0)
115	110, 113, 114	mpd3an23 1465	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(𝑁 + 1)) = 0)
116	109, 115	sylan9eqr 2786	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝐾) = 0)
117		oveq1 7394	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = (𝑁 + 1) → (𝐾 − 1) = ((𝑁 + 1) − 1))
118	117, 42	sylan9eqr 2786	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝐾 − 1) = 𝑁)
119	118	oveq2d 7403	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = (𝑁C𝑁))
120		bcnn 14277	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C𝑁) = 1)
121	120	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝑁) = 1)
122	119, 121	eqtrd 2764	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = 1)
123	116, 122	oveq12d 7405	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 1))
124		oveq2 7395	. . . . . . . . . . . 12 ⊢ (𝐾 = (𝑁 + 1) → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C(𝑁 + 1)))
125		bcnn 14277	. . . . . . . . . . . . 13 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
126	1, 125	syl 17	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
127	124, 126	sylan9eqr 2786	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁 + 1)C𝐾) = 1)
128	30, 123, 127	3eqtr4a 2790	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
129	108, 128	jaodan 959	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 ∈ (1...((𝑁 + 1) − 1)) ∨ 𝐾 = (𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
130	38, 129	syldan 591	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
131	32, 130	syldan 591	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
132	131	ex 412	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ ((0 + 1)...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
133	28, 132	jaod 859	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → ((𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
134	5, 133	sylbid 240	. . . 4 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾)))
135	134	imp 406	. . 3 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
136	135	adantlr 715	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
137		00id 11349	. . 3 ⊢ (0 + 0) = 0
138		fzelp1 13537	. . . . . 6 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1)))
139	138	con3i 154	. . . . 5 ⊢ (¬ 𝐾 ∈ (0...(𝑁 + 1)) → ¬ 𝐾 ∈ (0...𝑁))
140		bcval3 14271	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
141	140	3expa 1118	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
142	139, 141	sylan2 593	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C𝐾) = 0)
143		simpll 766	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝑁 ∈ ℕ₀)
144		simplr 768	. . . . . 6 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → 𝐾 ∈ ℤ)
145		peano2zm 12576	. . . . . 6 ⊢ (𝐾 ∈ ℤ → (𝐾 − 1) ∈ ℤ)
146	144, 145	syl 17	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝐾 − 1) ∈ ℤ)
147	39	adantr 480	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → 𝑁 ∈ ℂ)
148	147, 40, 41	sylancl 586	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁 + 1) − 1) = 𝑁)
149	148	oveq2d 7403	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
150	149	eleq2d 2814	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) ↔ (𝐾 − 1) ∈ (0...𝑁)))
151		id 22	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℤ)
152	1	nn0zd 12555	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
153	151, 152, 89	syl2anr 597	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
154		fz1ssfz0 13584	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
155	154	sseli 3942	. . . . . . . 8 ⊢ (𝐾 ∈ (1...(𝑁 + 1)) → 𝐾 ∈ (0...(𝑁 + 1)))
156	153, 155	biimtrrdi 254	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) → 𝐾 ∈ (0...(𝑁 + 1))))
157	150, 156	sylbird 260	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1))))
158	157	con3dimp 408	. . . . 5 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ (𝐾 − 1) ∈ (0...𝑁))
159		bcval3 14271	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 − 1) ∈ ℤ ∧ ¬ (𝐾 − 1) ∈ (0...𝑁)) → (𝑁C(𝐾 − 1)) = 0)
160	143, 146, 158, 159	syl3anc 1373	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C(𝐾 − 1)) = 0)
161	142, 160	oveq12d 7405	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 0))
162	143, 1	syl 17	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁 + 1) ∈ ℕ₀)
163		simpr 484	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ¬ 𝐾 ∈ (0...(𝑁 + 1)))
164		bcval3 14271	. . . 4 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
165	162, 144, 163, 164	syl3anc 1373	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
166	137, 161, 165	3eqtr4a 2790	. 2 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
167	136, 166	pm2.61dan 812	1 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 847 = wceq 1540 ∈ wcel 2109 class class class wbr 5107 ‘cfv 6511 (class class class)co 7387 ℂcc 11066 ℝcr 11067 0cc0 11068 1c1 11069 + caddc 11071 · cmul 11073 < clt 11208 − cmin 11405 / cdiv 11835 ℕcn 12186 ℕ₀cn0 12442 ℤcz 12529 ℤ_≥cuz 12793 ℝ⁺crp 12951 ...cfz 13468 Ccbc 14267

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-sep 5251 ax-nul 5261 ax-pow 5320 ax-pr 5387 ax-un 7711 ax-cnex 11124 ax-resscn 11125 ax-1cn 11126 ax-icn 11127 ax-addcl 11128 ax-addrcl 11129 ax-mulcl 11130 ax-mulrcl 11131 ax-mulcom 11132 ax-addass 11133 ax-mulass 11134 ax-distr 11135 ax-i2m1 11136 ax-1ne0 11137 ax-1rid 11138 ax-rnegex 11139 ax-rrecex 11140 ax-cnre 11141 ax-pre-lttri 11142 ax-pre-lttrn 11143 ax-pre-ltadd 11144 ax-pre-mulgt0 11145

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3354 df-reu 3355 df-rab 3406 df-v 3449 df-sbc 3754 df-csb 3863 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-pss 3934 df-nul 4297 df-if 4489 df-pw 4565 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4872 df-iun 4957 df-br 5108 df-opab 5170 df-mpt 5189 df-tr 5215 df-id 5533 df-eprel 5538 df-po 5546 df-so 5547 df-fr 5591 df-we 5593 df-xp 5644 df-rel 5645 df-cnv 5646 df-co 5647 df-dm 5648 df-rn 5649 df-res 5650 df-ima 5651 df-pred 6274 df-ord 6335 df-on 6336 df-lim 6337 df-suc 6338 df-iota 6464 df-fun 6513 df-fn 6514 df-f 6515 df-f1 6516 df-fo 6517 df-f1o 6518 df-fv 6519 df-riota 7344 df-ov 7390 df-oprab 7391 df-mpo 7392 df-om 7843 df-1st 7968 df-2nd 7969 df-frecs 8260 df-wrecs 8291 df-recs 8340 df-rdg 8378 df-er 8671 df-en 8919 df-dom 8920 df-sdom 8921 df-pnf 11210 df-mnf 11211 df-xr 11212 df-ltxr 11213 df-le 11214 df-sub 11407 df-neg 11408 df-div 11836 df-nn 12187 df-n0 12443 df-z 12530 df-uz 12794 df-rp 12952 df-fz 13469 df-seq 13967 df-fac 14239 df-bc 14268

This theorem is referenced by: bccl 14287 bcn2m1 14289 bcn2p1 14290 hashbclem 14417 binomlem 15795 bcxmas 15801 binomfallfaclem2 16006 srgbinomlem 20139 bcp1ctr 27190 ex-bc 30381 bccolsum 35726 fwddifnp1 36153 5bc2eq10 42130 sticksstones22 42156 dvnmul 45941 bcpascm1 48339

W3C validator