MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bcmono Structured version   Unicode version

Theorem bcmono 23677
Description: The binomial coefficient is monotone in its second argument, up to the midway point. (Contributed by Mario Carneiro, 5-Mar-2014.)
Assertion
Ref Expression
bcmono  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )

Proof of Theorem bcmono
Dummy variables  x  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl2 1000 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  B  e.  ( ZZ>= `  A )
)
2 simpl1 999 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  N  e.  NN0 )
3 eluzel2 11111 . . . . . 6  |-  ( B  e.  ( ZZ>= `  A
)  ->  A  e.  ZZ )
433ad2ant2 1018 . . . . 5  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  A  e.  ZZ )
54anim1i 568 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  ( A  e.  ZZ  /\  0  <_  A ) )
6 elnn0z 10898 . . . 4  |-  ( A  e.  NN0  <->  ( A  e.  ZZ  /\  0  <_  A ) )
75, 6sylibr 212 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  A  e.  NN0 )
8 simpl3 1001 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  B  <_  ( N  /  2
) )
9 breq1 4459 . . . . . . 7  |-  ( x  =  A  ->  (
x  <_  ( N  /  2 )  <->  A  <_  ( N  /  2 ) ) )
10 oveq2 6304 . . . . . . . 8  |-  ( x  =  A  ->  ( N  _C  x )  =  ( N  _C  A
) )
1110breq2d 4468 . . . . . . 7  |-  ( x  =  A  ->  (
( N  _C  A
)  <_  ( N  _C  x )  <->  ( N  _C  A )  <_  ( N  _C  A ) ) )
129, 11imbi12d 320 . . . . . 6  |-  ( x  =  A  ->  (
( x  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  x ) )  <->  ( A  <_  ( N  /  2
)  ->  ( N  _C  A )  <_  ( N  _C  A ) ) ) )
1312imbi2d 316 . . . . 5  |-  ( 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 4459 . . . . . . 7  |-  ( x  =  k  ->  (
x  <_  ( N  /  2 )  <->  k  <_  ( N  /  2 ) ) )
15 oveq2 6304 . . . . . . . 8  |-  ( x  =  k  ->  ( N  _C  x )  =  ( N  _C  k
) )
1615breq2d 4468 . . . . . . 7  |-  ( x  =  k  ->  (
( N  _C  A
)  <_  ( N  _C  x )  <->  ( N  _C  A )  <_  ( N  _C  k ) ) )
1714, 16imbi12d 320 . . . . . 6  |-  ( x  =  k  ->  (
( x  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  x ) )  <->  ( k  <_  ( N  /  2
)  ->  ( N  _C  A )  <_  ( N  _C  k ) ) ) )
1817imbi2d 316 . . . . 5  |-  ( 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 4459 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
x  <_  ( N  /  2 )  <->  ( k  +  1 )  <_ 
( N  /  2
) ) )
20 oveq2 6304 . . . . . . . 8  |-  ( x  =  ( k  +  1 )  ->  ( N  _C  x )  =  ( N  _C  (
k  +  1 ) ) )
2120breq2d 4468 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
( N  _C  A
)  <_  ( N  _C  x )  <->  ( N  _C  A )  <_  ( N  _C  ( k  +  1 ) ) ) )
2219, 21imbi12d 320 . . . . . 6  |-  ( x  =  ( k  +  1 )  ->  (
( x  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  x ) )  <->  ( (
k  +  1 )  <_  ( N  / 
2 )  ->  ( N  _C  A )  <_ 
( N  _C  (
k  +  1 ) ) ) ) )
2322imbi2d 316 . . . . 5  |-  ( 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 4459 . . . . . . 7  |-  ( x  =  B  ->  (
x  <_  ( N  /  2 )  <->  B  <_  ( N  /  2 ) ) )
25 oveq2 6304 . . . . . . . 8  |-  ( x  =  B  ->  ( N  _C  x )  =  ( N  _C  B
) )
2625breq2d 4468 . . . . . . 7  |-  ( x  =  B  ->  (
( N  _C  A
)  <_  ( N  _C  x )  <->  ( N  _C  A )  <_  ( N  _C  B ) ) )
2724, 26imbi12d 320 . . . . . 6  |-  ( x  =  B  ->  (
( x  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  x ) )  <->  ( B  <_  ( N  /  2
)  ->  ( N  _C  A )  <_  ( N  _C  B ) ) ) )
2827imbi2d 316 . . . . 5  |-  ( 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 12402 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( N  _C  A
)  e.  NN0 )
3029nn0red 10874 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( N  _C  A
)  e.  RR )
3130leidd 10140 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( N  _C  A
)  <_  ( N  _C  A ) )
3231a1d 25 . . . . . . 7  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( A  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  A ) ) )
3332expcom 435 . . . . . 6  |-  ( A  e.  ZZ  ->  ( N  e.  NN0  ->  ( A  <_  ( N  / 
2 )  ->  ( N  _C  A )  <_ 
( N  _C  A
) ) ) )
3433adantrd 468 . . . . 5  |-  ( A  e.  ZZ  ->  (
( N  e.  NN0  /\  A  e.  NN0 )  ->  ( A  <_  ( N  /  2 )  -> 
( N  _C  A
)  <_  ( N  _C  A ) ) ) )
35 eluzelz 11115 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  A
)  ->  k  e.  ZZ )
36353ad2ant1 1017 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  e.  ZZ )
3736zred 10990 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  e.  RR )
3837lep1d 10497 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  <_  ( k  +  1 ) )
39 peano2re 9770 . . . . . . . . . . . 12  |-  ( k  e.  RR  ->  (
k  +  1 )  e.  RR )
4037, 39syl 16 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
k  +  1 )  e.  RR )
41 nn0re 10825 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  N  e.  RR )
42413ad2ant2 1018 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  N  e.  RR )
4342rehalfcld 10806 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  /  2 )  e.  RR )
44 letr 9695 . . . . . . . . . . 11  |-  ( ( k  e.  RR  /\  ( k  +  1 )  e.  RR  /\  ( N  /  2
)  e.  RR )  ->  ( ( k  <_  ( k  +  1 )  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  <_  ( N  /  2 ) ) )
4537, 40, 43, 44syl3anc 1228 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
( k  <_  (
k  +  1 )  /\  ( k  +  1 )  <_  ( N  /  2 ) )  ->  k  <_  ( N  /  2 ) ) )
4638, 45mpand 675 . . . . . . . . 9  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
( k  +  1 )  <_  ( N  /  2 )  -> 
k  <_  ( N  /  2 ) ) )
4746imim1d 75 . . . . . . . 8  |-  ( ( 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 11176 . . . . . . . . . . . . 13  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A ) )  -> 
k  e.  NN0 )
49 nn0re 10825 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  k  e.  RR )
50493ad2ant1 1017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  RR )
51 nn0p1nn 10856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  NN )
52513ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  NN )
5352nnnn0d 10873 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  NN0 )
5453nn0red 10874 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  RR )
5550, 54readdcld 9640 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  e.  RR )
5654, 54readdcld 9640 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  +  ( k  +  1 ) )  e.  RR )
57413ad2ant2 1018 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  RR )
5850lep1d 10497 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  <_  ( k  +  1 ) )
5950, 54, 54, 58leadd1dd 10187 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  <_  ( (
k  +  1 )  +  ( k  +  1 ) ) )
6052nncnd 10572 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  CC )
61602timesd 10802 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 2  x.  (
k  +  1 ) )  =  ( ( k  +  1 )  +  ( k  +  1 ) ) )
62 simp3 998 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  <_  ( N  /  2 ) )
63 2re 10626 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR
64 2pos 10648 . . . . . . . . . . . . . . . . . . . . . . 23  |-  0  <  2
6563, 64pm3.2i 455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2  e.  RR  /\  0  <  2 )
6665a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 2  e.  RR  /\  0  <  2 ) )
67 lemuldiv2 10445 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( k  +  1 )  e.  RR  /\  N  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( 2  x.  ( k  +  1 ) )  <_  N 
<->  ( k  +  1 )  <_  ( N  /  2 ) ) )
6854, 57, 66, 67syl3anc 1228 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( 2  x.  ( k  +  1 ) )  <_  N  <->  ( k  +  1 )  <_  ( N  / 
2 ) ) )
6962, 68mpbird 232 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 2  x.  (
k  +  1 ) )  <_  N )
7061, 69eqbrtrrd 4478 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  +  ( k  +  1 ) )  <_  N )
7155, 56, 57, 59, 70letrd 9756 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  <_  N )
7250, 54, 57leaddsub2d 10175 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  ( k  +  1 ) )  <_  N  <->  ( k  +  1 )  <_  ( N  -  k ) ) )
7371, 72mpbid 210 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  <_  ( N  -  k ) )
74 nnre 10563 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  +  1 )  e.  NN  ->  (
k  +  1 )  e.  RR )
75 nngt0 10585 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  +  1 )  e.  NN  ->  0  <  ( k  +  1 ) )
7674, 75jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  +  1 )  e.  NN  ->  (
( k  +  1 )  e.  RR  /\  0  <  ( k  +  1 ) ) )
7752, 76syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  e.  RR  /\  0  <  ( k  +  1 ) ) )
78 nn0z 10908 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  N  e.  ZZ )
79783ad2ant2 1018 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  ZZ )
80 nn0z 10908 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN0  ->  k  e.  ZZ )
81803ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  ZZ )
8279, 81zsubcld 10995 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  ZZ )
8357rehalfcld 10806 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  /  2
)  e.  RR )
8457, 63jctir 538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  e.  RR  /\  2  e.  RR ) )
85 nn0ge0 10842 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN0  ->  0  <_  N )
86853ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  N )
87 1le2 10770 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  <_  2
8886, 87jctir 538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 0  <_  N  /\  1  <_  2 ) )
89 lemulge12 10426 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( N  e.  RR  /\  2  e.  RR )  /\  ( 0  <_  N  /\  1  <_  2
) )  ->  N  <_  ( 2  x.  N
) )
9084, 88, 89syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  <_  ( 2  x.  N ) )
91 ledivmul 10439 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  RR  /\  N  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( N  /  2 )  <_  N 
<->  N  <_  ( 2  x.  N ) ) )
9257, 57, 66, 91syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( N  / 
2 )  <_  N  <->  N  <_  ( 2  x.  N ) ) )
9390, 92mpbird 232 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  /  2
)  <_  N )
9454, 83, 57, 62, 93letrd 9756 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  <_  N )
95 1red 9628 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  e.  RR )
9650, 95, 57leaddsub2d 10175 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  <_  N  <->  1  <_  ( N  -  k ) ) )
9794, 96mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  <_  ( N  -  k ) )
98 elnnz1 10911 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  <->  ( ( N  -  k )  e.  ZZ  /\  1  <_ 
( N  -  k
) ) )
9982, 97, 98sylanbrc 664 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  NN )
100 nnre 10563 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  ->  ( N  -  k )  e.  RR )
101 nngt0 10585 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  ->  0  <  ( N  -  k
) )
102100, 101jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  -  k )  e.  NN  ->  (
( N  -  k
)  e.  RR  /\  0  <  ( N  -  k ) ) )
10399, 102syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( N  -  k )  e.  RR  /\  0  <  ( N  -  k ) ) )
104 faccl 12365 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
1051043ad2ant2 1018 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  N
)  e.  NN )
106 nnm1nn0 10858 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  k )  e.  NN  ->  (
( N  -  k
)  -  1 )  e.  NN0 )
107 faccl 12365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  -  k
)  -  1 )  e.  NN0  ->  ( ! `
 ( ( N  -  k )  - 
1 ) )  e.  NN )
10899, 106, 1073syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
( N  -  k
)  -  1 ) )  e.  NN )
109 faccl 12365 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
1101093ad2ant1 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  k
)  e.  NN )
111108, 110nnmulcld 10604 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  NN )
112 nnrp 11254 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  RR+ )
113 nnrp 11254 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  NN  ->  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  RR+ )
114 rpdivcl 11267 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ! `  N
)  e.  RR+  /\  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  RR+ )  ->  (
( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  e.  RR+ )
115112, 113, 114syl2an 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ! `  N
)  e.  NN  /\  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  NN )  ->  ( ( ! `
 N )  / 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
) )  e.  RR+ )
116105, 111, 115syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  N )  /  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) ) )  e.  RR+ )
117116rpregt0d 11287 . . . . . . . . . . . . . . . . 17  |-  ( ( 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
) ) ) ) )
118 lediv2 10455 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 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 ) ) ) )
11977, 103, 117, 118syl3anc 1228 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
12073, 119mpbid 210 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
121 facnn2 12364 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  -  k )  e.  NN  ->  ( ! `  ( N  -  k ) )  =  ( ( ! `
 ( ( N  -  k )  - 
1 ) )  x.  ( N  -  k
) ) )
12299, 121syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  ( N  -  k )
)  =  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( N  -  k ) ) )
123122oveq1d 6311 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  k
) )  x.  ( ! `  k )
)  =  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( N  -  k ) )  x.  ( ! `  k ) ) )
124108nncnd 10572 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
( N  -  k
)  -  1 ) )  e.  CC )
125110nncnd 10572 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  k
)  e.  CC )
12682zcnd 10991 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  CC )
127124, 125, 126mul32d 9807 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) )
128123, 127eqtr4d 2501 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  k
) )  x.  ( ! `  k )
)  =  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  x.  ( N  -  k ) ) )
129128oveq2d 6312 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  N )  /  (
( ! `  ( N  -  k )
)  x.  ( ! `
 k ) ) )  =  ( ( ! `  N )  /  ( ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) )  x.  ( N  -  k
) ) ) )
130 nn0ge0 10842 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN0  ->  0  <_ 
k )
1311303ad2ant1 1017 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  k )
13250, 54, 57, 58, 94letrd 9756 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  <_  N )
133 0zd 10897 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  e.  ZZ )
134 elfz 11703 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
k  e.  ( 0 ... N )  <->  ( 0  <_  k  /\  k  <_  N ) ) )
13581, 133, 79, 134syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  e.  ( 0 ... N )  <-> 
( 0  <_  k  /\  k  <_  N ) ) )
136131, 132, 135mpbir2and 922 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  ( 0 ... N ) )
137 bcval2 12385 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... N )  ->  ( N  _C  k )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  k )
)  x.  ( ! `
 k ) ) ) )
138136, 137syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  =  ( ( ! `  N )  /  ( ( ! `
 ( N  -  k ) )  x.  ( ! `  k
) ) ) )
139105nncnd 10572 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  N
)  e.  CC )
140111nncnd 10572 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  CC )
141111nnne0d 10601 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  =/=  0 )
14299nnne0d 10601 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  =/=  0 )
143139, 140, 126, 141, 142divdiv1d 10372 . . . . . . . . . . . . . . . 16  |-  ( ( 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
) ) ) )
144129, 138, 1433eqtr4d 2508 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  =  ( ( ( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  /  ( N  -  k ) ) )
145 nn0cn 10826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN0  ->  N  e.  CC )
1461453ad2ant2 1018 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  CC )
147 nn0cn 10826 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN0  ->  k  e.  CC )
1481473ad2ant1 1017 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  CC )
149 1cnd 9629 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  e.  CC )
150146, 148, 149subsub4d 9981 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( N  -  k )  -  1 )  =  ( N  -  ( k  +  1 ) ) )
151150eqcomd 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  (
k  +  1 ) )  =  ( ( N  -  k )  -  1 ) )
152151fveq2d 5876 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  ( N  -  ( k  +  1 ) ) )  =  ( ! `
 ( ( N  -  k )  - 
1 ) ) )
153 facp1 12360 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  ( ! `
 ( k  +  1 ) )  =  ( ( ! `  k )  x.  (
k  +  1 ) ) )
1541533ad2ant1 1017 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
k  +  1 ) )  =  ( ( ! `  k )  x.  ( k  +  1 ) ) )
155152, 154oveq12d 6314 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  (
k  +  1 ) ) )  x.  ( ! `  ( k  +  1 ) ) )  =  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ( ! `
 k )  x.  ( k  +  1 ) ) ) )
156124, 125, 60mulassd 9636 . . . . . . . . . . . . . . . . . 18  |-  ( ( 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 ) ) ) )
157155, 156eqtr4d 2501 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  (
k  +  1 ) ) )  x.  ( ! `  ( k  +  1 ) ) )  =  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  x.  ( k  +  1 ) ) )
158157oveq2d 6312 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
15953nn0ge0d 10876 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  ( k  +  1 ) )
16052nnzd 10989 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  ZZ )
161 elfz 11703 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  +  1 )  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  +  1 )  e.  ( 0 ... N )  <->  ( 0  <_  ( k  +  1 )  /\  (
k  +  1 )  <_  N ) ) )
162160, 133, 79, 161syl3anc 1228 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  e.  ( 0 ... N )  <-> 
( 0  <_  (
k  +  1 )  /\  ( k  +  1 )  <_  N
) ) )
163159, 94, 162mpbir2and 922 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  ( 0 ... N ) )
164 bcval2 12385 . . . . . . . . . . . . . . . . 17  |-  ( ( k  +  1 )  e.  ( 0 ... N )  ->  ( N  _C  ( k  +  1 ) )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  ( k  +  1 ) ) )  x.  ( ! `
 ( k  +  1 ) ) ) ) )
165163, 164syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  (
k  +  1 ) )  =  ( ( ! `  N )  /  ( ( ! `
 ( N  -  ( k  +  1 ) ) )  x.  ( ! `  (
k  +  1 ) ) ) ) )
16652nnne0d 10601 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  =/=  0 )
167139, 140, 60, 141, 166divdiv1d 10372 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) ) ) )
168158, 165, 1673eqtr4d 2508 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  (
k  +  1 ) )  =  ( ( ( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  /  ( k  +  1 ) ) )
169120, 144, 1683brtr4d 4486 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) )
1701693exp 1195 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( N  e.  NN0  ->  ( ( k  +  1 )  <_  ( N  / 
2 )  ->  ( N  _C  k )  <_ 
( N  _C  (
k  +  1 ) ) ) ) )
17148, 170syl 16 . . . . . . . . . . . 12  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A ) )  -> 
( N  e.  NN0  ->  ( ( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) ) )
1721713impia 1193 . . . . . . . . . . 11  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A )  /\  N  e.  NN0 )  ->  (
( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) )
1731723coml 1203 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) )
174 simp2 997 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  N  e.  NN0 )
175 nn0z 10908 . . . . . . . . . . . . . . 15  |-  ( A  e.  NN0  ->  A  e.  ZZ )
1761753ad2ant3 1019 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  A  e.  ZZ )
177174, 176, 29syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  A )  e. 
NN0 )
178177nn0red 10874 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  A )  e.  RR )
179 bccl 12402 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  k  e.  ZZ )  ->  ( N  _C  k
)  e.  NN0 )
180174, 36, 179syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  k )  e. 
NN0 )
181180nn0red 10874 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  k )  e.  RR )
18236peano2zd 10993 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
k  +  1 )  e.  ZZ )
183 bccl 12402 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( k  +  1 )  e.  ZZ )  ->  ( N  _C  ( k  +  1 ) )  e.  NN0 )
184174, 182, 183syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  ( k  +  1 ) )  e. 
NN0 )
185184nn0red 10874 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  ( k  +  1 ) )  e.  RR )
186 letr 9695 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) ) )
187178, 181, 185, 186syl3anc 1228 . . . . . . . . . . 11  |-  ( ( 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 ) ) ) )
188187expcomd 438 . . . . . . . . . 10  |-  ( ( 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 ) ) ) ) )
189173, 188syld 44 . . . . . . . . 9  |-  ( ( 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 ) ) ) ) )
190189a2d 26 . . . . . . . 8  |-  ( ( 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 ) ) ) ) )
19147, 190syld 44 . . . . . . 7  |-  ( ( 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 ) ) ) ) )
1921913expib 1199 . . . . . 6  |-  ( 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 ) ) ) ) ) )
193192a2d 26 . . . . 5  |-  ( 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 ) ) ) ) ) )
19413, 18, 23, 28, 34, 193uzind4 11164 . . . 4  |-  ( B  e.  ( ZZ>= `  A
)  ->  ( ( N  e.  NN0  /\  A  e.  NN0 )  ->  ( B  <_  ( N  / 
2 )  ->  ( N  _C  A )  <_ 
( N  _C  B
) ) ) )
1951943imp 1190 . . 3  |-  ( ( B  e.  ( ZZ>= `  A )  /\  ( N  e.  NN0  /\  A  e.  NN0 )  /\  B  <_  ( N  /  2
) )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
1961, 2, 7, 8, 195syl121anc 1233 . 2  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
197 simpl1 999 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  N  e.  NN0 )
1984adantr 465 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  A  e.  ZZ )
199 orc 385 . . . . 5  |-  ( A  <  0  ->  ( A  <  0  \/  N  <  A ) )
200199adantl 466 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( A  <  0  \/  N  <  A ) )
201 bcval4 12387 . . . 4  |-  ( ( N  e.  NN0  /\  A  e.  ZZ  /\  ( A  <  0  \/  N  <  A ) )  -> 
( N  _C  A
)  =  0 )
202197, 198, 200, 201syl3anc 1228 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  A )  =  0 )
203 simpl2 1000 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  B  e.  ( ZZ>= `  A )
)
204 eluzelz 11115 . . . . . 6  |-  ( B  e.  ( ZZ>= `  A
)  ->  B  e.  ZZ )
205203, 204syl 16 . . . . 5  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  B  e.  ZZ )
206 bccl 12402 . . . . 5  |-  ( ( N  e.  NN0  /\  B  e.  ZZ )  ->  ( N  _C  B
)  e.  NN0 )
207197, 205, 206syl2anc 661 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  B )  e. 
NN0 )
208207nn0ge0d 10876 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  0  <_  ( N  _C  B
) )
209202, 208eqbrtrd 4476 . 2  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
210 0re 9613 . . 3  |-  0  e.  RR
2114zred 10990 . . 3  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  A  e.  RR )
212 lelttric 9708 . . 3  |-  ( ( 0  e.  RR  /\  A  e.  RR )  ->  ( 0  <_  A  \/  A  <  0
) )
213210, 211, 212sylancr 663 . 2  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  (
0  <_  A  \/  A  <  0 ) )
214196, 209, 213mpjaodan 786 1  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 973    = wceq 1395    e. wcel 1819   class class class wbr 4456   ` cfv 5594  (class class class)co 6296   CCcc 9507   RRcr 9508   0cc0 9509   1c1 9510    + caddc 9512    x. cmul 9514    < clt 9645    <_ cle 9646    - cmin 9824    / cdiv 10227   NNcn 10556   2c2 10606   NN0cn0 10816   ZZcz 10885   ZZ>=cuz 11106   RR+crp 11245   ...cfz 11697   !cfa 12355    _C cbc 12382
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591  ax-cnex 9565  ax-resscn 9566  ax-1cn 9567  ax-icn 9568  ax-addcl 9569  ax-addrcl 9570  ax-mulcl 9571  ax-mulrcl 9572  ax-mulcom 9573  ax-addass 9574  ax-mulass 9575  ax-distr 9576  ax-i2m1 9577  ax-1ne0 9578  ax-1rid 9579  ax-rnegex 9580  ax-rrecex 9581  ax-cnre 9582  ax-pre-lttri 9583  ax-pre-lttrn 9584  ax-pre-ltadd 9585  ax-pre-mulgt0 9586
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-nel 2655  df-ral 2812  df-rex 2813  df-reu 2814  df-rmo 2815  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-tp 4037  df-op 4039  df-uni 4252  df-iun 4334  df-br 4457  df-opab 4516  df-mpt 4517  df-tr 4551  df-eprel 4800  df-id 4804  df-po 4809  df-so 4810  df-fr 4847  df-we 4849  df-ord 4890  df-on 4891  df-lim 4892  df-suc 4893  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-f1 5599  df-fo 5600  df-f1o 5601  df-fv 5602  df-riota 6258  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6700  df-1st 6799  df-2nd 6800  df-recs 7060  df-rdg 7094  df-er 7329  df-en 7536  df-dom 7537  df-sdom 7538  df-pnf 9647  df-mnf 9648  df-xr 9649  df-ltxr 9650  df-le 9651  df-sub 9826  df-neg 9827  df-div 10228  df-nn 10557  df-2 10615  df-n0 10817  df-z 10886  df-uz 11107  df-rp 11246  df-fz 11698  df-seq 12110  df-fac 12356  df-bc 12383
This theorem is referenced by:  bcmax  23678
  Copyright terms: Public domain W3C validator