Metamath Proof Explorer

Theorem bcm1n

Description: The proportion of one binomial coefficient to another with N decreased by 1. (Contributed by Thierry Arnoux, 9-Nov-2016)

Ref Expression
Assertion bcm1n 
|- ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) _C K ) / ( N _C K ) ) = ( ( N - K ) / N ) )

Proof

Step Hyp Ref Expression
1 bcp1n 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) )
2 nnz 
 |-  ( N e. NN -> N e. ZZ )
3 2 zcnd 
 |-  ( N e. NN -> N e. CC )
4 3 adantl 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N e. CC )
5 1cnd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> 1 e. CC )
6 4 5 npcand 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( N - 1 ) + 1 ) = N )
7 6 oveq1d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) + 1 ) _C K ) = ( N _C K ) )
8 6 oveq1d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) + 1 ) - K ) = ( N - K ) )
9 6 8 oveq12d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) = ( N / ( N - K ) ) )
10 9 oveq2d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )
11 7 10 eqeq12d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( ( N - 1 ) + 1 ) _C K ) = ( ( ( N - 1 ) _C K ) x. ( ( ( N - 1 ) + 1 ) / ( ( ( N - 1 ) + 1 ) - K ) ) ) <-> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) ) )
12 1 11 imbitrid 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K e. ( 0 ... ( N - 1 ) ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) ) )
13 12 3impia 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN /\ K e. ( 0 ... ( N - 1 ) ) ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )
14 13 3anidm13 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) )
15 elfznn0 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> K e. NN0 )
16 15 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K e. NN0 )
17 simpr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N e. NN )
18 17 nnnn0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N e. NN0 )
19 elfzelz 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> K e. ZZ )
20 19 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K e. ZZ )
21 20 zred 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K e. RR )
22 2 adantl 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N e. ZZ )
23 22 zred 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N e. RR )
24 elfzle2 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> K <_ ( N - 1 ) )
25 24 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K <_ ( N - 1 ) )
26 zltlem1 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( K < N <-> K <_ ( N - 1 ) ) )
27 19 2 26 syl2an 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K < N <-> K <_ ( N - 1 ) ) )
28 25 27 mpbird 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K < N )
29 21 23 28 ltled 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K <_ N )
30 elfz2nn0 
 |-  ( K e. ( 0 ... N ) <-> ( K e. NN0 /\ N e. NN0 /\ K <_ N ) )
31 16 18 29 30 syl3anbrc 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K e. ( 0 ... N ) )
32 bcrpcl 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) e. RR+ )
33 31 32 syl 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N _C K ) e. RR+ )
34 33 rpcnd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N _C K ) e. CC )
35 19 zcnd 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> K e. CC )
36 35 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K e. CC )
37 4 36 subcld 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N - K ) e. CC )
38 36 4 negsubdi2d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> -u ( K - N ) = ( N - K ) )
39 21 23 resubcld 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K - N ) e. RR )
40 39 recnd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K - N ) e. CC )
41 4 addlidd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( 0 + N ) = N )
42 28 41 breqtrrd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> K < ( 0 + N ) )
43 0red 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> 0 e. RR )
44 21 23 43 ltsubaddd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( K - N ) < 0 <-> K < ( 0 + N ) ) )
45 42 44 mpbird 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K - N ) < 0 )
46 45 lt0ne0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( K - N ) =/= 0 )
47 40 46 negne0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> -u ( K - N ) =/= 0 )
48 38 47 eqnetrrd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N - K ) =/= 0 )
49 4 37 48 divcld 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N / ( N - K ) ) e. CC )
50 bcrpcl 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) _C K ) e. RR+ )
51 50 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( N - 1 ) _C K ) e. RR+ )
52 51 rpcnne0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) _C K ) e. CC /\ ( ( N - 1 ) _C K ) =/= 0 ) )
53 divmul2 
 |-  ( ( ( N _C K ) e. CC /\ ( N / ( N - K ) ) e. CC /\ ( ( ( N - 1 ) _C K ) e. CC /\ ( ( N - 1 ) _C K ) =/= 0 ) ) -> ( ( ( N _C K ) / ( ( N - 1 ) _C K ) ) = ( N / ( N - K ) ) <-> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) ) )
54 34 49 52 53 syl3anc 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N _C K ) / ( ( N - 1 ) _C K ) ) = ( N / ( N - K ) ) <-> ( N _C K ) = ( ( ( N - 1 ) _C K ) x. ( N / ( N - K ) ) ) ) )
55 14 54 mpbird 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( N _C K ) / ( ( N - 1 ) _C K ) ) = ( N / ( N - K ) ) )
56 55 oveq2d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( 1 / ( ( N _C K ) / ( ( N - 1 ) _C K ) ) ) = ( 1 / ( N / ( N - K ) ) ) )
57 51 rpcnd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( N - 1 ) _C K ) e. CC )
58 bccl2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) e. NN )
59 31 58 syl 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N _C K ) e. NN )
60 59 nnne0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( N _C K ) =/= 0 )
61 bccl2 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) _C K ) e. NN )
62 61 nnne0d 
 |-  ( K e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) _C K ) =/= 0 )
63 62 adantr 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( N - 1 ) _C K ) =/= 0 )
64 34 57 60 63 recdivd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( 1 / ( ( N _C K ) / ( ( N - 1 ) _C K ) ) ) = ( ( ( N - 1 ) _C K ) / ( N _C K ) ) )
65 17 nnne0d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> N =/= 0 )
66 4 37 65 48 recdivd 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( 1 / ( N / ( N - K ) ) ) = ( ( N - K ) / N ) )
67 56 64 66 3eqtr3d 
 |-  ( ( K e. ( 0 ... ( N - 1 ) ) /\ N e. NN ) -> ( ( ( N - 1 ) _C K ) / ( N _C K ) ) = ( ( N - K ) / N ) )