Metamath Proof Explorer

Theorem bcmax

Description: The binomial coefficient takes its maximum value at the center. (Contributed by Mario Carneiro, 5-Mar-2014)

Ref Expression
Assertion bcmax 
|- ( ( N e. NN0 /\ K e. ZZ ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )

Proof

Step Hyp Ref Expression
1 2nn0 
 |-  2 e. NN0
2 simpll 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> N e. NN0 )
3 nn0mulcl 
 |-  ( ( 2 e. NN0 /\ N e. NN0 ) -> ( 2 x. N ) e. NN0 )
4 1 2 3 sylancr 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> ( 2 x. N ) e. NN0 )
5 simpr 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> N e. ( ZZ>= ` K ) )
6 nn0re 
 |-  ( N e. NN0 -> N e. RR )
7 6 leidd 
 |-  ( N e. NN0 -> N <_ N )
8 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
9 2cn 
 |-  2 e. CC
10 2ne0 
 |-  2 =/= 0
11 divcan3 
 |-  ( ( N e. CC /\ 2 e. CC /\ 2 =/= 0 ) -> ( ( 2 x. N ) / 2 ) = N )
12 9 10 11 mp3an23 
 |-  ( N e. CC -> ( ( 2 x. N ) / 2 ) = N )
13 8 12 syl 
 |-  ( N e. NN0 -> ( ( 2 x. N ) / 2 ) = N )
14 7 13 breqtrrd 
 |-  ( N e. NN0 -> N <_ ( ( 2 x. N ) / 2 ) )
15 2 14 syl 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> N <_ ( ( 2 x. N ) / 2 ) )
16 bcmono 
 |-  ( ( ( 2 x. N ) e. NN0 /\ N e. ( ZZ>= ` K ) /\ N <_ ( ( 2 x. N ) / 2 ) ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )
17 4 5 15 16 syl3anc 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ N e. ( ZZ>= ` K ) ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )
18 simpll 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N e. NN0 )
19 1 18 3 sylancr 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( 2 x. N ) e. NN0 )
20 simplr 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> K e. ZZ )
21 bccmpl 
 |-  ( ( ( 2 x. N ) e. NN0 /\ K e. ZZ ) -> ( ( 2 x. N ) _C K ) = ( ( 2 x. N ) _C ( ( 2 x. N ) - K ) ) )
22 19 20 21 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) _C K ) = ( ( 2 x. N ) _C ( ( 2 x. N ) - K ) ) )
23 18 nn0red 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N e. RR )
24 23 recnd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N e. CC )
25 24 2timesd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( 2 x. N ) = ( N + N ) )
26 20 zred 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> K e. RR )
27 eluzle 
 |-  ( K e. ( ZZ>= ` N ) -> N <_ K )
28 27 adantl 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N <_ K )
29 23 26 23 28 leadd2dd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( N + N ) <_ ( N + K ) )
30 25 29 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( 2 x. N ) <_ ( N + K ) )
31 19 nn0red 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( 2 x. N ) e. RR )
32 31 26 23 lesubaddd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( ( 2 x. N ) - K ) <_ N <-> ( 2 x. N ) <_ ( N + K ) ) )
33 30 32 mpbird 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) - K ) <_ N )
34 19 nn0zd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( 2 x. N ) e. ZZ )
35 34 20 zsubcld 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) - K ) e. ZZ )
36 18 nn0zd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N e. ZZ )
37 eluz 
 |-  ( ( ( ( 2 x. N ) - K ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( ( 2 x. N ) - K ) ) <-> ( ( 2 x. N ) - K ) <_ N ) )
38 35 36 37 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( N e. ( ZZ>= ` ( ( 2 x. N ) - K ) ) <-> ( ( 2 x. N ) - K ) <_ N ) )
39 33 38 mpbird 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` ( ( 2 x. N ) - K ) ) )
40 18 14 syl 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> N <_ ( ( 2 x. N ) / 2 ) )
41 bcmono 
 |-  ( ( ( 2 x. N ) e. NN0 /\ N e. ( ZZ>= ` ( ( 2 x. N ) - K ) ) /\ N <_ ( ( 2 x. N ) / 2 ) ) -> ( ( 2 x. N ) _C ( ( 2 x. N ) - K ) ) <_ ( ( 2 x. N ) _C N ) )
42 19 39 40 41 syl3anc 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) _C ( ( 2 x. N ) - K ) ) <_ ( ( 2 x. N ) _C N ) )
43 22 42 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ K e. ZZ ) /\ K e. ( ZZ>= ` N ) ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )
44 simpr 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> K e. ZZ )
45 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
46 45 adantr 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> N e. ZZ )
47 uztric 
 |-  ( ( K e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` K ) \/ K e. ( ZZ>= ` N ) ) )
48 44 46 47 syl2anc 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( N e. ( ZZ>= ` K ) \/ K e. ( ZZ>= ` N ) ) )
49 17 43 48 mpjaodan 
 |-  ( ( N e. NN0 /\ K e. ZZ ) -> ( ( 2 x. N ) _C K ) <_ ( ( 2 x. N ) _C N ) )