MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  pcfac Unicode version

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.
StepHypRef Expression
1 fveq2 5871 . . . . . . . 8
2 fveq2 5871 . . . . . . . . . 10
32oveq2d 6312 . . . . . . . . 9
4 oveq1 6303 . . . . . . . . . . 11
54fveq2d 5875 . . . . . . . . . 10
65sumeq2sdv 13526 . . . . . . . . 9
73, 6eqeq12d 2479 . . . . . . . 8
81, 7raleqbidv 3068 . . . . . . 7
98imbi2d 316 . . . . . 6
10 fveq2 5871 . . . . . . . 8
11 fveq2 5871 . . . . . . . . . 10
1211oveq2d 6312 . . . . . . . . 9
13 oveq1 6303 . . . . . . . . . . 11
1413fveq2d 5875 . . . . . . . . . 10
1514sumeq2sdv 13526 . . . . . . . . 9
1612, 15eqeq12d 2479 . . . . . . . 8
1710, 16raleqbidv 3068 . . . . . . 7
1817imbi2d 316 . . . . . 6
19 fveq2 5871 . . . . . . . 8
20 fveq2 5871 . . . . . . . . . 10
2120oveq2d 6312 . . . . . . . . 9
22 oveq1 6303 . . . . . . . . . . 11
2322fveq2d 5875 . . . . . . . . . 10
2423sumeq2sdv 13526 . . . . . . . . 9
2521, 24eqeq12d 2479 . . . . . . . 8
2619, 25raleqbidv 3068 . . . . . . 7
2726imbi2d 316 . . . . . 6
28 fveq2 5871 . . . . . . . 8
29 fveq2 5871 . . . . . . . . . 10
3029oveq2d 6312 . . . . . . . . 9
31 oveq1 6303 . . . . . . . . . . 11
3231fveq2d 5875 . . . . . . . . . 10
3332sumeq2sdv 13526 . . . . . . . . 9
3430, 33eqeq12d 2479 . . . . . . . 8
3528, 34raleqbidv 3068 . . . . . . 7
3635imbi2d 316 . . . . . 6
37 fzfid 12083 . . . . . . . . 9
38 sumz 13544 . . . . . . . . . 10
3938olcs 395 . . . . . . . . 9
4037, 39syl 16 . . . . . . . 8
41 0nn0 10835 . . . . . . . . . . 11
4241a1i 11 . . . . . . . . . 10
43 elfznn 11743 . . . . . . . . . . . . 13
4443nnnn0d 10877 . . . . . . . . . . . 12
45 nn0uz 11144 . . . . . . . . . . . 12
4644, 45syl6eleq 2555 . . . . . . . . . . 11
4746adantl 466 . . . . . . . . . 10
48 simpll 753 . . . . . . . . . 10
49 pcfaclem 14417 . . . . . . . . . 10
5042, 47, 48, 49syl3anc 1228 . . . . . . . . 9
5150sumeq2dv 13525 . . . . . . . 8
52 fac0 12356 . . . . . . . . . . 11
5352oveq2i 6307 . . . . . . . . . 10
54 pc1 14379 . . . . . . . . . 10
5553, 54syl5eq 2510 . . . . . . . . 9
5655adantr 465 . . . . . . . 8
5740, 51, 563eqtr4rd 2509 . . . . . . 7
5857ralrimiva 2871 . . . . . 6
59 nn0z 10912 . . . . . . . . . . . 12
6059adantr 465 . . . . . . . . . . 11
61 uzid 11124 . . . . . . . . . . 11
62 peano2uz 11163 . . . . . . . . . . 11
6360, 61, 623syl 20 . . . . . . . . . 10
64 uzss 11130 . . . . . . . . . 10
65 ssralv 3563 . . . . . . . . . 10
6663, 64, 653syl 20 . . . . . . . . 9
67 oveq1 6303 . . . . . . . . . . 11
68 simpll 753 . . . . . . . . . . . . . . 15
69 facp1 12358 . . . . . . . . . . . . . . 15
7068, 69syl 16 . . . . . . . . . . . . . 14
7170oveq2d 6312 . . . . . . . . . . . . 13
72 simplr 755 . . . . . . . . . . . . . 14
73 faccl 12363 . . . . . . . . . . . . . . 15
74 nnz 10911 . . . . . . . . . . . . . . . 16
75 nnne0 10593 . . . . . . . . . . . . . . . 16
7674, 75jca 532 . . . . . . . . . . . . . . 15
7768, 73, 763syl 20 . . . . . . . . . . . . . 14
78 nn0p1nn 10860 . . . . . . . . . . . . . . 15
79 nnz 10911 . . . . . . . . . . . . . . . 16
80 nnne0 10593 . . . . . . . . . . . . . . . 16
8179, 80jca 532 . . . . . . . . . . . . . . 15
8268, 78, 813syl 20 . . . . . . . . . . . . . 14
83 pcmul 14375 . . . . . . . . . . . . . 14
8472, 77, 82, 83syl3anc 1228 . . . . . . . . . . . . 13
8571, 84eqtr2d 2499 . . . . . . . . . . . 12
8668adantr 465 . . . . . . . . . . . . . . . . . 18
8786nn0zd 10992 . . . . . . . . . . . . . . . . 17
88 prmnn 14220 . . . . . . . . . . . . . . . . . . 19
8988ad2antlr 726 . . . . . . . . . . . . . . . . . 18
90 nnexpcl 12179 . . . . . . . . . . . . . . . . . 18
9189, 44, 90syl2an 477 . . . . . . . . . . . . . . . . 17
92 fldivp1 14416 . . . . . . . . . . . . . . . . 17
9387, 91, 92syl2anc 661 . . . . . . . . . . . . . . . 16
94 elfzuz 11713 . . . . . . . . . . . . . . . . . . 19
9568, 78syl 16 . . . . . . . . . . . . . . . . . . . . 21
9672, 95pccld 14374 . . . . . . . . . . . . . . . . . . . 20
9796nn0zd 10992 . . . . . . . . . . . . . . . . . . 19
98 elfz5 11709 . . . . . . . . . . . . . . . . . . 19
9994, 97, 98syl2anr 478 . . . . . . . . . . . . . . . . . 18
100 simpllr 760 . . . . . . . . . . . . . . . . . . 19
10186, 78syl 16 . . . . . . . . . . . . . . . . . . . 20
102101nnzd 10993 . . . . . . . . . . . . . . . . . . 19
10344adantl 466 . . . . . . . . . . . . . . . . . . 19
104 pcdvdsb 14392 . . . . . . . . . . . . . . . . . . 19
105100, 102, 103, 104syl3anc 1228 . . . . . . . . . . . . . . . . . 18
10699, 105bitr2d 254 . . . . . . . . . . . . . . . . 17
107106ifbid 3963 . . . . . . . . . . . . . . . 16
10893, 107eqtrd 2498 . . . . . . . . . . . . . . 15
109108sumeq2dv 13525 . . . . . . . . . . . . . 14
110 fzfid 12083 . . . . . . . . . . . . . . 15
11168nn0red 10878 . . . . . . . . . . . . . . . . . . . 20
112 peano2re 9774 . . . . . . . . . . . . . . . . . . . 20
113111, 112syl 16 . . . . . . . . . . . . . . . . . . 19
114113adantr 465 . . . . . . . . . . . . . . . . . 18
115114, 91nndivred 10609 . . . . . . . . . . . . . . . . 17
116115flcld 11935 . . . . . . . . . . . . . . . 16
117116zcnd 10995 . . . . . . . . . . . . . . 15
118111adantr 465 . . . . . . . . . . . . . . . . . 18
119118, 91nndivred 10609 . . . . . . . . . . . . . . . . 17
120119flcld 11935 . . . . . . . . . . . . . . . 16
121120zcnd 10995 . . . . . . . . . . . . . . 15
122110, 117, 121fsumsub 13603 . . . . . . . . . . . . . 14
123 fzfi 12082 . . . . . . . . . . . . . . . 16
12496nn0red 10878 . . . . . . . . . . . . . . . . . . 19
125 eluzelz 11119 . . . . . . . . . . . . . . . . . . . . 21
126125adantl 466 . . . . . . . . . . . . . . . . . . . 20
127126zred 10994 . . . . . . . . . . . . . . . . . . 19
128 prmuz2 14235 . . . . . . . . . . . . . . . . . . . . . 22
129128ad2antlr 726 . . . . . . . . . . . . . . . . . . . . 21
13095nnnn0d 10877 . . . . . . . . . . . . . . . . . . . . 21
131 bernneq3 12294 . . . . . . . . . . . . . . . . . . . . 21
132129, 130, 131syl2anc 661 . . . . . . . . . . . . . . . . . . . 20
133124, 113letrid 9756 . . . . . . . . . . . . . . . . . . . . . 22
134133ord 377 . . . . . . . . . . . . . . . . . . . . 21
13595nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . 23
136 pcdvdsb 14392 . . . . . . . . . . . . . . . . . . . . . . 23
13772, 135, 130, 136syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . 22
13889, 130nnexpcld 12331 . . . . . . . . . . . . . . . . . . . . . . . . 25
139138nnzd 10993 . . . . . . . . . . . . . . . . . . . . . . . 24
140 dvdsle 14031 . . . . . . . . . . . . . . . . . . . . . . . 24
141139, 95, 140syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . 23
142138nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . 24
143142, 113lenltd 9752 . . . . . . . . . . . . . . . . . . . . . . 23
144141, 143sylibd 214 . . . . . . . . . . . . . . . . . . . . . 22
145137, 144sylbid 215 . . . . . . . . . . . . . . . . . . . . 21
146134, 145syld 44 . . . . . . . . . . . . . . . . . . . 20
147132, 146mt4d 138 . . . . . . . . . . . . . . . . . . 19
148 eluzle 11122 . . . . . . . . . . . . . . . . . . . 20
149148adantl 466 . . . . . . . . . . . . . . . . . . 19
150124, 113, 127, 147, 149letrd 9760 . . . . . . . . . . . . . . . . . 18
151 eluz 11123 . . . . . . . . . . . . . . . . . . 19
15297, 126, 151syl2anc 661 . . . . . . . . . . . . . . . . . 18
153150, 152mpbird 232 . . . . . . . . . . . . . . . . 17
154 fzss2 11752 . . . . . . . . . . . . . . . . 17
155153, 154syl 16 . . . . . . . . . . . . . . . 16
156 sumhash 14415 . . . . . . . . . . . . . . . 16
157123, 155, 156sylancr 663 . . . . . . . . . . . . . . 15
158 hashfz1 12419 . . . . . . . . . . . . . . . 16
15996, 158syl 16 . . . . . . . . . . . . . . 15
160157, 159eqtrd 2498 . . . . . . . . . . . . . 14
161109, 122, 1603eqtr3d 2506 . . . . . . . . . . . . 13
162110, 117fsumcl 13555 . . . . . . . . . . . . . 14
163110, 121fsumcl 13555 . . . . . . . . . . . . . 14
164124recnd 9643 . . . . . . . . . . . . . 14
165162, 163, 164subaddd 9972 . . . . . . . . . . . . 13
166161, 165mpbid 210 . . . . . . . . . . . 12
16785, 166eqeq12d 2479 . . . . . . . . . . 11
16867, 167syl5ib 219 . . . . . . . . . 10
169168ralimdva 2865 . . . . . . . . 9
17066, 169syld 44 . . . . . . . 8
171170ex 434 . . . . . . 7
172171a2d 26 . . . . . 6
1739, 18, 27, 36, 58, 172nn0ind 10984 . . . . 5
174173imp 429 . . . 4