Metamath Proof Explorer


Theorem bclbnd

Description: A bound on the binomial coefficient. (Contributed by Mario Carneiro, 11-Mar-2014)

Ref Expression
Assertion bclbnd N 4 4 N N < ( 2 N N)

Proof

Step Hyp Ref Expression
1 oveq2 x = 4 4 x = 4 4
2 id x = 4 x = 4
3 1 2 oveq12d x = 4 4 x x = 4 4 4
4 oveq2 x = 4 2 x = 2 4
5 4 2 oveq12d x = 4 ( 2 x x) = ( 2 4 4 )
6 3 5 breq12d x = 4 4 x x < ( 2 x x) 4 4 4 < ( 2 4 4 )
7 oveq2 x = n 4 x = 4 n
8 id x = n x = n
9 7 8 oveq12d x = n 4 x x = 4 n n
10 oveq2 x = n 2 x = 2 n
11 10 8 oveq12d x = n ( 2 x x) = ( 2 n n)
12 9 11 breq12d x = n 4 x x < ( 2 x x) 4 n n < ( 2 n n)
13 oveq2 x = n + 1 4 x = 4 n + 1
14 id x = n + 1 x = n + 1
15 13 14 oveq12d x = n + 1 4 x x = 4 n + 1 n + 1
16 oveq2 x = n + 1 2 x = 2 n + 1
17 16 14 oveq12d x = n + 1 ( 2 x x) = ( 2 n + 1 n + 1 )
18 15 17 breq12d x = n + 1 4 x x < ( 2 x x) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
19 oveq2 x = N 4 x = 4 N
20 id x = N x = N
21 19 20 oveq12d x = N 4 x x = 4 N N
22 oveq2 x = N 2 x = 2 N
23 22 20 oveq12d x = N ( 2 x x) = ( 2 N N)
24 21 23 breq12d x = N 4 x x < ( 2 x x) 4 N N < ( 2 N N)
25 6nn0 6 0
26 7nn0 7 0
27 4nn0 4 0
28 0nn0 0 0
29 4lt10 4 < 10
30 6lt7 6 < 7
31 25 26 27 28 29 30 decltc 64 < 70
32 2cn 2
33 2nn0 2 0
34 3nn0 3 0
35 expmul 2 2 0 3 0 2 2 3 = 2 2 3
36 32 33 34 35 mp3an 2 2 3 = 2 2 3
37 sq2 2 2 = 4
38 37 eqcomi 4 = 2 2
39 4m1e3 4 1 = 3
40 38 39 oveq12i 4 4 1 = 2 2 3
41 36 40 eqtr4i 2 2 3 = 4 4 1
42 3cn 3
43 3t2e6 3 2 = 6
44 42 32 43 mulcomli 2 3 = 6
45 44 oveq2i 2 2 3 = 2 6
46 2exp6 2 6 = 64
47 45 46 eqtri 2 2 3 = 64
48 4cn 4
49 4ne0 4 0
50 4z 4
51 expm1 4 4 0 4 4 4 1 = 4 4 4
52 48 49 50 51 mp3an 4 4 1 = 4 4 4
53 41 47 52 3eqtr3ri 4 4 4 = 64
54 df-4 4 = 3 + 1
55 54 oveq2i 2 4 = 2 3 + 1
56 55 54 oveq12i ( 2 4 4 ) = ( 2 3 + 1 3 + 1 )
57 bcp1ctr 3 0 ( 2 3 + 1 3 + 1 ) = ( 2 3 3 ) 2 2 3 + 1 3 + 1
58 34 57 ax-mp ( 2 3 + 1 3 + 1 ) = ( 2 3 3 ) 2 2 3 + 1 3 + 1
59 df-3 3 = 2 + 1
60 59 oveq2i 2 3 = 2 2 + 1
61 60 59 oveq12i ( 2 3 3 ) = ( 2 2 + 1 2 + 1 )
62 bcp1ctr 2 0 ( 2 2 + 1 2 + 1 ) = ( 2 2 2 ) 2 2 2 + 1 2 + 1
63 33 62 ax-mp ( 2 2 + 1 2 + 1 ) = ( 2 2 2 ) 2 2 2 + 1 2 + 1
64 df-2 2 = 1 + 1
65 64 oveq2i 2 2 = 2 1 + 1
66 65 64 oveq12i ( 2 2 2 ) = ( 2 1 + 1 1 + 1 )
67 1nn0 1 0
68 bcp1ctr 1 0 ( 2 1 + 1 1 + 1 ) = ( 2 1 1 ) 2 2 1 + 1 1 + 1
69 67 68 ax-mp ( 2 1 + 1 1 + 1 ) = ( 2 1 1 ) 2 2 1 + 1 1 + 1
70 1e0p1 1 = 0 + 1
71 70 oveq2i 2 1 = 2 0 + 1
72 71 70 oveq12i ( 2 1 1 ) = ( 2 0 + 1 0 + 1 )
73 bcp1ctr 0 0 ( 2 0 + 1 0 + 1 ) = ( 2 0 0 ) 2 2 0 + 1 0 + 1
74 28 73 ax-mp ( 2 0 + 1 0 + 1 ) = ( 2 0 0 ) 2 2 0 + 1 0 + 1
75 33 28 nn0mulcli 2 0 0
76 bcn0 2 0 0 ( 2 0 0 ) = 1
77 75 76 ax-mp ( 2 0 0 ) = 1
78 2t0e0 2 0 = 0
79 78 oveq1i 2 0 + 1 = 0 + 1
80 79 70 eqtr4i 2 0 + 1 = 1
81 70 eqcomi 0 + 1 = 1
82 80 81 oveq12i 2 0 + 1 0 + 1 = 1 1
83 1div1e1 1 1 = 1
84 82 83 eqtri 2 0 + 1 0 + 1 = 1
85 84 oveq2i 2 2 0 + 1 0 + 1 = 2 1
86 2t1e2 2 1 = 2
87 85 86 eqtri 2 2 0 + 1 0 + 1 = 2
88 77 87 oveq12i ( 2 0 0 ) 2 2 0 + 1 0 + 1 = 1 2
89 32 mulid2i 1 2 = 2
90 88 89 eqtri ( 2 0 0 ) 2 2 0 + 1 0 + 1 = 2
91 72 74 90 3eqtri ( 2 1 1 ) = 2
92 86 oveq1i 2 1 + 1 = 2 + 1
93 92 59 eqtr4i 2 1 + 1 = 3
94 64 eqcomi 1 + 1 = 2
95 93 94 oveq12i 2 1 + 1 1 + 1 = 3 2
96 95 oveq2i 2 2 1 + 1 1 + 1 = 2 3 2
97 2ne0 2 0
98 42 32 97 divcan2i 2 3 2 = 3
99 96 98 eqtri 2 2 1 + 1 1 + 1 = 3
100 91 99 oveq12i ( 2 1 1 ) 2 2 1 + 1 1 + 1 = 2 3
101 100 44 eqtri ( 2 1 1 ) 2 2 1 + 1 1 + 1 = 6
102 66 69 101 3eqtri ( 2 2 2 ) = 6
103 2t2e4 2 2 = 4
104 103 oveq1i 2 2 + 1 = 4 + 1
105 df-5 5 = 4 + 1
106 104 105 eqtr4i 2 2 + 1 = 5
107 59 eqcomi 2 + 1 = 3
108 106 107 oveq12i 2 2 + 1 2 + 1 = 5 3
109 108 oveq2i 2 2 2 + 1 2 + 1 = 2 5 3
110 5cn 5
111 3ne0 3 0
112 32 110 42 111 divassi 2 5 3 = 2 5 3
113 109 112 eqtr4i 2 2 2 + 1 2 + 1 = 2 5 3
114 102 113 oveq12i ( 2 2 2 ) 2 2 2 + 1 2 + 1 = 6 2 5 3
115 63 114 eqtri ( 2 2 + 1 2 + 1 ) = 6 2 5 3
116 6cn 6
117 2nn 2
118 5nn 5
119 117 118 nnmulcli 2 5
120 119 nncni 2 5
121 42 111 pm3.2i 3 3 0
122 div12 6 2 5 3 3 0 6 2 5 3 = 2 5 6 3
123 116 120 121 122 mp3an 6 2 5 3 = 2 5 6 3
124 5t2e10 5 2 = 10
125 110 32 124 mulcomli 2 5 = 10
126 116 42 32 111 divmuli 6 3 = 2 3 2 = 6
127 43 126 mpbir 6 3 = 2
128 125 127 oveq12i 2 5 6 3 = 10 2
129 123 128 eqtri 6 2 5 3 = 10 2
130 61 115 129 3eqtri ( 2 3 3 ) = 10 2
131 44 oveq1i 2 3 + 1 = 6 + 1
132 df-7 7 = 6 + 1
133 131 132 eqtr4i 2 3 + 1 = 7
134 3p1e4 3 + 1 = 4
135 133 134 oveq12i 2 3 + 1 3 + 1 = 7 4
136 135 oveq2i 2 2 3 + 1 3 + 1 = 2 7 4
137 130 136 oveq12i ( 2 3 3 ) 2 2 3 + 1 3 + 1 = 10 2 2 7 4
138 56 58 137 3eqtri ( 2 4 4 ) = 10 2 2 7 4
139 10nn 10
140 139 nncni 10
141 7cn 7
142 141 48 49 divcli 7 4
143 32 142 mulcli 2 7 4
144 140 32 143 mulassi 10 2 2 7 4 = 10 2 2 7 4
145 103 oveq1i 2 2 7 4 = 4 7 4
146 32 32 142 mulassi 2 2 7 4 = 2 2 7 4
147 141 48 49 divcan2i 4 7 4 = 7
148 145 146 147 3eqtr3i 2 2 7 4 = 7
149 148 oveq2i 10 2 2 7 4 = 10 7
150 144 149 eqtri 10 2 2 7 4 = 10 7
151 26 dec0u 10 7 = 70
152 138 150 151 3eqtri ( 2 4 4 ) = 70
153 31 53 152 3brtr4i 4 4 4 < ( 2 4 4 )
154 4nn 4
155 eluznn 4 n 4 n
156 154 155 mpan n 4 n
157 nnnn0 n n 0
158 nnexpcl 4 n 0 4 n
159 154 157 158 sylancr n 4 n
160 159 nnrpd n 4 n +
161 nnrp n n +
162 160 161 rpdivcld n 4 n n +
163 162 rpred n 4 n n
164 nnmulcl 2 n 2 n
165 117 164 mpan n 2 n
166 165 nnnn0d n 2 n 0
167 nnz n n
168 bccl 2 n 0 n ( 2 n n) 0
169 166 167 168 syl2anc n ( 2 n n) 0
170 169 nn0red n ( 2 n n)
171 2rp 2 +
172 165 peano2nnd n 2 n + 1
173 172 nnrpd n 2 n + 1 +
174 peano2nn n n + 1
175 174 nnrpd n n + 1 +
176 173 175 rpdivcld n 2 n + 1 n + 1 +
177 rpmulcl 2 + 2 n + 1 n + 1 + 2 2 n + 1 n + 1 +
178 171 176 177 sylancr n 2 2 n + 1 n + 1 +
179 163 170 178 ltmul1d n 4 n n < ( 2 n n) 4 n n 2 2 n + 1 n + 1 < ( 2 n n) 2 2 n + 1 n + 1
180 bcp1ctr n 0 ( 2 n + 1 n + 1 ) = ( 2 n n) 2 2 n + 1 n + 1
181 157 180 syl n ( 2 n + 1 n + 1 ) = ( 2 n n) 2 2 n + 1 n + 1
182 181 breq2d n 4 n n 2 2 n + 1 n + 1 < ( 2 n + 1 n + 1 ) 4 n n 2 2 n + 1 n + 1 < ( 2 n n) 2 2 n + 1 n + 1
183 179 182 bitr4d n 4 n n < ( 2 n n) 4 n n 2 2 n + 1 n + 1 < ( 2 n + 1 n + 1 )
184 2re 2
185 184 a1i n 2
186 173 161 rpdivcld n 2 n + 1 n +
187 186 rpred n 2 n + 1 n
188 nnmulcl 4 n 2 4 n 2
189 159 117 188 sylancl n 4 n 2
190 189 nnrpd n 4 n 2 +
191 190 175 rpdivcld n 4 n 2 n + 1 +
192 161 rpreccld n 1 n +
193 ltaddrp 2 1 n + 2 < 2 + 1 n
194 184 192 193 sylancr n 2 < 2 + 1 n
195 165 nncnd n 2 n
196 1cnd n 1
197 nncn n n
198 nnne0 n n 0
199 195 196 197 198 divdird n 2 n + 1 n = 2 n n + 1 n
200 32 a1i n 2
201 200 197 198 divcan4d n 2 n n = 2
202 201 oveq1d n 2 n n + 1 n = 2 + 1 n
203 199 202 eqtr2d n 2 + 1 n = 2 n + 1 n
204 194 203 breqtrd n 2 < 2 n + 1 n
205 185 187 191 204 ltmul2dd n 4 n 2 n + 1 2 < 4 n 2 n + 1 2 n + 1 n
206 expp1 4 n 0 4 n + 1 = 4 n 4
207 48 157 206 sylancr n 4 n + 1 = 4 n 4
208 159 nncnd n 4 n
209 208 200 200 mulassd n 4 n 2 2 = 4 n 2 2
210 103 oveq2i 4 n 2 2 = 4 n 4
211 209 210 eqtrdi n 4 n 2 2 = 4 n 4
212 207 211 eqtr4d n 4 n + 1 = 4 n 2 2
213 212 oveq1d n 4 n + 1 n + 1 = 4 n 2 2 n + 1
214 189 nncnd n 4 n 2
215 174 nncnd n n + 1
216 174 nnne0d n n + 1 0
217 214 200 215 216 div23d n 4 n 2 2 n + 1 = 4 n 2 n + 1 2
218 213 217 eqtrd n 4 n + 1 n + 1 = 4 n 2 n + 1 2
219 208 200 197 198 div23d n 4 n 2 n = 4 n n 2
220 219 oveq1d n 4 n 2 n 2 n + 1 n + 1 = 4 n n 2 2 n + 1 n + 1
221 172 nncnd n 2 n + 1
222 214 197 221 215 198 216 divmul24d n 4 n 2 n 2 n + 1 n + 1 = 4 n 2 n + 1 2 n + 1 n
223 162 rpcnd n 4 n n
224 176 rpcnd n 2 n + 1 n + 1
225 223 200 224 mulassd n 4 n n 2 2 n + 1 n + 1 = 4 n n 2 2 n + 1 n + 1
226 220 222 225 3eqtr3rd n 4 n n 2 2 n + 1 n + 1 = 4 n 2 n + 1 2 n + 1 n
227 205 218 226 3brtr4d n 4 n + 1 n + 1 < 4 n n 2 2 n + 1 n + 1
228 174 nnnn0d n n + 1 0
229 nnexpcl 4 n + 1 0 4 n + 1
230 154 228 229 sylancr n 4 n + 1
231 230 nnrpd n 4 n + 1 +
232 231 175 rpdivcld n 4 n + 1 n + 1 +
233 232 rpred n 4 n + 1 n + 1
234 178 rpred n 2 2 n + 1 n + 1
235 163 234 remulcld n 4 n n 2 2 n + 1 n + 1
236 nn0mulcl 2 0 n + 1 0 2 n + 1 0
237 33 228 236 sylancr n 2 n + 1 0
238 174 nnzd n n + 1
239 bccl 2 n + 1 0 n + 1 ( 2 n + 1 n + 1 ) 0
240 237 238 239 syl2anc n ( 2 n + 1 n + 1 ) 0
241 240 nn0red n ( 2 n + 1 n + 1 )
242 lttr 4 n + 1 n + 1 4 n n 2 2 n + 1 n + 1 ( 2 n + 1 n + 1 ) 4 n + 1 n + 1 < 4 n n 2 2 n + 1 n + 1 4 n n 2 2 n + 1 n + 1 < ( 2 n + 1 n + 1 ) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
243 233 235 241 242 syl3anc n 4 n + 1 n + 1 < 4 n n 2 2 n + 1 n + 1 4 n n 2 2 n + 1 n + 1 < ( 2 n + 1 n + 1 ) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
244 227 243 mpand n 4 n n 2 2 n + 1 n + 1 < ( 2 n + 1 n + 1 ) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
245 183 244 sylbid n 4 n n < ( 2 n n) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
246 156 245 syl n 4 4 n n < ( 2 n n) 4 n + 1 n + 1 < ( 2 n + 1 n + 1 )
247 6 12 18 24 153 246 uzind4i N 4 4 N N < ( 2 N N)