Definition df-bc 6957

Description: Define the binomial coefficient operation. In the literature, this function is often written as a column vector of the two arguments, or with the arguments as subscripts before and after the letter "C". (N C. K) is read "N choose K." Definition of binomial coefficient in [Gleason] p. 295. As suggested by Gleason, we define it to be 0 when 0 <_ k <_ n does not hold.

Assertion

Ref	Expression
df-bc	|- C. = {<.<.n, k>., m>. | ((n e. NN0 /\ k e. ZZ) /\ m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0))}

Distinct variable group:   k,n,m

Detailed syntax breakdown of Definition df-bc

Step	Hyp	Ref	Expression
1		cbc 6956	. 2 class C.
2		vn	. . . . . . 7 set n
3	2	cv 955	. . . . . 6 class n
4		cn0 5297	. . . . . 6 class NN0
5	3, 4	wcel 958	. . . . 5 wff n e. NN0
6		vk	. . . . . . 7 set k
7	6	cv 955	. . . . . 6 class k
8		cz 5298	. . . . . 6 class ZZ
9	7, 8	wcel 958	. . . . 5 wff k e. ZZ
10	5, 9	wa 223	. . . 4 wff (n e. NN0 /\ k e. ZZ)
11		vm	. . . . . 6 set m
12	11	cv 955	. . . . 5 class m
13		cc0 5234	. . . . . . . 8 class 0
14		cle 5295	. . . . . . . 8 class <_
15	13, 7, 14	wbr 2619	. . . . . . 7 wff 0 <_ k
16	7, 3, 14	wbr 2619	. . . . . . 7 wff k <_ n
17	15, 16	wa 223	. . . . . 6 wff (0 <_ k /\ k <_ n)
18		cfa 6931	. . . . . . . 8 class !
19	3, 18	cfv 3182	. . . . . . 7 class (!` n)
20		cmin 5292	. . . . . . . . . 10 class -
21	3, 7, 20	co 3963	. . . . . . . . 9 class (n - k)
22	21, 18	cfv 3182	. . . . . . . 8 class (!` (n - k))
23	7, 18	cfv 3182	. . . . . . . 8 class (!` k)
24		cmul 5239	. . . . . . . 8 class x.
25	22, 23, 24	co 3963	. . . . . . 7 class ((!` (n - k)) x. (!` k))
26		cdiv 5294	. . . . . . 7 class /
27	19, 25, 26	co 3963	. . . . . 6 class ((!` n) / ((!` (n - k)) x. (!` k)))
28	17, 27, 13	cif 2361	. . . . 5 class if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0)
29	12, 28	wceq 956	. . . 4 wff m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0)
30	10, 29	wa 223	. . 3 wff ((n e. NN0 /\ k e. ZZ) /\ m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0))
31	30, 2, 6, 11	copab2 3964	. 2 class {<.<.n, k>., m>. | ((n e. NN0 /\ k e. ZZ) /\ m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0))}
32	1, 31	wceq 956	1 wff C. = {<.<.n, k>., m>. | ((n e. NN0 /\ k e. ZZ) /\ m = if((0 <_ k /\ k <_ n), ((!` n) / ((!` (n - k)) x. (!` k))), 0))}

This definition is referenced by:  bcvalt 6958

Copyright terms: Public domain