Metamath Proof Explorer

Theorem 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 
|- ( ph -> N e. NN0 )
bccbc.k 
|- ( ph -> K e. NN0 )
Assertion bccbc 
|- ( ph -> ( N _Cc K ) = ( N _C K ) )

Proof

Step Hyp Ref Expression
1 bccbc.c 
 |-  ( ph -> N e. NN0 )
2 bccbc.k 
 |-  ( ph -> K e. NN0 )
3 1 nn0cnd 
 |-  ( ph -> N e. CC )
4 3 2 bccval 
 |-  ( ph -> ( N _Cc K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
5 4 adantr 
 |-  ( ( ph /\ K e. ( 0 ... N ) ) -> ( N _Cc K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
6 bcfallfac 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
7 6 adantl 
 |-  ( ( ph /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( N FallFac K ) / ( ! ` K ) ) )
8 5 7 eqtr4d 
 |-  ( ( ph /\ K e. ( 0 ... N ) ) -> ( N _Cc K ) = ( N _C K ) )
9 nn0split 
 |-  ( N e. NN0 -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
10 1 9 syl 
 |-  ( ph -> NN0 = ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
11 2 10 eleqtrd 
 |-  ( ph -> K e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) )
12 elun 
 |-  ( K e. ( ( 0 ... N ) u. ( ZZ>= ` ( N + 1 ) ) ) <-> ( K e. ( 0 ... N ) \/ K e. ( ZZ>= ` ( N + 1 ) ) ) )
13 11 12 sylib 
 |-  ( ph -> ( K e. ( 0 ... N ) \/ K e. ( ZZ>= ` ( N + 1 ) ) ) )
14 13 orcanai 
 |-  ( ( ph /\ -. K e. ( 0 ... N ) ) -> K e. ( ZZ>= ` ( N + 1 ) ) )
15 eluzle 
 |-  ( K e. ( ZZ>= ` ( N + 1 ) ) -> ( N + 1 ) <_ K )
16 15 adantl 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N + 1 ) <_ K )
17 1 nn0zd 
 |-  ( ph -> N e. ZZ )
18 2 nn0zd 
 |-  ( ph -> K e. ZZ )
19 zltp1le 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N < K <-> ( N + 1 ) <_ K ) )
20 17 18 19 syl2anc 
 |-  ( ph -> ( N < K <-> ( N + 1 ) <_ K ) )
21 20 adantr 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( N + 1 ) ) ) -> ( N < K <-> ( N + 1 ) <_ K ) )
22 16 21 mpbird 
 |-  ( ( ph /\ K e. ( ZZ>= ` ( N + 1 ) ) ) -> N < K )
23 14 22 syldan 
 |-  ( ( ph /\ -. K e. ( 0 ... N ) ) -> N < K )
24 1 nn0ge0d 
 |-  ( ph -> 0 <_ N )
25 0zd 
 |-  ( ph -> 0 e. ZZ )
26 elfzo 
 |-  ( ( N e. ZZ /\ 0 e. ZZ /\ K e. ZZ ) -> ( N e. ( 0 ..^ K ) <-> ( 0 <_ N /\ N < K ) ) )
27 17 25 18 26 syl3anc 
 |-  ( ph -> ( N e. ( 0 ..^ K ) <-> ( 0 <_ N /\ N < K ) ) )
28 27 biimpar 
 |-  ( ( ph /\ ( 0 <_ N /\ N < K ) ) -> N e. ( 0 ..^ K ) )
29 fzoval 
 |-  ( K e. ZZ -> ( 0 ..^ K ) = ( 0 ... ( K - 1 ) ) )
30 18 29 syl 
 |-  ( ph -> ( 0 ..^ K ) = ( 0 ... ( K - 1 ) ) )
31 30 eleq2d 
 |-  ( ph -> ( N e. ( 0 ..^ K ) <-> N e. ( 0 ... ( K - 1 ) ) ) )
32 31 biimpa 
 |-  ( ( ph /\ N e. ( 0 ..^ K ) ) -> N e. ( 0 ... ( K - 1 ) ) )
33 3 2 bcc0 
 |-  ( ph -> ( ( N _Cc K ) = 0 <-> N e. ( 0 ... ( K - 1 ) ) ) )
34 33 biimpar 
 |-  ( ( ph /\ N e. ( 0 ... ( K - 1 ) ) ) -> ( N _Cc K ) = 0 )
35 32 34 syldan 
 |-  ( ( ph /\ N e. ( 0 ..^ K ) ) -> ( N _Cc K ) = 0 )
36 28 35 syldan 
 |-  ( ( ph /\ ( 0 <_ N /\ N < K ) ) -> ( N _Cc K ) = 0 )
37 24 36 sylanr1 
 |-  ( ( ph /\ ( ph /\ N < K ) ) -> ( N _Cc K ) = 0 )
38 37 anabss5 
 |-  ( ( ph /\ N < K ) -> ( N _Cc K ) = 0 )
39 23 38 syldan 
 |-  ( ( ph /\ -. K e. ( 0 ... N ) ) -> ( N _Cc K ) = 0 )
40 1 18 jca 
 |-  ( ph -> ( N e. NN0 /\ K e. ZZ ) )
41 bcval3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
42 41 3expa 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
43 40 42 sylan 
 |-  ( ( ph /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
44 39 43 eqtr4d 
 |-  ( ( ph /\ -. K e. ( 0 ... N ) ) -> ( N _Cc K ) = ( N _C K ) )
45 8 44 pm2.61dan 
 |-  ( ph -> ( N _Cc K ) = ( N _C K ) )