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

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

Proof of Theorem bposlem1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fzfid 11736 . . . 4
2 2nn 10425 . . . . . . . . . . 11
3 nnmulcl 10291 . . . . . . . . . . 11
42, 3mpan 655 . . . . . . . . . 10
54ad2antrr 710 . . . . . . . . 9
6 prmnn 13706 . . . . . . . . . . 11
76ad2antlr 711 . . . . . . . . . 10
8 elfznn 11422 . . . . . . . . . . . 12
98adantl 456 . . . . . . . . . . 11
109nnnn0d 10581 . . . . . . . . . 10
117, 10nnexpcld 11970 . . . . . . . . 9
12 nnrp 10945 . . . . . . . . . 10
13 nnrp 10945 . . . . . . . . . 10
14 rpdivcl 10958 . . . . . . . . . 10
1512, 13, 14syl2an 467 . . . . . . . . 9
165, 11, 15syl2anc 646 . . . . . . . 8
1716rpred 10972 . . . . . . 7
1817flcld 11589 . . . . . 6
19 2z 10623 . . . . . . 7
20 simpll 738 . . . . . . . . . 10
21 nnrp 10945 . . . . . . . . . . 11
22 rpdivcl 10958 . . . . . . . . . . 11
2321, 13, 22syl2an 467 . . . . . . . . . 10
2420, 11, 23syl2anc 646 . . . . . . . . 9
2524rpred 10972 . . . . . . . 8
2625flcld 11589 . . . . . . 7
27 zmulcl 10638 . . . . . . 7
2819, 26, 27sylancr 648 . . . . . 6
2918, 28zsubcld 10697 . . . . 5
3029zred 10692 . . . 4
31 1re 9331 . . . . . 6
32 0re 9332 . . . . . 6
3331, 32keepel 3834 . . . . 5
3433a1i 11 . . . 4
3528zred 10692 . . . . . . . . . 10
3617, 35resubcld 9722 . . . . . . . . 9
37 2re 10337 . . . . . . . . . 10
3837a1i 11 . . . . . . . . 9
3918zred 10692 . . . . . . . . . 10
40 flle 11590 . . . . . . . . . . 11
4117, 40syl 16 . . . . . . . . . 10
4239, 17, 35, 41lesub1dd 9901 . . . . . . . . 9
43 resubcl 9619 . . . . . . . . . . . . 13
4425, 31, 43sylancl 647 . . . . . . . . . . . 12
45 remulcl 9313 . . . . . . . . . . . 12
4637, 44, 45sylancr 648 . . . . . . . . . . 11
47 flltp1 11591 . . . . . . . . . . . . . 14
4825, 47syl 16 . . . . . . . . . . . . 13
49 1red 9347 . . . . . . . . . . . . . 14
5026zred 10692 . . . . . . . . . . . . . 14
5125, 49, 50ltsubaddd 9881 . . . . . . . . . . . . 13
5248, 51mpbird 226 . . . . . . . . . . . 12
53 2pos 10359 . . . . . . . . . . . . . . 15
5437, 53pm3.2i 445 . . . . . . . . . . . . . 14
55 ltmul2 10126 . . . . . . . . . . . . . 14
5654, 55mp3an3 1288 . . . . . . . . . . . . 13
5744, 50, 56syl2anc 646 . . . . . . . . . . . 12
5852, 57mpbid 204 . . . . . . . . . . 11
5946, 35, 17, 58ltsub2dd 9898 . . . . . . . . . 10
60 2cnd 10340 . . . . . . . . . . . . 13
61 nncn 10276 . . . . . . . . . . . . . 14
6261ad2antrr 710 . . . . . . . . . . . . 13
6311nncnd 10284 . . . . . . . . . . . . 13
6411nnne0d 10312 . . . . . . . . . . . . 13
6560, 62, 63, 64divassd 10088 . . . . . . . . . . . 12
6625recnd 9358 . . . . . . . . . . . . . 14
67 1cnd 9348 . . . . . . . . . . . . . 14
6860, 66, 67subdid 9746 . . . . . . . . . . . . 13
69 2t1e2 10416 . . . . . . . . . . . . . 14
7069oveq2i 6072 . . . . . . . . . . . . 13
7168, 70syl6eq 2470 . . . . . . . . . . . 12
7265, 71oveq12d 6079 . . . . . . . . . . 11
73 remulcl 9313 . . . . . . . . . . . . . 14
7437, 25, 73sylancr 648 . . . . . . . . . . . . 13
7574recnd 9358 . . . . . . . . . . . 12
76 2cn 10338 . . . . . . . . . . . 12
77 nncan 9584 . . . . . . . . . . . 12
7875, 76, 77sylancl 647 . . . . . . . . . . 11
7972, 78eqtrd 2454 . . . . . . . . . 10
8059, 79breqtrd 4291 . . . . . . . . 9
8130, 36, 38, 42, 80lelttrd 9475 . . . . . . . 8
82 df-2 10326 . . . . . . . 8
8381, 82syl6breq 4306 . . . . . . 7
84 1z 10621 . . . . . . . 8
85 zleltp1 10640 . . . . . . . 8
8629, 84, 85sylancl 647 . . . . . . 7
8783, 86mpbird 226 . . . . . 6
88 iftrue 3774 . . . . . . 7
8988breq2d 4279 . . . . . 6
9087, 89syl5ibrcom 216 . . . . 5
919nnge1d 10310 . . . . . . . . . . 11
9291biantrurd 498 . . . . . . . . . 10
936adantl 456 . . . . . . . . . . . . . 14
9493nnred 10283 . . . . . . . . . . . . 13
95 prmuz2 13721 . . . . . . . . . . . . . . 15
9695adantl 456 . . . . . . . . . . . . . 14
97 eluz2b1 10871 . . . . . . . . . . . . . . 15
9897simprbi 454 . . . . . . . . . . . . . 14
9996, 98syl 16 . . . . . . . . . . . . 13
10094, 99jca 522 . . . . . . . . . . . 12
101100adantr 455 . . . . . . . . . . 11
102 elfzelz 11397 . . . . . . . . . . . 12
103102adantl 456 . . . . . . . . . . 11
1044adantr 455 . . . . . . . . . . . . 13
105104nnrpd 10971 . . . . . . . . . . . 12
106105adantr 455 . . . . . . . . . . 11
107 efexple 22361 . . . . . . . . . . 11
108101, 103, 106, 107syl3anc 1203 . . . . . . . . . 10
1099nnzd 10691 . . . . . . . . . . 11
11084a1i 11 . . . . . . . . . . 11
111104nnred 10283 . . . . . . . . . . . . . . . 16
112 1red 9347 . . . . . . . . . . . . . . . . 17
11337a1i 11 . . . . . . . . . . . . . . . . 17
114 1lt2 10434 . . . . . . . . . . . . . . . . . 18
115114a1i 11 . . . . . . . . . . . . . . . . 17
116 nnre 10275 . . . . . . . . . . . . . . . . . . . 20
117116adantr 455 . . . . . . . . . . . . . . . . . . 19
118 0le2 10358 . . . . . . . . . . . . . . . . . . . . 21
11937, 118pm3.2i 445 . . . . . . . . . . . . . . . . . . . 20
120119a1i 11 . . . . . . . . . . . . . . . . . . 19
121 nnge1 10294 . . . . . . . . . . . . . . . . . . . 20
122121adantr 455 . . . . . . . . . . . . . . . . . . 19
123 lemul2a 10130 . . . . . . . . . . . . . . . . . . 19
124112, 117, 120, 122, 123syl31anc 1206 . . . . . . . . . . . . . . . . . 18
12569, 124syl5eqbrr 4301 . . . . . . . . . . . . . . . . 17
126112, 113, 111, 115, 125ltletrd 9477 . . . . . . . . . . . . . . . 16
127111, 126rplogcld 21819 . . . . . . . . . . . . . . 15
12894, 99rplogcld 21819 . . . . . . . . . . . . . . 15
129127, 128rpdivcld 10989 . . . . . . . . . . . . . 14
130129rpred 10972 . . . . . . . . . . . . 13
131130flcld 11589 . . . . . . . . . . . 12
132131adantr 455 . . . . . . . . . . 11
133 elfz 11387 . . . . . . . . . . 11
134109, 110, 132, 133syl3anc 1203 . . . . . . . . . 10
13592, 108, 1343bitr4rd 280 . . . . . . . . 9
136135notbid 288 . . . . . . . 8
137111adantr 455 . . . . . . . . 9
13811nnred 10283 . . . . . . . . 9
139137, 138ltnled 9467 . . . . . . . 8
140136, 139bitr4d 250 . . . . . . 7
14116rpge0d 10976 . . . . . . . . . . . . 13
142141adantrr 701 . . . . . . . . . . . 12
14311nngt0d 10311 . . . . . . . . . . . . . . . . 17
144 ltdivmul 10150 . . . . . . . . . . . . . . . . 17
145137, 49, 138, 143, 144syl112anc 1207 . . . . . . . . . . . . . . . 16
14663mulid1d 9349 . . . . . . . . . . . . . . . . 17
147146breq2d 4279 . . . . . . . . . . . . . . . 16
148145, 147bitrd 247 . . . . . . . . . . . . . . 15
149148biimprd 217 . . . . . . . . . . . . . 14
150149impr 606 . . . . . . . . . . . . 13
151 0p1e1 10379 . . . . . . . . . . . . 13
152150, 151syl6breqr 4307 . . . . . . . . . . . 12
15317adantrr 701 . . . . . . . . . . . . 13
154 0z 10602 . . . . . . . . . . . . 13
155 flbi 11605 . . . . . . . . . . . . 13
156153, 154, 155sylancl 647 . . . . . . . . . . . 12
157142, 152, 156mpbir2and 898 . . . . . . . . . . 11
15824rpge0d 10976 . . . . . . . . . . . . . . 15
159158adantrr 701 . . . . . . . . . . . . . 14
160116, 21ltaddrp2d 11002 . . . . . . . . . . . . . . . . . . . 20
161612timesd 10513 . . . . . . . . . . . . . . . . . . . 20
162160, 161breqtrrd 4293 . . . . . . . . . . . . . . . . . . 19
163162ad2antrr 710 . . . . . . . . . . . . . . . . . 18
164116ad2antrr 710 . . . . . . . . . . . . . . . . . . 19
165 lttr 9397 . . . . . . . . . . . . . . . . . . 19
166164, 137, 138, 165syl3anc 1203 . . . . . . . . . . . . . . . . . 18
167163, 166mpand 660 . . . . . . . . . . . . . . . . 17
168 ltdivmul 10150 . . . . . . . . . . . . . . . . . . 19
169164, 49, 138, 143, 168syl112anc 1207 . . . . . . . . . . . . . . . . . 18
170146breq2d 4279 . . . . . . . . . . . . . . . . . 18
171169, 170bitrd 247 . . . . . . . . . . . . . . . . 17
172167, 171sylibrd 228 . . . . . . . . . . . . . . . 16
173172impr 606 . . . . . . . . . . . . . . 15
174173, 151syl6breqr 4307 . . . . . . . . . . . . . 14
17525adantrr 701 . . . . . . . . . . . . . . 15
176 flbi 11605 . . . . . . . . . . . . . . 15
177175, 154, 176sylancl 647 . . . . . . . . . . . . . 14
178159, 174, 177mpbir2and 898 . . . . . . . . . . . . 13
179178oveq2d 6077 . . . . . . . . . . . 12
180 2t0e0 10423 . . . . . . . . . . . 12
181179, 180syl6eq 2470 . . . . . . . . . . 11
182157, 181oveq12d 6079 . . . . . . . . . 10
183 0m0e0 10377 . . . . . . . . . 10
184182, 183syl6eq 2470 . . . . . . . . 9
185 0le0 10357 . . . . . . . . 9
186184, 185syl6eqbr 4304 . . . . . . . 8
187186expr 602 . . . . . . 7
188140, 187sylbid 209 . . . . . 6
189 iffalse 3776 . . . . . . . 8
190189eqcomd 2427 . . . . . . 7
191190breq2d 4279 . . . . . 6
192188, 191mpbidi 210 . . . . 5
19390, 192pm2.61d 153 . . . 4
1941, 30, 34, 193fsumle 13202 . . 3
195 pcbcctr 22356 . . 3
196131zred 10692 . . . . . . . 8
197 flle 11590 . . . . . . . . 9
198130, 197syl 16 . . . . . . . 8
199104nnnn0d 10581 . . . . . . . . . . . . . 14
20093, 199nnexpcld 11970 . . . . . . . . . . . . 13
201200nnred 10283 . . . . . . . . . . . 12