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 14353

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 12539	. . . . . 6 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ₀)
2		elfzp12 13627	. . . . . . 7 ⊢ ((𝑁 + 1) ∈ (ℤ_≥‘0) → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
3		nn0uz 12895	. . . . . . 7 ⊢ ℕ₀ = (ℤ_≥‘0)
4	2, 3	eleq2s 2881	. . . . . 6 ⊢ ((𝑁 + 1) ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
5	1, 4	syl 18	. . . . 5 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (0...(𝑁 + 1)) ↔ (𝐾 = 0 ∨ 𝐾 ∈ ((0 + 1)...(𝑁 + 1)))))
6		1p0e1 12358	. . . . . . . 8 ⊢ (1 + 0) = 1
7		bcn0 14342	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C0) = 1)
8		0z 12597	. . . . . . . . . . 11 ⊢ 0 ∈ ℤ
9		1z 12619	. . . . . . . . . . 11 ⊢ 1 ∈ ℤ
10		zsubcl 12631	. . . . . . . . . . 11 ⊢ ((0 ∈ ℤ ∧ 1 ∈ ℤ) → (0 − 1) ∈ ℤ)
11	8, 9, 10	mp2an 704	. . . . . . . . . 10 ⊢ (0 − 1) ∈ ℤ
12		0re 11205	. . . . . . . . . . . 12 ⊢ 0 ∈ ℝ
13		ltm1 12052	. . . . . . . . . . . 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 14339	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ (0 − 1) ∈ ℤ ∧ ((0 − 1) < 0 ∨ 𝑁 < (0 − 1))) → (𝑁C(0 − 1)) = 0)
17	11, 15, 16	mp3an23 1482	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(0 − 1)) = 0)
18	7, 17	oveq12d 7428	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = (1 + 0))
19		bcn0 14342	. . . . . . . . 9 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
20	1, 19	syl 18	. . . . . . . 8 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C0) = 1)
21	6, 18, 20	3eqtr4a 2824	. . . . . . 7 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁C0) + (𝑁C(0 − 1))) = ((𝑁 + 1)C0))
22		oveq2 7418	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C𝐾) = (𝑁C0))
23		oveq1 7417	. . . . . . . . . 10 ⊢ (𝐾 = 0 → (𝐾 − 1) = (0 − 1))
24	23	oveq2d 7426	. . . . . . . . 9 ⊢ (𝐾 = 0 → (𝑁C(𝐾 − 1)) = (𝑁C(0 − 1)))
25	22, 24	oveq12d 7428	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁C0) + (𝑁C(0 − 1))))
26		oveq2 7418	. . . . . . . 8 ⊢ (𝐾 = 0 → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C0))
27	25, 26	eqeq12d 2779	. . . . . . 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 12356	. . . . . . . . . 10 ⊢ (0 + 1) = 1
31	30	oveq1i 7420	. . . . . . . . 9 ⊢ ((0 + 1)...(𝑁 + 1)) = (1...(𝑁 + 1))
32	29, 31	eleqtrdi 2873	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ((0 + 1)...(𝑁 + 1))) → 𝐾 ∈ (1...(𝑁 + 1)))
33		nn0p1nn 12538	. . . . . . . . . . 11 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℕ)
34		nnuz 12896	. . . . . . . . . . 11 ⊢ ℕ = (ℤ_≥‘1)
35	33, 34	eleqtrdi 2873	. . . . . . . . . 10 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ (ℤ_≥‘1))
36		fzm1 13631	. . . . . . . . . . 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 12509	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℂ)
40		ax-1cn 11153	. . . . . . . . . . . . . . 15 ⊢ 1 ∈ ℂ
41		pncan 11458	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℂ ∧ 1 ∈ ℂ) → ((𝑁 + 1) − 1) = 𝑁)
42	39, 40, 41	sylancl 597	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) − 1) = 𝑁)
43	42	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (1...((𝑁 + 1) − 1)) = (1...𝑁))
44	43	eleq2d 2849	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → (𝐾 ∈ (1...((𝑁 + 1) − 1)) ↔ 𝐾 ∈ (1...𝑁)))
45	44	biimpa 481	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → 𝐾 ∈ (1...𝑁))
46		fz1ssfz0 13647	. . . . . . . . . . . . . 14 ⊢ (1...𝑁) ⊆ (0...𝑁)
47	46	sseli 3933	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (0...𝑁))
48		bcp1n 14348	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (0...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
49	47, 48	syl 18	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1)C𝐾) = ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))))
50		bcrpcl 14340	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (0...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
51	47, 50	syl 18	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℝ⁺)
52	51	rpcnd 13057	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) ∈ ℂ)
53		elfzuz2 13552	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ (ℤ_≥‘1))
54	53, 34	eleqtrrdi 2874	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℕ)
55	54	peano2nnd 12245	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℕ)
56	55	nncnd 12244	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℂ)
57	54	nncnd 12244	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝑁 ∈ ℂ)
58		1cnd 11197	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 1 ∈ ℂ)
59		elfzelz 13547	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℤ)
60	59	zcnd 12696	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℂ)
61	57, 58, 60	addsubd 11585	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) = ((𝑁 − 𝐾) + 1))
62		fznn0sub 13580	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − 𝐾) ∈ ℕ₀)
63		nn0p1nn 12538	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑁 − 𝐾) ∈ ℕ₀ → ((𝑁 − 𝐾) + 1) ∈ ℕ)
64	62, 63	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − 𝐾) + 1) ∈ ℕ)
65	61, 64	eqeltrd 2863	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℕ)
66	65	nncnd 12244	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℂ)
67	65	nnne0d 12281	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ≠ 0)
68	52, 56, 66, 67	div12d 12022	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))))
69	65	nnrpd 13053	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) − 𝐾) ∈ ℝ⁺)
70	51, 69	rpdivcld 13072	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℝ⁺)
71	70	rpcnd 13057	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) ∈ ℂ)
72	56, 71	mulcomd 11225	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 + 1) · ((𝑁C𝐾) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
73	68, 72	eqtrd 2798	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
74	56, 60	npcand 11568	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) + 𝐾) = (𝑁 + 1))
75	74	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (𝑁 + 1)))
76	71, 66, 60	adddid 11228	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · (((𝑁 + 1) − 𝐾) + 𝐾)) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
77	73, 75, 76	3eqtr2d 2804	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) · ((𝑁 + 1) / ((𝑁 + 1) − 𝐾))) = ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)))
78	52, 66, 67	divcan1d 11987	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) = (𝑁C𝐾))
79		elfznn 13577	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℕ)
80	79	nnne0d 12281	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ≠ 0)
81	52, 66, 60, 67, 80	divdiv2d 12018	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) / (((𝑁 + 1) − 𝐾) / 𝐾)) = (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)))
82		bcm1k 14347	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)))
83	57, 60, 58	subsub3d 11594	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 − (𝐾 − 1)) = ((𝑁 + 1) − 𝐾))
84	83	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁 − (𝐾 − 1)) / 𝐾) = (((𝑁 + 1) − 𝐾) / 𝐾))
85	84	oveq2d 7426	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C(𝐾 − 1)) · ((𝑁 − (𝐾 − 1)) / 𝐾)) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
86	82, 85	eqtrd 2798	. . . . . . . . . . . . . . 15 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C𝐾) = ((𝑁C(𝐾 − 1)) · (((𝑁 + 1) − 𝐾) / 𝐾)))
87		fzelp1 13600	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ (1...(𝑁 + 1)))
88	55	nnzd 12612	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁 + 1) ∈ ℤ)
89		elfzm1b 13626	. . . . . . . . . . . . . . . . . . . . 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 7426	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝐾 ∈ (1...𝑁) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
94	91, 93	eleqtrd 2865	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → (𝐾 − 1) ∈ (0...𝑁))
95		bcrpcl 14340	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 − 1) ∈ (0...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
96	94, 95	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℝ⁺)
97	96	rpcnd 13057	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (𝑁C(𝐾 − 1)) ∈ ℂ)
98	79	nnrpd 13053	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐾 ∈ (1...𝑁) → 𝐾 ∈ ℝ⁺)
99	69, 98	rpdivcld 13072	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℝ⁺)
100	99	rpcnd 13057	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ∈ ℂ)
101	99	rpne0d 13060	. . . . . . . . . . . . . . . 16 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁 + 1) − 𝐾) / 𝐾) ≠ 0)
102	52, 97, 100, 101	divmul3d 12020	. . . . . . . . . . . . . . 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 12023	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) · 𝐾) / ((𝑁 + 1) − 𝐾)) = (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾))
105	81, 103, 104	3eqtr3rd 2807	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ (1...𝑁) → (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾) = (𝑁C(𝐾 − 1)))
106	78, 105	oveq12d 7428	. . . . . . . . . . . 12 ⊢ (𝐾 ∈ (1...𝑁) → ((((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · ((𝑁 + 1) − 𝐾)) + (((𝑁C𝐾) / ((𝑁 + 1) − 𝐾)) · 𝐾)) = ((𝑁C𝐾) + (𝑁C(𝐾 − 1))))
107	49, 77, 106	3eqtrrd 2803	. . . . . . . . . . 11 ⊢ (𝐾 ∈ (1...𝑁) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
108	45, 107	syl 18	. . . . . . . . . 10 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ (1...((𝑁 + 1) − 1))) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = ((𝑁 + 1)C𝐾))
109		oveq2 7418	. . . . . . . . . . . . 13 ⊢ (𝐾 = (𝑁 + 1) → (𝑁C𝐾) = (𝑁C(𝑁 + 1)))
110	33	nnzd 12612	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
111		nn0re 12508	. . . . . . . . . . . . . . . 16 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 ∈ ℝ)
112	111	ltp1d 12140	. . . . . . . . . . . . . . 15 ⊢ (𝑁 ∈ ℕ₀ → 𝑁 < (𝑁 + 1))
113	112	olcd 887	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1)))
114		bcval4 14339	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝑁 + 1) ∈ ℤ ∧ ((𝑁 + 1) < 0 ∨ 𝑁 < (𝑁 + 1))) → (𝑁C(𝑁 + 1)) = 0)
115	110, 113, 114	mpd3an23 1492	. . . . . . . . . . . . 13 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C(𝑁 + 1)) = 0)
116	109, 115	sylan9eqr 2820	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝐾) = 0)
117		oveq1 7417	. . . . . . . . . . . . . . 15 ⊢ (𝐾 = (𝑁 + 1) → (𝐾 − 1) = ((𝑁 + 1) − 1))
118	117, 42	sylan9eqr 2820	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝐾 − 1) = 𝑁)
119	118	oveq2d 7426	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = (𝑁C𝑁))
120		bcnn 14344	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℕ₀ → (𝑁C𝑁) = 1)
121	120	adantr 485	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C𝑁) = 1)
122	119, 121	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → (𝑁C(𝐾 − 1)) = 1)
123	116, 122	oveq12d 7428	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁C𝐾) + (𝑁C(𝐾 − 1))) = (0 + 1))
124		oveq2 7418	. . . . . . . . . . . 12 ⊢ (𝐾 = (𝑁 + 1) → ((𝑁 + 1)C𝐾) = ((𝑁 + 1)C(𝑁 + 1)))
125		bcnn 14344	. . . . . . . . . . . . 13 ⊢ ((𝑁 + 1) ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
126	1, 125	syl 18	. . . . . . . . . . . 12 ⊢ (𝑁 ∈ ℕ₀ → ((𝑁 + 1)C(𝑁 + 1)) = 1)
127	124, 126	sylan9eqr 2820	. . . . . . . . . . 11 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 = (𝑁 + 1)) → ((𝑁 + 1)C𝐾) = 1)
128	30, 123, 127	3eqtr4a 2824	. . . . . . . . . 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 11380	. . 3 ⊢ (0 + 0) = 0
138		fzelp1 13600	. . . . . 6 ⊢ (𝐾 ∈ (0...𝑁) → 𝐾 ∈ (0...(𝑁 + 1)))
139	138	con3i 155	. . . . 5 ⊢ (¬ 𝐾 ∈ (0...(𝑁 + 1)) → ¬ 𝐾 ∈ (0...𝑁))
140		bcval3 14338	. . . . . 6 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...𝑁)) → (𝑁C𝐾) = 0)
141	140	3expa 1136	. . . . 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 12632	. . . . . 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 7426	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (0...((𝑁 + 1) − 1)) = (0...𝑁))
150	149	eleq2d 2849	. . . . . . 7 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → ((𝐾 − 1) ∈ (0...((𝑁 + 1) − 1)) ↔ (𝐾 − 1) ∈ (0...𝑁)))
151		id 23	. . . . . . . . 9 ⊢ (𝐾 ∈ ℤ → 𝐾 ∈ ℤ)
152	1	nn0zd 12611	. . . . . . . . 9 ⊢ (𝑁 ∈ ℕ₀ → (𝑁 + 1) ∈ ℤ)
153	151, 152, 89	syl2anr 608	. . . . . . . 8 ⊢ ((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈ (1...(𝑁 + 1)) ↔ (𝐾 − 1) ∈ (0...((𝑁 + 1) − 1))))
154		fz1ssfz0 13647	. . . . . . . . 9 ⊢ (1...(𝑁 + 1)) ⊆ (0...(𝑁 + 1))
155	154	sseli 3933	. . . . . . . 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 14338	. . . . 5 ⊢ ((𝑁 ∈ ℕ₀ ∧ (𝐾 − 1) ∈ ℤ ∧ ¬ (𝐾 − 1) ∈ (0...𝑁)) → (𝑁C(𝐾 − 1)) = 0)
160	143, 146, 158, 159	syl3anc 1398	. . . 4 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → (𝑁C(𝐾 − 1)) = 0)
161	142, 160	oveq12d 7428	. . 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 14338	. . . 4 ⊢ (((𝑁 + 1) ∈ ℕ₀ ∧ 𝐾 ∈ ℤ ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
165	162, 144, 163, 164	syl3anc 1398	. . 3 ⊢ (((𝑁 ∈ ℕ₀ ∧ 𝐾 ∈ ℤ) ∧ ¬ 𝐾 ∈ (0...(𝑁 + 1))) → ((𝑁 + 1)C𝐾) = 0)
166	137, 161, 165	3eqtr4a 2824	. 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 1570 ∈ wcel 2143 class class class wbr 5109 ‘cfv 6536 (class class class)co 7410 ℂcc 11093 ℝcr 11094 0cc0 11095 1c1 11096 + caddc 11098 · cmul 11100 < clt 11238 − cmin 11436 / cdiv 11866 ℕcn 12228 ℕ₀cn0 12499 ℤcz 12586 ℤ_≥cuz 12857 ℝ⁺crp 13011 ...cfz 13530 Ccbc 14334

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-op 4596 df-uni 4873 df-iun 4958 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-om 7859 df-1st 7982 df-2nd 7983 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-er 8690 df-en 8940 df-dom 8941 df-sdom 8942 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-div 11867 df-nn 12229 df-n0 12500 df-z 12587 df-uz 12858 df-rp 13012 df-fz 13531 df-seq 14034 df-fac 14306 df-bc 14335

This theorem is referenced by: bccl 14354 bcn2m1 14356 bcn2p1 14357 hashbclem 14485 binomlem 15879 bcxmas 15885 binomfallfaclem2 16089 srgbinomlem 20307 bcp1ctr 27443 ex-bc 30803 bccolsum 36231 fwddifnp1 36657 5bc2eq10 42929 sticksstones22 42955 dvnmul 46677 bcpascm1 49151

W3C validator