pcfac - Intuitionistic Logic Explorer

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

Theorem pcfac 12913

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 5635	. . . . . . . 8
2		fveq2 5635	. . . . . . . . . 10
3	2	oveq2d 6029	. . . . . . . . 9
4		fvoveq1 6036	. . . . . . . . . 10
5	4	sumeq2sdv 11921	. . . . . . . . 9
6	3, 5	eqeq12d 2244	. . . . . . . 8
7	1, 6	raleqbidv 2744	. . . . . . 7
8	7	imbi2d 230	. . . . . 6
9		fveq2 5635	. . . . . . . 8
10		fveq2 5635	. . . . . . . . . 10
11	10	oveq2d 6029	. . . . . . . . 9
12		fvoveq1 6036	. . . . . . . . . 10
13	12	sumeq2sdv 11921	. . . . . . . . 9
14	11, 13	eqeq12d 2244	. . . . . . . 8
15	9, 14	raleqbidv 2744	. . . . . . 7
16	15	imbi2d 230	. . . . . 6
17		fveq2 5635	. . . . . . . 8
18		fveq2 5635	. . . . . . . . . 10
19	18	oveq2d 6029	. . . . . . . . 9
20		fvoveq1 6036	. . . . . . . . . 10
21	20	sumeq2sdv 11921	. . . . . . . . 9
22	19, 21	eqeq12d 2244	. . . . . . . 8
23	17, 22	raleqbidv 2744	. . . . . . 7
24	23	imbi2d 230	. . . . . 6
25		fveq2 5635	. . . . . . . 8
26		fveq2 5635	. . . . . . . . . 10
27	26	oveq2d 6029	. . . . . . . . 9
28		fvoveq1 6036	. . . . . . . . . 10
29	28	sumeq2sdv 11921	. . . . . . . . 9
30	27, 29	eqeq12d 2244	. . . . . . . 8
31	25, 30	raleqbidv 2744	. . . . . . 7
32	31	imbi2d 230	. . . . . 6
33		1zzd 9496	. . . . . . . . . 10 $/\$
34		eluzelz 9755	. . . . . . . . . . 11
35	34	adantl 277	. . . . . . . . . 10 $/\$
36	33, 35	fzfigd 10683	. . . . . . . . 9 $/\$
37		isumz 11940	. . . . . . . . . 10 $/\$ $/\$ DECID $\/$
38	37	olcs 741	. . . . . . . . 9
39	36, 38	syl 14	. . . . . . . 8 $/\$
40		0nn0 9407	. . . . . . . . . 10
41		elfznn 10279	. . . . . . . . . . . . 13
42	41	nnnn0d 9445	. . . . . . . . . . . 12
43		nn0uz 9781	. . . . . . . . . . . 12
44	42, 43	eleqtrdi 2322	. . . . . . . . . . 11
45	44	adantl 277	. . . . . . . . . 10 $/\$ $/\$
46		simpll 527	. . . . . . . . . 10 $/\$ $/\$
47		pcfaclem 12912	. . . . . . . . . 10 $/\$ $/\$
48	40, 45, 46, 47	mp3an2i 1376	. . . . . . . . 9 $/\$ $/\$
49	48	sumeq2dv 11919	. . . . . . . 8 $/\$
50		fac0 10980	. . . . . . . . . . 11
51	50	oveq2i 6024	. . . . . . . . . 10
52		pc1 12868	. . . . . . . . . 10
53	51, 52	eqtrid 2274	. . . . . . . . 9
54	53	adantr 276	. . . . . . . 8 $/\$
55	39, 49, 54	3eqtr4rd 2273	. . . . . . 7 $/\$
56	55	ralrimiva 2603	. . . . . 6
57		nn0z 9489	. . . . . . . . . . . 12
58	57	adantr 276	. . . . . . . . . . 11 $/\$
59		uzid 9760	. . . . . . . . . . 11
60		peano2uz 9807	. . . . . . . . . . 11
61	58, 59, 60	3syl 17	. . . . . . . . . 10 $/\$
62		uzss 9767	. . . . . . . . . 10
63		ssralv 3289	. . . . . . . . . 10
64	61, 62, 63	3syl 17	. . . . . . . . 9 $/\$
65		oveq1 6020	. . . . . . . . . . 11
66		simpll 527	. . . . . . . . . . . . . . 15 $/\$ $/\$
67		facp1 10982	. . . . . . . . . . . . . . 15
68	66, 67	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
69	68	oveq2d 6029	. . . . . . . . . . . . 13 $/\$ $/\$
70		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$
71		faccl 10987	. . . . . . . . . . . . . . 15
72		nnz 9488	. . . . . . . . . . . . . . . 16
73		nnne0 9161	. . . . . . . . . . . . . . . 16
74	72, 73	jca 306	. . . . . . . . . . . . . . 15 $/\$
75	66, 71, 74	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76		nn0p1nn 9431	. . . . . . . . . . . . . . 15
77		nnz 9488	. . . . . . . . . . . . . . . 16
78		nnne0 9161	. . . . . . . . . . . . . . . 16
79	77, 78	jca 306	. . . . . . . . . . . . . . 15 $/\$
80	66, 76, 79	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
81		pcmul 12864	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
82	70, 75, 80, 81	syl3anc 1271	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 82	eqtr2d 2263	. . . . . . . . . . . 12 $/\$ $/\$
84	66	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	84	nn0zd 9590	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		prmnn 12672	. . . . . . . . . . . . . . . . . . 19
87	86	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
88		nnexpcl 10804	. . . . . . . . . . . . . . . . . 18 $/\$
89	87, 42, 88	syl2an 289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
90		fldivp1 12911	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92		elfzuz 10246	. . . . . . . . . . . . . . . . . . 19
93	66, 76	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
94	70, 93	pccld 12863	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
95	94	nn0zd 9590	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
96		elfz5 10242	. . . . . . . . . . . . . . . . . . 19 $/\$
97	92, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
98		simpllr 534	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
99	84, 76	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
100	99	nnzd 9591	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
101	42	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		pcdvdsb 12883	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
103	98, 100, 101, 102	syl3anc 1271	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104	97, 103	bitr2d 189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	104	ifbid 3625	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	91, 105	eqtrd 2262	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107	106	sumeq2dv 11919	. . . . . . . . . . . . . 14 $/\$ $/\$
108		1zzd 9496	. . . . . . . . . . . . . . . 16 $/\$ $/\$
109		eluzelz 9755	. . . . . . . . . . . . . . . . 17
110	109	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	108, 110	fzfigd 10683	. . . . . . . . . . . . . . 15 $/\$ $/\$
112		znq 9848	. . . . . . . . . . . . . . . . . 18 $/\$
113	100, 89, 112	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
114	113	flqcld 10527	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	114	zcnd 9593	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
116		znq 9848	. . . . . . . . . . . . . . . . . 18 $/\$
117	85, 89, 116	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	117	flqcld 10527	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	118	zcnd 9593	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	111, 115, 119	fsumsub 12003	. . . . . . . . . . . . . 14 $/\$ $/\$
121	94	nn0red 9446	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122	66	nn0red 9446	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123		peano2re 8305	. . . . . . . . . . . . . . . . . . . 20
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	110	zred 9592	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	93	nnzd 9591	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127		zdcle 9546	. . . . . . . . . . . . . . . . . . . . 21 $/\$ DECID
128	95, 126, 127	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ DECID
129		zletric 9513	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
130	95, 126, 129	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
131	130	ord 729	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
132	93	nnnn0d 9445	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
133		pcdvdsb 12883	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
134	70, 126, 132, 133	syl3anc 1271	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
135	87, 132	nnexpcld 10947	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
136	135	nnzd 9591	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
137		dvdsle 12395	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
138	136, 93, 137	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
139	135	nnred 9146	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	139, 124	lenltd 8287	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141	138, 140	sylibd 149	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
142	134, 141	sylbid 150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
143	131, 142	syld 45	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
144		prmuz2 12693	. . . . . . . . . . . . . . . . . . . . . 22
145	144	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
146		bernneq3 10914	. . . . . . . . . . . . . . . . . . . . 21 $/\$
147	145, 132, 146	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148		condc 858	. . . . . . . . . . . . . . . . . . . 20 DECID
149	128, 143, 147, 148	syl3c 63	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
150		eluzle 9758	. . . . . . . . . . . . . . . . . . . 20
151	150	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
152	121, 124, 125, 149, 151	letrd 8293	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153		eluz 9759	. . . . . . . . . . . . . . . . . . 19 $/\$
154	95, 110, 153	syl2anc 411	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
155	152, 154	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
156		fzss2 10289	. . . . . . . . . . . . . . . . 17
157	155, 156	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$
158		elfzelz 10250	. . . . . . . . . . . . . . . . . . 19
159	158	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160		1zzd 9496	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
161	95	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
162		fzdcel 10265	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ DECID
163	159, 160, 161, 162	syl3anc 1271	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ DECID
164	163	ralrimiva 2603	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID
165		sumhashdc 12910	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID ♯
166	111, 157, 164, 165	syl3anc 1271	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
167		hashfz1 11035	. . . . . . . . . . . . . . . 16 ♯
168	94, 167	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
169	166, 168	eqtrd 2262	. . . . . . . . . . . . . 14 $/\$ $/\$
170	107, 120, 169	3eqtr3d 2270	. . . . . . . . . . . . 13 $/\$ $/\$
171	111, 115	fsumcl 11951	. . . . . . . . . . . . . 14 $/\$ $/\$
172	111, 119	fsumcl 11951	. . . . . . . . . . . . . 14 $/\$ $/\$
173	94	nn0cnd 9447	. . . . . . . . . . . . . 14 $/\$ $/\$
174	171, 172, 173	subaddd 8498	. . . . . . . . . . . . 13 $/\$ $/\$
175	170, 174	mpbid 147	. . . . . . . . . . . 12 $/\$ $/\$
176	83, 175	eqeq12d 2244	. . . . . . . . . . 11 $/\$ $/\$
177	65, 176	imbitrid 154	. . . . . . . . . 10 $/\$ $/\$
178	177	ralimdva 2597	. . . . . . . . 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 9584	. . . . 5
183	182	imp 124	. . . 4 $/\$
184		oveq2 6021	. . . . . . 7
185	184	sumeq1d 11917	. . . . . 6
186	185	eqeq2d 2241	. . . . 5
187	186	rspcv 2904	. . . 4
188	183, 187	syl5 32	. . 3 $/\$
189	188	3impib 1225	. 2 $/\$ $/\$
190	189	3com12 1231	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 713 DECID wdc 839 $/\$ w3a 1002

wceq 1395

wcel 2200

wne 2400

wral 2508

wss 3198

cif 3603 class class class wbr 4086

cfv 5324 (class class class)co 6013

cfn 6904

cr 8021

cc0 8022

c1 8023

caddc 8025

cmul 8027

clt 8204

cle 8205

cmin 8340

cdiv 8842

cn 9133

c2 9184

cn0 9392

cz 9469

cuz 9745

cq 9843

cfz 10233

cfl 10518

cexp 10790

cfa 10977 ♯chash 11027

csu 11904

cdvds 12338

cprime 12669

cpc 12847

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 617 ax-in2 618 ax-io 714 ax-5 1493 ax-7 1494 ax-gen 1495 ax-ie1 1539 ax-ie2 1540 ax-8 1550 ax-10 1551 ax-11 1552 ax-i12 1553 ax-bndl 1555 ax-4 1556 ax-17 1572 ax-i9 1576 ax-ial 1580 ax-i5r 1581 ax-13 2202 ax-14 2203 ax-ext 2211 ax-coll 4202 ax-sep 4205 ax-nul 4213 ax-pow 4262 ax-pr 4297 ax-un 4528 ax-setind 4633 ax-iinf 4684 ax-cnex 8113 ax-resscn 8114 ax-1cn 8115 ax-1re 8116 ax-icn 8117 ax-addcl 8118 ax-addrcl 8119 ax-mulcl 8120 ax-mulrcl 8121 ax-addcom 8122 ax-mulcom 8123 ax-addass 8124 ax-mulass 8125 ax-distr 8126 ax-i2m1 8127 ax-0lt1 8128 ax-1rid 8129 ax-0id 8130 ax-rnegex 8131 ax-precex 8132 ax-cnre 8133 ax-pre-ltirr 8134 ax-pre-ltwlin 8135 ax-pre-lttrn 8136 ax-pre-apti 8137 ax-pre-ltadd 8138 ax-pre-mulgt0 8139 ax-pre-mulext 8140 ax-arch 8141 ax-caucvg 8142

This theorem depends on definitions: df-bi 117 df-stab 836 df-dc 840 df-3or 1003 df-3an 1004 df-tru 1398 df-fal 1401 df-nf 1507 df-sb 1809 df-eu 2080 df-mo 2081 df-clab 2216 df-cleq 2222 df-clel 2225 df-nfc 2361 df-ne 2401 df-nel 2496 df-ral 2513 df-rex 2514 df-reu 2515 df-rmo 2516 df-rab 2517 df-v 2802 df-sbc 3030 df-csb 3126 df-dif 3200 df-un 3202 df-in 3204 df-ss 3211 df-nul 3493 df-if 3604 df-pw 3652 df-sn 3673 df-pr 3674 df-op 3676 df-uni 3892 df-int 3927 df-iun 3970 df-br 4087 df-opab 4149 df-mpt 4150 df-tr 4186 df-id 4388 df-po 4391 df-iso 4392 df-iord 4461 df-on 4463 df-ilim 4464 df-suc 4466 df-iom 4687 df-xp 4729 df-rel 4730 df-cnv 4731 df-co 4732 df-dm 4733 df-rn 4734 df-res 4735 df-ima 4736 df-iota 5284 df-fun 5326 df-fn 5327 df-f 5328 df-f1 5329 df-fo 5330 df-f1o 5331 df-fv 5332 df-isom 5333 df-riota 5966 df-ov 6016 df-oprab 6017 df-mpo 6018 df-1st 6298 df-2nd 6299 df-recs 6466 df-irdg 6531 df-frec 6552 df-1o 6577 df-2o 6578 df-oadd 6581 df-er 6697 df-en 6905 df-dom 6906 df-fin 6907 df-sup 7174 df-inf 7175 df-pnf 8206 df-mnf 8207 df-xr 8208 df-ltxr 8209 df-le 8210 df-sub 8342 df-neg 8343 df-reap 8745 df-ap 8752 df-div 8843 df-inn 9134 df-2 9192 df-3 9193 df-4 9194 df-n0 9393 df-z 9470 df-uz 9746 df-q 9844 df-rp 9879 df-fz 10234 df-fzo 10368 df-fl 10520 df-mod 10575 df-seqfrec 10700 df-exp 10791 df-fac 10978 df-ihash 11028 df-cj 11393 df-re 11394 df-im 11395 df-rsqrt 11549 df-abs 11550 df-clim 11830 df-sumdc 11905 df-dvds 12339 df-gcd 12515 df-prm 12670 df-pc 12848

This theorem is referenced by: pcbc 12914

W3C validator