pcfac - Intuitionistic Logic Explorer

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

Theorem pcfac 12289

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 5494	. . . . . . . 8
2		fveq2 5494	. . . . . . . . . 10
3	2	oveq2d 5866	. . . . . . . . 9
4		fvoveq1 5873	. . . . . . . . . 10
5	4	sumeq2sdv 11320	. . . . . . . . 9
6	3, 5	eqeq12d 2185	. . . . . . . 8
7	1, 6	raleqbidv 2677	. . . . . . 7
8	7	imbi2d 229	. . . . . 6
9		fveq2 5494	. . . . . . . 8
10		fveq2 5494	. . . . . . . . . 10
11	10	oveq2d 5866	. . . . . . . . 9
12		fvoveq1 5873	. . . . . . . . . 10
13	12	sumeq2sdv 11320	. . . . . . . . 9
14	11, 13	eqeq12d 2185	. . . . . . . 8
15	9, 14	raleqbidv 2677	. . . . . . 7
16	15	imbi2d 229	. . . . . 6
17		fveq2 5494	. . . . . . . 8
18		fveq2 5494	. . . . . . . . . 10
19	18	oveq2d 5866	. . . . . . . . 9
20		fvoveq1 5873	. . . . . . . . . 10
21	20	sumeq2sdv 11320	. . . . . . . . 9
22	19, 21	eqeq12d 2185	. . . . . . . 8
23	17, 22	raleqbidv 2677	. . . . . . 7
24	23	imbi2d 229	. . . . . 6
25		fveq2 5494	. . . . . . . 8
26		fveq2 5494	. . . . . . . . . 10
27	26	oveq2d 5866	. . . . . . . . 9
28		fvoveq1 5873	. . . . . . . . . 10
29	28	sumeq2sdv 11320	. . . . . . . . 9
30	27, 29	eqeq12d 2185	. . . . . . . 8
31	25, 30	raleqbidv 2677	. . . . . . 7
32	31	imbi2d 229	. . . . . 6
33		1zzd 9226	. . . . . . . . . 10 $/\$
34		eluzelz 9483	. . . . . . . . . . 11
35	34	adantl 275	. . . . . . . . . 10 $/\$
36	33, 35	fzfigd 10374	. . . . . . . . 9 $/\$
37		isumz 11339	. . . . . . . . . 10 $/\$ $/\$ DECID $\/$
38	37	olcs 731	. . . . . . . . 9
39	36, 38	syl 14	. . . . . . . 8 $/\$
40		0nn0 9137	. . . . . . . . . 10
41		elfznn 9997	. . . . . . . . . . . . 13
42	41	nnnn0d 9175	. . . . . . . . . . . 12
43		nn0uz 9508	. . . . . . . . . . . 12
44	42, 43	eleqtrdi 2263	. . . . . . . . . . 11
45	44	adantl 275	. . . . . . . . . 10 $/\$ $/\$
46		simpll 524	. . . . . . . . . 10 $/\$ $/\$
47		pcfaclem 12288	. . . . . . . . . 10 $/\$ $/\$
48	40, 45, 46, 47	mp3an2i 1337	. . . . . . . . 9 $/\$ $/\$
49	48	sumeq2dv 11318	. . . . . . . 8 $/\$
50		fac0 10649	. . . . . . . . . . 11
51	50	oveq2i 5861	. . . . . . . . . 10
52		pc1 12246	. . . . . . . . . 10
53	51, 52	eqtrid 2215	. . . . . . . . 9
54	53	adantr 274	. . . . . . . 8 $/\$
55	39, 49, 54	3eqtr4rd 2214	. . . . . . 7 $/\$
56	55	ralrimiva 2543	. . . . . 6
57		nn0z 9219	. . . . . . . . . . . 12
58	57	adantr 274	. . . . . . . . . . 11 $/\$
59		uzid 9488	. . . . . . . . . . 11
60		peano2uz 9529	. . . . . . . . . . 11
61	58, 59, 60	3syl 17	. . . . . . . . . 10 $/\$
62		uzss 9494	. . . . . . . . . 10
63		ssralv 3211	. . . . . . . . . 10
64	61, 62, 63	3syl 17	. . . . . . . . 9 $/\$
65		oveq1 5857	. . . . . . . . . . 11
66		simpll 524	. . . . . . . . . . . . . . 15 $/\$ $/\$
67		facp1 10651	. . . . . . . . . . . . . . 15
68	66, 67	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
69	68	oveq2d 5866	. . . . . . . . . . . . 13 $/\$ $/\$
70		simplr 525	. . . . . . . . . . . . . 14 $/\$ $/\$
71		faccl 10656	. . . . . . . . . . . . . . 15
72		nnz 9218	. . . . . . . . . . . . . . . 16
73		nnne0 8893	. . . . . . . . . . . . . . . 16
74	72, 73	jca 304	. . . . . . . . . . . . . . 15 $/\$
75	66, 71, 74	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76		nn0p1nn 9161	. . . . . . . . . . . . . . 15
77		nnz 9218	. . . . . . . . . . . . . . . 16
78		nnne0 8893	. . . . . . . . . . . . . . . 16
79	77, 78	jca 304	. . . . . . . . . . . . . . 15 $/\$
80	66, 76, 79	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
81		pcmul 12242	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
82	70, 75, 80, 81	syl3anc 1233	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 82	eqtr2d 2204	. . . . . . . . . . . 12 $/\$ $/\$
84	66	adantr 274	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	84	nn0zd 9319	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		prmnn 12051	. . . . . . . . . . . . . . . . . . 19
87	86	ad2antlr 486	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
88		nnexpcl 10476	. . . . . . . . . . . . . . . . . 18 $/\$
89	87, 42, 88	syl2an 287	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
90		fldivp1 12287	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 409	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92		elfzuz 9964	. . . . . . . . . . . . . . . . . . 19
93	66, 76	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
94	70, 93	pccld 12241	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
95	94	nn0zd 9319	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
96		elfz5 9960	. . . . . . . . . . . . . . . . . . 19 $/\$
97	92, 95, 96	syl2anr 288	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
98		simpllr 529	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
99	84, 76	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
100	99	nnzd 9320	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
101	42	adantl 275	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		pcdvdsb 12260	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
103	98, 100, 101, 102	syl3anc 1233	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104	97, 103	bitr2d 188	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	104	ifbid 3546	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	91, 105	eqtrd 2203	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107	106	sumeq2dv 11318	. . . . . . . . . . . . . 14 $/\$ $/\$
108		1zzd 9226	. . . . . . . . . . . . . . . 16 $/\$ $/\$
109		eluzelz 9483	. . . . . . . . . . . . . . . . 17
110	109	adantl 275	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	108, 110	fzfigd 10374	. . . . . . . . . . . . . . 15 $/\$ $/\$
112		znq 9570	. . . . . . . . . . . . . . . . . 18 $/\$
113	100, 89, 112	syl2anc 409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
114	113	flqcld 10220	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	114	zcnd 9322	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
116		znq 9570	. . . . . . . . . . . . . . . . . 18 $/\$
117	85, 89, 116	syl2anc 409	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	117	flqcld 10220	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	118	zcnd 9322	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	111, 115, 119	fsumsub 11402	. . . . . . . . . . . . . 14 $/\$ $/\$
121	94	nn0red 9176	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122	66	nn0red 9176	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123		peano2re 8042	. . . . . . . . . . . . . . . . . . . 20
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	110	zred 9321	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	93	nnzd 9320	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127		zdcle 9275	. . . . . . . . . . . . . . . . . . . . 21 $/\$ DECID
128	95, 126, 127	syl2anc 409	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ DECID
129		zletric 9243	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
130	95, 126, 129	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
131	130	ord 719	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
132	93	nnnn0d 9175	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
133		pcdvdsb 12260	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
134	70, 126, 132, 133	syl3anc 1233	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
135	87, 132	nnexpcld 10618	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
136	135	nnzd 9320	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
137		dvdsle 11791	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
138	136, 93, 137	syl2anc 409	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
139	135	nnred 8878	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	139, 124	lenltd 8024	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141	138, 140	sylibd 148	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
142	134, 141	sylbid 149	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
143	131, 142	syld 45	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
144		prmuz2 12072	. . . . . . . . . . . . . . . . . . . . . 22
145	144	ad2antlr 486	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
146		bernneq3 10585	. . . . . . . . . . . . . . . . . . . . 21 $/\$
147	145, 132, 146	syl2anc 409	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148		condc 848	. . . . . . . . . . . . . . . . . . . 20 DECID
149	128, 143, 147, 148	syl3c 63	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
150		eluzle 9486	. . . . . . . . . . . . . . . . . . . 20
151	150	adantl 275	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
152	121, 124, 125, 149, 151	letrd 8030	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153		eluz 9487	. . . . . . . . . . . . . . . . . . 19 $/\$
154	95, 110, 153	syl2anc 409	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
155	152, 154	mpbird 166	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
156		fzss2 10007	. . . . . . . . . . . . . . . . 17
157	155, 156	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$
158		elfzelz 9968	. . . . . . . . . . . . . . . . . . 19
159	158	adantl 275	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160		1zzd 9226	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
161	95	adantr 274	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
162		fzdcel 9983	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ DECID
163	159, 160, 161, 162	syl3anc 1233	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ DECID
164	163	ralrimiva 2543	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID
165		sumhashdc 12286	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID ♯
166	111, 157, 164, 165	syl3anc 1233	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
167		hashfz1 10704	. . . . . . . . . . . . . . . 16 ♯
168	94, 167	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
169	166, 168	eqtrd 2203	. . . . . . . . . . . . . 14 $/\$ $/\$
170	107, 120, 169	3eqtr3d 2211	. . . . . . . . . . . . 13 $/\$ $/\$
171	111, 115	fsumcl 11350	. . . . . . . . . . . . . 14 $/\$ $/\$
172	111, 119	fsumcl 11350	. . . . . . . . . . . . . 14 $/\$ $/\$
173	94	nn0cnd 9177	. . . . . . . . . . . . . 14 $/\$ $/\$
174	171, 172, 173	subaddd 8235	. . . . . . . . . . . . 13 $/\$ $/\$
175	170, 174	mpbid 146	. . . . . . . . . . . 12 $/\$ $/\$
176	83, 175	eqeq12d 2185	. . . . . . . . . . 11 $/\$ $/\$
177	65, 176	syl5ib 153	. . . . . . . . . 10 $/\$ $/\$
178	177	ralimdva 2537	. . . . . . . . 9 $/\$
179	64, 178	syld 45	. . . . . . . 8 $/\$
180	179	ex 114	. . . . . . 7
181	180	a2d 26	. . . . . 6
182	8, 16, 24, 32, 56, 181	nn0ind 9313	. . . . 5
183	182	imp 123	. . . 4 $/\$
184		oveq2 5858	. . . . . . 7
185	184	sumeq1d 11316	. . . . . 6
186	185	eqeq2d 2182	. . . . 5
187	186	rspcv 2830	. . . 4
188	183, 187	syl5 32	. . 3 $/\$
189	188	3impib 1196	. 2 $/\$ $/\$
190	189	3com12 1202	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 103

wb 104 $\/$ wo 703 DECID wdc 829 $/\$ w3a 973

wceq 1348

wcel 2141

wne 2340

wral 2448

wss 3121

cif 3525 class class class wbr 3987

cfv 5196 (class class class)co 5850

cfn 6714

cr 7760

cc0 7761

c1 7762

caddc 7764

cmul 7766

clt 7941

cle 7942

cmin 8077

cdiv 8576

cn 8865

c2 8916

cn0 9122

cz 9199

cuz 9474

cq 9565

cfz 9952

cfl 10211

cexp 10462

cfa 10646 ♯chash 10696

csu 11303

cdvds 11736

cprime 12048

cpc 12225

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 609 ax-in2 610 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-13 2143 ax-14 2144 ax-ext 2152 ax-coll 4102 ax-sep 4105 ax-nul 4113 ax-pow 4158 ax-pr 4192 ax-un 4416 ax-setind 4519 ax-iinf 4570 ax-cnex 7852 ax-resscn 7853 ax-1cn 7854 ax-1re 7855 ax-icn 7856 ax-addcl 7857 ax-addrcl 7858 ax-mulcl 7859 ax-mulrcl 7860 ax-addcom 7861 ax-mulcom 7862 ax-addass 7863 ax-mulass 7864 ax-distr 7865 ax-i2m1 7866 ax-0lt1 7867 ax-1rid 7868 ax-0id 7869 ax-rnegex 7870 ax-precex 7871 ax-cnre 7872 ax-pre-ltirr 7873 ax-pre-ltwlin 7874 ax-pre-lttrn 7875 ax-pre-apti 7876 ax-pre-ltadd 7877 ax-pre-mulgt0 7878 ax-pre-mulext 7879 ax-arch 7880 ax-caucvg 7881

This theorem depends on definitions: df-bi 116 df-stab 826 df-dc 830 df-3or 974 df-3an 975 df-tru 1351 df-fal 1354 df-nf 1454 df-sb 1756 df-eu 2022 df-mo 2023 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-ne 2341 df-nel 2436 df-ral 2453 df-rex 2454 df-reu 2455 df-rmo 2456 df-rab 2457 df-v 2732 df-sbc 2956 df-csb 3050 df-dif 3123 df-un 3125 df-in 3127 df-ss 3134 df-nul 3415 df-if 3526 df-pw 3566 df-sn 3587 df-pr 3588 df-op 3590 df-uni 3795 df-int 3830 df-iun 3873 df-br 3988 df-opab 4049 df-mpt 4050 df-tr 4086 df-id 4276 df-po 4279 df-iso 4280 df-iord 4349 df-on 4351 df-ilim 4352 df-suc 4354 df-iom 4573 df-xp 4615 df-rel 4616 df-cnv 4617 df-co 4618 df-dm 4619 df-rn 4620 df-res 4621 df-ima 4622 df-iota 5158 df-fun 5198 df-fn 5199 df-f 5200 df-f1 5201 df-fo 5202 df-f1o 5203 df-fv 5204 df-isom 5205 df-riota 5806 df-ov 5853 df-oprab 5854 df-mpo 5855 df-1st 6116 df-2nd 6117 df-recs 6281 df-irdg 6346 df-frec 6367 df-1o 6392 df-2o 6393 df-oadd 6396 df-er 6509 df-en 6715 df-dom 6716 df-fin 6717 df-sup 6957 df-inf 6958 df-pnf 7943 df-mnf 7944 df-xr 7945 df-ltxr 7946 df-le 7947 df-sub 8079 df-neg 8080 df-reap 8481 df-ap 8488 df-div 8577 df-inn 8866 df-2 8924 df-3 8925 df-4 8926 df-n0 9123 df-z 9200 df-uz 9475 df-q 9566 df-rp 9598 df-fz 9953 df-fzo 10086 df-fl 10213 df-mod 10266 df-seqfrec 10389 df-exp 10463 df-fac 10647 df-ihash 10697 df-cj 10793 df-re 10794 df-im 10795 df-rsqrt 10949 df-abs 10950 df-clim 11229 df-sumdc 11304 df-dvds 11737 df-gcd 11885 df-prm 12049 df-pc 12226

This theorem is referenced by: pcbc 12290

W3C validator