bcval5

Description: Write out the top and bottom parts of the binomial coefficient ( N _C K ) = ( N x. ( N - 1 ) x. ... x. ( ( N - K ) + 1 ) ) / K ! explicitly. In this form, it is valid even for N < K , although it is no longer valid for nonpositive K . (Contributed by Mario Carneiro, 22-May-2014)

		Ref	Expression
	Assertion	bcval5	$⊢ (N \in ℕ_{0} \land K \in ℕ) \to (\binom{N}{K}) = \frac{seq (N - K + 1) (\times I) (N)}{K!}$

Proof

Step	Hyp	Ref	Expression
1		bcval2	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
2	1	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{N!}{(N - K)! K!}$
3		mulcl	$⊢ (k \in ℂ \land x \in ℂ) \to k x \in ℂ$
4	3	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
5		mulass	$⊢ (k \in ℂ \land x \in ℂ \land y \in ℂ) \to k x y = k x y$
6	5	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \land (k \in ℂ \land x \in ℂ \land y \in ℂ)) \to k x y = k x y$
7		simplr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to K \in ℕ$
8		elfzuz3	$⊢ K \in (0 \dots N) \to N \in ℤ_{\geq K}$
9	8	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N \in ℤ_{\geq K}$
10		eluznn	$⊢ (K \in ℕ \land N \in ℤ_{\geq K}) \to N \in ℕ$
11	7 9 10	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N \in ℕ$
12	11	adantrr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N \in ℕ$
13		simplr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to K \in ℕ$
14		nnre	$⊢ N \in ℕ \to N \in ℝ$
15		nnrp	$⊢ K \in ℕ \to K \in ℝ^{+}$
16		ltsubrp	$⊢ (N \in ℝ \land K \in ℝ^{+}) \to N - K < N$
17	14 15 16	syl2an	$⊢ (N \in ℕ \land K \in ℕ) \to N - K < N$
18	12 13 17	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K < N$
19	12	nnzd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N \in ℤ$
20		nnz	$⊢ K \in ℕ \to K \in ℤ$
21	20	ad2antlr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to K \in ℤ$
22	19 21	zsubcld	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K \in ℤ$
23		zltp1le	$⊢ (N - K \in ℤ \land N \in ℤ) \to (N - K < N \leftrightarrow N - K + 1 \leq N)$
24	22 19 23	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to (N - K < N \leftrightarrow N - K + 1 \leq N)$
25	18 24	mpbid	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K + 1 \leq N$
26	22	peano2zd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K + 1 \in ℤ$
27		eluz	$⊢ (N - K + 1 \in ℤ \land N \in ℤ) \to (N \in ℤ_{\geq (N - K + 1)} \leftrightarrow N - K + 1 \leq N)$
28	26 19 27	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to (N \in ℤ_{\geq (N - K + 1)} \leftrightarrow N - K + 1 \leq N)$
29	25 28	mpbird	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N \in ℤ_{\geq (N - K + 1)}$
30		simprr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K \in ℕ$
31		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
32	30 31	eleqtrdi	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N - K \in ℤ_{\geq 1}$
33		fvi	$⊢ k \in (1 \dots N) \to I (k) = k$
34		elfzelz	$⊢ k \in (1 \dots N) \to k \in ℤ$
35	34	zcnd	$⊢ k \in (1 \dots N) \to k \in ℂ$
36	33 35	eqeltrd	$⊢ k \in (1 \dots N) \to I (k) \in ℂ$
37	36	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \land k \in (1 \dots N)) \to I (k) \in ℂ$
38	4 6 29 32 37	seqsplit	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to seq 1 (\times I) (N) = seq 1 (\times I) (N - K) seq (N - K + 1) (\times I) (N)$
39		facnn	$⊢ N \in ℕ \to N! = seq 1 (\times I) (N)$
40	12 39	syl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N! = seq 1 (\times I) (N)$
41		facnn	$⊢ N - K \in ℕ \to (N - K)! = seq 1 (\times I) (N - K)$
42	30 41	syl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to (N - K)! = seq 1 (\times I) (N - K)$
43	42	oveq1d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to (N - K)! seq (N - K + 1) (\times I) (N) = seq 1 (\times I) (N - K) seq (N - K + 1) (\times I) (N)$
44	38 40 43	3eqtr4d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land (K \in (0 \dots N) \land N - K \in ℕ)) \to N! = (N - K)! seq (N - K + 1) (\times I) (N)$
45	44	expr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K \in ℕ \to N! = (N - K)! seq (N - K + 1) (\times I) (N))$
46		simpll	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N \in ℕ_{0}$
47		faccl	$⊢ N \in ℕ_{0} \to N! \in ℕ$
48		nncn	$⊢ N! \in ℕ \to N! \in ℂ$
49	46 47 48	3syl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N! \in ℂ$
50	49	mulid2d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to 1 N! = N!$
51	11 39	syl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N! = seq 1 (\times I) (N)$
52	51	oveq2d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to 1 N! = 1 seq 1 (\times I) (N)$
53	50 52	eqtr3d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N! = 1 seq 1 (\times I) (N)$
54		fveq2	$⊢ N - K = 0 \to (N - K)! = 0!$
55		fac0	$⊢ 0! = 1$
56	54 55	eqtrdi	$⊢ N - K = 0 \to (N - K)! = 1$
57		oveq1	$⊢ N - K = 0 \to N - K + 1 = 0 + 1$
58		0p1e1	$⊢ 0 + 1 = 1$
59	57 58	eqtrdi	$⊢ N - K = 0 \to N - K + 1 = 1$
60	59	seqeq1d	$⊢ N - K = 0 \to seq (N - K + 1) (\times I) = seq 1 (\times I)$
61	60	fveq1d	$⊢ N - K = 0 \to seq (N - K + 1) (\times I) (N) = seq 1 (\times I) (N)$
62	56 61	oveq12d	$⊢ N - K = 0 \to (N - K)! seq (N - K + 1) (\times I) (N) = 1 seq 1 (\times I) (N)$
63	62	eqeq2d	$⊢ N - K = 0 \to (N! = (N - K)! seq (N - K + 1) (\times I) (N) \leftrightarrow N! = 1 seq 1 (\times I) (N))$
64	53 63	syl5ibrcom	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K = 0 \to N! = (N - K)! seq (N - K + 1) (\times I) (N))$
65		fznn0sub	$⊢ K \in (0 \dots N) \to N - K \in ℕ_{0}$
66	65	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N - K \in ℕ_{0}$
67		elnn0	$⊢ N - K \in ℕ_{0} \leftrightarrow (N - K \in ℕ \lor N - K = 0)$
68	66 67	sylib	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K \in ℕ \lor N - K = 0)$
69	45 64 68	mpjaod	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N! = (N - K)! seq (N - K + 1) (\times I) (N)$
70	69	oveq1d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to \frac{N!}{(N - K)! K!} = \frac{(N - K)! seq (N - K + 1) (\times I) (N)}{(N - K)! K!}$
71		eqid	$⊢ ℤ_{\geq (N - K + 1)} = ℤ_{\geq (N - K + 1)}$
72		nn0z	$⊢ N \in ℕ_{0} \to N \in ℤ$
73		zsubcl	$⊢ (N \in ℤ \land K \in ℤ) \to N - K \in ℤ$
74	72 20 73	syl2an	$⊢ (N \in ℕ_{0} \land K \in ℕ) \to N - K \in ℤ$
75	74	peano2zd	$⊢ (N \in ℕ_{0} \land K \in ℕ) \to N - K + 1 \in ℤ$
76	75	adantr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N - K + 1 \in ℤ$
77		fvi	$⊢ k \in ℤ_{\geq (N - K + 1)} \to I (k) = k$
78		eluzelcn	$⊢ k \in ℤ_{\geq (N - K + 1)} \to k \in ℂ$
79	77 78	eqeltrd	$⊢ k \in ℤ_{\geq (N - K + 1)} \to I (k) \in ℂ$
80	79	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \land k \in ℤ_{\geq (N - K + 1)}) \to I (k) \in ℂ$
81	3	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
82	71 76 80 81	seqf	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to seq (N - K + 1) (\times I) : ℤ_{\geq (N - K + 1)} ⟶ ℂ$
83	11 7 17	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N - K < N$
84	74	adantr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N - K \in ℤ$
85	11	nnzd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N \in ℤ$
86	84 85 23	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K < N \leftrightarrow N - K + 1 \leq N)$
87	83 86	mpbid	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N - K + 1 \leq N$
88	76 85 27	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N \in ℤ_{\geq (N - K + 1)} \leftrightarrow N - K + 1 \leq N)$
89	87 88	mpbird	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to N \in ℤ_{\geq (N - K + 1)}$
90	82 89	ffvelrnd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to seq (N - K + 1) (\times I) (N) \in ℂ$
91		elfznn0	$⊢ K \in (0 \dots N) \to K \in ℕ_{0}$
92	91	adantl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to K \in ℕ_{0}$
93	92	faccld	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to K! \in ℕ$
94	93	nncnd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to K! \in ℂ$
95	66	faccld	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K)! \in ℕ$
96	95	nncnd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K)! \in ℂ$
97	93	nnne0d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to K! \neq 0$
98	95	nnne0d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (N - K)! \neq 0$
99	90 94 96 97 98	divcan5d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to \frac{(N - K)! seq (N - K + 1) (\times I) (N)}{(N - K)! K!} = \frac{seq (N - K + 1) (\times I) (N)}{K!}$
100	2 70 99	3eqtrd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{seq (N - K + 1) (\times I) (N)}{K!}$
101		nnnn0	$⊢ K \in ℕ \to K \in ℕ_{0}$
102	101	ad2antlr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to K \in ℕ_{0}$
103		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
104		nncn	$⊢ K! \in ℕ \to K! \in ℂ$
105		nnne0	$⊢ K! \in ℕ \to K! \neq 0$
106	104 105	div0d	$⊢ K! \in ℕ \to \frac{0}{K!} = 0$
107	102 103 106	3syl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to \frac{0}{K!} = 0$
108	3	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \land (k \in ℂ \land x \in ℂ)) \to k x \in ℂ$
109		fvi	$⊢ k \in (N - K + 1 \dots N) \to I (k) = k$
110		elfzelz	$⊢ k \in (N - K + 1 \dots N) \to k \in ℤ$
111	110	zcnd	$⊢ k \in (N - K + 1 \dots N) \to k \in ℂ$
112	109 111	eqeltrd	$⊢ k \in (N - K + 1 \dots N) \to I (k) \in ℂ$
113	112	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \land k \in (N - K + 1 \dots N)) \to I (k) \in ℂ$
114		mul02	$⊢ k \in ℂ \to 0 \cdot k = 0$
115	114	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \land k \in ℂ) \to 0 \cdot k = 0$
116		mul01	$⊢ k \in ℂ \to k \cdot 0 = 0$
117	116	adantl	$⊢ (((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \land k \in ℂ) \to k \cdot 0 = 0$
118	75	adantr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N - K + 1 \in ℤ$
119	72	ad2antrr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N \in ℤ$
120		0zd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to 0 \in ℤ$
121		simpr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to \neg K \in (0 \dots N)$
122		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
123	102 122	eleqtrdi	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to K \in ℤ_{\geq 0}$
124		elfz5	$⊢ (K \in ℤ_{\geq 0} \land N \in ℤ) \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
125	123 119 124	syl2anc	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (K \in (0 \dots N) \leftrightarrow K \leq N)$
126		nn0re	$⊢ N \in ℕ_{0} \to N \in ℝ$
127	126	ad2antrr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N \in ℝ$
128		nnre	$⊢ K \in ℕ \to K \in ℝ$
129	128	ad2antlr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to K \in ℝ$
130	127 129	subge0d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (0 \leq N - K \leftrightarrow K \leq N)$
131	125 130	bitr4d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (K \in (0 \dots N) \leftrightarrow 0 \leq N - K)$
132	121 131	mtbid	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to \neg 0 \leq N - K$
133	74	adantr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N - K \in ℤ$
134	133	zred	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N - K \in ℝ$
135		0re	$⊢ 0 \in ℝ$
136		ltnle	$⊢ (N - K \in ℝ \land 0 \in ℝ) \to (N - K < 0 \leftrightarrow \neg 0 \leq N - K)$
137	134 135 136	sylancl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (N - K < 0 \leftrightarrow \neg 0 \leq N - K)$
138	132 137	mpbird	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N - K < 0$
139		0z	$⊢ 0 \in ℤ$
140		zltp1le	$⊢ (N - K \in ℤ \land 0 \in ℤ) \to (N - K < 0 \leftrightarrow N - K + 1 \leq 0)$
141	133 139 140	sylancl	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (N - K < 0 \leftrightarrow N - K + 1 \leq 0)$
142	138 141	mpbid	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N - K + 1 \leq 0$
143		nn0ge0	$⊢ N \in ℕ_{0} \to 0 \leq N$
144	143	ad2antrr	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to 0 \leq N$
145	118 119 120 142 144	elfzd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to 0 \in (N - K + 1 \dots N)$
146		simpll	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to N \in ℕ_{0}$
147		0cn	$⊢ 0 \in ℂ$
148		fvi	$⊢ 0 \in ℂ \to I (0) = 0$
149	147 148	mp1i	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to I (0) = 0$
150	108 113 115 117 145 146 149	seqz	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to seq (N - K + 1) (\times I) (N) = 0$
151	150	oveq1d	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to \frac{seq (N - K + 1) (\times I) (N)}{K!} = \frac{0}{K!}$
152		bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
153	20 152	syl3an2	$⊢ (N \in ℕ_{0} \land K \in ℕ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
154	153	3expa	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
155	107 151 154	3eqtr4rd	$⊢ ((N \in ℕ_{0} \land K \in ℕ) \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{seq (N - K + 1) (\times I) (N)}{K!}$
156	100 155	pm2.61dan	$⊢ (N \in ℕ_{0} \land K \in ℕ) \to (\binom{N}{K}) = \frac{seq (N - K + 1) (\times I) (N)}{K!}$

Metamath Proof Explorer

Theorem bcval5

Proof