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

Theorem bposlem1 23023
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 11940 . . . 4
2 2nn 10617 . . . . . . . . . . 11
3 nnmulcl 10483 . . . . . . . . . . 11
42, 3mpan 670 . . . . . . . . . 10
54ad2antrr 725 . . . . . . . . 9
6 prmnn 13924 . . . . . . . . . . 11
76ad2antlr 726 . . . . . . . . . 10
8 elfznn 11623 . . . . . . . . . . . 12
98adantl 466 . . . . . . . . . . 11
109nnnn0d 10774 . . . . . . . . . 10
117, 10nnexpcld 12186 . . . . . . . . 9
12 nnrp 11139 . . . . . . . . . 10
13 nnrp 11139 . . . . . . . . . 10
14 rpdivcl 11152 . . . . . . . . . 10
1512, 13, 14syl2an 477 . . . . . . . . 9
165, 11, 15syl2anc 661 . . . . . . . 8
1716rpred 11166 . . . . . . 7
1817flcld 11793 . . . . . 6
19 2z 10816 . . . . . . 7
20 simpll 753 . . . . . . . . . 10
21 nnrp 11139 . . . . . . . . . . 11
22 rpdivcl 11152 . . . . . . . . . . 11
2321, 13, 22syl2an 477 . . . . . . . . . 10
2420, 11, 23syl2anc 661 . . . . . . . . 9
2524rpred 11166 . . . . . . . 8
2625flcld 11793 . . . . . . 7
27 zmulcl 10831 . . . . . . 7
2819, 26, 27sylancr 663 . . . . . 6
2918, 28zsubcld 10890 . . . . 5
3029zred 10885 . . . 4
31 1re 9522 . . . . . 6
32 0re 9523 . . . . . 6
3331, 32keepel 3973 . . . . 5
3433a1i 11 . . . 4
3528zred 10885 . . . . . . . . . 10
3617, 35resubcld 9913 . . . . . . . . 9
37 2re 10529 . . . . . . . . . 10
3837a1i 11 . . . . . . . . 9
3918zred 10885 . . . . . . . . . 10
40 flle 11794 . . . . . . . . . . 11
4117, 40syl 16 . . . . . . . . . 10
4239, 17, 35, 41lesub1dd 10092 . . . . . . . . 9
43 resubcl 9810 . . . . . . . . . . . . 13
4425, 31, 43sylancl 662 . . . . . . . . . . . 12
45 remulcl 9504 . . . . . . . . . . . 12
4637, 44, 45sylancr 663 . . . . . . . . . . 11
47 flltp1 11795 . . . . . . . . . . . . . 14
4825, 47syl 16 . . . . . . . . . . . . 13
49 1red 9538 . . . . . . . . . . . . . 14
5026zred 10885 . . . . . . . . . . . . . 14
5125, 49, 50ltsubaddd 10072 . . . . . . . . . . . . 13
5248, 51mpbird 232 . . . . . . . . . . . 12
53 2pos 10551 . . . . . . . . . . . . . . 15
5437, 53pm3.2i 455 . . . . . . . . . . . . . 14
55 ltmul2 10317 . . . . . . . . . . . . . 14
5654, 55mp3an3 1304 . . . . . . . . . . . . 13
5744, 50, 56syl2anc 661 . . . . . . . . . . . 12
5852, 57mpbid 210 . . . . . . . . . . 11
5946, 35, 17, 58ltsub2dd 10089 . . . . . . . . . 10
60 2cnd 10532 . . . . . . . . . . . . 13
61 nncn 10468 . . . . . . . . . . . . . 14
6261ad2antrr 725 . . . . . . . . . . . . 13
6311nncnd 10476 . . . . . . . . . . . . 13
6411nnne0d 10504 . . . . . . . . . . . . 13
6560, 62, 63, 64divassd 10279 . . . . . . . . . . . 12
6625recnd 9549 . . . . . . . . . . . . . 14
67 1cnd 9539 . . . . . . . . . . . . . 14
6860, 66, 67subdid 9937 . . . . . . . . . . . . 13
69 2t1e2 10608 . . . . . . . . . . . . . 14
7069oveq2i 6233 . . . . . . . . . . . . 13
7168, 70syl6eq 2511 . . . . . . . . . . . 12
7265, 71oveq12d 6240 . . . . . . . . . . 11
73 remulcl 9504 . . . . . . . . . . . . . 14
7437, 25, 73sylancr 663 . . . . . . . . . . . . 13
7574recnd 9549 . . . . . . . . . . . 12
76 2cn 10530 . . . . . . . . . . . 12
77 nncan 9775 . . . . . . . . . . . 12
7875, 76, 77sylancl 662 . . . . . . . . . . 11
7972, 78eqtrd 2495 . . . . . . . . . 10
8059, 79breqtrd 4433 . . . . . . . . 9
8130, 36, 38, 42, 80lelttrd 9666 . . . . . . . 8
82 df-2 10518 . . . . . . . 8
8381, 82syl6breq 4448 . . . . . . 7
84 1z 10814 . . . . . . . 8
85 zleltp1 10833 . . . . . . . 8
8629, 84, 85sylancl 662 . . . . . . 7
8783, 86mpbird 232 . . . . . 6
88 iftrue 3911 . . . . . . 7
8988breq2d 4421 . . . . . 6
9087, 89syl5ibrcom 222 . . . . 5
919nnge1d 10502 . . . . . . . . . . 11
9291biantrurd 508 . . . . . . . . . 10
936adantl 466 . . . . . . . . . . . . . 14
9493nnred 10475 . . . . . . . . . . . . 13
95 prmuz2 13939 . . . . . . . . . . . . . . 15
9695adantl 466 . . . . . . . . . . . . . 14
97 eluz2b1 11065 . . . . . . . . . . . . . . 15
9897simprbi 464 . . . . . . . . . . . . . 14
9996, 98syl 16 . . . . . . . . . . . . 13
10094, 99jca 532 . . . . . . . . . . . 12
101100adantr 465 . . . . . . . . . . 11
102 elfzelz 11598 . . . . . . . . . . . 12
103102adantl 466 . . . . . . . . . . 11
1044adantr 465 . . . . . . . . . . . . 13
105104nnrpd 11165 . . . . . . . . . . . 12
106105adantr 465 . . . . . . . . . . 11
107 efexple 23020 . . . . . . . . . . 11
108101, 103, 106, 107syl3anc 1219 . . . . . . . . . 10
1099nnzd 10884 . . . . . . . . . . 11
11084a1i 11 . . . . . . . . . . 11
111104nnred 10475 . . . . . . . . . . . . . . . 16
112 1red 9538 . . . . . . . . . . . . . . . . 17
11337a1i 11 . . . . . . . . . . . . . . . . 17
114 1lt2 10626 . . . . . . . . . . . . . . . . . 18
115114a1i 11 . . . . . . . . . . . . . . . . 17
116 nnre 10467 . . . . . . . . . . . . . . . . . . . 20
117116adantr 465 . . . . . . . . . . . . . . . . . . 19
118 0le2 10550 . . . . . . . . . . . . . . . . . . . . 21
11937, 118pm3.2i 455 . . . . . . . . . . . . . . . . . . . 20
120119a1i 11 . . . . . . . . . . . . . . . . . . 19
121 nnge1 10486 . . . . . . . . . . . . . . . . . . . 20
122121adantr 465 . . . . . . . . . . . . . . . . . . 19
123 lemul2a 10321 . . . . . . . . . . . . . . . . . . 19
124112, 117, 120, 122, 123syl31anc 1222 . . . . . . . . . . . . . . . . . 18
12569, 124syl5eqbrr 4443 . . . . . . . . . . . . . . . . 17
126112, 113, 111, 115, 125ltletrd 9668 . . . . . . . . . . . . . . . 16
127111, 126rplogcld 22478 . . . . . . . . . . . . . . 15
12894, 99rplogcld 22478 . . . . . . . . . . . . . . 15
129127, 128rpdivcld 11183 . . . . . . . . . . . . . 14
130129rpred 11166 . . . . . . . . . . . . 13
131130flcld 11793 . . . . . . . . . . . 12
132131adantr 465 . . . . . . . . . . 11
133 elfz 11588 . . . . . . . . . . 11
134109, 110, 132, 133syl3anc 1219 . . . . . . . . . 10
13592, 108, 1343bitr4rd 286 . . . . . . . . 9
136135notbid 294 . . . . . . . 8
137111adantr 465 . . . . . . . . 9
13811nnred 10475 . . . . . . . . 9
139137, 138ltnled 9658 . . . . . . . 8
140136, 139bitr4d 256 . . . . . . 7
14116rpge0d 11170 . . . . . . . . . . . . 13
142141adantrr 716 . . . . . . . . . . . 12
14311nngt0d 10503 . . . . . . . . . . . . . . . . 17
144 ltdivmul 10341 . . . . . . . . . . . . . . . . 17
145137, 49, 138, 143, 144syl112anc 1223 . . . . . . . . . . . . . . . 16
14663mulid1d 9540 . . . . . . . . . . . . . . . . 17
147146breq2d 4421 . . . . . . . . . . . . . . . 16
148145, 147bitrd 253 . . . . . . . . . . . . . . 15
149148biimprd 223 . . . . . . . . . . . . . 14
150149impr 619 . . . . . . . . . . . . 13
151 0p1e1 10571 . . . . . . . . . . . . 13
152150, 151syl6breqr 4449 . . . . . . . . . . . 12
15317adantrr 716 . . . . . . . . . . . . 13
154 0z 10795 . . . . . . . . . . . . 13
155 flbi 11809 . . . . . . . . . . . . 13
156153, 154, 155sylancl 662 . . . . . . . . . . . 12
157142, 152, 156mpbir2and 913 . . . . . . . . . . 11
15824rpge0d 11170 . . . . . . . . . . . . . . 15
159158adantrr 716 . . . . . . . . . . . . . 14
160116, 21ltaddrp2d 11196 . . . . . . . . . . . . . . . . . . . 20
161612timesd 10705 . . . . . . . . . . . . . . . . . . . 20
162160, 161breqtrrd 4435 . . . . . . . . . . . . . . . . . . 19
163162ad2antrr 725 . . . . . . . . . . . . . . . . . 18
164116ad2antrr 725 . . . . . . . . . . . . . . . . . . 19
165 lttr 9588 . . . . . . . . . . . . . . . . . . 19
166164, 137, 138, 165syl3anc 1219 . . . . . . . . . . . . . . . . . 18
167163, 166mpand 675 . . . . . . . . . . . . . . . . 17
168 ltdivmul 10341 . . . . . . . . . . . . . . . . . . 19
169164, 49, 138, 143, 168syl112anc 1223 . . . . . . . . . . . . . . . . . 18
170146breq2d 4421 . . . . . . . . . . . . . . . . . 18
171169, 170bitrd 253 . . . . . . . . . . . . . . . . 17
172167, 171sylibrd 234 . . . . . . . . . . . . . . . 16
173172impr 619 . . . . . . . . . . . . . . 15
174173, 151syl6breqr 4449 . . . . . . . . . . . . . 14
17525adantrr 716 . . . . . . . . . . . . . . 15
176 flbi 11809 . . . . . . . . . . . . . . 15
177175, 154, 176sylancl 662 . . . . . . . . . . . . . 14
178159, 174, 177mpbir2and 913 . . . . . . . . . . . . 13
179178oveq2d 6238 . . . . . . . . . . . 12
180 2t0e0 10615 . . . . . . . . . . . 12
181179, 180syl6eq 2511 . . . . . . . . . . 11
182157, 181oveq12d 6240 . . . . . . . . . 10
183 0m0e0 10569 . . . . . . . . . 10
184182, 183syl6eq 2511 . . . . . . . . 9
185 0le0 10549 . . . . . . . . 9
186184, 185syl6eqbr 4446 . . . . . . . 8
187186expr 615 . . . . . . 7
188140, 187sylbid 215 . . . . . 6
189 iffalse 3914 . . . . . . . 8
190189eqcomd 2462 . . . . . . 7
191190breq2d 4421 . . . . . 6
192188, 191mpbidi 216 . . . . 5
19390, 192pm2.61d 158 . . . 4
1941, 30, 34, 193fsumle 13420 . . 3
195 pcbcctr 23015 . . 3
196131zred 10885 . . . . . . . 8
197 flle 11794 . . . . . . . . 9
198130, 197syl 16 . . . . . . . 8
199104nnnn0d 10774 . . . . . . . . . . . . . 14
20093, 199nnexpcld 12186 . . . . . . . . . . . . 13
201200nnred 10475 . . . . . . . . . . . 12