Metamath Proof Explorer

Theorem bcmono

Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014)

Ref Expression
Assertion bcmono 
|- ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )

Proof

Step Hyp Ref Expression
1 simpl2 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> B e. ( ZZ>= ` A ) )
2 simpl1 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> N e. NN0 )
3 eluzel2 
 |-  ( B e. ( ZZ>= ` A ) -> A e. ZZ )
4 3 3ad2ant2 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> A e. ZZ )
5 4 anim1i 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> ( A e. ZZ /\ 0 <_ A ) )
6 elnn0z 
 |-  ( A e. NN0 <-> ( A e. ZZ /\ 0 <_ A ) )
7 5 6 sylibr 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> A e. NN0 )
8 simpl3 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> B <_ ( N / 2 ) )
9 breq1 
 |-  ( x = A -> ( x <_ ( N / 2 ) <-> A <_ ( N / 2 ) ) )
10 oveq2 
 |-  ( x = A -> ( N _C x ) = ( N _C A ) )
11 10 breq2d 
 |-  ( x = A -> ( ( N _C A ) <_ ( N _C x ) <-> ( N _C A ) <_ ( N _C A ) ) )
12 9 11 imbi12d 
 |-  ( x = A -> ( ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) <-> ( A <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C A ) ) ) )
13 12 imbi2d 
 |-  ( x = A -> ( ( ( N e. NN0 /\ A e. NN0 ) -> ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) ) <-> ( ( N e. NN0 /\ A e. NN0 ) -> ( A <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C A ) ) ) ) )
14 breq1 
 |-  ( x = k -> ( x <_ ( N / 2 ) <-> k <_ ( N / 2 ) ) )
15 oveq2 
 |-  ( x = k -> ( N _C x ) = ( N _C k ) )
16 15 breq2d 
 |-  ( x = k -> ( ( N _C A ) <_ ( N _C x ) <-> ( N _C A ) <_ ( N _C k ) ) )
17 14 16 imbi12d 
 |-  ( x = k -> ( ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) <-> ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) ) )
18 17 imbi2d 
 |-  ( x = k -> ( ( ( N e. NN0 /\ A e. NN0 ) -> ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) ) <-> ( ( N e. NN0 /\ A e. NN0 ) -> ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) ) ) )
19 breq1 
 |-  ( x = ( k + 1 ) -> ( x <_ ( N / 2 ) <-> ( k + 1 ) <_ ( N / 2 ) ) )
20 oveq2 
 |-  ( x = ( k + 1 ) -> ( N _C x ) = ( N _C ( k + 1 ) ) )
21 20 breq2d 
 |-  ( x = ( k + 1 ) -> ( ( N _C A ) <_ ( N _C x ) <-> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) )
22 19 21 imbi12d 
 |-  ( x = ( k + 1 ) -> ( ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) <-> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) )
23 22 imbi2d 
 |-  ( x = ( k + 1 ) -> ( ( ( N e. NN0 /\ A e. NN0 ) -> ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) ) <-> ( ( N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) ) )
24 breq1 
 |-  ( x = B -> ( x <_ ( N / 2 ) <-> B <_ ( N / 2 ) ) )
25 oveq2 
 |-  ( x = B -> ( N _C x ) = ( N _C B ) )
26 25 breq2d 
 |-  ( x = B -> ( ( N _C A ) <_ ( N _C x ) <-> ( N _C A ) <_ ( N _C B ) ) )
27 24 26 imbi12d 
 |-  ( x = B -> ( ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) <-> ( B <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C B ) ) ) )
28 27 imbi2d 
 |-  ( x = B -> ( ( ( N e. NN0 /\ A e. NN0 ) -> ( x <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C x ) ) ) <-> ( ( N e. NN0 /\ A e. NN0 ) -> ( B <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C B ) ) ) ) )
29 bccl 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( N _C A ) e. NN0 )
30 29 nn0red 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( N _C A ) e. RR )
31 30 leidd 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( N _C A ) <_ ( N _C A ) )
32 31 a1d 
 |-  ( ( N e. NN0 /\ A e. ZZ ) -> ( A <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C A ) ) )
33 32 expcom 
 |-  ( A e. ZZ -> ( N e. NN0 -> ( A <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C A ) ) ) )
34 33 adantrd 
 |-  ( A e. ZZ -> ( ( N e. NN0 /\ A e. NN0 ) -> ( A <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C A ) ) ) )
35 eluzelz 
 |-  ( k e. ( ZZ>= ` A ) -> k e. ZZ )
36 35 3ad2ant1 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> k e. ZZ )
37 36 zred 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> k e. RR )
38 37 lep1d 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> k <_ ( k + 1 ) )
39 peano2re 
 |-  ( k e. RR -> ( k + 1 ) e. RR )
40 37 39 syl 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( k + 1 ) e. RR )
41 nn0re 
 |-  ( N e. NN0 -> N e. RR )
42 41 3ad2ant2 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> N e. RR )
43 42 rehalfcld 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N / 2 ) e. RR )
44 letr 
 |-  ( ( k e. RR /\ ( k + 1 ) e. RR /\ ( N / 2 ) e. RR ) -> ( ( k <_ ( k + 1 ) /\ ( k + 1 ) <_ ( N / 2 ) ) -> k <_ ( N / 2 ) ) )
45 37 40 43 44 syl3anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k <_ ( k + 1 ) /\ ( k + 1 ) <_ ( N / 2 ) ) -> k <_ ( N / 2 ) ) )
46 38 45 mpand 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> k <_ ( N / 2 ) ) )
47 46 imim1d 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) ) )
48 eluznn0 
 |-  ( ( A e. NN0 /\ k e. ( ZZ>= ` A ) ) -> k e. NN0 )
49 41 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> N e. RR )
50 nn0re 
 |-  ( k e. NN0 -> k e. RR )
51 50 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. RR )
52 nn0p1nn 
 |-  ( k e. NN0 -> ( k + 1 ) e. NN )
53 52 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. NN )
54 53 nnnn0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. NN0 )
55 54 nn0red 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. RR )
56 53 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. CC )
57 56 2timesd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( 2 x. ( k + 1 ) ) = ( ( k + 1 ) + ( k + 1 ) ) )
58 simp3 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) <_ ( N / 2 ) )
59 2re 
 |-  2 e. RR
60 2pos 
 |-  0 < 2
61 59 60 pm3.2i 
 |-  ( 2 e. RR /\ 0 < 2 )
62 61 a1i 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( 2 e. RR /\ 0 < 2 ) )
63 lemuldiv2 
 |-  ( ( ( k + 1 ) e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( 2 x. ( k + 1 ) ) <_ N <-> ( k + 1 ) <_ ( N / 2 ) ) )
64 55 49 62 63 syl3anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( 2 x. ( k + 1 ) ) <_ N <-> ( k + 1 ) <_ ( N / 2 ) ) )
65 58 64 mpbird 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( 2 x. ( k + 1 ) ) <_ N )
66 57 65 eqbrtrrd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( k + 1 ) + ( k + 1 ) ) <_ N )
67 51 lep1d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k <_ ( k + 1 ) )
68 49 51 55 55 66 67 lesub3d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) <_ ( N - k ) )
69 nnre 
 |-  ( ( k + 1 ) e. NN -> ( k + 1 ) e. RR )
70 nngt0 
 |-  ( ( k + 1 ) e. NN -> 0 < ( k + 1 ) )
71 69 70 jca 
 |-  ( ( k + 1 ) e. NN -> ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) )
72 53 71 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) )
73 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
74 73 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> N e. ZZ )
75 nn0z 
 |-  ( k e. NN0 -> k e. ZZ )
76 75 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. ZZ )
77 74 76 zsubcld 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - k ) e. ZZ )
78 49 rehalfcld 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N / 2 ) e. RR )
79 49 59 jctir 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N e. RR /\ 2 e. RR ) )
80 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
81 80 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 <_ N )
82 1le2 
 |-  1 <_ 2
83 81 82 jctir 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( 0 <_ N /\ 1 <_ 2 ) )
84 lemulge12 
 |-  ( ( ( N e. RR /\ 2 e. RR ) /\ ( 0 <_ N /\ 1 <_ 2 ) ) -> N <_ ( 2 x. N ) )
85 79 83 84 syl2anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> N <_ ( 2 x. N ) )
86 ledivmul 
 |-  ( ( N e. RR /\ N e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( N / 2 ) <_ N <-> N <_ ( 2 x. N ) ) )
87 49 49 62 86 syl3anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( N / 2 ) <_ N <-> N <_ ( 2 x. N ) ) )
88 85 87 mpbird 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N / 2 ) <_ N )
89 55 78 49 58 88 letrd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) <_ N )
90 1red 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 1 e. RR )
91 51 90 49 leaddsub2d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( k + 1 ) <_ N <-> 1 <_ ( N - k ) ) )
92 89 91 mpbid 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 1 <_ ( N - k ) )
93 elnnz1 
 |-  ( ( N - k ) e. NN <-> ( ( N - k ) e. ZZ /\ 1 <_ ( N - k ) ) )
94 77 92 93 sylanbrc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - k ) e. NN )
95 nnre 
 |-  ( ( N - k ) e. NN -> ( N - k ) e. RR )
96 nngt0 
 |-  ( ( N - k ) e. NN -> 0 < ( N - k ) )
97 95 96 jca 
 |-  ( ( N - k ) e. NN -> ( ( N - k ) e. RR /\ 0 < ( N - k ) ) )
98 94 97 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( N - k ) e. RR /\ 0 < ( N - k ) ) )
99 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
100 99 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` N ) e. NN )
101 nnm1nn0 
 |-  ( ( N - k ) e. NN -> ( ( N - k ) - 1 ) e. NN0 )
102 faccl 
 |-  ( ( ( N - k ) - 1 ) e. NN0 -> ( ! ` ( ( N - k ) - 1 ) ) e. NN )
103 94 101 102 3syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( ( N - k ) - 1 ) ) e. NN )
104 faccl 
 |-  ( k e. NN0 -> ( ! ` k ) e. NN )
105 104 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` k ) e. NN )
106 103 105 nnmulcld 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. NN )
107 nnrp 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. RR+ )
108 nnrp 
 |-  ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. NN -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. RR+ )
109 rpdivcl 
 |-  ( ( ( ! ` N ) e. RR+ /\ ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. RR+ ) -> ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) e. RR+ )
110 107 108 109 syl2an 
 |-  ( ( ( ! ` N ) e. NN /\ ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. NN ) -> ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) e. RR+ )
111 100 106 110 syl2anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) e. RR+ )
112 111 rpregt0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) e. RR /\ 0 < ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) ) )
113 lediv2 
 |-  ( ( ( ( k + 1 ) e. RR /\ 0 < ( k + 1 ) ) /\ ( ( N - k ) e. RR /\ 0 < ( N - k ) ) /\ ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) e. RR /\ 0 < ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) ) ) -> ( ( k + 1 ) <_ ( N - k ) <-> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) <_ ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) ) )
114 72 98 112 113 syl3anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( k + 1 ) <_ ( N - k ) <-> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) <_ ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) ) )
115 68 114 mpbid 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) <_ ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) )
116 facnn2 
 |-  ( ( N - k ) e. NN -> ( ! ` ( N - k ) ) = ( ( ! ` ( ( N - k ) - 1 ) ) x. ( N - k ) ) )
117 94 116 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( N - k ) ) = ( ( ! ` ( ( N - k ) - 1 ) ) x. ( N - k ) ) )
118 117 oveq1d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) = ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( N - k ) ) x. ( ! ` k ) ) )
119 103 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( ( N - k ) - 1 ) ) e. CC )
120 105 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` k ) e. CC )
121 77 zcnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - k ) e. CC )
122 119 120 121 mul32d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( N - k ) ) = ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( N - k ) ) x. ( ! ` k ) ) )
123 118 122 eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) = ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( N - k ) ) )
124 123 oveq2d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) = ( ( ! ` N ) / ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( N - k ) ) ) )
125 0zd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 e. ZZ )
126 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
127 126 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 <_ k )
128 51 55 49 67 89 letrd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k <_ N )
129 125 74 76 127 128 elfzd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. ( 0 ... N ) )
130 bcval2 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) )
131 129 130 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) )
132 100 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` N ) e. CC )
133 106 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. CC )
134 106 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) =/= 0 )
135 94 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - k ) =/= 0 )
136 132 133 121 134 135 divdiv1d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) = ( ( ! ` N ) / ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( N - k ) ) ) )
137 124 131 136 3eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) = ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) )
138 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
139 138 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> N e. CC )
140 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
141 140 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. CC )
142 1cnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 1 e. CC )
143 139 141 142 subsub4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( N - k ) - 1 ) = ( N - ( k + 1 ) ) )
144 143 eqcomd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - ( k + 1 ) ) = ( ( N - k ) - 1 ) )
145 144 fveq2d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( N - ( k + 1 ) ) ) = ( ! ` ( ( N - k ) - 1 ) ) )
146 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
147 146 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
148 145 147 oveq12d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) = ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ( ! ` k ) x. ( k + 1 ) ) ) )
149 119 120 56 mulassd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( k + 1 ) ) = ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ( ! ` k ) x. ( k + 1 ) ) ) )
150 148 149 eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) = ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( k + 1 ) ) )
151 150 oveq2d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` N ) / ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) ) = ( ( ! ` N ) / ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( k + 1 ) ) ) )
152 53 nnzd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. ZZ )
153 54 nn0ge0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 <_ ( k + 1 ) )
154 125 74 152 153 89 elfzd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. ( 0 ... N ) )
155 bcval2 
 |-  ( ( k + 1 ) e. ( 0 ... N ) -> ( N _C ( k + 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) ) )
156 154 155 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C ( k + 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) ) )
157 53 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) =/= 0 )
158 132 133 56 134 157 divdiv1d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) = ( ( ! ` N ) / ( ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) x. ( k + 1 ) ) ) )
159 151 156 158 3eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C ( k + 1 ) ) = ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) )
160 115 137 159 3brtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) )
161 160 3exp 
 |-  ( k e. NN0 -> ( N e. NN0 -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) ) )
162 48 161 syl 
 |-  ( ( A e. NN0 /\ k e. ( ZZ>= ` A ) ) -> ( N e. NN0 -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) ) )
163 162 3impia 
 |-  ( ( A e. NN0 /\ k e. ( ZZ>= ` A ) /\ N e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) )
164 163 3coml 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) )
165 simp2 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> N e. NN0 )
166 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
167 166 3ad2ant3 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> A e. ZZ )
168 165 167 29 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C A ) e. NN0 )
169 168 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C A ) e. RR )
170 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
171 165 36 170 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C k ) e. NN0 )
172 171 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C k ) e. RR )
173 36 peano2zd 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( k + 1 ) e. ZZ )
174 bccl 
 |-  ( ( N e. NN0 /\ ( k + 1 ) e. ZZ ) -> ( N _C ( k + 1 ) ) e. NN0 )
175 165 173 174 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C ( k + 1 ) ) e. NN0 )
176 175 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C ( k + 1 ) ) e. RR )
177 letr 
 |-  ( ( ( N _C A ) e. RR /\ ( N _C k ) e. RR /\ ( N _C ( k + 1 ) ) e. RR ) -> ( ( ( N _C A ) <_ ( N _C k ) /\ ( N _C k ) <_ ( N _C ( k + 1 ) ) ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) )
178 169 172 176 177 syl3anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( ( N _C A ) <_ ( N _C k ) /\ ( N _C k ) <_ ( N _C ( k + 1 ) ) ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) )
179 178 expcomd 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( N _C k ) <_ ( N _C ( k + 1 ) ) -> ( ( N _C A ) <_ ( N _C k ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) )
180 164 179 syld 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( ( N _C A ) <_ ( N _C k ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) )
181 180 a2d 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) )
182 47 181 syld 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) )
183 182 3expib 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( N e. NN0 /\ A e. NN0 ) -> ( ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) ) )
184 183 a2d 
 |-  ( k e. ( ZZ>= ` A ) -> ( ( ( N e. NN0 /\ A e. NN0 ) -> ( k <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C k ) ) ) -> ( ( N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C ( k + 1 ) ) ) ) ) )
185 13 18 23 28 34 184 uzind4 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( N e. NN0 /\ A e. NN0 ) -> ( B <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C B ) ) ) )
186 185 3imp 
 |-  ( ( B e. ( ZZ>= ` A ) /\ ( N e. NN0 /\ A e. NN0 ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )
187 1 2 7 8 186 syl121anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> ( N _C A ) <_ ( N _C B ) )
188 simpl1 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> N e. NN0 )
189 4 adantr 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> A e. ZZ )
190 animorrl 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( A < 0 \/ N < A ) )
191 bcval4 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ ( A < 0 \/ N < A ) ) -> ( N _C A ) = 0 )
192 188 189 190 191 syl3anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C A ) = 0 )
193 simpl2 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> B e. ( ZZ>= ` A ) )
194 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
195 193 194 syl 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> B e. ZZ )
196 bccl 
 |-  ( ( N e. NN0 /\ B e. ZZ ) -> ( N _C B ) e. NN0 )
197 188 195 196 syl2anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C B ) e. NN0 )
198 197 nn0ge0d 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> 0 <_ ( N _C B ) )
199 192 198 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C A ) <_ ( N _C B ) )
200 0re 
 |-  0 e. RR
201 4 zred 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> A e. RR )
202 lelttric 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A \/ A < 0 ) )
203 200 201 202 sylancr 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( 0 <_ A \/ A < 0 ) )
204 187 199 203 mpjaodan 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )