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 nn0ge0 
 |-  ( k e. NN0 -> 0 <_ k )
126 125 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 <_ k )
127 51 55 49 67 89 letrd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k <_ N )
128 0zd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 e. ZZ )
129 elfz 
 |-  ( ( k e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( k e. ( 0 ... N ) <-> ( 0 <_ k /\ k <_ N ) ) )
130 76 128 74 129 syl3anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k e. ( 0 ... N ) <-> ( 0 <_ k /\ k <_ N ) ) )
131 126 127 130 mpbir2and 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. ( 0 ... N ) )
132 bcval2 
 |-  ( k e. ( 0 ... N ) -> ( N _C k ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) )
133 131 132 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) = ( ( ! ` N ) / ( ( ! ` ( N - k ) ) x. ( ! ` k ) ) ) )
134 100 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` N ) e. CC )
135 106 nncnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) e. CC )
136 106 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) =/= 0 )
137 94 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - k ) =/= 0 )
138 134 135 121 136 137 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 ) ) ) )
139 124 133 138 3eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) = ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( N - k ) ) )
140 nn0cn 
 |-  ( N e. NN0 -> N e. CC )
141 140 3ad2ant2 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> N e. CC )
142 nn0cn 
 |-  ( k e. NN0 -> k e. CC )
143 142 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> k e. CC )
144 1cnd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 1 e. CC )
145 141 143 144 subsub4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( N - k ) - 1 ) = ( N - ( k + 1 ) ) )
146 145 eqcomd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N - ( k + 1 ) ) = ( ( N - k ) - 1 ) )
147 146 fveq2d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( N - ( k + 1 ) ) ) = ( ! ` ( ( N - k ) - 1 ) ) )
148 facp1 
 |-  ( k e. NN0 -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
149 148 3ad2ant1 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ! ` ( k + 1 ) ) = ( ( ! ` k ) x. ( k + 1 ) ) )
150 147 149 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 ) ) ) )
151 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 ) ) ) )
152 150 151 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 ) ) )
153 152 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 ) ) ) )
154 54 nn0ge0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> 0 <_ ( k + 1 ) )
155 53 nnzd 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. ZZ )
156 elfz 
 |-  ( ( ( k + 1 ) e. ZZ /\ 0 e. ZZ /\ N e. ZZ ) -> ( ( k + 1 ) e. ( 0 ... N ) <-> ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
157 155 128 74 156 syl3anc 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( ( k + 1 ) e. ( 0 ... N ) <-> ( 0 <_ ( k + 1 ) /\ ( k + 1 ) <_ N ) ) )
158 154 89 157 mpbir2and 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) e. ( 0 ... N ) )
159 bcval2 
 |-  ( ( k + 1 ) e. ( 0 ... N ) -> ( N _C ( k + 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) ) )
160 158 159 syl 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C ( k + 1 ) ) = ( ( ! ` N ) / ( ( ! ` ( N - ( k + 1 ) ) ) x. ( ! ` ( k + 1 ) ) ) ) )
161 53 nnne0d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( k + 1 ) =/= 0 )
162 134 135 56 136 161 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 ) ) ) )
163 153 160 162 3eqtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C ( k + 1 ) ) = ( ( ( ! ` N ) / ( ( ! ` ( ( N - k ) - 1 ) ) x. ( ! ` k ) ) ) / ( k + 1 ) ) )
164 115 139 163 3brtr4d 
 |-  ( ( k e. NN0 /\ N e. NN0 /\ ( k + 1 ) <_ ( N / 2 ) ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) )
165 164 3exp 
 |-  ( k e. NN0 -> ( N e. NN0 -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) ) )
166 48 165 syl 
 |-  ( ( A e. NN0 /\ k e. ( ZZ>= ` A ) ) -> ( N e. NN0 -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) ) )
167 166 3impia 
 |-  ( ( A e. NN0 /\ k e. ( ZZ>= ` A ) /\ N e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) )
168 167 3coml 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( ( k + 1 ) <_ ( N / 2 ) -> ( N _C k ) <_ ( N _C ( k + 1 ) ) ) )
169 simp2 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> N e. NN0 )
170 nn0z 
 |-  ( A e. NN0 -> A e. ZZ )
171 170 3ad2ant3 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> A e. ZZ )
172 169 171 29 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C A ) e. NN0 )
173 172 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C A ) e. RR )
174 bccl 
 |-  ( ( N e. NN0 /\ k e. ZZ ) -> ( N _C k ) e. NN0 )
175 169 36 174 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C k ) e. NN0 )
176 175 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C k ) e. RR )
177 36 peano2zd 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( k + 1 ) e. ZZ )
178 bccl 
 |-  ( ( N e. NN0 /\ ( k + 1 ) e. ZZ ) -> ( N _C ( k + 1 ) ) e. NN0 )
179 169 177 178 syl2anc 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C ( k + 1 ) ) e. NN0 )
180 179 nn0red 
 |-  ( ( k e. ( ZZ>= ` A ) /\ N e. NN0 /\ A e. NN0 ) -> ( N _C ( k + 1 ) ) e. RR )
181 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 ) ) ) )
182 173 176 180 181 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 ) ) ) )
183 182 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 ) ) ) ) )
184 168 183 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 ) ) ) ) )
185 184 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 ) ) ) ) )
186 47 185 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 ) ) ) ) )
187 186 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 ) ) ) ) ) )
188 187 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 ) ) ) ) ) )
189 13 18 23 28 34 188 uzind4 
 |-  ( B e. ( ZZ>= ` A ) -> ( ( N e. NN0 /\ A e. NN0 ) -> ( B <_ ( N / 2 ) -> ( N _C A ) <_ ( N _C B ) ) ) )
190 189 3imp 
 |-  ( ( B e. ( ZZ>= ` A ) /\ ( N e. NN0 /\ A e. NN0 ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )
191 1 2 7 8 190 syl121anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ 0 <_ A ) -> ( N _C A ) <_ ( N _C B ) )
192 simpl1 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> N e. NN0 )
193 4 adantr 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> A e. ZZ )
194 animorrl 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( A < 0 \/ N < A ) )
195 bcval4 
 |-  ( ( N e. NN0 /\ A e. ZZ /\ ( A < 0 \/ N < A ) ) -> ( N _C A ) = 0 )
196 192 193 194 195 syl3anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C A ) = 0 )
197 simpl2 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> B e. ( ZZ>= ` A ) )
198 eluzelz 
 |-  ( B e. ( ZZ>= ` A ) -> B e. ZZ )
199 197 198 syl 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> B e. ZZ )
200 bccl 
 |-  ( ( N e. NN0 /\ B e. ZZ ) -> ( N _C B ) e. NN0 )
201 192 199 200 syl2anc 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C B ) e. NN0 )
202 201 nn0ge0d 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> 0 <_ ( N _C B ) )
203 196 202 eqbrtrd 
 |-  ( ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) /\ A < 0 ) -> ( N _C A ) <_ ( N _C B ) )
204 0re 
 |-  0 e. RR
205 4 zred 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> A e. RR )
206 lelttric 
 |-  ( ( 0 e. RR /\ A e. RR ) -> ( 0 <_ A \/ A < 0 ) )
207 204 205 206 sylancr 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( 0 <_ A \/ A < 0 ) )
208 191 203 207 mpjaodan 
 |-  ( ( N e. NN0 /\ B e. ( ZZ>= ` A ) /\ B <_ ( N / 2 ) ) -> ( N _C A ) <_ ( N _C B ) )