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

Theorem bcval5 12500
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 12487 . . . 4  |-  ( K  e.  ( 0 ... N )  ->  ( N  _C  K )  =  ( ( ! `  N )  /  (
( ! `  ( N  -  K )
)  x.  ( ! `
 K ) ) ) )
21adantl 468 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  ( ( ! `  N
)  /  ( ( ! `  ( N  -  K ) )  x.  ( ! `  K ) ) ) )
3 mulcl 9620 . . . . . . . . 9  |-  ( ( k  e.  CC  /\  x  e.  CC )  ->  ( k  x.  x
)  e.  CC )
43adantl 468 . . . . . . . 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 9624 . . . . . . . . 9  |-  ( ( k  e.  CC  /\  x  e.  CC  /\  y  e.  CC )  ->  (
( k  x.  x
)  x.  y )  =  ( k  x.  ( x  x.  y
) ) )
65adantl 468 . . . . . . . 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 761 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  K  e.  NN )
8 elfzuz3 11794 . . . . . . . . . . . . . 14  |-  ( K  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  K )
)
98adantl 468 . . . . . . . . . . . . 13  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ( ZZ>= `  K )
)
10 eluznn 11226 . . . . . . . . . . . . 13  |-  ( ( K  e.  NN  /\  N  e.  ( ZZ>= `  K ) )  ->  N  e.  NN )
117, 9, 10syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  NN )
1211adantrr 722 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  NN )
13 simplr 761 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  K  e.  NN )
14 nnre 10613 . . . . . . . . . . . 12  |-  ( N  e.  NN  ->  N  e.  RR )
15 nnrp 11308 . . . . . . . . . . . 12  |-  ( K  e.  NN  ->  K  e.  RR+ )
16 ltsubrp 11332 . . . . . . . . . . . 12  |-  ( ( N  e.  RR  /\  K  e.  RR+ )  -> 
( N  -  K
)  <  N )
1714, 15, 16syl2an 480 . . . . . . . . . . 11  |-  ( ( N  e.  NN  /\  K  e.  NN )  ->  ( N  -  K
)  <  N )
1812, 13, 17syl2anc 666 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  <  N )
1912nnzd 11036 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  ZZ )
20 nnz 10956 . . . . . . . . . . . . 13  |-  ( K  e.  NN  ->  K  e.  ZZ )
2120ad2antlr 732 . . . . . . . . . . . 12  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  K  e.  ZZ )
2219, 21zsubcld 11042 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  ZZ )
23 zltp1le 10983 . . . . . . . . . . 11  |-  ( ( ( N  -  K
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( N  -  K )  <  N  <->  ( ( N  -  K
)  +  1 )  <_  N ) )
2422, 19, 23syl2anc 666 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  <  N  <->  ( ( N  -  K )  +  1 )  <_  N ) )
2518, 24mpbid 214 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  +  1 )  <_  N )
2622peano2zd 11040 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  (
( N  -  K
)  +  1 )  e.  ZZ )
27 eluz 11169 . . . . . . . . . 10  |-  ( ( ( ( N  -  K )  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( ( N  -  K )  +  1 ) )  <->  ( ( N  -  K )  +  1 )  <_  N ) )
2826, 19, 27syl2anc 666 . . . . . . . . 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 236 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )
30 simprr 765 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  NN )
31 nnuz 11191 . . . . . . . . 9  |-  NN  =  ( ZZ>= `  1 )
3230, 31syl6eleq 2538 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( N  -  K )  e.  ( ZZ>= `  1 )
)
33 fvi 5920 . . . . . . . . . 10  |-  ( k  e.  ( 1 ... N )  ->  (  _I  `  k )  =  k )
34 elfzelz 11797 . . . . . . . . . . 11  |-  ( k  e.  ( 1 ... N )  ->  k  e.  ZZ )
3534zcnd 11038 . . . . . . . . . 10  |-  ( k  e.  ( 1 ... N )  ->  k  e.  CC )
3633, 35eqeltrd 2528 . . . . . . . . 9  |-  ( k  e.  ( 1 ... N )  ->  (  _I  `  k )  e.  CC )
3736adantl 468 . . . . . . . 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 12243 . . . . . . 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 12458 . . . . . . . 8  |-  ( N  e.  NN  ->  ( ! `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
4012, 39syl 17 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( ! `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
41 facnn 12458 . . . . . . . . 9  |-  ( ( N  -  K )  e.  NN  ->  ( ! `  ( N  -  K ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( N  -  K
) ) )
4230, 41syl 17 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  ( K  e.  ( 0 ... N
)  /\  ( N  -  K )  e.  NN ) )  ->  ( ! `  ( N  -  K ) )  =  (  seq 1 (  x.  ,  _I  ) `  ( N  -  K
) ) )
4342oveq1d 6303 . . . . . . 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 2494 . . . . . 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 619 . . . . 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 759 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  NN0 )
47 faccl 12466 . . . . . . . . 9  |-  ( N  e.  NN0  ->  ( ! `
 N )  e.  NN )
48 nncn 10614 . . . . . . . . 9  |-  ( ( ! `  N )  e.  NN  ->  ( ! `  N )  e.  CC )
4946, 47, 483syl 18 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  e.  CC )
5049mulid2d 9658 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( 1  x.  ( ! `  N ) )  =  ( ! `  N
) )
5111, 39syl 17 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  (  seq 1 (  x.  ,  _I  ) `  N ) )
5251oveq2d 6304 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( 1  x.  ( ! `  N ) )  =  ( 1  x.  (  seq 1 (  x.  ,  _I  ) `  N ) ) )
5350, 52eqtr3d 2486 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  ( 1  x.  (  seq 1 (  x.  ,  _I  ) `  N ) ) )
54 fveq2 5863 . . . . . . . . 9  |-  ( ( N  -  K )  =  0  ->  ( ! `  ( N  -  K ) )  =  ( ! `  0
) )
55 fac0 12459 . . . . . . . . 9  |-  ( ! `
 0 )  =  1
5654, 55syl6eq 2500 . . . . . . . 8  |-  ( ( N  -  K )  =  0  ->  ( ! `  ( N  -  K ) )  =  1 )
57 oveq1 6295 . . . . . . . . . . 11  |-  ( ( N  -  K )  =  0  ->  (
( N  -  K
)  +  1 )  =  ( 0  +  1 ) )
58 0p1e1 10718 . . . . . . . . . . 11  |-  ( 0  +  1 )  =  1
5957, 58syl6eq 2500 . . . . . . . . . 10  |-  ( ( N  -  K )  =  0  ->  (
( N  -  K
)  +  1 )  =  1 )
6059seqeq1d 12216 . . . . . . . . 9  |-  ( ( N  -  K )  =  0  ->  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  )  =  seq 1 (  x.  ,  _I  ) )
6160fveq1d 5865 . . . . . . . 8  |-  ( ( N  -  K )  =  0  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  =  (  seq 1
(  x.  ,  _I  ) `  N )
)
6256, 61oveq12d 6306 . . . . . . 7  |-  ( ( N  -  K )  =  0  ->  (
( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) )  =  ( 1  x.  (  seq 1
(  x.  ,  _I  ) `  N )
) )
6362eqeq2d 2460 . . . . . 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 226 . . . . 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 11828 . . . . . . 7  |-  ( K  e.  ( 0 ... N )  ->  ( N  -  K )  e.  NN0 )
6665adantl 468 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  e.  NN0 )
67 elnn0 10868 . . . . . 6  |-  ( ( N  -  K )  e.  NN0  <->  ( ( N  -  K )  e.  NN  \/  ( N  -  K )  =  0 ) )
6866, 67sylib 200 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  e.  NN  \/  ( N  -  K )  =  0 ) )
6945, 64, 68mpjaod 383 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  N )  =  ( ( ! `  ( N  -  K )
)  x.  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N ) ) )
7069oveq1d 6303 . . 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 2450 . . . . . 6  |-  ( ZZ>= `  ( ( N  -  K )  +  1 ) )  =  (
ZZ>= `  ( ( N  -  K )  +  1 ) )
72 nn0z 10957 . . . . . . . . 9  |-  ( N  e.  NN0  ->  N  e.  ZZ )
73 zsubcl 10976 . . . . . . . . 9  |-  ( ( N  e.  ZZ  /\  K  e.  ZZ )  ->  ( N  -  K
)  e.  ZZ )
7472, 20, 73syl2an 480 . . . . . . . 8  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( N  -  K
)  e.  ZZ )
7574peano2zd 11040 . . . . . . 7  |-  ( ( N  e.  NN0  /\  K  e.  NN )  ->  ( ( N  -  K )  +  1 )  e.  ZZ )
7675adantr 467 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  +  1 )  e.  ZZ )
77 fvi 5920 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  (  _I  `  k )  =  k )
78 eluzelcn 11167 . . . . . . . 8  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  k  e.  CC )
7977, 78eqeltrd 2528 . . . . . . 7  |-  ( k  e.  ( ZZ>= `  (
( N  -  K
)  +  1 ) )  ->  (  _I  `  k )  e.  CC )
8079adantl 468 . . . . . 6  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N
) )  /\  k  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )  ->  (  _I  `  k )  e.  CC )
813adantl 468 . . . . . 6  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N
) )  /\  (
k  e.  CC  /\  x  e.  CC )
)  ->  ( k  x.  x )  e.  CC )
8271, 76, 80, 81seqf 12231 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) : ( ZZ>= `  (
( N  -  K
)  +  1 ) ) --> CC )
8311, 7, 17syl2anc 666 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  <  N
)
8474adantr 467 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  -  K )  e.  ZZ )
8511nnzd 11036 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ZZ )
8684, 85, 23syl2anc 666 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  <  N  <->  ( ( N  -  K )  +  1 )  <_  N
) )
8783, 86mpbid 214 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ( N  -  K )  +  1 )  <_  N )
8876, 85, 27syl2anc 666 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) )  <-> 
( ( N  -  K )  +  1 )  <_  N )
)
8987, 88mpbird 236 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  N  e.  ( ZZ>= `  ( ( N  -  K )  +  1 ) ) )
9082, 89ffvelrnd 6021 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  e.  CC )
91 elfznn0 11884 . . . . . . 7  |-  ( K  e.  ( 0 ... N )  ->  K  e.  NN0 )
9291adantl 468 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  K  e.  NN0 )
93 faccl 12466 . . . . . 6  |-  ( K  e.  NN0  ->  ( ! `
 K )  e.  NN )
9492, 93syl 17 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  e.  NN )
9594nncnd 10622 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  e.  CC )
96 faccl 12466 . . . . . 6  |-  ( ( N  -  K )  e.  NN0  ->  ( ! `
 ( N  -  K ) )  e.  NN )
9766, 96syl 17 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  e.  NN )
9897nncnd 10622 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  e.  CC )
9994nnne0d 10651 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  K )  =/=  0
)
10097nnne0d 10651 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( ! `  ( N  -  K
) )  =/=  0
)
10190, 95, 98, 99, 100divcan5d 10406 . . 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 ) ) )
1022, 70, 1013eqtrd 2488 . 2  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  ( (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
) )
103 nnnn0 10873 . . . . 5  |-  ( K  e.  NN  ->  K  e.  NN0 )
104103ad2antlr 732 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  NN0 )
105 nncn 10614 . . . . 5  |-  ( ( ! `  K )  e.  NN  ->  ( ! `  K )  e.  CC )
106 nnne0 10639 . . . . 5  |-  ( ( ! `  K )  e.  NN  ->  ( ! `  K )  =/=  0 )
107105, 106div0d 10379 . . . 4  |-  ( ( ! `  K )  e.  NN  ->  (
0  /  ( ! `
 K ) )  =  0 )
108104, 93, 1073syl 18 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  /  ( ! `
 K ) )  =  0 )
1093adantl 468 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  (
k  e.  CC  /\  x  e.  CC )
)  ->  ( k  x.  x )  e.  CC )
110 fvi 5920 . . . . . . 7  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  (  _I  `  k )  =  k )
111 elfzelz 11797 . . . . . . . 8  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  k  e.  ZZ )
112111zcnd 11038 . . . . . . 7  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  k  e.  CC )
113110, 112eqeltrd 2528 . . . . . 6  |-  ( k  e.  ( ( ( N  -  K )  +  1 ) ... N )  ->  (  _I  `  k )  e.  CC )
114113adantl 468 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  ( ( ( N  -  K )  +  1 ) ... N
) )  ->  (  _I  `  k )  e.  CC )
115 mul02 9808 . . . . . 6  |-  ( k  e.  CC  ->  (
0  x.  k )  =  0 )
116115adantl 468 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  CC )  ->  (
0  x.  k )  =  0 )
117 mul01 9809 . . . . . 6  |-  ( k  e.  CC  ->  (
k  x.  0 )  =  0 )
118117adantl 468 . . . . 5  |-  ( ( ( ( N  e. 
NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  /\  k  e.  CC )  ->  (
k  x.  0 )  =  0 )
119 simpr 463 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  -.  K  e.  ( 0 ... N ) )
120 nn0uz 11190 . . . . . . . . . . . 12  |-  NN0  =  ( ZZ>= `  0 )
121104, 120syl6eleq 2538 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  ( ZZ>= `  0 )
)
12272ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  ZZ )
123 elfz5 11789 . . . . . . . . . . 11  |-  ( ( K  e.  ( ZZ>= ` 
0 )  /\  N  e.  ZZ )  ->  ( K  e.  ( 0 ... N )  <->  K  <_  N ) )
124121, 122, 123syl2anc 666 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( K  e.  ( 0 ... N )  <->  K  <_  N ) )
125 nn0re 10875 . . . . . . . . . . . 12  |-  ( N  e.  NN0  ->  N  e.  RR )
126125ad2antrr 731 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  RR )
127 nnre 10613 . . . . . . . . . . . 12  |-  ( K  e.  NN  ->  K  e.  RR )
128127ad2antlr 732 . . . . . . . . . . 11  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  K  e.  RR )
129126, 128subge0d 10200 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  <_  ( N  -  K )  <->  K  <_  N ) )
130124, 129bitr4d 260 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( K  e.  ( 0 ... N )  <->  0  <_  ( N  -  K ) ) )
131119, 130mtbid 302 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  -.  0  <_  ( N  -  K ) )
13274adantr 467 . . . . . . . . . 10  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  e.  ZZ )
133132zred 11037 . . . . . . . . 9  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  e.  RR )
134 0re 9640 . . . . . . . . 9  |-  0  e.  RR
135 ltnle 9710 . . . . . . . . 9  |-  ( ( ( N  -  K
)  e.  RR  /\  0  e.  RR )  ->  ( ( N  -  K )  <  0  <->  -.  0  <_  ( N  -  K ) ) )
136133, 134, 135sylancl 667 . . . . . . . 8  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  <  0  <->  -.  0  <_  ( N  -  K
) ) )
137131, 136mpbird 236 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  -  K )  <  0 )
138 0z 10945 . . . . . . . 8  |-  0  e.  ZZ
139 zltp1le 10983 . . . . . . . 8  |-  ( ( ( N  -  K
)  e.  ZZ  /\  0  e.  ZZ )  ->  ( ( N  -  K )  <  0  <->  ( ( N  -  K
)  +  1 )  <_  0 ) )
140132, 138, 139sylancl 667 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  <  0  <->  ( ( N  -  K )  +  1 )  <_ 
0 ) )
141137, 140mpbid 214 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  +  1 )  <_  0 )
142 nn0ge0 10892 . . . . . . 7  |-  ( N  e.  NN0  ->  0  <_  N )
143142ad2antrr 731 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  <_  N )
144 0zd 10946 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  e.  ZZ )
14575adantr 467 . . . . . . 7  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
( N  -  K
)  +  1 )  e.  ZZ )
146 elfz 11787 . . . . . . 7  |-  ( ( 0  e.  ZZ  /\  ( ( N  -  K )  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( 0  e.  ( ( ( N  -  K )  +  1 ) ... N )  <-> 
( ( ( N  -  K )  +  1 )  <_  0  /\  0  <_  N ) ) )
147144, 145, 122, 146syl3anc 1267 . . . . . 6  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
0  e.  ( ( ( N  -  K
)  +  1 ) ... N )  <->  ( (
( N  -  K
)  +  1 )  <_  0  /\  0  <_  N ) ) )
148141, 143, 147mpbir2and 932 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  0  e.  ( ( ( N  -  K )  +  1 ) ... N
) )
149 simpll 759 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  N  e.  NN0 )
150 0cn 9632 . . . . . 6  |-  0  e.  CC
151 fvi 5920 . . . . . 6  |-  ( 0  e.  CC  ->  (  _I  `  0 )  =  0 )
152150, 151mp1i 13 . . . . 5  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (  _I  `  0 )  =  0 )
153109, 114, 116, 118, 148, 149, 152seqz 12258 . . . 4  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  =  0 )
154153oveq1d 6303 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  (
(  seq ( ( N  -  K )  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K )
)  =  ( 0  /  ( ! `  K ) ) )
155 bcval3 12488 . . . . 5  |-  ( ( N  e.  NN0  /\  K  e.  ZZ  /\  -.  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  0 )
15620, 155syl3an2 1301 . . . 4  |-  ( ( N  e.  NN0  /\  K  e.  NN  /\  -.  K  e.  ( 0 ... N ) )  ->  ( N  _C  K )  =  0 )
1571563expa 1207 . . 3  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  _C  K )  =  0 )
158108, 154, 1573eqtr4rd 2495 . 2  |-  ( ( ( N  e.  NN0  /\  K  e.  NN )  /\  -.  K  e.  ( 0 ... N
) )  ->  ( N  _C  K )  =  ( (  seq (
( N  -  K
)  +  1 ) (  x.  ,  _I  ) `  N )  /  ( ! `  K ) ) )
159102, 158pm2.61dan 799 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 188    \/ wo 370    /\ wa 371    /\ w3a 984    = wceq 1443    e. wcel 1886   class class class wbr 4401    _I cid 4743   ` cfv 5581  (class class class)co 6288   CCcc 9534   RRcr 9535   0cc0 9536   1c1 9537    + caddc 9539    x. cmul 9541    < clt 9672    <_ cle 9673    - cmin 9857    / cdiv 10266   NNcn 10606   NN0cn0 10866   ZZcz 10934   ZZ>=cuz 11156   RR+crp 11299   ...cfz 11781    seqcseq 12210   !cfa 12456    _C cbc 12484
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-8 1888  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pow 4580  ax-pr 4638  ax-un 6580  ax-cnex 9592  ax-resscn 9593  ax-1cn 9594  ax-icn 9595  ax-addcl 9596  ax-addrcl 9597  ax-mulcl 9598  ax-mulrcl 9599  ax-mulcom 9600  ax-addass 9601  ax-mulass 9602  ax-distr 9603  ax-i2m1 9604  ax-1ne0 9605  ax-1rid 9606  ax-rnegex 9607  ax-rrecex 9608  ax-cnre 9609  ax-pre-lttri 9610  ax-pre-lttrn 9611  ax-pre-ltadd 9612  ax-pre-mulgt0 9613
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 985  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-eu 2302  df-mo 2303  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-nel 2624  df-ral 2741  df-rex 2742  df-reu 2743  df-rmo 2744  df-rab 2745  df-v 3046  df-sbc 3267  df-csb 3363  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-pss 3419  df-nul 3731  df-if 3881  df-pw 3952  df-sn 3968  df-pr 3970  df-tp 3972  df-op 3974  df-uni 4198  df-iun 4279  df-br 4402  df-opab 4461  df-mpt 4462  df-tr 4497  df-eprel 4744  df-id 4748  df-po 4754  df-so 4755  df-fr 4792  df-we 4794  df-xp 4839  df-rel 4840  df-cnv 4841  df-co 4842  df-dm 4843  df-rn 4844  df-res 4845  df-ima 4846  df-pred 5379  df-ord 5425  df-on 5426  df-lim 5427  df-suc 5428  df-iota 5545  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-riota 6250  df-ov 6291  df-oprab 6292  df-mpt2 6293  df-om 6690  df-1st 6790  df-2nd 6791  df-wrecs 7025  df-recs 7087  df-rdg 7125  df-er 7360  df-en 7567  df-dom 7568  df-sdom 7569  df-pnf 9674  df-mnf 9675  df-xr 9676  df-ltxr 9677  df-le 9678  df-sub 9859  df-neg 9860  df-div 10267  df-nn 10607  df-n0 10867  df-z 10935  df-uz 11157  df-rp 11300  df-fz 11782  df-seq 12211  df-fac 12457  df-bc 12485
This theorem is referenced by:  bcn2  12501
  Copyright terms: Public domain W3C validator