Metamath Proof Explorer


Theorem bposlem1

Description: An upper bound on the prime powers dividing a central binomial coefficient. (Contributed by Mario Carneiro, 9-Mar-2014)

Ref Expression
Assertion bposlem1 N P P P pCnt ( 2 N N) 2 N

Proof

Step Hyp Ref Expression
1 fzfid N P 1 2 N Fin
2 2nn 2
3 nnmulcl 2 N 2 N
4 2 3 mpan N 2 N
5 4 ad2antrr N P k 1 2 N 2 N
6 prmnn P P
7 6 ad2antlr N P k 1 2 N P
8 elfznn k 1 2 N k
9 8 adantl N P k 1 2 N k
10 9 nnnn0d N P k 1 2 N k 0
11 7 10 nnexpcld N P k 1 2 N P k
12 nnrp 2 N 2 N +
13 nnrp P k P k +
14 rpdivcl 2 N + P k + 2 N P k +
15 12 13 14 syl2an 2 N P k 2 N P k +
16 5 11 15 syl2anc N P k 1 2 N 2 N P k +
17 16 rpred N P k 1 2 N 2 N P k
18 17 flcld N P k 1 2 N 2 N P k
19 2z 2
20 simpll N P k 1 2 N N
21 nnrp N N +
22 rpdivcl N + P k + N P k +
23 21 13 22 syl2an N P k N P k +
24 20 11 23 syl2anc N P k 1 2 N N P k +
25 24 rpred N P k 1 2 N N P k
26 25 flcld N P k 1 2 N N P k
27 zmulcl 2 N P k 2 N P k
28 19 26 27 sylancr N P k 1 2 N 2 N P k
29 18 28 zsubcld N P k 1 2 N 2 N P k 2 N P k
30 29 zred N P k 1 2 N 2 N P k 2 N P k
31 1re 1
32 0re 0
33 31 32 ifcli if k 1 log 2 N log P 1 0
34 33 a1i N P k 1 2 N if k 1 log 2 N log P 1 0
35 28 zred N P k 1 2 N 2 N P k
36 17 35 resubcld N P k 1 2 N 2 N P k 2 N P k
37 2re 2
38 37 a1i N P k 1 2 N 2
39 18 zred N P k 1 2 N 2 N P k
40 flle 2 N P k 2 N P k 2 N P k
41 17 40 syl N P k 1 2 N 2 N P k 2 N P k
42 39 17 35 41 lesub1dd N P k 1 2 N 2 N P k 2 N P k 2 N P k 2 N P k
43 resubcl N P k 1 N P k 1
44 25 31 43 sylancl N P k 1 2 N N P k 1
45 remulcl 2 N P k 1 2 N P k 1
46 37 44 45 sylancr N P k 1 2 N 2 N P k 1
47 flltp1 N P k N P k < N P k + 1
48 25 47 syl N P k 1 2 N N P k < N P k + 1
49 1red N P k 1 2 N 1
50 26 zred N P k 1 2 N N P k
51 25 49 50 ltsubaddd N P k 1 2 N N P k 1 < N P k N P k < N P k + 1
52 48 51 mpbird N P k 1 2 N N P k 1 < N P k
53 2pos 0 < 2
54 37 53 pm3.2i 2 0 < 2
55 ltmul2 N P k 1 N P k 2 0 < 2 N P k 1 < N P k 2 N P k 1 < 2 N P k
56 54 55 mp3an3 N P k 1 N P k N P k 1 < N P k 2 N P k 1 < 2 N P k
57 44 50 56 syl2anc N P k 1 2 N N P k 1 < N P k 2 N P k 1 < 2 N P k
58 52 57 mpbid N P k 1 2 N 2 N P k 1 < 2 N P k
59 46 35 17 58 ltsub2dd N P k 1 2 N 2 N P k 2 N P k < 2 N P k 2 N P k 1
60 2cnd N P k 1 2 N 2
61 nncn N N
62 61 ad2antrr N P k 1 2 N N
63 11 nncnd N P k 1 2 N P k
64 11 nnne0d N P k 1 2 N P k 0
65 60 62 63 64 divassd N P k 1 2 N 2 N P k = 2 N P k
66 25 recnd N P k 1 2 N N P k
67 60 66 muls1d N P k 1 2 N 2 N P k 1 = 2 N P k 2
68 65 67 oveq12d N P k 1 2 N 2 N P k 2 N P k 1 = 2 N P k 2 N P k 2
69 remulcl 2 N P k 2 N P k
70 37 25 69 sylancr N P k 1 2 N 2 N P k
71 70 recnd N P k 1 2 N 2 N P k
72 2cn 2
73 nncan 2 N P k 2 2 N P k 2 N P k 2 = 2
74 71 72 73 sylancl N P k 1 2 N 2 N P k 2 N P k 2 = 2
75 68 74 eqtrd N P k 1 2 N 2 N P k 2 N P k 1 = 2
76 59 75 breqtrd N P k 1 2 N 2 N P k 2 N P k < 2
77 30 36 38 42 76 lelttrd N P k 1 2 N 2 N P k 2 N P k < 2
78 df-2 2 = 1 + 1
79 77 78 breqtrdi N P k 1 2 N 2 N P k 2 N P k < 1 + 1
80 1z 1
81 zleltp1 2 N P k 2 N P k 1 2 N P k 2 N P k 1 2 N P k 2 N P k < 1 + 1
82 29 80 81 sylancl N P k 1 2 N 2 N P k 2 N P k 1 2 N P k 2 N P k < 1 + 1
83 79 82 mpbird N P k 1 2 N 2 N P k 2 N P k 1
84 iftrue k 1 log 2 N log P if k 1 log 2 N log P 1 0 = 1
85 84 breq2d k 1 log 2 N log P 2 N P k 2 N P k if k 1 log 2 N log P 1 0 2 N P k 2 N P k 1
86 83 85 syl5ibrcom N P k 1 2 N k 1 log 2 N log P 2 N P k 2 N P k if k 1 log 2 N log P 1 0
87 9 nnge1d N P k 1 2 N 1 k
88 87 biantrurd N P k 1 2 N k log 2 N log P 1 k k log 2 N log P
89 6 adantl N P P
90 89 nnred N P P
91 prmuz2 P P 2
92 91 adantl N P P 2
93 eluz2gt1 P 2 1 < P
94 92 93 syl N P 1 < P
95 90 94 jca N P P 1 < P
96 95 adantr N P k 1 2 N P 1 < P
97 elfzelz k 1 2 N k
98 97 adantl N P k 1 2 N k
99 4 adantr N P 2 N
100 99 nnrpd N P 2 N +
101 100 adantr N P k 1 2 N 2 N +
102 efexple P 1 < P k 2 N + P k 2 N k log 2 N log P
103 96 98 101 102 syl3anc N P k 1 2 N P k 2 N k log 2 N log P
104 9 nnzd N P k 1 2 N k
105 80 a1i N P k 1 2 N 1
106 99 nnred N P 2 N
107 1red N P 1
108 37 a1i N P 2
109 1lt2 1 < 2
110 109 a1i N P 1 < 2
111 2t1e2 2 1 = 2
112 nnre N N
113 112 adantr N P N
114 0le2 0 2
115 37 114 pm3.2i 2 0 2
116 115 a1i N P 2 0 2
117 nnge1 N 1 N
118 117 adantr N P 1 N
119 lemul2a 1 N 2 0 2 1 N 2 1 2 N
120 107 113 116 118 119 syl31anc N P 2 1 2 N
121 111 120 eqbrtrrid N P 2 2 N
122 107 108 106 110 121 ltletrd N P 1 < 2 N
123 106 122 rplogcld N P log 2 N +
124 90 94 rplogcld N P log P +
125 123 124 rpdivcld N P log 2 N log P +
126 125 rpred N P log 2 N log P
127 126 flcld N P log 2 N log P
128 127 adantr N P k 1 2 N log 2 N log P
129 elfz k 1 log 2 N log P k 1 log 2 N log P 1 k k log 2 N log P
130 104 105 128 129 syl3anc N P k 1 2 N k 1 log 2 N log P 1 k k log 2 N log P
131 88 103 130 3bitr4rd N P k 1 2 N k 1 log 2 N log P P k 2 N
132 131 notbid N P k 1 2 N ¬ k 1 log 2 N log P ¬ P k 2 N
133 106 adantr N P k 1 2 N 2 N
134 11 nnred N P k 1 2 N P k
135 133 134 ltnled N P k 1 2 N 2 N < P k ¬ P k 2 N
136 132 135 bitr4d N P k 1 2 N ¬ k 1 log 2 N log P 2 N < P k
137 16 rpge0d N P k 1 2 N 0 2 N P k
138 137 adantrr N P k 1 2 N 2 N < P k 0 2 N P k
139 11 nngt0d N P k 1 2 N 0 < P k
140 ltdivmul 2 N 1 P k 0 < P k 2 N P k < 1 2 N < P k 1
141 133 49 134 139 140 syl112anc N P k 1 2 N 2 N P k < 1 2 N < P k 1
142 63 mulid1d N P k 1 2 N P k 1 = P k
143 142 breq2d N P k 1 2 N 2 N < P k 1 2 N < P k
144 141 143 bitrd N P k 1 2 N 2 N P k < 1 2 N < P k
145 144 biimprd N P k 1 2 N 2 N < P k 2 N P k < 1
146 145 impr N P k 1 2 N 2 N < P k 2 N P k < 1
147 0p1e1 0 + 1 = 1
148 146 147 breqtrrdi N P k 1 2 N 2 N < P k 2 N P k < 0 + 1
149 17 adantrr N P k 1 2 N 2 N < P k 2 N P k
150 0z 0
151 flbi 2 N P k 0 2 N P k = 0 0 2 N P k 2 N P k < 0 + 1
152 149 150 151 sylancl N P k 1 2 N 2 N < P k 2 N P k = 0 0 2 N P k 2 N P k < 0 + 1
153 138 148 152 mpbir2and N P k 1 2 N 2 N < P k 2 N P k = 0
154 24 rpge0d N P k 1 2 N 0 N P k
155 154 adantrr N P k 1 2 N 2 N < P k 0 N P k
156 112 21 ltaddrp2d N N < N + N
157 61 2timesd N 2 N = N + N
158 156 157 breqtrrd N N < 2 N
159 158 ad2antrr N P k 1 2 N N < 2 N
160 112 ad2antrr N P k 1 2 N N
161 lttr N 2 N P k N < 2 N 2 N < P k N < P k
162 160 133 134 161 syl3anc N P k 1 2 N N < 2 N 2 N < P k N < P k
163 159 162 mpand N P k 1 2 N 2 N < P k N < P k
164 ltdivmul N 1 P k 0 < P k N P k < 1 N < P k 1
165 160 49 134 139 164 syl112anc N P k 1 2 N N P k < 1 N < P k 1
166 142 breq2d N P k 1 2 N N < P k 1 N < P k
167 165 166 bitrd N P k 1 2 N N P k < 1 N < P k
168 163 167 sylibrd N P k 1 2 N 2 N < P k N P k < 1
169 168 impr N P k 1 2 N 2 N < P k N P k < 1
170 169 147 breqtrrdi N P k 1 2 N 2 N < P k N P k < 0 + 1
171 25 adantrr N P k 1 2 N 2 N < P k N P k
172 flbi N P k 0 N P k = 0 0 N P k N P k < 0 + 1
173 171 150 172 sylancl N P k 1 2 N 2 N < P k N P k = 0 0 N P k N P k < 0 + 1
174 155 170 173 mpbir2and N P k 1 2 N 2 N < P k N P k = 0
175 174 oveq2d N P k 1 2 N 2 N < P k 2 N P k = 2 0
176 2t0e0 2 0 = 0
177 175 176 syl6eq N P k 1 2 N 2 N < P k 2 N P k = 0
178 153 177 oveq12d N P k 1 2 N 2 N < P k 2 N P k 2 N P k = 0 0
179 0m0e0 0 0 = 0
180 178 179 syl6eq N P k 1 2 N 2 N < P k 2 N P k 2 N P k = 0
181 0le0 0 0
182 180 181 eqbrtrdi N P k 1 2 N 2 N < P k 2 N P k 2 N P k 0
183 182 expr N P k 1 2 N 2 N < P k 2 N P k 2 N P k 0
184 136 183 sylbid N P k 1 2 N ¬ k 1 log 2 N log P 2 N P k 2 N P k 0
185 iffalse ¬ k 1 log 2 N log P if k 1 log 2 N log P 1 0 = 0
186 185 eqcomd ¬ k 1 log 2 N log P 0 = if k 1 log 2 N log P 1 0
187 186 breq2d ¬ k 1 log 2 N log P 2 N P k 2 N P k 0 2 N P k 2 N P k if k 1 log 2 N log P 1 0
188 184 187 mpbidi N P k 1 2 N ¬ k 1 log 2 N log P 2 N P k 2 N P k if k 1 log 2 N log P 1 0
189 86 188 pm2.61d N P k 1 2 N 2 N P k 2 N P k if k 1 log 2 N log P 1 0
190 1 30 34 189 fsumle N P k = 1 2 N 2 N P k 2 N P k k = 1 2 N if k 1 log 2 N log P 1 0
191 pcbcctr N P P pCnt ( 2 N N) = k = 1 2 N 2 N P k 2 N P k
192 127 zred N P log 2 N log P
193 flle log 2 N log P log 2 N log P log 2 N log P
194 126 193 syl N P log 2 N log P log 2 N log P
195 99 nnnn0d N P 2 N 0
196 89 195 nnexpcld N P P 2 N
197 196 nnred N P P 2 N
198 bernneq3 P 2 2 N 0 2 N < P 2 N
199 92 195 198 syl2anc N P 2 N < P 2 N
200 106 197 199 ltled N P 2 N P 2 N
201 100 reeflogd N P e log 2 N = 2 N
202 89 nnrpd N P P +
203 99 nnzd N P 2 N
204 reexplog P + 2 N P 2 N = e 2 N log P
205 202 203 204 syl2anc N P P 2 N = e 2 N log P
206 205 eqcomd N P e 2 N log P = P 2 N
207 200 201 206 3brtr4d N P e log 2 N e 2 N log P
208 100 relogcld N P log 2 N
209 124 rpred N P log P
210 106 209 remulcld N P 2 N log P
211 efle log 2 N 2 N log P log 2 N 2 N log P e log 2 N e 2 N log P
212 208 210 211 syl2anc N P log 2 N 2 N log P e log 2 N e 2 N log P
213 207 212 mpbird N P log 2 N 2 N log P
214 208 106 124 ledivmul2d N P log 2 N log P 2 N log 2 N 2 N log P
215 213 214 mpbird N P log 2 N log P 2 N
216 192 126 106 194 215 letrd N P log 2 N log P 2 N
217 eluz log 2 N log P 2 N 2 N log 2 N log P log 2 N log P 2 N
218 127 203 217 syl2anc N P 2 N log 2 N log P log 2 N log P 2 N
219 216 218 mpbird N P 2 N log 2 N log P
220 fzss2 2 N log 2 N log P 1 log 2 N log P 1 2 N
221 219 220 syl N P 1 log 2 N log P 1 2 N
222 sumhash 1 2 N Fin 1 log 2 N log P 1 2 N k = 1 2 N if k 1 log 2 N log P 1 0 = 1 log 2 N log P
223 1 221 222 syl2anc N P k = 1 2 N if k 1 log 2 N log P 1 0 = 1 log 2 N log P
224 125 rprege0d N P log 2 N log P 0 log 2 N log P
225 flge0nn0 log 2 N log P 0 log 2 N log P log 2 N log P 0
226 hashfz1 log 2 N log P 0 1 log 2 N log P = log 2 N log P
227 224 225 226 3syl N P 1 log 2 N log P = log 2 N log P
228 223 227 eqtr2d N P log 2 N log P = k = 1 2 N if k 1 log 2 N log P 1 0
229 190 191 228 3brtr4d N P P pCnt ( 2 N N) log 2 N log P
230 simpr N P P
231 nnnn0 N N 0
232 fzctr N 0 N 0 2 N
233 bccl2 N 0 2 N ( 2 N N)
234 231 232 233 3syl N ( 2 N N)
235 234 adantr N P ( 2 N N)
236 230 235 pccld N P P pCnt ( 2 N N) 0
237 236 nn0zd N P P pCnt ( 2 N N)
238 efexple P 1 < P P pCnt ( 2 N N) 2 N + P P pCnt ( 2 N N) 2 N P pCnt ( 2 N N) log 2 N log P
239 90 94 237 100 238 syl211anc N P P P pCnt ( 2 N N) 2 N P pCnt ( 2 N N) log 2 N log P
240 229 239 mpbird N P P P pCnt ( 2 N N) 2 N