bccbc

Description: The binomial coefficient and generalized binomial coefficient are equal when their arguments are nonnegative integers. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccbc.c	$⊢ φ \to N \in ℕ_{0}$
	bccbc.k	$⊢ φ \to K \in ℕ_{0}$
Assertion	bccbc	$⊢ φ \to N C_{𝑐} K = (\binom{N}{K})$

Proof

Step	Hyp	Ref	Expression
1		bccbc.c	$⊢ φ \to N \in ℕ_{0}$
2		bccbc.k	$⊢ φ \to K \in ℕ_{0}$
3	1	nn0cnd	$⊢ φ \to N \in ℂ$
4	3 2	bccval	$⊢ φ \to N C_{𝑐} K = \frac{N^{\underline{K}}}{K!}$
5	4	adantr	$⊢ (φ \land K \in (0 \dots N)) \to N C_{𝑐} K = \frac{N^{\underline{K}}}{K!}$
6		bcfallfac	$⊢ K \in (0 \dots N) \to (\binom{N}{K}) = \frac{N^{\underline{K}}}{K!}$
7	6	adantl	$⊢ (φ \land K \in (0 \dots N)) \to (\binom{N}{K}) = \frac{N^{\underline{K}}}{K!}$
8	5 7	eqtr4d	$⊢ (φ \land K \in (0 \dots N)) \to N C_{𝑐} K = (\binom{N}{K})$
9		nn0split	$⊢ N \in ℕ_{0} \to ℕ_{0} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
10	1 9	syl	$⊢ φ \to ℕ_{0} = (0 \dots N) \cup ℤ_{\geq (N + 1)}$
11	2 10	eleqtrd	$⊢ φ \to K \in ((0 \dots N) \cup ℤ_{\geq (N + 1)})$
12		elun	$⊢ K \in ((0 \dots N) \cup ℤ_{\geq (N + 1)}) \leftrightarrow (K \in (0 \dots N) \lor K \in ℤ_{\geq (N + 1)})$
13	11 12	sylib	$⊢ φ \to (K \in (0 \dots N) \lor K \in ℤ_{\geq (N + 1)})$
14	13	orcanai	$⊢ (φ \land \neg K \in (0 \dots N)) \to K \in ℤ_{\geq (N + 1)}$
15		eluzle	$⊢ K \in ℤ_{\geq (N + 1)} \to N + 1 \leq K$
16	15	adantl	$⊢ (φ \land K \in ℤ_{\geq (N + 1)}) \to N + 1 \leq K$
17	1	nn0zd	$⊢ φ \to N \in ℤ$
18	2	nn0zd	$⊢ φ \to K \in ℤ$
19		zltp1le	$⊢ (N \in ℤ \land K \in ℤ) \to (N < K \leftrightarrow N + 1 \leq K)$
20	17 18 19	syl2anc	$⊢ φ \to (N < K \leftrightarrow N + 1 \leq K)$
21	20	adantr	$⊢ (φ \land K \in ℤ_{\geq (N + 1)}) \to (N < K \leftrightarrow N + 1 \leq K)$
22	16 21	mpbird	$⊢ (φ \land K \in ℤ_{\geq (N + 1)}) \to N < K$
23	14 22	syldan	$⊢ (φ \land \neg K \in (0 \dots N)) \to N < K$
24	1	nn0ge0d	$⊢ φ \to 0 \leq N$
25		0zd	$⊢ φ \to 0 \in ℤ$
26		elfzo	$⊢ (N \in ℤ \land 0 \in ℤ \land K \in ℤ) \to (N \in (0 ..^K) \leftrightarrow (0 \leq N \land N < K))$
27	17 25 18 26	syl3anc	$⊢ φ \to (N \in (0 ..^K) \leftrightarrow (0 \leq N \land N < K))$
28	27	biimpar	$⊢ (φ \land (0 \leq N \land N < K)) \to N \in (0 ..^K)$
29		fzoval	$⊢ K \in ℤ \to (0 ..^K) = (0 \dots K - 1)$
30	18 29	syl	$⊢ φ \to (0 ..^K) = (0 \dots K - 1)$
31	30	eleq2d	$⊢ φ \to (N \in (0 ..^K) \leftrightarrow N \in (0 \dots K - 1))$
32	31	biimpa	$⊢ (φ \land N \in (0 ..^K)) \to N \in (0 \dots K - 1)$
33	3 2	bcc0	$⊢ φ \to (N C_{𝑐} K = 0 \leftrightarrow N \in (0 \dots K - 1))$
34	33	biimpar	$⊢ (φ \land N \in (0 \dots K - 1)) \to N C_{𝑐} K = 0$
35	32 34	syldan	$⊢ (φ \land N \in (0 ..^K)) \to N C_{𝑐} K = 0$
36	28 35	syldan	$⊢ (φ \land (0 \leq N \land N < K)) \to N C_{𝑐} K = 0$
37	24 36	sylanr1	$⊢ (φ \land (φ \land N < K)) \to N C_{𝑐} K = 0$
38	37	anabss5	$⊢ (φ \land N < K) \to N C_{𝑐} K = 0$
39	23 38	syldan	$⊢ (φ \land \neg K \in (0 \dots N)) \to N C_{𝑐} K = 0$
40	1 18	jca	$⊢ φ \to (N \in ℕ_{0} \land K \in ℤ)$
41		bcval3	$⊢ (N \in ℕ_{0} \land K \in ℤ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
42	41	3expa	$⊢ ((N \in ℕ_{0} \land K \in ℤ) \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
43	40 42	sylan	$⊢ (φ \land \neg K \in (0 \dots N)) \to (\binom{N}{K}) = 0$
44	39 43	eqtr4d	$⊢ (φ \land \neg K \in (0 \dots N)) \to N C_{𝑐} K = (\binom{N}{K})$
45	8 44	pm2.61dan	$⊢ φ \to N C_{𝑐} K = (\binom{N}{K})$

Metamath Proof Explorer

Theorem bccbc

Proof