Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
bccval.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
Assertion bcc0 ( 𝜑 → ( ( 𝐶 C𝑐 𝐾 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 bccval.c ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 bccval.k ⊢ ( 𝜑 → 𝐾 ∈ ℕ0 )
3 1 2 bccval ⊢ ( 𝜑 → ( 𝐶 C𝑐 𝐾 ) = ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) )
4 3 eqeq1d ⊢ ( 𝜑 → ( ( 𝐶 C𝑐 𝐾 ) = 0 ↔ ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) = 0 ) )
5 fallfaccl ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
6 1 2 5 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) ∈ ℂ )
7 faccl ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ∈ ℕ )
8 2 7 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℕ )
9 8 nncnd ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ∈ ℂ )
10 facne0 ⊢ ( 𝐾 ∈ ℕ0 → ( ! ‘ 𝐾 ) ≠ 0 )
11 2 10 syl ⊢ ( 𝜑 → ( ! ‘ 𝐾 ) ≠ 0 )
12 6 9 11 diveq0ad ⊢ ( 𝜑 → ( ( ( 𝐶 FallFac 𝐾 ) / ( ! ‘ 𝐾 ) ) = 0 ↔ ( 𝐶 FallFac 𝐾 ) = 0 ) )
13 fallfacval ⊢ ( ( 𝐶 ∈ ℂ ∧ 𝐾 ∈ ℕ0 ) → ( 𝐶 FallFac 𝐾 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) )
14 1 2 13 syl2anc ⊢ ( 𝜑 → ( 𝐶 FallFac 𝐾 ) = ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) )
15 14 eqeq1d ⊢ ( 𝜑 → ( ( 𝐶 FallFac 𝐾 ) = 0 ↔ ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 ) )
16 elfzuz3 ⊢ ( 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
18 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
19 elfznn0 ⊢ ( 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝐶 ∈ ℕ0 )
20 19 adantl ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐶 ∈ ℕ0 )
21 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝐶 ∈ ℂ )
22 nn0cn ⊢ ( 𝑘 ∈ ℕ0 → 𝑘 ∈ ℂ )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → 𝑘 ∈ ℂ )
24 21 23 subcld ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ℕ0 ) → ( 𝐶 − 𝑘 ) ∈ ℂ )
25 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 = 𝐶 ) → 𝐶 ∈ ℂ )
26 eqcom ⊢ ( 𝑘 = 𝐶 ↔ 𝐶 = 𝑘 )
27 26 biimpi ⊢ ( 𝑘 = 𝐶 → 𝐶 = 𝑘 )
28 27 adantl ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 = 𝐶 ) → 𝐶 = 𝑘 )
29 25 28 subeq0bd ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 = 𝐶 ) → ( 𝐶 − 𝑘 ) = 0 )
30 18 20 24 29 fprodeq0 ⊢ ( ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ ( 𝐾 − 1 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 )
31 17 30 mpdan ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 )
32 31 ex ⊢ ( 𝜑 → ( 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 ) )
33 fzfid ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 0 ... ( 𝐾 − 1 ) ) ∈ Fin )
34 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐶 ∈ ℂ )
35 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑘 ∈ ℕ0 )
36 35 nn0cnd ⊢ ( 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) → 𝑘 ∈ ℂ )
37 36 adantl ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑘 ∈ ℂ )
38 34 37 subcld ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐶 − 𝑘 ) ∈ ℂ )
39 nelne2 ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝑘 ≠ 𝐶 )
40 39 necomd ⊢ ( ( 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐶 ≠ 𝑘 )
41 40 ancoms ⊢ ( ( ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐶 ≠ 𝑘 )
42 41 adantll ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → 𝐶 ≠ 𝑘 )
43 34 37 42 subne0d ⊢ ( ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) ∧ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ( 𝐶 − 𝑘 ) ≠ 0 )
44 33 38 43 fprodn0 ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) ≠ 0 )
45 44 ex ⊢ ( 𝜑 → ( ¬ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) → ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) ≠ 0 ) )
46 45 necon4bd ⊢ ( 𝜑 → ( ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 → 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )
47 32 46 impbid ⊢ ( 𝜑 → ( 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ↔ ∏ 𝑘 ∈ ( 0 ... ( 𝐾 − 1 ) ) ( 𝐶 − 𝑘 ) = 0 ) )
48 15 47 bitr4d ⊢ ( 𝜑 → ( ( 𝐶 FallFac 𝐾 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )
49 4 12 48 3bitrd ⊢ ( 𝜑 → ( ( 𝐶 C𝑐 𝐾 ) = 0 ↔ 𝐶 ∈ ( 0 ... ( 𝐾 − 1 ) ) ) )