Metamath Proof Explorer

Theorem bcval5

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)

Ref Expression
Assertion bcval5 
|- ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )

Proof

Step Hyp Ref Expression
1 bcval2 
 |-  ( K e. ( 0 ... N ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
2 1 adantl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( ! ` N ) / ( ( ! ` ( N - K ) ) x. ( ! ` K ) ) ) )
3 mulcl 
 |-  ( ( k e. CC /\ x e. CC ) -> ( k x. x ) e. CC )
4 3 adantl 
 |-  ( ( ( ( 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 
 |-  ( ( k e. CC /\ x e. CC /\ y e. CC ) -> ( ( k x. x ) x. y ) = ( k x. ( x x. y ) ) )
6 5 adantl 
 |-  ( ( ( ( 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 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN )
8 elfzuz3 
 |-  ( K e. ( 0 ... N ) -> N e. ( ZZ>= ` K ) )
9 8 adantl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` K ) )
10 eluznn 
 |-  ( ( K e. NN /\ N e. ( ZZ>= ` K ) ) -> N e. NN )
11 7 9 10 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN )
12 11 adantrr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. NN )
13 simplr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> K e. NN )
14 nnre 
 |-  ( N e. NN -> N e. RR )
15 nnrp 
 |-  ( K e. NN -> K e. RR+ )
16 ltsubrp 
 |-  ( ( N e. RR /\ K e. RR+ ) -> ( N - K ) < N )
17 14 15 16 syl2an 
 |-  ( ( N e. NN /\ K e. NN ) -> ( N - K ) < N )
18 12 13 17 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) < N )
19 12 nnzd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. ZZ )
20 nnz 
 |-  ( K e. NN -> K e. ZZ )
21 20 ad2antlr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> K e. ZZ )
22 19 21 zsubcld 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. ZZ )
23 zltp1le 
 |-  ( ( ( N - K ) e. ZZ /\ N e. ZZ ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
24 22 19 23 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
25 18 24 mpbid 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) + 1 ) <_ N )
26 22 peano2zd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ( N - K ) + 1 ) e. ZZ )
27 eluz 
 |-  ( ( ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
28 26 19 27 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
29 25 28 mpbird 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
30 simprr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. NN )
31 nnuz 
 |-  NN = ( ZZ>= ` 1 )
32 30 31 eleqtrdi 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( N - K ) e. ( ZZ>= ` 1 ) )
33 fvi 
 |-  ( k e. ( 1 ... N ) -> ( _I ` k ) = k )
34 elfzelz 
 |-  ( k e. ( 1 ... N ) -> k e. ZZ )
35 34 zcnd 
 |-  ( k e. ( 1 ... N ) -> k e. CC )
36 33 35 eqeltrd 
 |-  ( k e. ( 1 ... N ) -> ( _I ` k ) e. CC )
37 36 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) /\ k e. ( 1 ... N ) ) -> ( _I ` k ) e. CC )
38 4 6 29 32 37 seqsplit 
 |-  ( ( ( 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 
 |-  ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
40 12 39 syl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
41 facnn 
 |-  ( ( N - K ) e. NN -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I ) ` ( N - K ) ) )
42 30 41 syl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ ( K e. ( 0 ... N ) /\ ( N - K ) e. NN ) ) -> ( ! ` ( N - K ) ) = ( seq 1 ( x. , _I ) ` ( N - K ) ) )
43 42 oveq1d 
 |-  ( ( ( 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 ) ) )
44 38 40 43 3eqtr4d 
 |-  ( ( ( 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 ) ) )
45 44 expr 
 |-  ( ( ( 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 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. NN0 )
47 faccl 
 |-  ( N e. NN0 -> ( ! ` N ) e. NN )
48 nncn 
 |-  ( ( ! ` N ) e. NN -> ( ! ` N ) e. CC )
49 46 47 48 3syl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) e. CC )
50 49 mulid2d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( ! ` N ) )
51 11 39 syl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
52 51 oveq2d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( 1 x. ( ! ` N ) ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
53 50 52 eqtr3d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
54 fveq2 
 |-  ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = ( ! ` 0 ) )
55 fac0 
 |-  ( ! ` 0 ) = 1
56 54 55 eqtrdi 
 |-  ( ( N - K ) = 0 -> ( ! ` ( N - K ) ) = 1 )
57 oveq1 
 |-  ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = ( 0 + 1 ) )
58 0p1e1 
 |-  ( 0 + 1 ) = 1
59 57 58 eqtrdi 
 |-  ( ( N - K ) = 0 -> ( ( N - K ) + 1 ) = 1 )
60 59 seqeq1d 
 |-  ( ( N - K ) = 0 -> seq ( ( N - K ) + 1 ) ( x. , _I ) = seq 1 ( x. , _I ) )
61 60 fveq1d 
 |-  ( ( N - K ) = 0 -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) = ( seq 1 ( x. , _I ) ` N ) )
62 56 61 oveq12d 
 |-  ( ( N - K ) = 0 -> ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) )
63 62 eqeq2d 
 |-  ( ( N - K ) = 0 -> ( ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) <-> ( ! ` N ) = ( 1 x. ( seq 1 ( x. , _I ) ` N ) ) ) )
64 53 63 syl5ibrcom 
 |-  ( ( ( 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 
 |-  ( K e. ( 0 ... N ) -> ( N - K ) e. NN0 )
66 65 adantl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. NN0 )
67 elnn0 
 |-  ( ( N - K ) e. NN0 <-> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
68 66 67 sylib 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) e. NN \/ ( N - K ) = 0 ) )
69 45 64 68 mpjaod 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` N ) = ( ( ! ` ( N - K ) ) x. ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) ) )
70 69 oveq1d 
 |-  ( ( ( 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 
 |-  ( ZZ>= ` ( ( N - K ) + 1 ) ) = ( ZZ>= ` ( ( N - K ) + 1 ) )
72 nn0z 
 |-  ( N e. NN0 -> N e. ZZ )
73 zsubcl 
 |-  ( ( N e. ZZ /\ K e. ZZ ) -> ( N - K ) e. ZZ )
74 72 20 73 syl2an 
 |-  ( ( N e. NN0 /\ K e. NN ) -> ( N - K ) e. ZZ )
75 74 peano2zd 
 |-  ( ( N e. NN0 /\ K e. NN ) -> ( ( N - K ) + 1 ) e. ZZ )
76 75 adantr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
77 fvi 
 |-  ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> ( _I ` k ) = k )
78 eluzelcn 
 |-  ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> k e. CC )
79 77 78 eqeltrd 
 |-  ( k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) -> ( _I ` k ) e. CC )
80 79 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ k e. ( ZZ>= ` ( ( N - K ) + 1 ) ) ) -> ( _I ` k ) e. CC )
81 3 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
82 71 76 80 81 seqf 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> seq ( ( N - K ) + 1 ) ( x. , _I ) : ( ZZ>= ` ( ( N - K ) + 1 ) ) --> CC )
83 11 7 17 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) < N )
84 74 adantr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
85 11 nnzd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ZZ )
86 84 85 23 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) < N <-> ( ( N - K ) + 1 ) <_ N ) )
87 83 86 mpbid 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ N )
88 76 85 27 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) <-> ( ( N - K ) + 1 ) <_ N ) )
89 87 88 mpbird 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> N e. ( ZZ>= ` ( ( N - K ) + 1 ) ) )
90 82 89 ffvelrnd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) e. CC )
91 elfznn0 
 |-  ( K e. ( 0 ... N ) -> K e. NN0 )
92 91 adantl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> K e. NN0 )
93 92 faccld 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. NN )
94 93 nncnd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) e. CC )
95 66 faccld 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. NN )
96 95 nncnd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) e. CC )
97 93 nnne0d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` K ) =/= 0 )
98 95 nnne0d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( ! ` ( N - K ) ) =/= 0 )
99 90 94 96 97 98 divcan5d 
 |-  ( ( ( 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 ) ) )
100 2 70 99 3eqtrd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
101 nnnn0 
 |-  ( K e. NN -> K e. NN0 )
102 101 ad2antlr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. NN0 )
103 faccl 
 |-  ( K e. NN0 -> ( ! ` K ) e. NN )
104 nncn 
 |-  ( ( ! ` K ) e. NN -> ( ! ` K ) e. CC )
105 nnne0 
 |-  ( ( ! ` K ) e. NN -> ( ! ` K ) =/= 0 )
106 104 105 div0d 
 |-  ( ( ! ` K ) e. NN -> ( 0 / ( ! ` K ) ) = 0 )
107 102 103 106 3syl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 / ( ! ` K ) ) = 0 )
108 3 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ ( k e. CC /\ x e. CC ) ) -> ( k x. x ) e. CC )
109 fvi 
 |-  ( k e. ( ( ( N - K ) + 1 ) ... N ) -> ( _I ` k ) = k )
110 elfzelz 
 |-  ( k e. ( ( ( N - K ) + 1 ) ... N ) -> k e. ZZ )
111 110 zcnd 
 |-  ( k e. ( ( ( N - K ) + 1 ) ... N ) -> k e. CC )
112 109 111 eqeltrd 
 |-  ( k e. ( ( ( N - K ) + 1 ) ... N ) -> ( _I ` k ) e. CC )
113 112 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. ( ( ( N - K ) + 1 ) ... N ) ) -> ( _I ` k ) e. CC )
114 mul02 
 |-  ( k e. CC -> ( 0 x. k ) = 0 )
115 114 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( 0 x. k ) = 0 )
116 mul01 
 |-  ( k e. CC -> ( k x. 0 ) = 0 )
117 116 adantl 
 |-  ( ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) /\ k e. CC ) -> ( k x. 0 ) = 0 )
118 simpr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. K e. ( 0 ... N ) )
119 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
120 102 119 eleqtrdi 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. ( ZZ>= ` 0 ) )
121 72 ad2antrr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. ZZ )
122 elfz5 
 |-  ( ( K e. ( ZZ>= ` 0 ) /\ N e. ZZ ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
123 120 121 122 syl2anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> K <_ N ) )
124 nn0re 
 |-  ( N e. NN0 -> N e. RR )
125 124 ad2antrr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. RR )
126 nnre 
 |-  ( K e. NN -> K e. RR )
127 126 ad2antlr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> K e. RR )
128 125 127 subge0d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 <_ ( N - K ) <-> K <_ N ) )
129 123 128 bitr4d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( K e. ( 0 ... N ) <-> 0 <_ ( N - K ) ) )
130 118 129 mtbid 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> -. 0 <_ ( N - K ) )
131 74 adantr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. ZZ )
132 131 zred 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) e. RR )
133 0re 
 |-  0 e. RR
134 ltnle 
 |-  ( ( ( N - K ) e. RR /\ 0 e. RR ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
135 132 133 134 sylancl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> -. 0 <_ ( N - K ) ) )
136 130 135 mpbird 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N - K ) < 0 )
137 0z 
 |-  0 e. ZZ
138 zltp1le 
 |-  ( ( ( N - K ) e. ZZ /\ 0 e. ZZ ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
139 131 137 138 sylancl 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) < 0 <-> ( ( N - K ) + 1 ) <_ 0 ) )
140 136 139 mpbid 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) <_ 0 )
141 nn0ge0 
 |-  ( N e. NN0 -> 0 <_ N )
142 141 ad2antrr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 <_ N )
143 0zd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ZZ )
144 75 adantr 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( N - K ) + 1 ) e. ZZ )
145 elfz 
 |-  ( ( 0 e. ZZ /\ ( ( N - K ) + 1 ) e. ZZ /\ N e. ZZ ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
146 143 144 121 145 syl3anc 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( 0 e. ( ( ( N - K ) + 1 ) ... N ) <-> ( ( ( N - K ) + 1 ) <_ 0 /\ 0 <_ N ) ) )
147 140 142 146 mpbir2and 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> 0 e. ( ( ( N - K ) + 1 ) ... N ) )
148 simpll 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> N e. NN0 )
149 0cn 
 |-  0 e. CC
150 fvi 
 |-  ( 0 e. CC -> ( _I ` 0 ) = 0 )
151 149 150 mp1i 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( _I ` 0 ) = 0 )
152 108 113 115 117 147 148 151 seqz 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) = 0 )
153 152 oveq1d 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) = ( 0 / ( ! ` K ) ) )
154 bcval3 
 |-  ( ( N e. NN0 /\ K e. ZZ /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
155 20 154 syl3an2 
 |-  ( ( N e. NN0 /\ K e. NN /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
156 155 3expa 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = 0 )
157 107 153 156 3eqtr4rd 
 |-  ( ( ( N e. NN0 /\ K e. NN ) /\ -. K e. ( 0 ... N ) ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )
158 100 157 pm2.61dan 
 |-  ( ( N e. NN0 /\ K e. NN ) -> ( N _C K ) = ( ( seq ( ( N - K ) + 1 ) ( x. , _I ) ` N ) / ( ! ` K ) ) )