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 
|- ( ph -> C e. CC )
bccval.k 
|- ( ph -> K e. NN0 )
Assertion bcc0 
|- ( ph -> ( ( C _Cc K ) = 0 <-> C e. ( 0 ... ( K - 1 ) ) ) )

Proof

Step Hyp Ref Expression
1 bccval.c 
 |-  ( ph -> C e. CC )
2 bccval.k 
 |-  ( ph -> K e. NN0 )
3 1 2 bccval 
 |-  ( ph -> ( C _Cc K ) = ( ( C FallFac K ) / ( ! ` K ) ) )
4 3 eqeq1d 
 |-  ( ph -> ( ( C _Cc K ) = 0 <-> ( ( C FallFac K ) / ( ! ` K ) ) = 0 ) )
5 fallfaccl 
 |-  ( ( C e. CC /\ K e. NN0 ) -> ( C FallFac K ) e. CC )
6 1 2 5 syl2anc 
 |-  ( ph -> ( C FallFac K ) e. CC )
7 faccl 
 |-  ( K e. NN0 -> ( ! ` K ) e. NN )
8 2 7 syl 
 |-  ( ph -> ( ! ` K ) e. NN )
9 8 nncnd 
 |-  ( ph -> ( ! ` K ) e. CC )
10 facne0 
 |-  ( K e. NN0 -> ( ! ` K ) =/= 0 )
11 2 10 syl 
 |-  ( ph -> ( ! ` K ) =/= 0 )
12 6 9 11 diveq0ad 
 |-  ( ph -> ( ( ( C FallFac K ) / ( ! ` K ) ) = 0 <-> ( C FallFac K ) = 0 ) )
13 fallfacval 
 |-  ( ( C e. CC /\ K e. NN0 ) -> ( C FallFac K ) = prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) )
14 1 2 13 syl2anc 
 |-  ( ph -> ( C FallFac K ) = prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) )
15 14 eqeq1d 
 |-  ( ph -> ( ( C FallFac K ) = 0 <-> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 ) )
16 elfzuz3 
 |-  ( C e. ( 0 ... ( K - 1 ) ) -> ( K - 1 ) e. ( ZZ>= ` C ) )
17 16 adantl 
 |-  ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) -> ( K - 1 ) e. ( ZZ>= ` C ) )
18 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
19 elfznn0 
 |-  ( C e. ( 0 ... ( K - 1 ) ) -> C e. NN0 )
20 19 adantl 
 |-  ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) -> C e. NN0 )
21 1 ad2antrr 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k e. NN0 ) -> C e. CC )
22 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
23 22 adantl 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k e. NN0 ) -> k e. CC )
24 21 23 subcld 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k e. NN0 ) -> ( C - k ) e. CC )
25 1 ad2antrr 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k = C ) -> C e. CC )
26 eqcom 
 |-  ( k = C <-> C = k )
27 26 biimpi 
 |-  ( k = C -> C = k )
28 27 adantl 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k = C ) -> C = k )
29 25 28 subeq0bd 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ k = C ) -> ( C - k ) = 0 )
30 18 20 24 29 fprodeq0 
 |-  ( ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) /\ ( K - 1 ) e. ( ZZ>= ` C ) ) -> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 )
31 17 30 mpdan 
 |-  ( ( ph /\ C e. ( 0 ... ( K - 1 ) ) ) -> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 )
32 31 ex 
 |-  ( ph -> ( C e. ( 0 ... ( K - 1 ) ) -> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 ) )
33 fzfid 
 |-  ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) -> ( 0 ... ( K - 1 ) ) e. Fin )
34 1 ad2antrr 
 |-  ( ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> C e. CC )
35 elfznn0 
 |-  ( k e. ( 0 ... ( K - 1 ) ) -> k e. NN0 )
36 35 nn0cnd 
 |-  ( k e. ( 0 ... ( K - 1 ) ) -> k e. CC )
37 36 adantl 
 |-  ( ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> k e. CC )
38 34 37 subcld 
 |-  ( ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( C - k ) e. CC )
39 nelne2 
 |-  ( ( k e. ( 0 ... ( K - 1 ) ) /\ -. C e. ( 0 ... ( K - 1 ) ) ) -> k =/= C )
40 39 necomd 
 |-  ( ( k e. ( 0 ... ( K - 1 ) ) /\ -. C e. ( 0 ... ( K - 1 ) ) ) -> C =/= k )
41 40 ancoms 
 |-  ( ( -. C e. ( 0 ... ( K - 1 ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> C =/= k )
42 41 adantll 
 |-  ( ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> C =/= k )
43 34 37 42 subne0d 
 |-  ( ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) /\ k e. ( 0 ... ( K - 1 ) ) ) -> ( C - k ) =/= 0 )
44 33 38 43 fprodn0 
 |-  ( ( ph /\ -. C e. ( 0 ... ( K - 1 ) ) ) -> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) =/= 0 )
45 44 ex 
 |-  ( ph -> ( -. C e. ( 0 ... ( K - 1 ) ) -> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) =/= 0 ) )
46 45 necon4bd 
 |-  ( ph -> ( prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 -> C e. ( 0 ... ( K - 1 ) ) ) )
47 32 46 impbid 
 |-  ( ph -> ( C e. ( 0 ... ( K - 1 ) ) <-> prod_ k e. ( 0 ... ( K - 1 ) ) ( C - k ) = 0 ) )
48 15 47 bitr4d 
 |-  ( ph -> ( ( C FallFac K ) = 0 <-> C e. ( 0 ... ( K - 1 ) ) ) )
49 4 12 48 3bitrd 
 |-  ( ph -> ( ( C _Cc K ) = 0 <-> C e. ( 0 ... ( K - 1 ) ) ) )