Metamath Proof Explorer

Theorem bcm1k

Description: The proportion of one binomial coefficient to another with K decreased by 1. (Contributed by Mario Carneiro, 10-Mar-2014)

Ref Expression
Assertion bcm1k 
|- ( K e. ( 1 ... N ) -> ( N _C K ) = ( ( N _C ( K - 1 ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )

Proof

Step Hyp Ref Expression
1 elfzuz2 
 |-  ( K e. ( 1 ... N ) -> N e. ( ZZ>= ` 1 ) )
2 nnuz 
 |-  NN = ( ZZ>= ` 1 )
3 1 2 eleqtrrdi 
 |-  ( K e. ( 1 ... N ) -> N e. NN )
4 3 nnnn0d 
 |-  ( K e. ( 1 ... N ) -> N e. NN0 )
5 4 faccld 
 |-  ( K e. ( 1 ... N ) -> ( ! ` N ) e. NN )
6 5 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ! ` N ) e. CC )
7 fznn0sub 
 |-  ( K e. ( 1 ... N ) -> ( N - K ) e. NN0 )
8 nn0p1nn 
 |-  ( ( N - K ) e. NN0 -> ( ( N - K ) + 1 ) e. NN )
9 7 8 syl 
 |-  ( K e. ( 1 ... N ) -> ( ( N - K ) + 1 ) e. NN )
10 9 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ( N - K ) + 1 ) e. CC )
11 9 nnnn0d 
 |-  ( K e. ( 1 ... N ) -> ( ( N - K ) + 1 ) e. NN0 )
12 11 faccld 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( ( N - K ) + 1 ) ) e. NN )
13 elfznn 
 |-  ( K e. ( 1 ... N ) -> K e. NN )
14 nnm1nn0 
 |-  ( K e. NN -> ( K - 1 ) e. NN0 )
15 faccl 
 |-  ( ( K - 1 ) e. NN0 -> ( ! ` ( K - 1 ) ) e. NN )
16 13 14 15 3syl 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( K - 1 ) ) e. NN )
17 12 16 nnmulcld 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. NN )
18 nncn 
 |-  ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. NN -> ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. CC )
19 nnne0 
 |-  ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. NN -> ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) =/= 0 )
20 18 19 jca 
 |-  ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. NN -> ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. CC /\ ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) =/= 0 ) )
21 17 20 syl 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. CC /\ ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) =/= 0 ) )
22 13 nncnd 
 |-  ( K e. ( 1 ... N ) -> K e. CC )
23 13 nnne0d 
 |-  ( K e. ( 1 ... N ) -> K =/= 0 )
24 22 23 jca 
 |-  ( K e. ( 1 ... N ) -> ( K e. CC /\ K =/= 0 ) )
25 divmuldiv 
 |-  ( ( ( ( ! ` N ) e. CC /\ ( ( N - K ) + 1 ) e. CC ) /\ ( ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) e. CC /\ ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) =/= 0 ) /\ ( K e. CC /\ K =/= 0 ) ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( ( N - K ) + 1 ) / K ) ) = ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) x. K ) ) )
26 6 10 21 24 25 syl22anc 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( ( N - K ) + 1 ) / K ) ) = ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) x. K ) ) )
27 elfzel2 
 |-  ( K e. ( 1 ... N ) -> N e. ZZ )
28 27 zcnd 
 |-  ( K e. ( 1 ... N ) -> N e. CC )
29 1cnd 
 |-  ( K e. ( 1 ... N ) -> 1 e. CC )
30 28 22 29 subsubd 
 |-  ( K e. ( 1 ... N ) -> ( N - ( K - 1 ) ) = ( ( N - K ) + 1 ) )
31 30 fveq2d 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( N - ( K - 1 ) ) ) = ( ! ` ( ( N - K ) + 1 ) ) )
32 31 oveq1d 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) = ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) )
33 32 oveq2d 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) = ( ( ! ` N ) / ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) ) )
34 30 oveq1d 
 |-  ( K e. ( 1 ... N ) -> ( ( N - ( K - 1 ) ) / K ) = ( ( ( N - K ) + 1 ) / K ) )
35 33 34 oveq12d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( N - ( K - 1 ) ) / K ) ) = ( ( ( ! ` N ) / ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( ( N - K ) + 1 ) / K ) ) )
36 facp1 
 |-  ( ( N - K ) e. NN0 -> ( ! ` ( ( N - K ) + 1 ) ) = ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) )
37 7 36 syl 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( ( N - K ) + 1 ) ) = ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) )
38 37 eqcomd 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) = ( ! ` ( ( N - K ) + 1 ) ) )
39 facnn2 
 |-  ( K e. NN -> ( ! ` K ) = ( ( ! ` ( K - 1 ) ) x. K ) )
40 13 39 syl 
 |-  ( K e. ( 1 ... N ) -> ( ! ` K ) = ( ( ! ` ( K - 1 ) ) x. K ) )
41 38 40 oveq12d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) x. ( ! ` K ) ) = ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ( ! ` ( K - 1 ) ) x. K ) ) )
42 7 faccld 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( N - K ) ) e. NN )
43 42 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( N - K ) ) e. CC )
44 13 nnnn0d 
 |-  ( K e. ( 1 ... N ) -> K e. NN0 )
45 44 faccld 
 |-  ( K e. ( 1 ... N ) -> ( ! ` K ) e. NN )
46 45 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ! ` K ) e. CC )
47 43 46 10 mul32d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) = ( ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) x. ( ! ` K ) ) )
48 12 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( ( N - K ) + 1 ) ) e. CC )
49 16 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ! ` ( K - 1 ) ) e. CC )
50 48 49 22 mulassd 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) x. K ) = ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ( ! ` ( K - 1 ) ) x. K ) ) )
51 41 47 50 3eqtr4d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) = ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) x. K ) )
52 51 oveq2d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) ) = ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( ( N - K ) + 1 ) ) x. ( ! ` ( K - 1 ) ) ) x. K ) ) )
53 26 35 52 3eqtr4d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( N - ( K - 1 ) ) / K ) ) = ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) ) )
54 6 10 mulcomd 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) = ( ( ( N - K ) + 1 ) x. ( ! ` N ) ) )
55 42 45 nnmulcld 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
56 55 nncnd 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. CC )
57 56 10 mulcomd 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) = ( ( ( N - K ) + 1 ) x. ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
58 54 57 oveq12d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ! ` N ) x. ( ( N - K ) + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N - K ) + 1 ) ) ) = ( ( ( ( N - K ) + 1 ) x. ( ! ` N ) ) / ( ( ( N - K ) + 1 ) x. ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) )
59 55 nnne0d 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) =/= 0 )
60 9 nnne0d 
 |-  ( K e. ( 1 ... N ) -> ( ( N - K ) + 1 ) =/= 0 )
61 6 56 10 59 60 divcan5d 
 |-  ( K e. ( 1 ... N ) -> ( ( ( ( N - K ) + 1 ) x. ( ! ` N ) ) / ( ( ( N - K ) + 1 ) x. ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
62 53 58 61 3eqtrrd 
 |-  ( K e. ( 1 ... N ) -> ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) = ( ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )
63 fz1ssfz0 
 |-  ( 1 ... N ) C_ ( 0 ... N )
64 63 sseli 
 |-  ( K e. ( 1 ... N ) -> K e. ( 0 ... N ) )
65 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
66 64 65 syl 
 |-  ( K e. ( 1 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
67 ax-1cn 
 |-  1 e. CC
68 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
69 28 67 68 sylancl 
 |-  ( K e. ( 1 ... N ) -> ( ( N - 1 ) + 1 ) = N )
70 peano2zm 
 |-  ( N e. ZZ -> ( N - 1 ) e. ZZ )
71 uzid 
 |-  ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
72 peano2uz 
 |-  ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
73 27 70 71 72 4syl 
 |-  ( K e. ( 1 ... N ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
74 69 73 eqeltrrd 
 |-  ( K e. ( 1 ... N ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
75 fzss2 
 |-  ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
76 74 75 syl 
 |-  ( K e. ( 1 ... N ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
77 elfzmlbm 
 |-  ( K e. ( 1 ... N ) -> ( K - 1 ) e. ( 0 ... ( N - 1 ) ) )
78 76 77 sseldd 
 |-  ( K e. ( 1 ... N ) -> ( K - 1 ) e. ( 0 ... N ) )
79 bcval2 
 |-  ( ( K - 1 ) e. ( 0 ... N ) -> ( N _C ( K - 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) )
80 78 79 syl 
 |-  ( K e. ( 1 ... N ) -> ( N _C ( K - 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) )
81 80 oveq1d 
 |-  ( K e. ( 1 ... N ) -> ( ( N _C ( K - 1 ) ) x. ( ( N - ( K - 1 ) ) / K ) ) = ( ( ( ! ` N ) / ( ( ! ` ( N - ( K - 1 ) ) ) x. ( ! ` ( K - 1 ) ) ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )
82 62 66 81 3eqtr4d 
 |-  ( K e. ( 1 ... N ) -> ( N _C K ) = ( ( N _C ( K - 1 ) ) x. ( ( N - ( K - 1 ) ) / K ) ) )