Metamath Proof Explorer

Theorem bcp1n

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

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

Proof

Step Hyp Ref Expression
1 elfz3nn0 
 |-  ( K e. ( 0 ... N ) -> N e. NN0 )
2 facp1 
 |-  ( N e. NN0 -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
3 1 2 syl 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N + 1 ) ) = ( ( ! ` N ) x. ( N + 1 ) ) )
4 fznn0sub 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
5 facp1 
 |-  ( ( N - K ) e. NN0 -> ( ! ` ( ( N - K ) + 1 ) ) = ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) )
6 4 5 syl 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( ( N - K ) + 1 ) ) = ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) )
7 1 nn0cnd 
 |-  ( K e. ( 0 ... N ) -> N e. CC )
8 1cnd 
 |-  ( K e. ( 0 ... N ) -> 1 e. CC )
9 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
10 9 nn0cnd 
 |-  ( K e. ( 0 ... N ) -> K e. CC )
11 7 8 10 addsubd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) = ( ( N - K ) + 1 ) )
12 11 fveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( ( N + 1 ) - K ) ) = ( ! ` ( ( N - K ) + 1 ) ) )
13 11 oveq2d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ( N + 1 ) - K ) ) = ( ( ! ` ( N - K ) ) x. ( ( N - K ) + 1 ) ) )
14 6 12 13 3eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( ( N + 1 ) - K ) ) = ( ( ! ` ( N - K ) ) x. ( ( N + 1 ) - K ) ) )
15 14 oveq1d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) = ( ( ( ! ` ( N - K ) ) x. ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) )
16 4 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. NN )
17 16 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` ( N - K ) ) e. CC )
18 nn0p1nn 
 |-  ( ( N - K ) e. NN0 -> ( ( N - K ) + 1 ) e. NN )
19 4 18 syl 
 |-  ( K e. ( 0 ... N ) -> ( ( N - K ) + 1 ) e. NN )
20 11 19 eqeltrd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) e. NN )
21 20 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) e. CC )
22 9 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. NN )
23 22 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` K ) e. CC )
24 17 21 23 mul32d 
 |-  ( K e. ( 0 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) = ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N + 1 ) - K ) ) )
25 15 24 eqtrd 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) = ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N + 1 ) - K ) ) )
26 3 25 oveq12d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N + 1 ) ) / ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N + 1 ) - K ) ) ) )
27 1 faccld 
 |-  ( K e. ( 0 ... N ) -> ( ! ` N ) e. NN )
28 27 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( ! ` N ) e. CC )
29 nn0p1nn 
 |-  ( N e. NN0 -> ( N + 1 ) e. NN )
30 1 29 syl 
 |-  ( K e. ( 0 ... N ) -> ( N + 1 ) e. NN )
31 30 nncnd 
 |-  ( K e. ( 0 ... N ) -> ( N + 1 ) e. CC )
32 16 22 nnmulcld 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN )
33 nncn 
 |-  ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. CC )
34 nnne0 
 |-  ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN -> ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) =/= 0 )
35 33 34 jca 
 |-  ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. NN -> ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. CC /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) =/= 0 ) )
36 32 35 syl 
 |-  ( K e. ( 0 ... N ) -> ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. CC /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) =/= 0 ) )
37 20 nnne0d 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) - K ) =/= 0 )
38 21 37 jca 
 |-  ( K e. ( 0 ... N ) -> ( ( ( N + 1 ) - K ) e. CC /\ ( ( N + 1 ) - K ) =/= 0 ) )
39 divmuldiv 
 |-  ( ( ( ( ! ` N ) e. CC /\ ( N + 1 ) e. CC ) /\ ( ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) e. CC /\ ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) =/= 0 ) /\ ( ( ( N + 1 ) - K ) e. CC /\ ( ( N + 1 ) - K ) =/= 0 ) ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N + 1 ) - K ) ) ) )
40 28 31 36 38 39 syl22anc 
 |-  ( K e. ( 0 ... N ) -> ( ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) = ( ( ( ! ` N ) x. ( N + 1 ) ) / ( ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) x. ( ( N + 1 ) - K ) ) ) )
41 26 40 eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( ( ! ` ( N + 1 ) ) / ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) ) = ( ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
42 fzelp1 
 |-  ( K e. ( 0 ... N ) -> K e. ( 0 ... ( N + 1 ) ) )
43 bcval2 
 |-  ( K e. ( 0 ... ( N + 1 ) ) -> ( ( N + 1 ) _C K ) = ( ( ! ` ( N + 1 ) ) / ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) ) )
44 42 43 syl 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C K ) = ( ( ! ` ( N + 1 ) ) / ( ( ! ` ( ( N + 1 ) - K ) ) x. ( ! ` K ) ) ) )
45 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
46 45 oveq1d 
 |-  ( K e. ( 0 ... N ) -> ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) = ( ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )
47 41 44 46 3eqtr4d 
 |-  ( K e. ( 0 ... N ) -> ( ( N + 1 ) _C K ) = ( ( N _C K ) x. ( ( N + 1 ) / ( ( N + 1 ) - K ) ) ) )