bposlem2 - Metamath Proof Explorer

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

Theorem bposlem2 23432

Description: There are no odd primes in the range

dividing the

-th central binomial coefficient. (Contributed by Mario Carneiro, 12-Mar-2014.)

**Hypotheses**
Ref	Expression
bposlem2.1
bposlem2.2
bposlem2.3
bposlem2.4
bposlem2.5

**Assertion**
Ref	Expression
bposlem2

Proof of Theorem bposlem2 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		bposlem2.1	. . 3
2		bposlem2.2	. . 3
3		pcbcctr 23423	. . 3 $/\$
4	1, 2, 3	syl2anc 661	. 2
5		elfznn 11723	. . . . . 6
6		elnn1uz2 11167	. . . . . 6 $\/$
7	5, 6	sylib 196	. . . . 5 $\/$
8		oveq2 6289	. . . . . . . . . . . 12
9		prmnn 14097	. . . . . . . . . . . . . . 15
10	2, 9	syl 16	. . . . . . . . . . . . . 14
11	10	nncnd 10558	. . . . . . . . . . . . 13
12	11	exp1d 12284	. . . . . . . . . . . 12
13	8, 12	sylan9eqr 2506	. . . . . . . . . . 11 $/\$
14	13	oveq2d 6297	. . . . . . . . . 10 $/\$
15	14	fveq2d 5860	. . . . . . . . 9 $/\$
16		2t1e2 10690	. . . . . . . . . . . . 13
17	11	mulid2d 9617	. . . . . . . . . . . . . . . 16
18		bposlem2.5	. . . . . . . . . . . . . . . 16
19	17, 18	eqbrtrd 4457	. . . . . . . . . . . . . . 15
20		1red 9614	. . . . . . . . . . . . . . . 16
21	1	nnred 10557	. . . . . . . . . . . . . . . 16
22	10	nnred 10557	. . . . . . . . . . . . . . . 16
23	10	nngt0d 10585	. . . . . . . . . . . . . . . 16
24		lemuldiv 10430	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
25	20, 21, 22, 23, 24	syl112anc 1233	. . . . . . . . . . . . . . 15
26	19, 25	mpbid 210	. . . . . . . . . . . . . 14
27	21, 10	nndivred 10590	. . . . . . . . . . . . . . 15
28		1re 9598	. . . . . . . . . . . . . . . 16
29		2re 10611	. . . . . . . . . . . . . . . . 17
30		2pos 10633	. . . . . . . . . . . . . . . . 17
31	29, 30	pm3.2i 455	. . . . . . . . . . . . . . . 16 $/\$
32		lemul2 10401	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	28, 31, 32	mp3an13 1316	. . . . . . . . . . . . . . 15
34	27, 33	syl 16	. . . . . . . . . . . . . 14
35	26, 34	mpbid 210	. . . . . . . . . . . . 13
36	16, 35	syl5eqbrr 4471	. . . . . . . . . . . 12
37		2cnd 10614	. . . . . . . . . . . . 13
38	1	nncnd 10558	. . . . . . . . . . . . 13
39	10	nnne0d 10586	. . . . . . . . . . . . 13
40	37, 38, 11, 39	divassd 10361	. . . . . . . . . . . 12
41	36, 40	breqtrrd 4463	. . . . . . . . . . 11
42		bposlem2.4	. . . . . . . . . . . . 13
43		2nn 10699	. . . . . . . . . . . . . . . 16
44		nnmulcl 10565	. . . . . . . . . . . . . . . 16 $/\$
45	43, 1, 44	sylancr 663	. . . . . . . . . . . . . . 15
46	45	nnred 10557	. . . . . . . . . . . . . 14
47		3re 10615	. . . . . . . . . . . . . . . 16
48		3pos 10635	. . . . . . . . . . . . . . . 16
49	47, 48	pm3.2i 455	. . . . . . . . . . . . . . 15 $/\$
50		ltdiv23 10442	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
51	49, 50	mp3an2 1313	. . . . . . . . . . . . . 14 $/\$ $/\$
52	46, 22, 23, 51	syl12anc 1227	. . . . . . . . . . . . 13
53	42, 52	mpbid 210	. . . . . . . . . . . 12
54		df-3 10601	. . . . . . . . . . . 12
55	53, 54	syl6breq 4476	. . . . . . . . . . 11
56	46, 10	nndivred 10590	. . . . . . . . . . . 12
57		2z 10902	. . . . . . . . . . . 12
58		flbi 11931	. . . . . . . . . . . 12 $/\$ $/\$
59	56, 57, 58	sylancl 662	. . . . . . . . . . 11 $/\$
60	41, 55, 59	mpbir2and 922	. . . . . . . . . 10
61	60	adantr 465	. . . . . . . . 9 $/\$
62	15, 61	eqtrd 2484	. . . . . . . 8 $/\$
63	13	oveq2d 6297	. . . . . . . . . . . 12 $/\$
64	63	fveq2d 5860	. . . . . . . . . . 11 $/\$
65		remulcl 9580	. . . . . . . . . . . . . . . . . 18 $/\$
66	29, 27, 65	sylancr 663	. . . . . . . . . . . . . . . . 17
67	47	a1i 11	. . . . . . . . . . . . . . . . 17
68		4re 10618	. . . . . . . . . . . . . . . . . 18
69	68	a1i 11	. . . . . . . . . . . . . . . . 17
70	40, 53	eqbrtrrd 4459	. . . . . . . . . . . . . . . . 17
71		3lt4 10711	. . . . . . . . . . . . . . . . . 18
72	71	a1i 11	. . . . . . . . . . . . . . . . 17
73	66, 67, 69, 70, 72	lttrd 9746	. . . . . . . . . . . . . . . 16
74		2t2e4 10691	. . . . . . . . . . . . . . . 16
75	73, 74	syl6breqr 4477	. . . . . . . . . . . . . . 15
76		ltmul2 10399	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	29, 31, 76	mp3an23 1317	. . . . . . . . . . . . . . . 16
78	27, 77	syl 16	. . . . . . . . . . . . . . 15
79	75, 78	mpbird 232	. . . . . . . . . . . . . 14
80		df-2 10600	. . . . . . . . . . . . . 14
81	79, 80	syl6breq 4476	. . . . . . . . . . . . 13
82		1z 10900	. . . . . . . . . . . . . 14
83		flbi 11931	. . . . . . . . . . . . . 14 $/\$ $/\$
84	27, 82, 83	sylancl 662	. . . . . . . . . . . . 13 $/\$
85	26, 81, 84	mpbir2and 922	. . . . . . . . . . . 12
86	85	adantr 465	. . . . . . . . . . 11 $/\$
87	64, 86	eqtrd 2484	. . . . . . . . . 10 $/\$
88	87	oveq2d 6297	. . . . . . . . 9 $/\$
89	88, 16	syl6eq 2500	. . . . . . . 8 $/\$
90	62, 89	oveq12d 6299	. . . . . . 7 $/\$
91		2cn 10612	. . . . . . . 8
92	91	subidi 9895	. . . . . . 7
93	90, 92	syl6eq 2500	. . . . . 6 $/\$
94	45	nnrpd 11264	. . . . . . . . . . . 12
95	94	adantr 465	. . . . . . . . . . 11 $/\$
96		eluzge2nn0 11129	. . . . . . . . . . . . 13
97		nnexpcl 12158	. . . . . . . . . . . . 13 $/\$
98	10, 96, 97	syl2an 477	. . . . . . . . . . . 12 $/\$
99	98	nnrpd 11264	. . . . . . . . . . 11 $/\$
100	95, 99	rpdivcld 11282	. . . . . . . . . 10 $/\$
101	100	rpge0d 11269	. . . . . . . . 9 $/\$
102	46	adantr 465	. . . . . . . . . . . . 13 $/\$
103		remulcl 9580	. . . . . . . . . . . . . . 15 $/\$
104	47, 22, 103	sylancr 663	. . . . . . . . . . . . . 14
105	104	adantr 465	. . . . . . . . . . . . 13 $/\$
106	98	nnred 10557	. . . . . . . . . . . . 13 $/\$
107		ltdivmul 10423	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
108	49, 107	mp3an3 1314	. . . . . . . . . . . . . . . 16 $/\$
109	46, 22, 108	syl2anc 661	. . . . . . . . . . . . . . 15
110	42, 109	mpbid 210	. . . . . . . . . . . . . 14
111	110	adantr 465	. . . . . . . . . . . . 13 $/\$
112	22, 22	remulcld 9627	. . . . . . . . . . . . . . 15
113	112	adantr 465	. . . . . . . . . . . . . 14 $/\$
114		bposlem2.3	. . . . . . . . . . . . . . . . . 18
115		nnltp1le 10925	. . . . . . . . . . . . . . . . . . 19 $/\$
116	43, 10, 115	sylancr 663	. . . . . . . . . . . . . . . . . 18
117	114, 116	mpbid 210	. . . . . . . . . . . . . . . . 17
118	54, 117	syl5eqbr 4470	. . . . . . . . . . . . . . . 16
119		lemul1 10400	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
120	47, 119	mp3an1 1312	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
121	22, 22, 23, 120	syl12anc 1227	. . . . . . . . . . . . . . . 16
122	118, 121	mpbid 210	. . . . . . . . . . . . . . 15
123	122	adantr 465	. . . . . . . . . . . . . 14 $/\$
124	11	sqvald 12286	. . . . . . . . . . . . . . . 16
125	124	adantr 465	. . . . . . . . . . . . . . 15 $/\$
126	22	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
127	10	nnge1d 10584	. . . . . . . . . . . . . . . . 17
128	127	adantr 465	. . . . . . . . . . . . . . . 16 $/\$
129		simpr 461	. . . . . . . . . . . . . . . 16 $/\$
130	126, 128, 129	leexp2ad 12321	. . . . . . . . . . . . . . 15 $/\$
131	125, 130	eqbrtrrd 4459	. . . . . . . . . . . . . 14 $/\$
132	105, 113, 106, 123, 131	letrd 9742	. . . . . . . . . . . . 13 $/\$
133	102, 105, 106, 111, 132	ltletrd 9745	. . . . . . . . . . . 12 $/\$
134	98	nncnd 10558	. . . . . . . . . . . . 13 $/\$
135	134	mulid1d 9616	. . . . . . . . . . . 12 $/\$
136	133, 135	breqtrrd 4463	. . . . . . . . . . 11 $/\$
137		1red 9614	. . . . . . . . . . . 12 $/\$
138	102, 137, 99	ltdivmuld 11312	. . . . . . . . . . 11 $/\$
139	136, 138	mpbird 232	. . . . . . . . . 10 $/\$
140		1e0p1 11012	. . . . . . . . . 10
141	139, 140	syl6breq 4476	. . . . . . . . 9 $/\$
142	100	rpred 11265	. . . . . . . . . 10 $/\$
143		0z 10881	. . . . . . . . . 10
144		flbi 11931	. . . . . . . . . 10 $/\$ $/\$
145	142, 143, 144	sylancl 662	. . . . . . . . 9 $/\$ $/\$
146	101, 141, 145	mpbir2and 922	. . . . . . . 8 $/\$
147	1	nnrpd 11264	. . . . . . . . . . . . . 14
148	147	adantr 465	. . . . . . . . . . . . 13 $/\$
149	148, 99	rpdivcld 11282	. . . . . . . . . . . 12 $/\$
150	149	rpge0d 11269	. . . . . . . . . . 11 $/\$
151	21	adantr 465	. . . . . . . . . . . . . . 15 $/\$
152	21, 147	ltaddrpd 11294	. . . . . . . . . . . . . . . . 17
153	38	2timesd 10787	. . . . . . . . . . . . . . . . 17
154	152, 153	breqtrrd 4463	. . . . . . . . . . . . . . . 16
155	154	adantr 465	. . . . . . . . . . . . . . 15 $/\$
156	151, 102, 106, 155, 133	lttrd 9746	. . . . . . . . . . . . . 14 $/\$
157	156, 135	breqtrrd 4463	. . . . . . . . . . . . 13 $/\$
158	151, 137, 99	ltdivmuld 11312	. . . . . . . . . . . . 13 $/\$
159	157, 158	mpbird 232	. . . . . . . . . . . 12 $/\$
160	159, 140	syl6breq 4476	. . . . . . . . . . 11 $/\$
161	149	rpred 11265	. . . . . . . . . . . 12 $/\$
162		flbi 11931	. . . . . . . . . . . 12 $/\$ $/\$
163	161, 143, 162	sylancl 662	. . . . . . . . . . 11 $/\$ $/\$
164	150, 160, 163	mpbir2and 922	. . . . . . . . . 10 $/\$
165	164	oveq2d 6297	. . . . . . . . 9 $/\$
166		2t0e0 10697	. . . . . . . . 9
167	165, 166	syl6eq 2500	. . . . . . . 8 $/\$
168	146, 167	oveq12d 6299	. . . . . . 7 $/\$
169		0m0e0 10651	. . . . . . 7
170	168, 169	syl6eq 2500	. . . . . 6 $/\$
171	93, 170	jaodan 785	. . . . 5 $/\$ $\/$
172	7, 171	sylan2 474	. . . 4 $/\$
173	172	sumeq2dv 13504	. . 3
174		fzfid 12062	. . . 4
175		sumz 13523	. . . . 5 $\/$
176	175	olcs 395	. . . 4
177	174, 176	syl 16	. . 3
178	173, 177	eqtrd 2484	. 2
179	4, 178	eqtrd 2484	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 368 $/\$ wa 369

wceq 1383

wcel 1804

wss 3461 class class class wbr 4437

cfv 5578 (class class class)co 6281

cfn 7518

cr 9494

cc0 9495

c1 9496

caddc 9498

cmul 9500

clt 9631

cle 9632

cmin 9810

cdiv 10212

cn 10542

c2 10591

c3 10592

c4 10593

cn0 10801

cz 10870

cuz 11090

crp 11229

cfz 11681

cfl 11906

cexp 12145

cbc 12359

csu 13487

cprime 14094

cpc 14237

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-inf2 8061 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572 ax-pre-sup 9573

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-fal 1389 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-se 4829 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-isom 5587 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-2o 7133 df-oadd 7136 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-sup 7903 df-oi 7938 df-card 8323 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-div 10213 df-nn 10543 df-2 10600 df-3 10601 df-4 10602 df-n0 10802 df-z 10871 df-uz 11091 df-q 11192 df-rp 11230 df-fz 11682 df-fzo 11804 df-fl 11908 df-mod 11976 df-seq 12087 df-exp 12146 df-fac 12333 df-bc 12360 df-hash 12385 df-cj 12911 df-re 12912 df-im 12913 df-sqrt 13047 df-abs 13048 df-clim 13290 df-sum 13488 df-dvds 13864 df-gcd 14022 df-prm 14095 df-pc 14238

This theorem is referenced by: bposlem3 23433

W3C validator