bcc0

Description: The generalized binomial coefficient C choose K is zero iff C is an integer between zero and ( K - 1 ) inclusive. (Contributed by Steve Rodriguez, 22-Apr-2020)

	Ref	Expression
Hypotheses	bccval.c	$⊢ φ \to C \in ℂ$
	bccval.k	$⊢ φ \to K \in ℕ_{0}$
Assertion	bcc0	$⊢ φ \to (C C_{𝑐} K = 0 \leftrightarrow C \in (0 \dots K - 1))$

Proof

Step	Hyp	Ref	Expression
1		bccval.c	$⊢ φ \to C \in ℂ$
2		bccval.k	$⊢ φ \to K \in ℕ_{0}$
3	1 2	bccval	$⊢ φ \to C C_{𝑐} K = \frac{C^{\underline{K}}}{K!}$
4	3	eqeq1d	$⊢ φ \to (C C_{𝑐} K = 0 \leftrightarrow \frac{C^{\underline{K}}}{K!} = 0)$
5		fallfaccl	$⊢ (C \in ℂ \land K \in ℕ_{0}) \to C^{\underline{K}} \in ℂ$
6	1 2 5	syl2anc	$⊢ φ \to C^{\underline{K}} \in ℂ$
7		faccl	$⊢ K \in ℕ_{0} \to K! \in ℕ$
8	2 7	syl	$⊢ φ \to K! \in ℕ$
9	8	nncnd	$⊢ φ \to K! \in ℂ$
10		facne0	$⊢ K \in ℕ_{0} \to K! \neq 0$
11	2 10	syl	$⊢ φ \to K! \neq 0$
12	6 9 11	diveq0ad	$⊢ φ \to (\frac{C^{\underline{K}}}{K!} = 0 \leftrightarrow C^{\underline{K}} = 0)$
13		fallfacval	$⊢ (C \in ℂ \land K \in ℕ_{0}) \to C^{\underline{K}} = \prod_{k = 0}^{K - 1} (C - k)$
14	1 2 13	syl2anc	$⊢ φ \to C^{\underline{K}} = \prod_{k = 0}^{K - 1} (C - k)$
15	14	eqeq1d	$⊢ φ \to (C^{\underline{K}} = 0 \leftrightarrow \prod_{k = 0}^{K - 1} (C - k) = 0)$
16		elfzuz3	$⊢ C \in (0 \dots K - 1) \to K - 1 \in ℤ_{\geq C}$
17	16	adantl	$⊢ (φ \land C \in (0 \dots K - 1)) \to K - 1 \in ℤ_{\geq C}$
18		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
19		elfznn0	$⊢ C \in (0 \dots K - 1) \to C \in ℕ_{0}$
20	19	adantl	$⊢ (φ \land C \in (0 \dots K - 1)) \to C \in ℕ_{0}$
21	1	ad2antrr	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k \in ℕ_{0}) \to C \in ℂ$
22		nn0cn	$⊢ k \in ℕ_{0} \to k \in ℂ$
23	22	adantl	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k \in ℕ_{0}) \to k \in ℂ$
24	21 23	subcld	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k \in ℕ_{0}) \to C - k \in ℂ$
25	1	ad2antrr	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k = C) \to C \in ℂ$
26		eqcom	$⊢ k = C \leftrightarrow C = k$
27	26	biimpi	$⊢ k = C \to C = k$
28	27	adantl	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k = C) \to C = k$
29	25 28	subeq0bd	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k = C) \to C - k = 0$
30	18 20 24 29	fprodeq0	$⊢ ((φ \land C \in (0 \dots K - 1)) \land K - 1 \in ℤ_{\geq C}) \to \prod_{k = 0}^{K - 1} (C - k) = 0$
31	17 30	mpdan	$⊢ (φ \land C \in (0 \dots K - 1)) \to \prod_{k = 0}^{K - 1} (C - k) = 0$
32	31	ex	$⊢ φ \to (C \in (0 \dots K - 1) \to \prod_{k = 0}^{K - 1} (C - k) = 0)$
33		fzfid	$⊢ (φ \land \neg C \in (0 \dots K - 1)) \to (0 \dots K - 1) \in Fin$
34	1	ad2antrr	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C \in ℂ$
35		elfznn0	$⊢ k \in (0 \dots K - 1) \to k \in ℕ_{0}$
36	35	nn0cnd	$⊢ k \in (0 \dots K - 1) \to k \in ℂ$
37	36	adantl	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to k \in ℂ$
38	34 37	subcld	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C - k \in ℂ$
39		nelne2	$⊢ (k \in (0 \dots K - 1) \land \neg C \in (0 \dots K - 1)) \to k \neq C$
40	39	necomd	$⊢ (k \in (0 \dots K - 1) \land \neg C \in (0 \dots K - 1)) \to C \neq k$
41	40	ancoms	$⊢ (\neg C \in (0 \dots K - 1) \land k \in (0 \dots K - 1)) \to C \neq k$
42	41	adantll	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C \neq k$
43	34 37 42	subne0d	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C - k \neq 0$
44	33 38 43	fprodn0	$⊢ (φ \land \neg C \in (0 \dots K - 1)) \to \prod_{k = 0}^{K - 1} (C - k) \neq 0$
45	44	ex	$⊢ φ \to (\neg C \in (0 \dots K - 1) \to \prod_{k = 0}^{K - 1} (C - k) \neq 0)$
46	45	necon4bd	$⊢ φ \to (\prod_{k = 0}^{K - 1} (C - k) = 0 \to C \in (0 \dots K - 1))$
47	32 46	impbid	$⊢ φ \to (C \in (0 \dots K - 1) \leftrightarrow \prod_{k = 0}^{K - 1} (C - k) = 0)$
48	15 47	bitr4d	$⊢ φ \to (C^{\underline{K}} = 0 \leftrightarrow C \in (0 \dots K - 1))$
49	4 12 48	3bitrd	$⊢ φ \to (C C_{𝑐} K = 0 \leftrightarrow C \in (0 \dots K - 1))$

Metamath Proof Explorer

Theorem bcc0

Proof