Theorem pcfac 14418

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:   P,   ,N   ,M

Proof of Theorem pcfac

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 5871	. . . . . . . 8
2		fveq2 5871	. . . . . . . . . 10
3	2	oveq2d 6312	. . . . . . . . 9
4		oveq1 6303	. . . . . . . . . . 11
5	4	fveq2d 5875	. . . . . . . . . 10
6	5	sumeq2sdv 13526	. . . . . . . . 9
7	3, 6	eqeq12d 2479	. . . . . . . 8
8	1, 7	raleqbidv 3068	. . . . . . 7
9	8	imbi2d 316	. . . . . 6
10		fveq2 5871	. . . . . . . 8
11		fveq2 5871	. . . . . . . . . 10
12	11	oveq2d 6312	. . . . . . . . 9
13		oveq1 6303	. . . . . . . . . . 11
14	13	fveq2d 5875	. . . . . . . . . 10
15	14	sumeq2sdv 13526	. . . . . . . . 9
16	12, 15	eqeq12d 2479	. . . . . . . 8
17	10, 16	raleqbidv 3068	. . . . . . 7
18	17	imbi2d 316	. . . . . 6
19		fveq2 5871	. . . . . . . 8
20		fveq2 5871	. . . . . . . . . 10
21	20	oveq2d 6312	. . . . . . . . 9
22		oveq1 6303	. . . . . . . . . . 11
23	22	fveq2d 5875	. . . . . . . . . 10
24	23	sumeq2sdv 13526	. . . . . . . . 9
25	21, 24	eqeq12d 2479	. . . . . . . 8
26	19, 25	raleqbidv 3068	. . . . . . 7
27	26	imbi2d 316	. . . . . 6
28		fveq2 5871	. . . . . . . 8
29		fveq2 5871	. . . . . . . . . 10
30	29	oveq2d 6312	. . . . . . . . 9
31		oveq1 6303	. . . . . . . . . . 11
32	31	fveq2d 5875	. . . . . . . . . 10
33	32	sumeq2sdv 13526	. . . . . . . . 9
34	30, 33	eqeq12d 2479	. . . . . . . 8
35	28, 34	raleqbidv 3068	. . . . . . 7
36	35	imbi2d 316	. . . . . 6
37		fzfid 12083	. . . . . . . . 9
38		sumz 13544	. . . . . . . . . 10
39	38	olcs 395	. . . . . . . . 9
40	37, 39	syl 16	. . . . . . . 8
41		0nn0 10835	. . . . . . . . . . 11
42	41	a1i 11	. . . . . . . . . 10
43		elfznn 11743	. . . . . . . . . . . . 13
44	43	nnnn0d 10877	. . . . . . . . . . . 12
45		nn0uz 11144	. . . . . . . . . . . 12
46	44, 45	syl6eleq 2555	. . . . . . . . . . 11
47	46	adantl 466	. . . . . . . . . 10
48		simpll 753	. . . . . . . . . 10
49		pcfaclem 14417	. . . . . . . . . 10
50	42, 47, 48, 49	syl3anc 1228	. . . . . . . . 9
51	50	sumeq2dv 13525	. . . . . . . 8
52		fac0 12356	. . . . . . . . . . 11
53	52	oveq2i 6307	. . . . . . . . . 10
54		pc1 14379	. . . . . . . . . 10
55	53, 54	syl5eq 2510	. . . . . . . . 9
56	55	adantr 465	. . . . . . . 8
57	40, 51, 56	3eqtr4rd 2509	. . . . . . 7
58	57	ralrimiva 2871	. . . . . 6
59		nn0z 10912	. . . . . . . . . . . 12
60	59	adantr 465	. . . . . . . . . . 11
61		uzid 11124	. . . . . . . . . . 11
62		peano2uz 11163	. . . . . . . . . . 11
63	60, 61, 62	3syl 20	. . . . . . . . . 10
64		uzss 11130	. . . . . . . . . 10
65		ssralv 3563	. . . . . . . . . 10
66	63, 64, 65	3syl 20	. . . . . . . . 9
67		oveq1 6303	. . . . . . . . . . 11
68		simpll 753	. . . . . . . . . . . . . . 15
69		facp1 12358	. . . . . . . . . . . . . . 15
70	68, 69	syl 16	. . . . . . . . . . . . . 14
71	70	oveq2d 6312	. . . . . . . . . . . . 13
72		simplr 755	. . . . . . . . . . . . . 14
73		faccl 12363	. . . . . . . . . . . . . . 15
74		nnz 10911	. . . . . . . . . . . . . . . 16
75		nnne0 10593	. . . . . . . . . . . . . . . 16
76	74, 75	jca 532	. . . . . . . . . . . . . . 15
77	68, 73, 76	3syl 20	. . . . . . . . . . . . . 14
78		nn0p1nn 10860	. . . . . . . . . . . . . . 15
79		nnz 10911	. . . . . . . . . . . . . . . 16
80		nnne0 10593	. . . . . . . . . . . . . . . 16
81	79, 80	jca 532	. . . . . . . . . . . . . . 15
82	68, 78, 81	3syl 20	. . . . . . . . . . . . . 14
83		pcmul 14375	. . . . . . . . . . . . . 14
84	72, 77, 82, 83	syl3anc 1228	. . . . . . . . . . . . 13
85	71, 84	eqtr2d 2499	. . . . . . . . . . . 12
86	68	adantr 465	. . . . . . . . . . . . . . . . . 18
87	86	nn0zd 10992	. . . . . . . . . . . . . . . . 17
88		prmnn 14220	. . . . . . . . . . . . . . . . . . 19
89	88	ad2antlr 726	. . . . . . . . . . . . . . . . . 18
90		nnexpcl 12179	. . . . . . . . . . . . . . . . . 18
91	89, 44, 90	syl2an 477	. . . . . . . . . . . . . . . . 17
92		fldivp1 14416	. . . . . . . . . . . . . . . . 17
93	87, 91, 92	syl2anc 661	. . . . . . . . . . . . . . . 16
94		elfzuz 11713	. . . . . . . . . . . . . . . . . . 19
95	68, 78	syl 16	. . . . . . . . . . . . . . . . . . . . 21
96	72, 95	pccld 14374	. . . . . . . . . . . . . . . . . . . 20
97	96	nn0zd 10992	. . . . . . . . . . . . . . . . . . 19
98		elfz5 11709	. . . . . . . . . . . . . . . . . . 19
99	94, 97, 98	syl2anr 478	. . . . . . . . . . . . . . . . . 18
100		simpllr 760	. . . . . . . . . . . . . . . . . . 19
101	86, 78	syl 16	. . . . . . . . . . . . . . . . . . . 20
102	101	nnzd 10993	. . . . . . . . . . . . . . . . . . 19
103	44	adantl 466	. . . . . . . . . . . . . . . . . . 19
104		pcdvdsb 14392	. . . . . . . . . . . . . . . . . . 19
105	100, 102, 103, 104	syl3anc 1228	. . . . . . . . . . . . . . . . . 18
106	99, 105	bitr2d 254	. . . . . . . . . . . . . . . . 17
107	106	ifbid 3963	. . . . . . . . . . . . . . . 16
108	93, 107	eqtrd 2498	. . . . . . . . . . . . . . 15
109	108	sumeq2dv 13525	. . . . . . . . . . . . . 14
110		fzfid 12083	. . . . . . . . . . . . . . 15
111	68	nn0red 10878	. . . . . . . . . . . . . . . . . . . 20
112		peano2re 9774	. . . . . . . . . . . . . . . . . . . 20
113	111, 112	syl 16	. . . . . . . . . . . . . . . . . . 19
114	113	adantr 465	. . . . . . . . . . . . . . . . . 18
115	114, 91	nndivred 10609	. . . . . . . . . . . . . . . . 17
116	115	flcld 11935	. . . . . . . . . . . . . . . 16
117	116	zcnd 10995	. . . . . . . . . . . . . . 15
118	111	adantr 465	. . . . . . . . . . . . . . . . . 18
119	118, 91	nndivred 10609	. . . . . . . . . . . . . . . . 17
120	119	flcld 11935	. . . . . . . . . . . . . . . 16
121	120	zcnd 10995	. . . . . . . . . . . . . . 15
122	110, 117, 121	fsumsub 13603	. . . . . . . . . . . . . 14
123		fzfi 12082	. . . . . . . . . . . . . . . 16
124	96	nn0red 10878	. . . . . . . . . . . . . . . . . . 19
125		eluzelz 11119	. . . . . . . . . . . . . . . . . . . . 21
126	125	adantl 466	. . . . . . . . . . . . . . . . . . . 20
127	126	zred 10994	. . . . . . . . . . . . . . . . . . 19
128		prmuz2 14235	. . . . . . . . . . . . . . . . . . . . . 22
129	128	ad2antlr 726	. . . . . . . . . . . . . . . . . . . . 21
130	95	nnnn0d 10877	. . . . . . . . . . . . . . . . . . . . 21
131		bernneq3 12294	. . . . . . . . . . . . . . . . . . . . 21
132	129, 130, 131	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20
133	124, 113	letrid 9756	. . . . . . . . . . . . . . . . . . . . . 22
134	133	ord 377	. . . . . . . . . . . . . . . . . . . . 21
135	95	nnzd 10993	. . . . . . . . . . . . . . . . . . . . . . 23
136		pcdvdsb 14392	. . . . . . . . . . . . . . . . . . . . . . 23
137	72, 135, 130, 136	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 22
138	89, 130	nnexpcld 12331	. . . . . . . . . . . . . . . . . . . . . . . . 25
139	138	nnzd 10993	. . . . . . . . . . . . . . . . . . . . . . . 24
140		dvdsle 14031	. . . . . . . . . . . . . . . . . . . . . . . 24
141	139, 95, 140	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . 23
142	138	nnred 10576	. . . . . . . . . . . . . . . . . . . . . . . 24
143	142, 113	lenltd 9752	. . . . . . . . . . . . . . . . . . . . . . 23
144	141, 143	sylibd 214	. . . . . . . . . . . . . . . . . . . . . 22
145	137, 144	sylbid 215	. . . . . . . . . . . . . . . . . . . . 21
146	134, 145	syld 44	. . . . . . . . . . . . . . . . . . . 20
147	132, 146	mt4d 138	. . . . . . . . . . . . . . . . . . 19
148		eluzle 11122	. . . . . . . . . . . . . . . . . . . 20
149	148	adantl 466	. . . . . . . . . . . . . . . . . . 19
150	124, 113, 127, 147, 149	letrd 9760	. . . . . . . . . . . . . . . . . 18
151		eluz 11123	. . . . . . . . . . . . . . . . . . 19
152	97, 126, 151	syl2anc 661	. . . . . . . . . . . . . . . . . 18
153	150, 152	mpbird 232	. . . . . . . . . . . . . . . . 17
154		fzss2 11752	. . . . . . . . . . . . . . . . 17
155	153, 154	syl 16	. . . . . . . . . . . . . . . 16
156		sumhash 14415	. . . . . . . . . . . . . . . 16
157	123, 155, 156	sylancr 663	. . . . . . . . . . . . . . 15
158		hashfz1 12419	. . . . . . . . . . . . . . . 16
159	96, 158	syl 16	. . . . . . . . . . . . . . 15
160	157, 159	eqtrd 2498	. . . . . . . . . . . . . 14
161	109, 122, 160	3eqtr3d 2506	. . . . . . . . . . . . 13
162	110, 117	fsumcl 13555	. . . . . . . . . . . . . 14
163	110, 121	fsumcl 13555	. . . . . . . . . . . . . 14
164	124	recnd 9643	. . . . . . . . . . . . . 14
165	162, 163, 164	subaddd 9972	. . . . . . . . . . . . 13
166	161, 165	mpbid 210	. . . . . . . . . . . 12
167	85, 166	eqeq12d 2479	. . . . . . . . . . 11
168	67, 167	syl5ib 219	. . . . . . . . . 10
169	168	ralimdva 2865	. . . . . . . . 9
170	66, 169	syld 44	. . . . . . . 8
171	170	ex 434	. . . . . . 7
172	171	a2d 26	. . . . . 6
173	9, 18, 27, 36, 58, 172	nn0ind 10984	. . . . 5
174	173	imp 429	. . . 4