pcfac - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > pcfac		Unicode version

Theorem pcfac 13158

Description: Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014.) (Revised by Mario Carneiro, 21-May-2014.)

**Assertion**
Ref	Expression
pcfac	$/\$ $/\$

Distinct variable groups:

Proof of Theorem pcfac Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5698	. . . . . . . 8
2		fveq2 5698	. . . . . . . . . 10
3	2	oveq2d 6104	. . . . . . . . 9
4		fvoveq1 6111	. . . . . . . . . 10
5	4	sumeq2sdv 12161	. . . . . . . . 9
6	3, 5	eqeq12d 2253	. . . . . . . 8
7	1, 6	raleqbidv 2765	. . . . . . 7
8	7	imbi2d 230	. . . . . 6
9		fveq2 5698	. . . . . . . 8
10		fveq2 5698	. . . . . . . . . 10
11	10	oveq2d 6104	. . . . . . . . 9
12		fvoveq1 6111	. . . . . . . . . 10
13	12	sumeq2sdv 12161	. . . . . . . . 9
14	11, 13	eqeq12d 2253	. . . . . . . 8
15	9, 14	raleqbidv 2765	. . . . . . 7
16	15	imbi2d 230	. . . . . 6
17		fveq2 5698	. . . . . . . 8
18		fveq2 5698	. . . . . . . . . 10
19	18	oveq2d 6104	. . . . . . . . 9
20		fvoveq1 6111	. . . . . . . . . 10
21	20	sumeq2sdv 12161	. . . . . . . . 9
22	19, 21	eqeq12d 2253	. . . . . . . 8
23	17, 22	raleqbidv 2765	. . . . . . 7
24	23	imbi2d 230	. . . . . 6
25		fveq2 5698	. . . . . . . 8
26		fveq2 5698	. . . . . . . . . 10
27	26	oveq2d 6104	. . . . . . . . 9
28		fvoveq1 6111	. . . . . . . . . 10
29	28	sumeq2sdv 12161	. . . . . . . . 9
30	27, 29	eqeq12d 2253	. . . . . . . 8
31	25, 30	raleqbidv 2765	. . . . . . 7
32	31	imbi2d 230	. . . . . 6
33		1zzd 9682	. . . . . . . . . 10 $/\$
34		eluzelz 9947	. . . . . . . . . . 11
35	34	adantl 277	. . . . . . . . . 10 $/\$
36	33, 35	fzfigd 10889	. . . . . . . . 9 $/\$
37		isumz 12181	. . . . . . . . . 10 $/\$ $/\$ DECID $\/$
38	37	olcs 748	. . . . . . . . 9
39	36, 38	syl 14	. . . . . . . 8 $/\$
40		0nn0 9589	. . . . . . . . . 10
41		elfznn 10477	. . . . . . . . . . . . 13
42	41	nnnn0d 9631	. . . . . . . . . . . 12
43		nn0uz 9973	. . . . . . . . . . . 12
44	42, 43	eleqtrdi 2331	. . . . . . . . . . 11
45	44	adantl 277	. . . . . . . . . 10 $/\$ $/\$
46		simpll 531	. . . . . . . . . 10 $/\$ $/\$
47		pcfaclem 13157	. . . . . . . . . 10 $/\$ $/\$
48	40, 45, 46, 47	mp3an2i 1383	. . . . . . . . 9 $/\$ $/\$
49	48	sumeq2dv 12159	. . . . . . . 8 $/\$
50		fac0 11188	. . . . . . . . . . 11
51	50	oveq2i 6099	. . . . . . . . . 10
52		pc1 13113	. . . . . . . . . 10
53	51, 52	eqtrid 2283	. . . . . . . . 9
54	53	adantr 276	. . . . . . . 8 $/\$
55	39, 49, 54	3eqtr4rd 2282	. . . . . . 7 $/\$
56	55	ralrimiva 2623	. . . . . 6
57		nn0z 9675	. . . . . . . . . . . 12
58	57	adantr 276	. . . . . . . . . . 11 $/\$
59		uzid 9952	. . . . . . . . . . 11
60		peano2uz 9999	. . . . . . . . . . 11
61	58, 59, 60	3syl 17	. . . . . . . . . 10 $/\$
62		uzss 9959	. . . . . . . . . 10
63		ssralv 3312	. . . . . . . . . 10
64	61, 62, 63	3syl 17	. . . . . . . . 9 $/\$
65		oveq1 6095	. . . . . . . . . . 11
66		simpll 531	. . . . . . . . . . . . . . 15 $/\$ $/\$
67		facp1 11190	. . . . . . . . . . . . . . 15
68	66, 67	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
69	68	oveq2d 6104	. . . . . . . . . . . . 13 $/\$ $/\$
70		simplr 533	. . . . . . . . . . . . . 14 $/\$ $/\$
71		faccl 11195	. . . . . . . . . . . . . . 15
72		nnz 9674	. . . . . . . . . . . . . . . 16
73		nnne0 9341	. . . . . . . . . . . . . . . 16
74	72, 73	jca 306	. . . . . . . . . . . . . . 15 $/\$
75	66, 71, 74	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76		nn0p1nn 9613	. . . . . . . . . . . . . . 15
77		nnz 9674	. . . . . . . . . . . . . . . 16
78		nnne0 9341	. . . . . . . . . . . . . . . 16
79	77, 78	jca 306	. . . . . . . . . . . . . . 15 $/\$
80	66, 76, 79	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
81		pcmul 13109	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
82	70, 75, 80, 81	syl3anc 1278	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 82	eqtr2d 2272	. . . . . . . . . . . 12 $/\$ $/\$
84	66	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	84	nn0zd 9777	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		prmnn 12913	. . . . . . . . . . . . . . . . . . 19
87	86	ad2antlr 493	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
88		nnexpcl 11010	. . . . . . . . . . . . . . . . . 18 $/\$
89	87, 42, 88	syl2an 289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
90		fldivp1 13156	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 415	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92		elfzuz 10441	. . . . . . . . . . . . . . . . . . 19
93	66, 76	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
94	70, 93	pccld 13108	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
95	94	nn0zd 9777	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
96		elfz5 10437	. . . . . . . . . . . . . . . . . . 19 $/\$
97	92, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
98		simpllr 540	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
99	84, 76	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
100	99	nnzd 9778	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
101	42	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		pcdvdsb 13128	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
103	98, 100, 101, 102	syl3anc 1278	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104	97, 103	bitr2d 189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	104	ifbid 3662	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	91, 105	eqtrd 2271	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107	106	sumeq2dv 12159	. . . . . . . . . . . . . 14 $/\$ $/\$
108		1zzd 9682	. . . . . . . . . . . . . . . 16 $/\$ $/\$
109		eluzelz 9947	. . . . . . . . . . . . . . . . 17
110	109	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	108, 110	fzfigd 10889	. . . . . . . . . . . . . . 15 $/\$ $/\$
112		znq 10040	. . . . . . . . . . . . . . . . . 18 $/\$
113	100, 89, 112	syl2anc 415	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
114	113	flqcld 10731	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	114	zcnd 9780	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
116		znq 10040	. . . . . . . . . . . . . . . . . 18 $/\$
117	85, 89, 116	syl2anc 415	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	117	flqcld 10731	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	118	zcnd 9780	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	111, 115, 119	fsumsub 12244	. . . . . . . . . . . . . 14 $/\$ $/\$
121	94	nn0red 9632	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122	66	nn0red 9632	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123		peano2re 8469	. . . . . . . . . . . . . . . . . . . 20
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	110	zred 9779	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	93	nnzd 9778	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127		zdcle 9732	. . . . . . . . . . . . . . . . . . . . 21 $/\$ DECID
128	95, 126, 127	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ DECID
129		zletric 9699	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
130	95, 126, 129	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
131	130	ord 736	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
132	93	nnnn0d 9631	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
133		pcdvdsb 13128	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
134	70, 126, 132, 133	syl3anc 1278	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
135	87, 132	nnexpcld 11154	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
136	135	nnzd 9778	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
137		dvdsle 12636	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
138	136, 93, 137	syl2anc 415	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
139	135	nnred 9326	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	139, 124	lenltd 8451	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141	138, 140	sylibd 149	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
142	134, 141	sylbid 150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
143	131, 142	syld 45	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
144		prmuz2 12935	. . . . . . . . . . . . . . . . . . . . . 22
145	144	ad2antlr 493	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
146		bernneq3 11121	. . . . . . . . . . . . . . . . . . . . 21 $/\$
147	145, 132, 146	syl2anc 415	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148		condc 865	. . . . . . . . . . . . . . . . . . . 20 DECID
149	128, 143, 147, 148	syl3c 63	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
150		eluzle 9950	. . . . . . . . . . . . . . . . . . . 20
151	150	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
152	121, 124, 125, 149, 151	letrd 8457	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153		eluz 9951	. . . . . . . . . . . . . . . . . . 19 $/\$
154	95, 110, 153	syl2anc 415	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
155	152, 154	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
156		fzss2 10487	. . . . . . . . . . . . . . . . 17
157	155, 156	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$
158		elfzelz 10445	. . . . . . . . . . . . . . . . . . 19
159	158	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160		1zzd 9682	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
161	95	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
162		fzdcel 10461	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ DECID
163	159, 160, 161, 162	syl3anc 1278	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ DECID
164	163	ralrimiva 2623	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID
165		sumhashdc 13155	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID ♯
166	111, 157, 164, 165	syl3anc 1278	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
167		hashfz1 11244	. . . . . . . . . . . . . . . 16 ♯
168	94, 167	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
169	166, 168	eqtrd 2271	. . . . . . . . . . . . . 14 $/\$ $/\$
170	107, 120, 169	3eqtr3d 2279	. . . . . . . . . . . . 13 $/\$ $/\$
171	111, 115	fsumcl 12192	. . . . . . . . . . . . . 14 $/\$ $/\$
172	111, 119	fsumcl 12192	. . . . . . . . . . . . . 14 $/\$ $/\$
173	94	nn0cnd 9633	. . . . . . . . . . . . . 14 $/\$ $/\$
174	171, 172, 173	subaddd 8662	. . . . . . . . . . . . 13 $/\$ $/\$
175	170, 174	mpbid 147	. . . . . . . . . . . 12 $/\$ $/\$
176	83, 175	eqeq12d 2253	. . . . . . . . . . 11 $/\$ $/\$
177	65, 176	imbitrid 154	. . . . . . . . . 10 $/\$ $/\$
178	177	ralimdva 2617	. . . . . . . . 9 $/\$
179	64, 178	syld 45	. . . . . . . 8 $/\$
180	179	ex 115	. . . . . . 7
181	180	a2d 26	. . . . . 6
182	8, 16, 24, 32, 56, 181	nn0ind 9771	. . . . 5
183	182	imp 124	. . . 4 $/\$
184		oveq2 6096	. . . . . . 7
185	184	sumeq1d 12157	. . . . . 6
186	185	eqeq2d 2250	. . . . 5
187	186	rspcv 2925	. . . 4
188	183, 187	syl5 32	. . 3 $/\$
189	188	3impib 1232	. 2 $/\$ $/\$
190	189	3com12 1238	1 $/\$ $/\$

Colors of variables: wff set class

This proof depends on syntax axioms:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 720 DECID wdc 846 $/\$ w3a 1009

wceq 1402

wcel 2209

wne 2420

wral 2528

wss 3220

cif 3638 class class class wbr 4131

cfv 5380 (class class class)co 6088

cfn 7026

cr 8184

cc0 8185

c1 8186

caddc 8188

cmul 8190

clt 8366

cle 8367

cmin 8504

cdiv 9010

cn 9313

c2 9364

cn0 9574

cz 9655

cuz 9937

cq 10035

cfz 10428

cfl 10720

cexp 10996

cfa 11185 ♯chash 11236

csu 12144

cdvds 12579

cprime 12910

cpc 13092

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 623 ax-in2 624 ax-io 721 ax-5 1500 ax-7 1501 ax-gen 1502 ax-ie1 1546 ax-ie2 1547 ax-8 1557 ax-10 1558 ax-11 1559 ax-i12 1560 ax-bndl 1562 ax-4 1563 ax-17 1579 ax-i9 1583 ax-ial 1587 ax-i5r 1588 ax-14 2212 ax-ext 2220 ax-coll 4248 ax-sep 4251 ax-nul 4261 ax-pow 4313 ax-pr 4348 ax-un 4580 ax-setind 4686 ax-iinf 4737 ax-cnex 8276 ax-resscn 8277 ax-1cn 8278 ax-1re 8279 ax-icn 8280 ax-addcl 8281 ax-addrcl 8282 ax-mulcl 8283 ax-mulrcl 8284 ax-addcom 8285 ax-mulcom 8286 ax-addass 8287 ax-mulass 8288 ax-distr 8289 ax-i2m1 8290 ax-0lt1 8291 ax-1rid 8292 ax-0id 8293 ax-rnegex 8294 ax-precex 8295 ax-cnre 8296 ax-pre-ltirr 8297 ax-pre-ltwlin 8298 ax-pre-lttrn 8299 ax-pre-apti 8300 ax-pre-ltadd 8301 ax-pre-mulgt0 8302 ax-pre-mulext 8303 ax-arch 8304 ax-caucvg 8305

This proof depends on definitions: df-bi 117 df-stab 843 df-dc 847 df-3or 1010 df-3an 1011 df-tru 1405 df-fal 1408 df-nf 1514 df-sb 1816 df-eu 2089 df-mo 2090 df-clab 2225 df-cleq 2231 df-clel 2234 df-nfc 2381 df-ne 2421 df-nel 2516 df-ral 2533 df-rex 2534 df-reu 2535 df-rmo 2536 df-rab 2537 df-v 2823 df-sbc 3052 df-csb 3148 df-dif 3222 df-un 3224 df-in 3226 df-ss 3233 df-nul 3521 df-if 3639 df-pw 3690 df-sn 3715 df-pr 3716 df-op 3718 df-uni 3936 df-int 3971 df-iun 4014 df-br 4132 df-opab 4194 df-mpt 4195 df-tr 4232 df-id 4440 df-po 4443 df-iso 4444 df-iord 4513 df-on 4515 df-ilim 4516 df-suc 4518 df-iom 4740 df-xp 4782 df-rel 4783 df-cnv 4784 df-co 4785 df-dm 4786 df-rn 4787 df-res 4788 df-ima 4789 df-iota 5340 df-fun 5382 df-fn 5383 df-f 5384 df-f1 5385 df-fo 5386 df-f1o 5387 df-fv 5388 df-isom 5389 df-riota 6041 df-ov 6091 df-oprab 6092 df-mpo 6093 df-1st 6378 df-2nd 6379 df-recs 6580 df-irdg 6645 df-frec 6666 df-1o 6691 df-2o 6692 df-oadd 6695 df-er 6811 df-en 7027 df-dom 7028 df-fin 7029 df-sup 7330 df-inf 7331 df-pnf 8368 df-mnf 8369 df-xr 8370 df-ltxr 8371 df-le 8372 df-sub 8506 df-neg 8507 df-reap 8911 df-ap 8918 df-div 9011 df-inn 9314 df-2 9372 df-3 9373 df-4 9374 df-n0 9575 df-z 9656 df-uz 9938 df-q 10036 df-rp 10072 df-fz 10429 df-fzo 10567 df-fl 10722 df-mod 10781 df-seqfrec 10906 df-exp 10997 df-fac 11186 df-ihash 11237 df-cj 11629 df-re 11630 df-im 11631 df-rsqrt 11786 df-abs 11787 df-clim 12070 df-sumdc 12145 df-dvds 12580 df-gcd 12756 df-prm 12911 df-pc 13093

This theorem is used by: pcbc 13159

W3C validator