bposlem2 - Metamath Proof Explorer

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

Theorem bposlem2 23677

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 23668	. . 3 $/\$
4	1, 2, 3	syl2anc 659	. 2
5		elfznn 11635	. . . . . 6
6		elnn1uz2 11077	. . . . . 6 $\/$
7	5, 6	sylib 196	. . . . 5 $\/$
8		oveq2 6204	. . . . . . . . . . . 12
9		prmnn 14222	. . . . . . . . . . . . . . 15
10	2, 9	syl 16	. . . . . . . . . . . . . 14
11	10	nncnd 10468	. . . . . . . . . . . . 13
12	11	exp1d 12207	. . . . . . . . . . . 12
13	8, 12	sylan9eqr 2445	. . . . . . . . . . 11 $/\$
14	13	oveq2d 6212	. . . . . . . . . 10 $/\$
15	14	fveq2d 5778	. . . . . . . . 9 $/\$
16		2t1e2 10601	. . . . . . . . . . . . 13
17	11	mulid2d 9525	. . . . . . . . . . . . . . . 16
18		bposlem2.5	. . . . . . . . . . . . . . . 16
19	17, 18	eqbrtrd 4387	. . . . . . . . . . . . . . 15
20		1red 9522	. . . . . . . . . . . . . . . 16
21	1	nnred 10467	. . . . . . . . . . . . . . . 16
22	10	nnred 10467	. . . . . . . . . . . . . . . 16
23	10	nngt0d 10496	. . . . . . . . . . . . . . . 16
24		lemuldiv 10340	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
25	20, 21, 22, 23, 24	syl112anc 1230	. . . . . . . . . . . . . . 15
26	19, 25	mpbid 210	. . . . . . . . . . . . . 14
27	21, 10	nndivred 10501	. . . . . . . . . . . . . . 15
28		1re 9506	. . . . . . . . . . . . . . . 16
29		2re 10522	. . . . . . . . . . . . . . . . 17
30		2pos 10544	. . . . . . . . . . . . . . . . 17
31	29, 30	pm3.2i 453	. . . . . . . . . . . . . . . 16 $/\$
32		lemul2 10312	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
33	28, 31, 32	mp3an13 1313	. . . . . . . . . . . . . . 15
34	27, 33	syl 16	. . . . . . . . . . . . . 14
35	26, 34	mpbid 210	. . . . . . . . . . . . 13
36	16, 35	syl5eqbrr 4401	. . . . . . . . . . . 12
37		2cnd 10525	. . . . . . . . . . . . 13
38	1	nncnd 10468	. . . . . . . . . . . . 13
39	10	nnne0d 10497	. . . . . . . . . . . . 13
40	37, 38, 11, 39	divassd 10272	. . . . . . . . . . . 12
41	36, 40	breqtrrd 4393	. . . . . . . . . . 11
42		bposlem2.4	. . . . . . . . . . . . 13
43		2nn 10610	. . . . . . . . . . . . . . . 16
44		nnmulcl 10475	. . . . . . . . . . . . . . . 16 $/\$
45	43, 1, 44	sylancr 661	. . . . . . . . . . . . . . 15
46	45	nnred 10467	. . . . . . . . . . . . . 14
47		3re 10526	. . . . . . . . . . . . . . . 16
48		3pos 10546	. . . . . . . . . . . . . . . 16
49	47, 48	pm3.2i 453	. . . . . . . . . . . . . . 15 $/\$
50		ltdiv23 10352	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
51	49, 50	mp3an2 1310	. . . . . . . . . . . . . 14 $/\$ $/\$
52	46, 22, 23, 51	syl12anc 1224	. . . . . . . . . . . . 13
53	42, 52	mpbid 210	. . . . . . . . . . . 12
54		df-3 10512	. . . . . . . . . . . 12
55	53, 54	syl6breq 4406	. . . . . . . . . . 11
56	46, 10	nndivred 10501	. . . . . . . . . . . 12
57		2z 10813	. . . . . . . . . . . 12
58		flbi 11851	. . . . . . . . . . . 12 $/\$ $/\$
59	56, 57, 58	sylancl 660	. . . . . . . . . . 11 $/\$
60	41, 55, 59	mpbir2and 920	. . . . . . . . . 10
61	60	adantr 463	. . . . . . . . 9 $/\$
62	15, 61	eqtrd 2423	. . . . . . . 8 $/\$
63	13	oveq2d 6212	. . . . . . . . . . . 12 $/\$
64	63	fveq2d 5778	. . . . . . . . . . 11 $/\$
65		remulcl 9488	. . . . . . . . . . . . . . . . . 18 $/\$
66	29, 27, 65	sylancr 661	. . . . . . . . . . . . . . . . 17
67	47	a1i 11	. . . . . . . . . . . . . . . . 17
68		4re 10529	. . . . . . . . . . . . . . . . . 18
69	68	a1i 11	. . . . . . . . . . . . . . . . 17
70	40, 53	eqbrtrrd 4389	. . . . . . . . . . . . . . . . 17
71		3lt4 10622	. . . . . . . . . . . . . . . . . 18
72	71	a1i 11	. . . . . . . . . . . . . . . . 17
73	66, 67, 69, 70, 72	lttrd 9654	. . . . . . . . . . . . . . . 16
74		2t2e4 10602	. . . . . . . . . . . . . . . 16
75	73, 74	syl6breqr 4407	. . . . . . . . . . . . . . 15
76		ltmul2 10310	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
77	29, 31, 76	mp3an23 1314	. . . . . . . . . . . . . . . 16
78	27, 77	syl 16	. . . . . . . . . . . . . . 15
79	75, 78	mpbird 232	. . . . . . . . . . . . . 14
80		df-2 10511	. . . . . . . . . . . . . 14
81	79, 80	syl6breq 4406	. . . . . . . . . . . . 13
82		1z 10811	. . . . . . . . . . . . . 14
83		flbi 11851	. . . . . . . . . . . . . 14 $/\$ $/\$
84	27, 82, 83	sylancl 660	. . . . . . . . . . . . 13 $/\$
85	26, 81, 84	mpbir2and 920	. . . . . . . . . . . 12
86	85	adantr 463	. . . . . . . . . . 11 $/\$
87	64, 86	eqtrd 2423	. . . . . . . . . 10 $/\$
88	87	oveq2d 6212	. . . . . . . . 9 $/\$
89	88, 16	syl6eq 2439	. . . . . . . 8 $/\$
90	62, 89	oveq12d 6214	. . . . . . 7 $/\$
91		2cn 10523	. . . . . . . 8
92	91	subidi 9803	. . . . . . 7
93	90, 92	syl6eq 2439	. . . . . 6 $/\$
94	45	nnrpd 11175	. . . . . . . . . . . 12
95	94	adantr 463	. . . . . . . . . . 11 $/\$
96		eluzge2nn0 11040	. . . . . . . . . . . . 13
97		nnexpcl 12082	. . . . . . . . . . . . 13 $/\$
98	10, 96, 97	syl2an 475	. . . . . . . . . . . 12 $/\$
99	98	nnrpd 11175	. . . . . . . . . . 11 $/\$
100	95, 99	rpdivcld 11194	. . . . . . . . . 10 $/\$
101	100	rpge0d 11181	. . . . . . . . 9 $/\$
102	46	adantr 463	. . . . . . . . . . . . 13 $/\$
103		remulcl 9488	. . . . . . . . . . . . . . 15 $/\$
104	47, 22, 103	sylancr 661	. . . . . . . . . . . . . 14
105	104	adantr 463	. . . . . . . . . . . . 13 $/\$
106	98	nnred 10467	. . . . . . . . . . . . 13 $/\$
107		ltdivmul 10334	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
108	49, 107	mp3an3 1311	. . . . . . . . . . . . . . . 16 $/\$
109	46, 22, 108	syl2anc 659	. . . . . . . . . . . . . . 15
110	42, 109	mpbid 210	. . . . . . . . . . . . . 14
111	110	adantr 463	. . . . . . . . . . . . 13 $/\$
112	22, 22	remulcld 9535	. . . . . . . . . . . . . . 15
113	112	adantr 463	. . . . . . . . . . . . . 14 $/\$
114		bposlem2.3	. . . . . . . . . . . . . . . . . 18
115		nnltp1le 10836	. . . . . . . . . . . . . . . . . . 19 $/\$
116	43, 10, 115	sylancr 661	. . . . . . . . . . . . . . . . . 18
117	114, 116	mpbid 210	. . . . . . . . . . . . . . . . 17
118	54, 117	syl5eqbr 4400	. . . . . . . . . . . . . . . 16
119		lemul1 10311	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
120	47, 119	mp3an1 1309	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
121	22, 22, 23, 120	syl12anc 1224	. . . . . . . . . . . . . . . 16
122	118, 121	mpbid 210	. . . . . . . . . . . . . . 15
123	122	adantr 463	. . . . . . . . . . . . . 14 $/\$
124	11	sqvald 12209	. . . . . . . . . . . . . . . 16
125	124	adantr 463	. . . . . . . . . . . . . . 15 $/\$
126	22	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
127	10	nnge1d 10495	. . . . . . . . . . . . . . . . 17
128	127	adantr 463	. . . . . . . . . . . . . . . 16 $/\$
129		simpr 459	. . . . . . . . . . . . . . . 16 $/\$
130	126, 128, 129	leexp2ad 12244	. . . . . . . . . . . . . . 15 $/\$
131	125, 130	eqbrtrrd 4389	. . . . . . . . . . . . . 14 $/\$
132	105, 113, 106, 123, 131	letrd 9650	. . . . . . . . . . . . 13 $/\$
133	102, 105, 106, 111, 132	ltletrd 9653	. . . . . . . . . . . 12 $/\$
134	98	nncnd 10468	. . . . . . . . . . . . 13 $/\$
135	134	mulid1d 9524	. . . . . . . . . . . 12 $/\$
136	133, 135	breqtrrd 4393	. . . . . . . . . . 11 $/\$
137		1red 9522	. . . . . . . . . . . 12 $/\$
138	102, 137, 99	ltdivmuld 11224	. . . . . . . . . . 11 $/\$
139	136, 138	mpbird 232	. . . . . . . . . 10 $/\$
140		1e0p1 10923	. . . . . . . . . 10
141	139, 140	syl6breq 4406	. . . . . . . . 9 $/\$
142	100	rpred 11177	. . . . . . . . . 10 $/\$
143		0z 10792	. . . . . . . . . 10
144		flbi 11851	. . . . . . . . . 10 $/\$ $/\$
145	142, 143, 144	sylancl 660	. . . . . . . . 9 $/\$ $/\$
146	101, 141, 145	mpbir2and 920	. . . . . . . 8 $/\$
147	1	nnrpd 11175	. . . . . . . . . . . . . 14
148	147	adantr 463	. . . . . . . . . . . . 13 $/\$
149	148, 99	rpdivcld 11194	. . . . . . . . . . . 12 $/\$
150	149	rpge0d 11181	. . . . . . . . . . 11 $/\$
151	21	adantr 463	. . . . . . . . . . . . . . 15 $/\$
152	21, 147	ltaddrpd 11206	. . . . . . . . . . . . . . . . 17
153	38	2timesd 10698	. . . . . . . . . . . . . . . . 17
154	152, 153	breqtrrd 4393	. . . . . . . . . . . . . . . 16
155	154	adantr 463	. . . . . . . . . . . . . . 15 $/\$
156	151, 102, 106, 155, 133	lttrd 9654	. . . . . . . . . . . . . 14 $/\$
157	156, 135	breqtrrd 4393	. . . . . . . . . . . . 13 $/\$
158	151, 137, 99	ltdivmuld 11224	. . . . . . . . . . . . 13 $/\$
159	157, 158	mpbird 232	. . . . . . . . . . . 12 $/\$
160	159, 140	syl6breq 4406	. . . . . . . . . . 11 $/\$
161	149	rpred 11177	. . . . . . . . . . . 12 $/\$
162		flbi 11851	. . . . . . . . . . . 12 $/\$ $/\$
163	161, 143, 162	sylancl 660	. . . . . . . . . . 11 $/\$ $/\$
164	150, 160, 163	mpbir2and 920	. . . . . . . . . 10 $/\$
165	164	oveq2d 6212	. . . . . . . . 9 $/\$
166		2t0e0 10608	. . . . . . . . 9
167	165, 166	syl6eq 2439	. . . . . . . 8 $/\$
168	146, 167	oveq12d 6214	. . . . . . 7 $/\$
169		0m0e0 10562	. . . . . . 7
170	168, 169	syl6eq 2439	. . . . . 6 $/\$
171	93, 170	jaodan 783	. . . . 5 $/\$ $\/$
172	7, 171	sylan2 472	. . . 4 $/\$
173	172	sumeq2dv 13527	. . 3
174		fzfid 11986	. . . 4
175		sumz 13546	. . . . 5 $\/$
176	175	olcs 393	. . . 4
177	174, 176	syl 16	. . 3
178	173, 177	eqtrd 2423	. 2
179	4, 178	eqtrd 2423	1

Colors of variables: wff setvar class

Syntax hints:

wi 4

wb 184 $\/$ wo 366 $/\$ wa 367

wceq 1399

wcel 1826

wss 3389 class class class wbr 4367

cfv 5496 (class class class)co 6196

cfn 7435

cr 9402

cc0 9403

c1 9404

caddc 9406

cmul 9408

clt 9539

cle 9540

cmin 9718

cdiv 10123

cn 10452

c2 10502

c3 10503

c4 10504

cn0 10712

cz 10781

cuz 11001

crp 11139

cfz 11593

cfl 11826

cexp 12069

cbc 12282

csu 13510

cprime 14219

cpc 14362

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-inf2 7972 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480 ax-pre-sup 9481

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-fal 1405 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-se 4753 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-isom 5505 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-1o 7048 df-2o 7049 df-oadd 7052 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-sup 7816 df-oi 7850 df-card 8233 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-div 10124 df-nn 10453 df-2 10511 df-3 10512 df-4 10513 df-n0 10713 df-z 10782 df-uz 11002 df-q 11102 df-rp 11140 df-fz 11594 df-fzo 11718 df-fl 11828 df-mod 11897 df-seq 12011 df-exp 12070 df-fac 12256 df-bc 12283 df-hash 12308 df-cj 12934 df-re 12935 df-im 12936 df-sqrt 13070 df-abs 13071 df-clim 13313 df-sum 13511 df-dvds 13989 df-gcd 14147 df-prm 14220 df-pc 14363

This theorem is referenced by: bposlem3 23678

W3C validator