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	bilani	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k = C) \to C = k$
28	25 27	subeq0bd	$⊢ ((φ \land C \in (0 \dots K - 1)) \land k = C) \to C - k = 0$
29	18 20 24 28	fprodeq0	$⊢ ((φ \land C \in (0 \dots K - 1)) \land K - 1 \in ℤ_{\geq C}) \to \prod_{k = 0}^{K - 1} (C - k) = 0$
30	17 29	mpdan	$⊢ (φ \land C \in (0 \dots K - 1)) \to \prod_{k = 0}^{K - 1} (C - k) = 0$
31	30	ex	$⊢ φ \to (C \in (0 \dots K - 1) \to \prod_{k = 0}^{K - 1} (C - k) = 0)$
32		fzfid	$⊢ (φ \land \neg C \in (0 \dots K - 1)) \to (0 \dots K - 1) \in Fin$
33	1	ad2antrr	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C \in ℂ$
34		elfznn0	$⊢ k \in (0 \dots K - 1) \to k \in ℕ_{0}$
35	34	nn0cnd	$⊢ k \in (0 \dots K - 1) \to k \in ℂ$
36	35	adantl	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to k \in ℂ$
37	33 36	subcld	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C - k \in ℂ$
38		nelne2	$⊢ (k \in (0 \dots K - 1) \land \neg C \in (0 \dots K - 1)) \to k \neq C$
39	38	necomd	$⊢ (k \in (0 \dots K - 1) \land \neg C \in (0 \dots K - 1)) \to C \neq k$
40	39	ancoms	$⊢ (\neg C \in (0 \dots K - 1) \land k \in (0 \dots K - 1)) \to C \neq k$
41	40	adantll	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C \neq k$
42	33 36 41	subne0d	$⊢ ((φ \land \neg C \in (0 \dots K - 1)) \land k \in (0 \dots K - 1)) \to C - k \neq 0$
43	32 37 42	fprodn0	$⊢ (φ \land \neg C \in (0 \dots K - 1)) \to \prod_{k = 0}^{K - 1} (C - k) \neq 0$
44	43	ex	$⊢ φ \to (\neg C \in (0 \dots K - 1) \to \prod_{k = 0}^{K - 1} (C - k) \neq 0)$
45	44	necon4bd	$⊢ φ \to (\prod_{k = 0}^{K - 1} (C - k) = 0 \to C \in (0 \dots K - 1))$
46	31 45	impbid	$⊢ φ \to (C \in (0 \dots K - 1) \leftrightarrow \prod_{k = 0}^{K - 1} (C - k) = 0)$
47	15 46	bitr4d	$⊢ φ \to (C^{\underline{K}} = 0 \leftrightarrow C \in (0 \dots K - 1))$
48	4 12 47	3bitrd	$⊢ φ \to (C C_{𝑐} K = 0 \leftrightarrow C \in (0 \dots K - 1))$

Metamath Proof Explorer

Theorem bcc0

Proof