Theorem bcm1k

Description: The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014)

	Ref	Expression
Assertion	bcm1k	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		elfzuz2	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
2		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
3	1 2	eleqtrrdi	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ )
4	3	nnnn0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℕ0 )
5	4	faccld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℕ )
6	5	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝑁 ) ∈ ℂ )
7		fznn0sub	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − 𝐾 ) ∈ ℕ0 )
8		nn0p1nn	⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
9	7 8	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ )
10	9	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℂ )
11	9	nnnn0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℕ0 )
12	11	faccld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ∈ ℕ )
13		elfznn	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ )
14		nnm1nn0	⊢ ( 𝐾 ∈ ℕ → ( 𝐾 − 1 ) ∈ ℕ0 )
15		faccl	⊢ ( ( 𝐾 − 1 ) ∈ ℕ0 → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
16	13 14 15	3syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℕ )
17	12 16	nnmulcld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ )
18		nncn	⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ )
19		nnne0	⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 )
20	18 19	jca	⊢ ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℕ → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) )
21	17 20	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) )
22	13	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℂ )
23	13	nnne0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ≠ 0 )
24	22 23	jca	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) )
25		divmuldiv	⊢ ( ( ( ( ! ‘ 𝑁 ) ∈ ℂ ∧ ( ( 𝑁 − 𝐾 ) + 1 ) ∈ ℂ ) ∧ ( ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ∈ ℂ ∧ ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ≠ 0 ) ∧ ( 𝐾 ∈ ℂ ∧ 𝐾 ≠ 0 ) ) ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
26	6 10 21 24 25	syl22anc	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
27		elfzel2	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℤ )
28	27	zcnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ℂ )
29		1cnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 1 ∈ ℂ )
30	28 22 29	subsubd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 − ( 𝐾 − 1 ) ) = ( ( 𝑁 − 𝐾 ) + 1 ) )
31	30	fveq2d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
32	31	oveq1d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) )
33	32	oveq2d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
34	30	oveq1d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) )
35	33 34	oveq12d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( ( 𝑁 − 𝐾 ) + 1 ) / 𝐾 ) ) )
36		facp1	⊢ ( ( 𝑁 − 𝐾 ) ∈ ℕ0 → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
37	7 36	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) )
38	37	eqcomd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) )
39		facnn2	⊢ ( 𝐾 ∈ ℕ → ( ! ‘ 𝐾 ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
40	13 39	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) = ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) )
41	38 40	oveq12d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ 𝐾 ) ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) ) )
42	7	faccld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℕ )
43	42	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝑁 − 𝐾 ) ) ∈ ℂ )
44	13	nnnn0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ℕ0 )
45	44	faccld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℕ )
46	45	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ 𝐾 ) ∈ ℂ )
47	43 46 10	mul32d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ 𝐾 ) ) )
48	12	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) ∈ ℂ )
49	16	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ! ‘ ( 𝐾 − 1 ) ) ∈ ℂ )
50	48 49 22	mulassd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) = ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ( ! ‘ ( 𝐾 − 1 ) ) · 𝐾 ) ) )
51	41 47 50	3eqtr4d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) )
52	51	oveq2d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( ( 𝑁 − 𝐾 ) + 1 ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) · 𝐾 ) ) )
53	26 35 52	3eqtr4d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) )
54	6 10	mulcomd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) )
55	42 45	nnmulcld	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℕ )
56	55	nncnd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ∈ ℂ )
57	56 10	mulcomd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) = ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
58	54 57	oveq12d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ! ‘ 𝑁 ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) / ( ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) · ( ( 𝑁 − 𝐾 ) + 1 ) ) ) = ( ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) / ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) )
59	55	nnne0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ≠ 0 )
60	9	nnne0d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 𝐾 ) + 1 ) ≠ 0 )
61	6 56 10 59 60	divcan5d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ! ‘ 𝑁 ) ) / ( ( ( 𝑁 − 𝐾 ) + 1 ) · ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
62	53 58 61	3eqtrrd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )
63		fz1ssfz0	⊢ ( 1 ... 𝑁 ) ⊆ ( 0 ... 𝑁 )
64	63	sseli	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝐾 ∈ ( 0 ... 𝑁 ) )
65		bcval2	⊢ ( 𝐾 ∈ ( 0 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
66	64 65	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − 𝐾 ) ) · ( ! ‘ 𝐾 ) ) ) )
67		ax-1cn	⊢ 1 ∈ ℂ
68		npcan	⊢ ( ( 𝑁 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
69	28 67 68	sylancl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 1 ) + 1 ) = 𝑁 )
70		peano2zm	⊢ ( 𝑁 ∈ ℤ → ( 𝑁 − 1 ) ∈ ℤ )
71		uzid	⊢ ( ( 𝑁 − 1 ) ∈ ℤ → ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
72		peano2uz	⊢ ( ( 𝑁 − 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
73	27 70 71 72	4syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 − 1 ) + 1 ) ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
74	69 73	eqeltrrd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) )
75		fzss2	⊢ ( 𝑁 ∈ ( ℤ≥ ‘ ( 𝑁 − 1 ) ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
76	74 75	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 0 ... ( 𝑁 − 1 ) ) ⊆ ( 0 ... 𝑁 ) )
77		elfzmlbm	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... ( 𝑁 − 1 ) ) )
78	76 77	sseldd	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) )
79		bcval2	⊢ ( ( 𝐾 − 1 ) ∈ ( 0 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
80	78 79	syl	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C ( 𝐾 − 1 ) ) = ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) )
81	80	oveq1d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) = ( ( ( ! ‘ 𝑁 ) / ( ( ! ‘ ( 𝑁 − ( 𝐾 − 1 ) ) ) · ( ! ‘ ( 𝐾 − 1 ) ) ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )
82	62 66 81	3eqtr4d	⊢ ( 𝐾 ∈ ( 1 ... 𝑁 ) → ( 𝑁 C 𝐾 ) = ( ( 𝑁 C ( 𝐾 − 1 ) ) · ( ( 𝑁 − ( 𝐾 − 1 ) ) / 𝐾 ) ) )