pcfac - Intuitionistic Logic Explorer

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

Theorem pcfac 12519

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 5558	. . . . . . . 8
2		fveq2 5558	. . . . . . . . . 10
3	2	oveq2d 5938	. . . . . . . . 9
4		fvoveq1 5945	. . . . . . . . . 10
5	4	sumeq2sdv 11535	. . . . . . . . 9
6	3, 5	eqeq12d 2211	. . . . . . . 8
7	1, 6	raleqbidv 2709	. . . . . . 7
8	7	imbi2d 230	. . . . . 6
9		fveq2 5558	. . . . . . . 8
10		fveq2 5558	. . . . . . . . . 10
11	10	oveq2d 5938	. . . . . . . . 9
12		fvoveq1 5945	. . . . . . . . . 10
13	12	sumeq2sdv 11535	. . . . . . . . 9
14	11, 13	eqeq12d 2211	. . . . . . . 8
15	9, 14	raleqbidv 2709	. . . . . . 7
16	15	imbi2d 230	. . . . . 6
17		fveq2 5558	. . . . . . . 8
18		fveq2 5558	. . . . . . . . . 10
19	18	oveq2d 5938	. . . . . . . . 9
20		fvoveq1 5945	. . . . . . . . . 10
21	20	sumeq2sdv 11535	. . . . . . . . 9
22	19, 21	eqeq12d 2211	. . . . . . . 8
23	17, 22	raleqbidv 2709	. . . . . . 7
24	23	imbi2d 230	. . . . . 6
25		fveq2 5558	. . . . . . . 8
26		fveq2 5558	. . . . . . . . . 10
27	26	oveq2d 5938	. . . . . . . . 9
28		fvoveq1 5945	. . . . . . . . . 10
29	28	sumeq2sdv 11535	. . . . . . . . 9
30	27, 29	eqeq12d 2211	. . . . . . . 8
31	25, 30	raleqbidv 2709	. . . . . . 7
32	31	imbi2d 230	. . . . . 6
33		1zzd 9353	. . . . . . . . . 10 $/\$
34		eluzelz 9610	. . . . . . . . . . 11
35	34	adantl 277	. . . . . . . . . 10 $/\$
36	33, 35	fzfigd 10523	. . . . . . . . 9 $/\$
37		isumz 11554	. . . . . . . . . 10 $/\$ $/\$ DECID $\/$
38	37	olcs 737	. . . . . . . . 9
39	36, 38	syl 14	. . . . . . . 8 $/\$
40		0nn0 9264	. . . . . . . . . 10
41		elfznn 10129	. . . . . . . . . . . . 13
42	41	nnnn0d 9302	. . . . . . . . . . . 12
43		nn0uz 9636	. . . . . . . . . . . 12
44	42, 43	eleqtrdi 2289	. . . . . . . . . . 11
45	44	adantl 277	. . . . . . . . . 10 $/\$ $/\$
46		simpll 527	. . . . . . . . . 10 $/\$ $/\$
47		pcfaclem 12518	. . . . . . . . . 10 $/\$ $/\$
48	40, 45, 46, 47	mp3an2i 1353	. . . . . . . . 9 $/\$ $/\$
49	48	sumeq2dv 11533	. . . . . . . 8 $/\$
50		fac0 10820	. . . . . . . . . . 11
51	50	oveq2i 5933	. . . . . . . . . 10
52		pc1 12474	. . . . . . . . . 10
53	51, 52	eqtrid 2241	. . . . . . . . 9
54	53	adantr 276	. . . . . . . 8 $/\$
55	39, 49, 54	3eqtr4rd 2240	. . . . . . 7 $/\$
56	55	ralrimiva 2570	. . . . . 6
57		nn0z 9346	. . . . . . . . . . . 12
58	57	adantr 276	. . . . . . . . . . 11 $/\$
59		uzid 9615	. . . . . . . . . . 11
60		peano2uz 9657	. . . . . . . . . . 11
61	58, 59, 60	3syl 17	. . . . . . . . . 10 $/\$
62		uzss 9622	. . . . . . . . . 10
63		ssralv 3247	. . . . . . . . . 10
64	61, 62, 63	3syl 17	. . . . . . . . 9 $/\$
65		oveq1 5929	. . . . . . . . . . 11
66		simpll 527	. . . . . . . . . . . . . . 15 $/\$ $/\$
67		facp1 10822	. . . . . . . . . . . . . . 15
68	66, 67	syl 14	. . . . . . . . . . . . . 14 $/\$ $/\$
69	68	oveq2d 5938	. . . . . . . . . . . . 13 $/\$ $/\$
70		simplr 528	. . . . . . . . . . . . . 14 $/\$ $/\$
71		faccl 10827	. . . . . . . . . . . . . . 15
72		nnz 9345	. . . . . . . . . . . . . . . 16
73		nnne0 9018	. . . . . . . . . . . . . . . 16
74	72, 73	jca 306	. . . . . . . . . . . . . . 15 $/\$
75	66, 71, 74	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
76		nn0p1nn 9288	. . . . . . . . . . . . . . 15
77		nnz 9345	. . . . . . . . . . . . . . . 16
78		nnne0 9018	. . . . . . . . . . . . . . . 16
79	77, 78	jca 306	. . . . . . . . . . . . . . 15 $/\$
80	66, 76, 79	3syl 17	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
81		pcmul 12470	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
82	70, 75, 80, 81	syl3anc 1249	. . . . . . . . . . . . 13 $/\$ $/\$
83	69, 82	eqtr2d 2230	. . . . . . . . . . . 12 $/\$ $/\$
84	66	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
85	84	nn0zd 9446	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
86		prmnn 12278	. . . . . . . . . . . . . . . . . . 19
87	86	ad2antlr 489	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
88		nnexpcl 10644	. . . . . . . . . . . . . . . . . 18 $/\$
89	87, 42, 88	syl2an 289	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
90		fldivp1 12517	. . . . . . . . . . . . . . . . 17 $/\$
91	85, 89, 90	syl2anc 411	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
92		elfzuz 10096	. . . . . . . . . . . . . . . . . . 19
93	66, 76	syl 14	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
94	70, 93	pccld 12469	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
95	94	nn0zd 9446	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
96		elfz5 10092	. . . . . . . . . . . . . . . . . . 19 $/\$
97	92, 95, 96	syl2anr 290	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
98		simpllr 534	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
99	84, 76	syl 14	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
100	99	nnzd 9447	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
101	42	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
102		pcdvdsb 12489	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
103	98, 100, 101, 102	syl3anc 1249	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
104	97, 103	bitr2d 189	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
105	104	ifbid 3582	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
106	91, 105	eqtrd 2229	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
107	106	sumeq2dv 11533	. . . . . . . . . . . . . 14 $/\$ $/\$
108		1zzd 9353	. . . . . . . . . . . . . . . 16 $/\$ $/\$
109		eluzelz 9610	. . . . . . . . . . . . . . . . 17
110	109	adantl 277	. . . . . . . . . . . . . . . 16 $/\$ $/\$
111	108, 110	fzfigd 10523	. . . . . . . . . . . . . . 15 $/\$ $/\$
112		znq 9698	. . . . . . . . . . . . . . . . . 18 $/\$
113	100, 89, 112	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
114	113	flqcld 10367	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
115	114	zcnd 9449	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
116		znq 9698	. . . . . . . . . . . . . . . . . 18 $/\$
117	85, 89, 116	syl2anc 411	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
118	117	flqcld 10367	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
119	118	zcnd 9449	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
120	111, 115, 119	fsumsub 11617	. . . . . . . . . . . . . 14 $/\$ $/\$
121	94	nn0red 9303	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
122	66	nn0red 9303	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
123		peano2re 8162	. . . . . . . . . . . . . . . . . . . 20
124	122, 123	syl 14	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
125	110	zred 9448	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
126	93	nnzd 9447	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
127		zdcle 9402	. . . . . . . . . . . . . . . . . . . . 21 $/\$ DECID
128	95, 126, 127	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ DECID
129		zletric 9370	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\/$
130	95, 126, 129	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $\/$
131	130	ord 725	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
132	93	nnnn0d 9302	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
133		pcdvdsb 12489	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
134	70, 126, 132, 133	syl3anc 1249	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
135	87, 132	nnexpcld 10787	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
136	135	nnzd 9447	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
137		dvdsle 12009	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
138	136, 93, 137	syl2anc 411	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
139	135	nnred 9003	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
140	139, 124	lenltd 8144	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
141	138, 140	sylibd 149	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
142	134, 141	sylbid 150	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
143	131, 142	syld 45	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
144		prmuz2 12299	. . . . . . . . . . . . . . . . . . . . . 22
145	144	ad2antlr 489	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
146		bernneq3 10754	. . . . . . . . . . . . . . . . . . . . 21 $/\$
147	145, 132, 146	syl2anc 411	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
148		condc 854	. . . . . . . . . . . . . . . . . . . 20 DECID
149	128, 143, 147, 148	syl3c 63	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
150		eluzle 9613	. . . . . . . . . . . . . . . . . . . 20
151	150	adantl 277	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
152	121, 124, 125, 149, 151	letrd 8150	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
153		eluz 9614	. . . . . . . . . . . . . . . . . . 19 $/\$
154	95, 110, 153	syl2anc 411	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
155	152, 154	mpbird 167	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
156		fzss2 10139	. . . . . . . . . . . . . . . . 17
157	155, 156	syl 14	. . . . . . . . . . . . . . . 16 $/\$ $/\$
158		elfzelz 10100	. . . . . . . . . . . . . . . . . . 19
159	158	adantl 277	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
160		1zzd 9353	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
161	95	adantr 276	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
162		fzdcel 10115	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ DECID
163	159, 160, 161, 162	syl3anc 1249	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$ DECID
164	163	ralrimiva 2570	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID
165		sumhashdc 12516	. . . . . . . . . . . . . . . 16 $/\$ $/\$ DECID ♯
166	111, 157, 164, 165	syl3anc 1249	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
167		hashfz1 10875	. . . . . . . . . . . . . . . 16 ♯
168	94, 167	syl 14	. . . . . . . . . . . . . . 15 $/\$ $/\$ ♯
169	166, 168	eqtrd 2229	. . . . . . . . . . . . . 14 $/\$ $/\$
170	107, 120, 169	3eqtr3d 2237	. . . . . . . . . . . . 13 $/\$ $/\$
171	111, 115	fsumcl 11565	. . . . . . . . . . . . . 14 $/\$ $/\$
172	111, 119	fsumcl 11565	. . . . . . . . . . . . . 14 $/\$ $/\$
173	94	nn0cnd 9304	. . . . . . . . . . . . . 14 $/\$ $/\$
174	171, 172, 173	subaddd 8355	. . . . . . . . . . . . 13 $/\$ $/\$
175	170, 174	mpbid 147	. . . . . . . . . . . 12 $/\$ $/\$
176	83, 175	eqeq12d 2211	. . . . . . . . . . 11 $/\$ $/\$
177	65, 176	imbitrid 154	. . . . . . . . . 10 $/\$ $/\$
178	177	ralimdva 2564	. . . . . . . . 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 9440	. . . . 5
183	182	imp 124	. . . 4 $/\$
184		oveq2 5930	. . . . . . 7
185	184	sumeq1d 11531	. . . . . 6
186	185	eqeq2d 2208	. . . . 5
187	186	rspcv 2864	. . . 4
188	183, 187	syl5 32	. . 3 $/\$
189	188	3impib 1203	. 2 $/\$ $/\$
190	189	3com12 1209	1 $/\$ $/\$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4 $/\$ wa 104

wb 105 $\/$ wo 709 DECID wdc 835 $/\$ w3a 980

wceq 1364

wcel 2167

wne 2367

wral 2475

wss 3157

cif 3561 class class class wbr 4033

cfv 5258 (class class class)co 5922

cfn 6799

cr 7878

cc0 7879

c1 7880

caddc 7882

cmul 7884

clt 8061

cle 8062

cmin 8197

cdiv 8699

cn 8990

c2 9041

cn0 9249

cz 9326

cuz 9601

cq 9693

cfz 10083

cfl 10358

cexp 10630

cfa 10817 ♯chash 10867

csu 11518

cdvds 11952

cprime 12275

cpc 12453

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 615 ax-in2 616 ax-io 710 ax-5 1461 ax-7 1462 ax-gen 1463 ax-ie1 1507 ax-ie2 1508 ax-8 1518 ax-10 1519 ax-11 1520 ax-i12 1521 ax-bndl 1523 ax-4 1524 ax-17 1540 ax-i9 1544 ax-ial 1548 ax-i5r 1549 ax-13 2169 ax-14 2170 ax-ext 2178 ax-coll 4148 ax-sep 4151 ax-nul 4159 ax-pow 4207 ax-pr 4242 ax-un 4468 ax-setind 4573 ax-iinf 4624 ax-cnex 7970 ax-resscn 7971 ax-1cn 7972 ax-1re 7973 ax-icn 7974 ax-addcl 7975 ax-addrcl 7976 ax-mulcl 7977 ax-mulrcl 7978 ax-addcom 7979 ax-mulcom 7980 ax-addass 7981 ax-mulass 7982 ax-distr 7983 ax-i2m1 7984 ax-0lt1 7985 ax-1rid 7986 ax-0id 7987 ax-rnegex 7988 ax-precex 7989 ax-cnre 7990 ax-pre-ltirr 7991 ax-pre-ltwlin 7992 ax-pre-lttrn 7993 ax-pre-apti 7994 ax-pre-ltadd 7995 ax-pre-mulgt0 7996 ax-pre-mulext 7997 ax-arch 7998 ax-caucvg 7999

This theorem depends on definitions: df-bi 117 df-stab 832 df-dc 836 df-3or 981 df-3an 982 df-tru 1367 df-fal 1370 df-nf 1475 df-sb 1777 df-eu 2048 df-mo 2049 df-clab 2183 df-cleq 2189 df-clel 2192 df-nfc 2328 df-ne 2368 df-nel 2463 df-ral 2480 df-rex 2481 df-reu 2482 df-rmo 2483 df-rab 2484 df-v 2765 df-sbc 2990 df-csb 3085 df-dif 3159 df-un 3161 df-in 3163 df-ss 3170 df-nul 3451 df-if 3562 df-pw 3607 df-sn 3628 df-pr 3629 df-op 3631 df-uni 3840 df-int 3875 df-iun 3918 df-br 4034 df-opab 4095 df-mpt 4096 df-tr 4132 df-id 4328 df-po 4331 df-iso 4332 df-iord 4401 df-on 4403 df-ilim 4404 df-suc 4406 df-iom 4627 df-xp 4669 df-rel 4670 df-cnv 4671 df-co 4672 df-dm 4673 df-rn 4674 df-res 4675 df-ima 4676 df-iota 5219 df-fun 5260 df-fn 5261 df-f 5262 df-f1 5263 df-fo 5264 df-f1o 5265 df-fv 5266 df-isom 5267 df-riota 5877 df-ov 5925 df-oprab 5926 df-mpo 5927 df-1st 6198 df-2nd 6199 df-recs 6363 df-irdg 6428 df-frec 6449 df-1o 6474 df-2o 6475 df-oadd 6478 df-er 6592 df-en 6800 df-dom 6801 df-fin 6802 df-sup 7050 df-inf 7051 df-pnf 8063 df-mnf 8064 df-xr 8065 df-ltxr 8066 df-le 8067 df-sub 8199 df-neg 8200 df-reap 8602 df-ap 8609 df-div 8700 df-inn 8991 df-2 9049 df-3 9050 df-4 9051 df-n0 9250 df-z 9327 df-uz 9602 df-q 9694 df-rp 9729 df-fz 10084 df-fzo 10218 df-fl 10360 df-mod 10415 df-seqfrec 10540 df-exp 10631 df-fac 10818 df-ihash 10868 df-cj 11007 df-re 11008 df-im 11009 df-rsqrt 11163 df-abs 11164 df-clim 11444 df-sumdc 11519 df-dvds 11953 df-gcd 12121 df-prm 12276 df-pc 12454

This theorem is referenced by: pcbc 12520

W3C validator