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

Theorem bcmono 22596
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 992 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  B  e.  ( ZZ>= `  A )
)
2 simpl1 991 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  N  e.  NN0 )
3 eluzel2 10858 . . . . . 6  |-  ( B  e.  ( ZZ>= `  A
)  ->  A  e.  ZZ )
433ad2ant2 1010 . . . . 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 10651 . . . 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 993 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  B  <_  ( N  /  2
) )
9 breq1 4290 . . . . . . 7  |-  ( x  =  A  ->  (
x  <_  ( N  /  2 )  <->  A  <_  ( N  /  2 ) ) )
10 oveq2 6094 . . . . . . . 8  |-  ( x  =  A  ->  ( N  _C  x )  =  ( N  _C  A
) )
1110breq2d 4299 . . . . . . 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 4290 . . . . . . 7  |-  ( x  =  k  ->  (
x  <_  ( N  /  2 )  <->  k  <_  ( N  /  2 ) ) )
15 oveq2 6094 . . . . . . . 8  |-  ( x  =  k  ->  ( N  _C  x )  =  ( N  _C  k
) )
1615breq2d 4299 . . . . . . 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 4290 . . . . . . 7  |-  ( x  =  ( k  +  1 )  ->  (
x  <_  ( N  /  2 )  <->  ( k  +  1 )  <_ 
( N  /  2
) ) )
20 oveq2 6094 . . . . . . . 8  |-  ( x  =  ( k  +  1 )  ->  ( N  _C  x )  =  ( N  _C  (
k  +  1 ) ) )
2120breq2d 4299 . . . . . . 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 4290 . . . . . . 7  |-  ( x  =  B  ->  (
x  <_  ( N  /  2 )  <->  B  <_  ( N  /  2 ) ) )
25 oveq2 6094 . . . . . . . 8  |-  ( x  =  B  ->  ( N  _C  x )  =  ( N  _C  B
) )
2625breq2d 4299 . . . . . . 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 12090 . . . . . . . . . 10  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( N  _C  A
)  e.  NN0 )
3029nn0red 10629 . . . . . . . . 9  |-  ( ( N  e.  NN0  /\  A  e.  ZZ )  ->  ( N  _C  A
)  e.  RR )
3130leidd 9898 . . . . . . . 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 10862 . . . . . . . . . . . . 13  |-  ( k  e.  ( ZZ>= `  A
)  ->  k  e.  ZZ )
36353ad2ant1 1009 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  e.  ZZ )
3736zred 10739 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  e.  RR )
3837lep1d 10256 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  k  <_  ( k  +  1 ) )
39 peano2re 9534 . . . . . . . . . . . 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 10580 . . . . . . . . . . . . 13  |-  ( N  e.  NN0  ->  N  e.  RR )
42413ad2ant2 1010 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  N  e.  RR )
4342rehalfcld 10563 . . . . . . . . . . 11  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  /  2 )  e.  RR )
44 letr 9460 . . . . . . . . . . 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 1218 . . . . . . . . . 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 10916 . . . . . . . . . . . . 13  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A ) )  -> 
k  e.  NN0 )
49 nn0re 10580 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  k  e.  RR )
50493ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  RR )
51 nn0p1nn 10611 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  e.  NN0  ->  ( k  +  1 )  e.  NN )
52513ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  NN )
5352nnnn0d 10628 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  NN0 )
5453nn0red 10629 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  RR )
5550, 54readdcld 9405 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  e.  RR )
5654, 54readdcld 9405 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  +  ( k  +  1 ) )  e.  RR )
57413ad2ant2 1010 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  RR )
5850lep1d 10256 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  <_  ( k  +  1 ) )
5950, 54, 54, 58leadd1dd 9945 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  <_  ( (
k  +  1 )  +  ( k  +  1 ) ) )
6052nncnd 10330 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  CC )
61602timesd 10559 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 2  x.  (
k  +  1 ) )  =  ( ( k  +  1 )  +  ( k  +  1 ) ) )
62 simp3 990 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  <_  ( N  /  2 ) )
63 2re 10383 . . . . . . . . . . . . . . . . . . . . . . 23  |-  2  e.  RR
64 2pos 10405 . . . . . . . . . . . . . . . . . . . . . . 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 10204 . . . . . . . . . . . . . . . . . . . . 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 1218 . . . . . . . . . . . . . . . . . . . 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 4309 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  +  ( k  +  1 ) )  <_  N )
7155, 56, 57, 59, 70letrd 9520 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  ( k  +  1 ) )  <_  N )
7250, 54, 57leaddsub2d 9933 . . . . . . . . . . . . . . . . 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 10321 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  +  1 )  e.  NN  ->  (
k  +  1 )  e.  RR )
75 nngt0 10343 . . . . . . . . . . . . . . . . . . 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 10661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  e.  NN0  ->  N  e.  ZZ )
79783ad2ant2 1010 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  ZZ )
80 nn0z 10661 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN0  ->  k  e.  ZZ )
81803ad2ant1 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  ZZ )
8279, 81zsubcld 10744 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  ZZ )
8357rehalfcld 10563 . . . . . . . . . . . . . . . . . . . . 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 10597 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( N  e.  NN0  ->  0  <_  N )
86853ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  N )
87 1le2 10527 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  1  <_  2
8886, 87jctir 538 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( 0  <_  N  /\  1  <_  2 ) )
89 lemulge12 10184 . . . . . . . . . . . . . . . . . . . . . . 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 10197 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( N  e.  RR  /\  N  e.  RR  /\  (
2  e.  RR  /\  0  <  2 ) )  ->  ( ( N  /  2 )  <_  N 
<->  N  <_  ( 2  x.  N ) ) )
9257, 57, 66, 91syl3anc 1218 . . . . . . . . . . . . . . . . . . . . . 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 9520 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  <_  N )
95 1re 9377 . . . . . . . . . . . . . . . . . . . . . 22  |-  1  e.  RR
9695a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  e.  RR )
9750, 96, 57leaddsub2d 9933 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  <_  N  <->  1  <_  ( N  -  k ) ) )
9894, 97mpbid 210 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  <_  ( N  -  k ) )
99 elnnz1 10664 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  <->  ( ( N  -  k )  e.  ZZ  /\  1  <_ 
( N  -  k
) ) )
10082, 98, 99sylanbrc 664 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  NN )
101 nnre 10321 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  ->  ( N  -  k )  e.  RR )
102 nngt0 10343 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  k )  e.  NN  ->  0  <  ( N  -  k
) )
103101, 102jca 532 . . . . . . . . . . . . . . . . . 18  |-  ( ( N  -  k )  e.  NN  ->  (
( N  -  k
)  e.  RR  /\  0  <  ( N  -  k ) ) )
104100, 103syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( N  -  k )  e.  RR  /\  0  <  ( N  -  k ) ) )
105 faccl 12053 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
1061053ad2ant2 1010 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  N
)  e.  NN )
107 nnm1nn0 10613 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( N  -  k )  e.  NN  ->  (
( N  -  k
)  -  1 )  e.  NN0 )
108 faccl 12053 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( N  -  k
)  -  1 )  e.  NN0  ->  ( ! `
 ( ( N  -  k )  - 
1 ) )  e.  NN )
109100, 107, 1083syl 20 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
( N  -  k
)  -  1 ) )  e.  NN )
110 faccl 12053 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  e.  NN0  ->  ( ! `
 k )  e.  NN )
1111103ad2ant1 1009 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  k
)  e.  NN )
112109, 111nnmulcld 10361 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  NN )
113 nnrp 10992 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  RR+ )
114 nnrp 10992 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  NN  ->  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  RR+ )
115 rpdivcl 11005 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ! `  N
)  e.  RR+  /\  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  e.  RR+ )  ->  (
( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  e.  RR+ )
116113, 114, 115syl2an 477 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ! `  N
)  e.  NN  /\  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  NN )  ->  ( ( ! `
 N )  / 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
) )  e.  RR+ )
117106, 112, 116syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  N )  /  (
( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) ) )  e.  RR+ )
118117rpregt0d 11025 . . . . . . . . . . . . . . . . 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
) ) ) ) )
119 lediv2 10214 . . . . . . . . . . . . . . . . 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 ) ) ) )
12077, 104, 118, 119syl3anc 1218 . . . . . . . . . . . . . . . 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 ) ) ) )
12173, 120mpbid 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 ) ) )
122 facnn2 12052 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  -  k )  e.  NN  ->  ( ! `  ( N  -  k ) )  =  ( ( ! `
 ( ( N  -  k )  - 
1 ) )  x.  ( N  -  k
) ) )
123100, 122syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  ( N  -  k )
)  =  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( N  -  k ) ) )
124123oveq1d 6101 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  k
) )  x.  ( ! `  k )
)  =  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( N  -  k ) )  x.  ( ! `  k ) ) )
125109nncnd 10330 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
( N  -  k
)  -  1 ) )  e.  CC )
126111nncnd 10330 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  k
)  e.  CC )
12782zcnd 10740 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  e.  CC )
128125, 126, 127mul32d 9571 . . . . . . . . . . . . . . . . . 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 ) ) )
129124, 128eqtr4d 2473 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( N  -  k
) )  x.  ( ! `  k )
)  =  ( ( ( ! `  (
( N  -  k
)  -  1 ) )  x.  ( ! `
 k ) )  x.  ( N  -  k ) ) )
130129oveq2d 6102 . . . . . . . . . . . . . . . 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
) ) ) )
131 nn0ge0 10597 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  NN0  ->  0  <_ 
k )
1321313ad2ant1 1009 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  k )
13350, 54, 57, 58, 94letrd 9520 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  <_  N )
134 0zd 10650 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  e.  ZZ )
135 elfz 11435 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
k  e.  ( 0 ... N )  <->  ( 0  <_  k  /\  k  <_  N ) ) )
13681, 134, 79, 135syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  e.  ( 0 ... N )  <-> 
( 0  <_  k  /\  k  <_  N ) ) )
137132, 133, 136mpbir2and 913 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  ( 0 ... N ) )
138 bcval2 12073 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( 0 ... N )  ->  ( N  _C  k )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  k )
)  x.  ( ! `
 k ) ) ) )
139137, 138syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  =  ( ( ! `  N )  /  ( ( ! `
 ( N  -  k ) )  x.  ( ! `  k
) ) ) )
140106nncnd 10330 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  N
)  e.  CC )
141112nncnd 10330 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  e.  CC )
142112nnne0d 10358 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k )
)  =/=  0 )
143100nnne0d 10358 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  k
)  =/=  0 )
144140, 141, 127, 142, 143divdiv1d 10130 . . . . . . . . . . . . . . . 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
) ) ) )
145130, 139, 1443eqtr4d 2480 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  =  ( ( ( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  /  ( N  -  k ) ) )
146 nn0cn 10581 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  e.  NN0  ->  N  e.  CC )
1471463ad2ant2 1010 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  ->  N  e.  CC )
148 nn0cn 10581 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  e.  NN0  ->  k  e.  CC )
1491483ad2ant1 1009 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
k  e.  CC )
150 ax-1cn 9332 . . . . . . . . . . . . . . . . . . . . . . 23  |-  1  e.  CC
151150a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
1  e.  CC )
152147, 149, 151subsub4d 9742 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( N  -  k )  -  1 )  =  ( N  -  ( k  +  1 ) ) )
153152eqcomd 2443 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  -  (
k  +  1 ) )  =  ( ( N  -  k )  -  1 ) )
154153fveq2d 5690 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  ( N  -  ( k  +  1 ) ) )  =  ( ! `
 ( ( N  -  k )  - 
1 ) ) )
155 facp1 12048 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  e.  NN0  ->  ( ! `
 ( k  +  1 ) )  =  ( ( ! `  k )  x.  (
k  +  1 ) ) )
1561553ad2ant1 1009 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ! `  (
k  +  1 ) )  =  ( ( ! `  k )  x.  ( k  +  1 ) ) )
157154, 156oveq12d 6104 . . . . . . . . . . . . . . . . . 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 ) ) ) )
158125, 126, 60mulassd 9401 . . . . . . . . . . . . . . . . . 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 ) ) ) )
159157, 158eqtr4d 2473 . . . . . . . . . . . . . . . . 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 ) ) )
160159oveq2d 6102 . . . . . . . . . . . . . . . 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 ) ) ) )
16153nn0ge0d 10631 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
0  <_  ( k  +  1 ) )
16252nnzd 10738 . . . . . . . . . . . . . . . . . . 19  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  ZZ )
163 elfz 11435 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( k  +  1 )  e.  ZZ  /\  0  e.  ZZ  /\  N  e.  ZZ )  ->  (
( k  +  1 )  e.  ( 0 ... N )  <->  ( 0  <_  ( k  +  1 )  /\  (
k  +  1 )  <_  N ) ) )
164162, 134, 79, 163syl3anc 1218 . . . . . . . . . . . . . . . . . 18  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( ( k  +  1 )  e.  ( 0 ... N )  <-> 
( 0  <_  (
k  +  1 )  /\  ( k  +  1 )  <_  N
) ) )
165161, 94, 164mpbir2and 913 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  e.  ( 0 ... N ) )
166 bcval2 12073 . . . . . . . . . . . . . . . . 17  |-  ( ( k  +  1 )  e.  ( 0 ... N )  ->  ( N  _C  ( k  +  1 ) )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  ( k  +  1 ) ) )  x.  ( ! `
 ( k  +  1 ) ) ) ) )
167165, 166syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  (
k  +  1 ) )  =  ( ( ! `  N )  /  ( ( ! `
 ( N  -  ( k  +  1 ) ) )  x.  ( ! `  (
k  +  1 ) ) ) ) )
16852nnne0d 10358 . . . . . . . . . . . . . . . . 17  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( k  +  1 )  =/=  0 )
169140, 141, 60, 142, 168divdiv1d 10130 . . . . . . . . . . . . . . . 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 ) ) ) )
170160, 167, 1693eqtr4d 2480 . . . . . . . . . . . . . . 15  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  (
k  +  1 ) )  =  ( ( ( ! `  N
)  /  ( ( ! `  ( ( N  -  k )  -  1 ) )  x.  ( ! `  k ) ) )  /  ( k  +  1 ) ) )
171121, 145, 1703brtr4d 4317 . . . . . . . . . . . . . 14  |-  ( ( k  e.  NN0  /\  N  e.  NN0  /\  (
k  +  1 )  <_  ( N  / 
2 ) )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) )
1721713exp 1186 . . . . . . . . . . . . 13  |-  ( k  e.  NN0  ->  ( N  e.  NN0  ->  ( ( k  +  1 )  <_  ( N  / 
2 )  ->  ( N  _C  k )  <_ 
( N  _C  (
k  +  1 ) ) ) ) )
17348, 172syl 16 . . . . . . . . . . . 12  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A ) )  -> 
( N  e.  NN0  ->  ( ( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) ) )
1741733impia 1184 . . . . . . . . . . 11  |-  ( ( A  e.  NN0  /\  k  e.  ( ZZ>= `  A )  /\  N  e.  NN0 )  ->  (
( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) )
1751743coml 1194 . . . . . . . . . 10  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
( k  +  1 )  <_  ( N  /  2 )  -> 
( N  _C  k
)  <_  ( N  _C  ( k  +  1 ) ) ) )
176 simp2 989 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  N  e.  NN0 )
177 nn0z 10661 . . . . . . . . . . . . . . 15  |-  ( A  e.  NN0  ->  A  e.  ZZ )
1781773ad2ant3 1011 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  A  e.  ZZ )
179176, 178, 29syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  A )  e. 
NN0 )
180179nn0red 10629 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  A )  e.  RR )
181 bccl 12090 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  k  e.  ZZ )  ->  ( N  _C  k
)  e.  NN0 )
182176, 36, 181syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  k )  e. 
NN0 )
183182nn0red 10629 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  k )  e.  RR )
18436peano2zd 10742 . . . . . . . . . . . . . 14  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  (
k  +  1 )  e.  ZZ )
185 bccl 12090 . . . . . . . . . . . . . 14  |-  ( ( N  e.  NN0  /\  ( k  +  1 )  e.  ZZ )  ->  ( N  _C  ( k  +  1 ) )  e.  NN0 )
186176, 184, 185syl2anc 661 . . . . . . . . . . . . 13  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  ( k  +  1 ) )  e. 
NN0 )
187186nn0red 10629 . . . . . . . . . . . 12  |-  ( ( k  e.  ( ZZ>= `  A )  /\  N  e.  NN0  /\  A  e. 
NN0 )  ->  ( N  _C  ( k  +  1 ) )  e.  RR )
188 letr 9460 . . . . . . . . . . . 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 ) ) ) )
189180, 183, 187, 188syl3anc 1218 . . . . . . . . . . 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 ) ) ) )
190189expcomd 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 ) ) ) ) )
191175, 190syld 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 ) ) ) ) )
192191a2d 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 ) ) ) ) )
19347, 192syld 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 ) ) ) ) )
1941933expib 1190 . . . . . 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 ) ) ) ) ) )
195194a2d 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 ) ) ) ) ) )
19613, 18, 23, 28, 34, 195uzind4 10904 . . . 4  |-  ( B  e.  ( ZZ>= `  A
)  ->  ( ( N  e.  NN0  /\  A  e.  NN0 )  ->  ( B  <_  ( N  / 
2 )  ->  ( N  _C  A )  <_ 
( N  _C  B
) ) ) )
1971963imp 1181 . . 3  |-  ( ( B  e.  ( ZZ>= `  A )  /\  ( N  e.  NN0  /\  A  e.  NN0 )  /\  B  <_  ( N  /  2
) )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
1981, 2, 7, 8, 197syl121anc 1223 . 2  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  0  <_  A )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
199 simpl1 991 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  N  e.  NN0 )
2004adantr 465 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  A  e.  ZZ )
201 orc 385 . . . . 5  |-  ( A  <  0  ->  ( A  <  0  \/  N  <  A ) )
202201adantl 466 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( A  <  0  \/  N  <  A ) )
203 bcval4 12075 . . . 4  |-  ( ( N  e.  NN0  /\  A  e.  ZZ  /\  ( A  <  0  \/  N  <  A ) )  -> 
( N  _C  A
)  =  0 )
204199, 200, 202, 203syl3anc 1218 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  A )  =  0 )
205 simpl2 992 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  B  e.  ( ZZ>= `  A )
)
206 eluzelz 10862 . . . . . 6  |-  ( B  e.  ( ZZ>= `  A
)  ->  B  e.  ZZ )
207205, 206syl 16 . . . . 5  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  B  e.  ZZ )
208 bccl 12090 . . . . 5  |-  ( ( N  e.  NN0  /\  B  e.  ZZ )  ->  ( N  _C  B
)  e.  NN0 )
209199, 207, 208syl2anc 661 . . . 4  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  B )  e. 
NN0 )
210209nn0ge0d 10631 . . 3  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  0  <_  ( N  _C  B
) )
211204, 210eqbrtrd 4307 . 2  |-  ( ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  /\  A  <  0 )  ->  ( N  _C  A )  <_ 
( N  _C  B
) )
212 0re 9378 . . 3  |-  0  e.  RR
2134zred 10739 . . 3  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  A  e.  RR )
214 lelttric 9473 . . 3  |-  ( ( 0  e.  RR  /\  A  e.  RR )  ->  ( 0  <_  A  \/  A  <  0
) )
215212, 213, 214sylancr 663 . 2  |-  ( ( N  e.  NN0  /\  B  e.  ( ZZ>= `  A )  /\  B  <_  ( N  /  2
) )  ->  (
0  <_  A  \/  A  <  0 ) )
216198, 211, 215mpjaodan 784 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 965    = wceq 1369    e. wcel 1756   class class class wbr 4287   ` cfv 5413  (class class class)co 6086   CCcc 9272   RRcr 9273   0cc0 9274   1c1 9275    + caddc 9277    x. cmul 9279    < clt 9410    <_ cle 9411    - cmin 9587    / cdiv 9985   NNcn 10314   2c2 10363   NN0cn0 10571   ZZcz 10638   ZZ>=cuz 10853   RR+crp 10983   ...cfz 11429   !cfa 12043    _C cbc 12070
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419  ax-sep 4408  ax-nul 4416  ax-pow 4465  ax-pr 4526  ax-un 6367  ax-cnex 9330  ax-resscn 9331  ax-1cn 9332  ax-icn 9333  ax-addcl 9334  ax-addrcl 9335  ax-mulcl 9336  ax-mulrcl 9337  ax-mulcom 9338  ax-addass 9339  ax-mulass 9340  ax-distr 9341  ax-i2m1 9342  ax-1ne0 9343  ax-1rid 9344  ax-rnegex 9345  ax-rrecex 9346  ax-cnre 9347  ax-pre-lttri 9348  ax-pre-lttrn 9349  ax-pre-ltadd 9350  ax-pre-mulgt0 9351
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-nel 2604  df-ral 2715  df-rex 2716  df-reu 2717  df-rmo 2718  df-rab 2719  df-v 2969  df-sbc 3182  df-csb 3284  df-dif 3326  df-un 3328  df-in 3330  df-ss 3337  df-pss 3339  df-nul 3633  df-if 3787  df-pw 3857  df-sn 3873  df-pr 3875  df-tp 3877  df-op 3879  df-uni 4087  df-iun 4168  df-br 4288  df-opab 4346  df-mpt 4347  df-tr 4381  df-eprel 4627  df-id 4631  df-po 4636  df-so 4637  df-fr 4674  df-we 4676  df-ord 4717  df-on 4718  df-lim 4719  df-suc 4720  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5376  df-fun 5415  df-fn 5416  df-f 5417  df-f1 5418  df-fo 5419  df-f1o 5420  df-fv 5421  df-riota 6047  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-om 6472  df-1st 6572  df-2nd 6573  df-recs 6824  df-rdg 6858  df-er 7093  df-en 7303  df-dom 7304  df-sdom 7305  df-pnf 9412  df-mnf 9413  df-xr 9414  df-ltxr 9415  df-le 9416  df-sub 9589  df-neg 9590  df-div 9986  df-nn 10315  df-2 10372  df-n0 10572  df-z 10639  df-uz 10854  df-rp 10984  df-fz 11430  df-seq 11799  df-fac 12044  df-bc 12071
This theorem is referenced by:  bcmax  22597
  Copyright terms: Public domain W3C validator