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

Theorem bcval5 12094
Description: Write out the top and bottom parts of the binomial coefficient  ( N  _C  K )  =  ( N  x.  ( N  -  1 )  x. 
...  x.  ( ( N  -  K )  +  1 ) )  /  K ! explicitly. In this form, it is valid even for  N  <  K, although it is no longer valid for nonpositive  K. (Contributed by Mario Carneiro, 22-May-2014.)
Assertion
Ref Expression
bcval5  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( N  _C  K
)  =  ( (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
) )

Proof of Theorem bcval5
Dummy variables  x  k  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 bcval2 12081 . . . 4  |-  ( K  e.  ( 0 ... N )  ->  ( N  _C  K )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  K )
)  x.  ( ! `
 K ) ) ) )
21adantl 466 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  ( ( ! `  N
)  /  ( ( ! `  ( N  -  K ) )  x.  ( ! `  K ) ) ) )
3 mulcl 9366 . . . . . . . . 9  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
43adantl 466 . . . . . . . 8  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  ( N  -  K
)  e.  NN ) )  /\  ( k  e.  CC  /\  x  e.  CC ) )  -> 
( k  x.  x
)  e.  CC )
5 mulass 9370 . . . . . . . . 9  |-  ( ( k  e.  CC  /\  x  e.  CC  /\  y  e.  CC )  ->  (
( k  x.  x
)  x.  y )  =  ( k  x.  ( x  x.  y
) ) )
65adantl 466 . . . . . . . 8  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  ( N  -  K
)  e.  NN ) )  /\  ( k  e.  CC  /\  x  e.  CC  /\  y  e.  CC ) )  -> 
( ( k  x.  x )  x.  y
)  =  ( k  x.  ( x  x.  y ) ) )
7 simplr 754 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  K  e.  NN )
8 elfzuz3 11450 . . . . . . . . . . . . . 14  |-  ( K  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  K )
)
98adantl 466 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ( ZZ>= `  K )
)
10 eluznn 10925 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN  /\  N  e.  ( ZZ>= `  K ) )  ->  N  e.  NN )
117, 9, 10syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  NN )
1211adantrr 716 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  NN )
13 simplr 754 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  K  e.  NN )
14 nnre 10329 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  RR )
15 nnrp 11000 . . . . . . . . . . . 12  |-  ( K  e.  NN  ->  K  e.  RR+ )
16 ltsubrp 11022 . . . . . . . . . . . 12  |-  ( ( N  e.  RR  /\  K  e.  RR+ )  -> 
( N  -  K
)  <  N )
1714, 15, 16syl2an 477 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  K  e.  NN )  ->  ( N  -  K
)  <  N )
1812, 13, 17syl2anc 661 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  <  N )
1912nnzd 10746 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  ZZ )
20 nnz 10668 . . . . . . . . . . . . 13  |-  ( K  e.  NN  ->  K  e.  ZZ )
2120ad2antlr 726 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  K  e.  ZZ )
2219, 21zsubcld 10752 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  ZZ )
23 zltp1le 10694 . . . . . . . . . . 11  |-  ( ( ( N  -  K
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( N  -  K )  <  N  <->  ( ( N  -  K
)  +  1 )  <_  N ) )
2422, 19, 23syl2anc 661 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  <  N  <->  ( ( N  -  K )  +  1 )  <_  N ) )
2518, 24mpbid 210 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  +  1 )  <_  N )
2622peano2zd 10750 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  +  1 )  e.  ZZ )
27 eluz 10874 . . . . . . . . . 10  |-  ( ( ( ( N  -  K )  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( ( N  -  K )  +  1 ) )  <->  ( ( N  -  K )  +  1 )  <_  N ) )
2826, 19, 27syl2anc 661 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) )  <->  ( ( N  -  K )  +  1 )  <_  N ) )
2925, 28mpbird 232 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )
30 simprr 756 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  NN )
31 nnuz 10896 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
3230, 31syl6eleq 2533 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  ( ZZ>= `  1 )
)
33 fvi 5748 . . . . . . . . . 10  |-  ( k  e.  ( 1 ... N )  ->  (  _I  `  k )  =  k )
34 elfzelz 11453 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  k  e.  ZZ )
3534zcnd 10748 . . . . . . . . . 10  |-  ( k  e.  ( 1 ... N )  ->  k  e.  CC )
3633, 35eqeltrd 2517 . . . . . . . . 9  |-  ( k  e.  ( 1 ... N )  ->  (  _I  `  k )  e.  CC )
3736adantl 466 . . . . . . . 8  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N )  /\  ( N  -  K
)  e.  NN ) )  /\  k  e.  ( 1 ... N
) )  ->  (  _I  `  k )  e.  CC )
384, 6, 29, 32, 37seqsplit 11839 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (  seq 1 (  x.  ,  _I  ) `  N )  =  ( (  seq 1 (  x.  ,  _I  ) `  ( N  -  K ) )  x.  (  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) `  N )
) )
39 facnn 12053 . . . . . . . 8  |-  ( N  e.  NN  ->  ( ! `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
4012, 39syl 16 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( ! `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
41 facnn 12053 . . . . . . . . 9  |-  ( ( N  -  K )  e.  NN  ->  ( ! `  ( N  -  K ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( N  -  K
) ) )
4230, 41syl 16 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( ! `  ( N  -  K ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( N  -  K
) ) )
4342oveq1d 6106 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) )  =  ( (  seq 1 (  x.  ,  _I  ) `  ( N  -  K
) )  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) )
4438, 40, 433eqtr4d 2485 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( ! `  N )  =  ( ( ! `
 ( N  -  K ) )  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) )
4544expr 615 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  e.  NN  ->  ( ! `  N )  =  ( ( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) ) )
46 simpll 753 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  NN0 )
47 faccl 12061 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
48 nncn 10330 . . . . . . . . 9  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  CC )
4946, 47, 483syl 20 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  e.  CC )
5049mulid2d 9404 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( 1  x.  ( ! `  N ) )  =  ( ! `  N
) )
5111, 39syl 16 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  (  seq 1 (  x.  ,  _I  ) `  N ) )
5251oveq2d 6107 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( 1  x.  ( ! `  N ) )  =  ( 1  x.  (  seq 1 (  x.  ,  _I  ) `  N ) ) )
5350, 52eqtr3d 2477 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  ( 1  x.  (  seq 1 (  x.  ,  _I  ) `  N ) ) )
54 fveq2 5691 . . . . . . . . 9  |-  ( ( N  -  K )  =  0  ->  ( ! `  ( N  -  K ) )  =  ( ! `  0
) )
55 fac0 12054 . . . . . . . . 9  |-  ( ! `
 0 )  =  1
5654, 55syl6eq 2491 . . . . . . . 8  |-  ( ( N  -  K )  =  0  ->  ( ! `  ( N  -  K ) )  =  1 )
57 oveq1 6098 . . . . . . . . . . 11  |-  ( ( N  -  K )  =  0  ->  (
( N  -  K
)  +  1 )  =  ( 0  +  1 ) )
58 0p1e1 10433 . . . . . . . . . . 11  |-  ( 0  +  1 )  =  1
5957, 58syl6eq 2491 . . . . . . . . . 10  |-  ( ( N  -  K )  =  0  ->  (
( N  -  K
)  +  1 )  =  1 )
6059seqeq1d 11812 . . . . . . . . 9  |-  ( ( N  -  K )  =  0  ->  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  )  =  seq 1 (  x.  ,  _I  ) )
6160fveq1d 5693 . . . . . . . 8  |-  ( ( N  -  K )  =  0  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
6256, 61oveq12d 6109 . . . . . . 7  |-  ( ( N  -  K )  =  0  ->  (
( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) )  =  ( 1  x.  (  seq 1
(  x.  ,  _I  ) `  N )
) )
6362eqeq2d 2454 . . . . . 6  |-  ( ( N  -  K )  =  0  ->  (
( ! `  N
)  =  ( ( ! `  ( N  -  K ) )  x.  (  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) `  N )
)  <->  ( ! `  N )  =  ( 1  x.  (  seq 1 (  x.  ,  _I  ) `  N ) ) ) )
6453, 63syl5ibrcom 222 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  =  0  ->  ( ! `  N )  =  ( ( ! `
 ( N  -  K ) )  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) ) )
65 fznn0sub 11487 . . . . . . 7  |-  ( K  e.  ( 0 ... N )  ->  ( N  -  K )  e.  NN0 )
6665adantl 466 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  e.  NN0 )
67 elnn0 10581 . . . . . 6  |-  ( ( N  -  K )  e.  NN0  <->  ( ( N  -  K )  e.  NN  \/  ( N  -  K )  =  0 ) )
6866, 67sylib 196 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  e.  NN  \/  ( N  -  K )  =  0 ) )
6945, 64, 68mpjaod 381 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  ( ( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) )
7069oveq1d 6106 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( ! `  N )  /  ( ( ! `
 ( N  -  K ) )  x.  ( ! `  K
) ) )  =  ( ( ( ! `
 ( N  -  K ) )  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) )  / 
( ( ! `  ( N  -  K
) )  x.  ( ! `  K )
) ) )
71 eqid 2443 . . . . . 6  |-  ( ZZ>= `  ( ( N  -  K )  +  1 ) )  =  (
ZZ>= `  ( ( N  -  K )  +  1 ) )
72 nn0z 10669 . . . . . . . . 9  |-  ( N  e.  NN0  ->  N  e.  ZZ )
73 zsubcl 10687 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  K  e.  ZZ )  ->  ( N  -  K
)  e.  ZZ )
7472, 20, 73syl2an 477 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( N  -  K
)  e.  ZZ )
7574peano2zd 10750 . . . . . . 7  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( ( N  -  K )  +  1 )  e.  ZZ )
7675adantr 465 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  +  1 )  e.  ZZ )
77 fvi 5748 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  (  _I  `  k )  =  k )
78 eluzelz 10870 . . . . . . . . 9  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  k  e.  ZZ )
7978zcnd 10748 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  k  e.  CC )
8077, 79eqeltrd 2517 . . . . . . 7  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  (  _I  `  k )  e.  CC )
8180adantl 466 . . . . . 6  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N
) )  /\  k  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )  ->  (  _I  `  k )  e.  CC )
823adantl 466 . . . . . 6  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N
) )  /\  (
k  e.  CC  /\  x  e.  CC )
)  ->  ( k  x.  x )  e.  CC )
8371, 76, 81, 82seqf 11827 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) : ( ZZ>= `  (
( N  -  K
)  +  1 ) ) --> CC )
8411, 7, 17syl2anc 661 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  <  N
)
8574adantr 465 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  e.  ZZ )
8611nnzd 10746 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ZZ )
8785, 86, 23syl2anc 661 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  <  N  <->  ( ( N  -  K )  +  1 )  <_  N
) )
8884, 87mpbid 210 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  +  1 )  <_  N )
8976, 86, 27syl2anc 661 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) )  <-> 
( ( N  -  K )  +  1 )  <_  N )
)
9088, 89mpbird 232 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )
9183, 90ffvelrnd 5844 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  e.  CC )
92 elfznn0 11481 . . . . . . 7  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
9392adantl 466 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  K  e.  NN0 )
94 faccl 12061 . . . . . 6  |-  ( K  e.  NN0  ->  ( ! `
 K )  e.  NN )
9593, 94syl 16 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  e.  NN )
9695nncnd 10338 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  e.  CC )
97 faccl 12061 . . . . . 6  |-  ( ( N  -  K )  e.  NN0  ->  ( ! `
 ( N  -  K ) )  e.  NN )
9866, 97syl 16 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  e.  NN )
9998nncnd 10338 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  e.  CC )
10095nnne0d 10366 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  =/=  0
)
10198nnne0d 10366 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  =/=  0
)
10291, 96, 99, 100, 101divcan5d 10133 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( (
( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) )  /  ( ( ! `  ( N  -  K ) )  x.  ( ! `  K ) ) )  =  ( (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K ) ) )
1032, 70, 1023eqtrd 2479 . 2  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  ( (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
) )
104 nnnn0 10586 . . . . 5  |-  ( K  e.  NN  ->  K  e.  NN0 )
105104ad2antlr 726 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  NN0 )
106 nncn 10330 . . . . 5  |-  ( ( ! `  K )  e.  NN  ->  ( ! `  K )  e.  CC )
107 nnne0 10354 . . . . 5  |-  ( ( ! `  K )  e.  NN  ->  ( ! `  K )  =/=  0 )
108106, 107div0d 10106 . . . 4  |-  ( ( ! `  K )  e.  NN  ->  (
0  /  ( ! `
 K ) )  =  0 )
109105, 94, 1083syl 20 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  /  ( ! `
 K ) )  =  0 )
1103adantl 466 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  (
k  e.  CC  /\  x  e.  CC )
)  ->  ( k  x.  x )  e.  CC )
111 fvi 5748 . . . . . . 7  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  (  _I  `  k )  =  k )
112 elfzelz 11453 . . . . . . . 8  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  k  e.  ZZ )
113112zcnd 10748 . . . . . . 7  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  k  e.  CC )
114111, 113eqeltrd 2517 . . . . . 6  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  (  _I  `  k )  e.  CC )
115114adantl 466 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  ( ( ( N  -  K )  +  1 ) ... N
) )  ->  (  _I  `  k )  e.  CC )
116 mul02 9547 . . . . . 6  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
117116adantl 466 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  CC )  ->  (
0  x.  k )  =  0 )
118 mul01 9548 . . . . . 6  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
119118adantl 466 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  CC )  ->  (
k  x.  0 )  =  0 )
120 simpr 461 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  -.  K  e.  ( 0 ... N ) )
121 nn0uz 10895 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
122105, 121syl6eleq 2533 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  ( ZZ>= `  0 )
)
12372ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  ZZ )
124 elfz5 11445 . . . . . . . . . . 11  |-  ( ( K  e.  ( ZZ>= ` 
0 )  /\  N  e.  ZZ )  ->  ( K  e.  ( 0 ... N )  <->  K  <_  N ) )
125122, 123, 124syl2anc 661 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( K  e.  ( 0 ... N )  <->  K  <_  N ) )
126 nn0re 10588 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  N  e.  RR )
127126ad2antrr 725 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  RR )
128 nnre 10329 . . . . . . . . . . . 12  |-  ( K  e.  NN  ->  K  e.  RR )
129128ad2antlr 726 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  RR )
130127, 129subge0d 9929 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  <_  ( N  -  K )  <->  K  <_  N ) )
131125, 130bitr4d 256 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( K  e.  ( 0 ... N )  <->  0  <_  ( N  -  K ) ) )
132120, 131mtbid 300 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  -.  0  <_  ( N  -  K ) )
13374adantr 465 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  e.  ZZ )
134133zred 10747 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  e.  RR )
135 0re 9386 . . . . . . . . 9  |-  0  e.  RR
136 ltnle 9454 . . . . . . . . 9  |-  ( ( ( N  -  K
)  e.  RR  /\  0  e.  RR )  ->  ( ( N  -  K )  <  0  <->  -.  0  <_  ( N  -  K ) ) )
137134, 135, 136sylancl 662 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  <  0  <->  -.  0  <_  ( N  -  K
) ) )
138132, 137mpbird 232 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  <  0 )
139 0z 10657 . . . . . . . 8  |-  0  e.  ZZ
140 zltp1le 10694 . . . . . . . 8  |-  ( ( ( N  -  K
)  e.  ZZ  /\  0  e.  ZZ )  ->  ( ( N  -  K )  <  0  <->  ( ( N  -  K
)  +  1 )  <_  0 ) )
141133, 139, 140sylancl 662 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  <  0  <->  ( ( N  -  K )  +  1 )  <_ 
0 ) )
142138, 141mpbid 210 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  +  1 )  <_  0 )
143 nn0ge0 10605 . . . . . . 7  |-  ( N  e.  NN0  ->  0  <_  N )
144143ad2antrr 725 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  <_  N )
145 0zd 10658 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  e.  ZZ )
14675adantr 465 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  +  1 )  e.  ZZ )
147 elfz 11443 . . . . . . 7  |-  ( ( 0  e.  ZZ  /\  ( ( N  -  K )  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( 0  e.  ( ( ( N  -  K )  +  1 ) ... N )  <-> 
( ( ( N  -  K )  +  1 )  <_  0  /\  0  <_  N ) ) )
148145, 146, 123, 147syl3anc 1218 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  e.  ( ( ( N  -  K
)  +  1 ) ... N )  <->  ( (
( N  -  K
)  +  1 )  <_  0  /\  0  <_  N ) ) )
149142, 144, 148mpbir2and 913 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  e.  ( ( ( N  -  K )  +  1 ) ... N
) )
150 simpll 753 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  NN0 )
151 0cn 9378 . . . . . 6  |-  0  e.  CC
152 fvi 5748 . . . . . 6  |-  ( 0  e.  CC  ->  (  _I  `  0 )  =  0 )
153151, 152mp1i 12 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (  _I  `  0 )  =  0 )
154110, 115, 117, 119, 149, 150, 153seqz 11854 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  =  0 )
155154oveq1d 6106 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
(  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
)  =  ( 0  /  ( ! `  K ) ) )
156 bcval3 12082 . . . . 5  |-  ( ( N  e.  NN0  /\  K  e.  ZZ  /\  -.  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  0 )
15720, 156syl3an2 1252 . . . 4  |-  ( ( N  e.  NN0  /\  K  e.  NN  /\  -.  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  0 )
1581573expa 1187 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  _C  K )  =  0 )
159109, 155, 1583eqtr4rd 2486 . 2  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  _C  K )  =  ( (  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K ) ) )
160103, 159pm2.61dan 789 1  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( N  _C  K
)  =  ( (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 965    = wceq 1369    e. wcel 1756   class class class wbr 4292    _I cid 4631   ` cfv 5418  (class class class)co 6091   CCcc 9280   RRcr 9281   0cc0 9282   1c1 9283    + caddc 9285    x. cmul 9287    < clt 9418    <_ cle 9419    - cmin 9595    / cdiv 9993   NNcn 10322   NN0cn0 10579   ZZcz 10646   ZZ>=cuz 10861   RR+crp 10991   ...cfz 11437    seqcseq 11806   !cfa 12051    _C cbc 12078
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 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372  ax-cnex 9338  ax-resscn 9339  ax-1cn 9340  ax-icn 9341  ax-addcl 9342  ax-addrcl 9343  ax-mulcl 9344  ax-mulrcl 9345  ax-mulcom 9346  ax-addass 9347  ax-mulass 9348  ax-distr 9349  ax-i2m1 9350  ax-1ne0 9351  ax-1rid 9352  ax-rnegex 9353  ax-rrecex 9354  ax-cnre 9355  ax-pre-lttri 9356  ax-pre-lttrn 9357  ax-pre-ltadd 9358  ax-pre-mulgt0 9359
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 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-nel 2609  df-ral 2720  df-rex 2721  df-reu 2722  df-rmo 2723  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-riota 6052  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-er 7101  df-en 7311  df-dom 7312  df-sdom 7313  df-pnf 9420  df-mnf 9421  df-xr 9422  df-ltxr 9423  df-le 9424  df-sub 9597  df-neg 9598  df-div 9994  df-nn 10323  df-n0 10580  df-z 10647  df-uz 10862  df-rp 10992  df-fz 11438  df-seq 11807  df-fac 12052  df-bc 12079
This theorem is referenced by:  bcn2  12095
  Copyright terms: Public domain W3C validator