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 0 K ( N K) = seq N - K + 1 × I N K !

Proof

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