Metamath Proof Explorer


Theorem pcfac

Description: Calculate the prime count of a factorial. (Contributed by Mario Carneiro, 11-Mar-2014) (Revised by Mario Carneiro, 21-May-2014)

Ref Expression
Assertion pcfac N 0 M N P P pCnt N ! = k = 1 M N P k

Proof

Step Hyp Ref Expression
1 fveq2 x = 0 x = 0
2 fveq2 x = 0 x ! = 0 !
3 2 oveq2d x = 0 P pCnt x ! = P pCnt 0 !
4 fvoveq1 x = 0 x P k = 0 P k
5 4 sumeq2sdv x = 0 k = 1 m x P k = k = 1 m 0 P k
6 3 5 eqeq12d x = 0 P pCnt x ! = k = 1 m x P k P pCnt 0 ! = k = 1 m 0 P k
7 1 6 raleqbidv x = 0 m x P pCnt x ! = k = 1 m x P k m 0 P pCnt 0 ! = k = 1 m 0 P k
8 7 imbi2d x = 0 P m x P pCnt x ! = k = 1 m x P k P m 0 P pCnt 0 ! = k = 1 m 0 P k
9 fveq2 x = n x = n
10 fveq2 x = n x ! = n !
11 10 oveq2d x = n P pCnt x ! = P pCnt n !
12 fvoveq1 x = n x P k = n P k
13 12 sumeq2sdv x = n k = 1 m x P k = k = 1 m n P k
14 11 13 eqeq12d x = n P pCnt x ! = k = 1 m x P k P pCnt n ! = k = 1 m n P k
15 9 14 raleqbidv x = n m x P pCnt x ! = k = 1 m x P k m n P pCnt n ! = k = 1 m n P k
16 15 imbi2d x = n P m x P pCnt x ! = k = 1 m x P k P m n P pCnt n ! = k = 1 m n P k
17 fveq2 x = n + 1 x = n + 1
18 fveq2 x = n + 1 x ! = n + 1 !
19 18 oveq2d x = n + 1 P pCnt x ! = P pCnt n + 1 !
20 fvoveq1 x = n + 1 x P k = n + 1 P k
21 20 sumeq2sdv x = n + 1 k = 1 m x P k = k = 1 m n + 1 P k
22 19 21 eqeq12d x = n + 1 P pCnt x ! = k = 1 m x P k P pCnt n + 1 ! = k = 1 m n + 1 P k
23 17 22 raleqbidv x = n + 1 m x P pCnt x ! = k = 1 m x P k m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
24 23 imbi2d x = n + 1 P m x P pCnt x ! = k = 1 m x P k P m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
25 fveq2 x = N x = N
26 fveq2 x = N x ! = N !
27 26 oveq2d x = N P pCnt x ! = P pCnt N !
28 fvoveq1 x = N x P k = N P k
29 28 sumeq2sdv x = N k = 1 m x P k = k = 1 m N P k
30 27 29 eqeq12d x = N P pCnt x ! = k = 1 m x P k P pCnt N ! = k = 1 m N P k
31 25 30 raleqbidv x = N m x P pCnt x ! = k = 1 m x P k m N P pCnt N ! = k = 1 m N P k
32 31 imbi2d x = N P m x P pCnt x ! = k = 1 m x P k P m N P pCnt N ! = k = 1 m N P k
33 fzfid P m 0 1 m Fin
34 sumz 1 m 1 1 m Fin k = 1 m 0 = 0
35 34 olcs 1 m Fin k = 1 m 0 = 0
36 33 35 syl P m 0 k = 1 m 0 = 0
37 0nn0 0 0
38 elfznn k 1 m k
39 38 nnnn0d k 1 m k 0
40 nn0uz 0 = 0
41 39 40 syl6eleq k 1 m k 0
42 41 adantl P m 0 k 1 m k 0
43 simpll P m 0 k 1 m P
44 pcfaclem 0 0 k 0 P 0 P k = 0
45 37 42 43 44 mp3an2i P m 0 k 1 m 0 P k = 0
46 45 sumeq2dv P m 0 k = 1 m 0 P k = k = 1 m 0
47 fac0 0 ! = 1
48 47 oveq2i P pCnt 0 ! = P pCnt 1
49 pc1 P P pCnt 1 = 0
50 48 49 syl5eq P P pCnt 0 ! = 0
51 50 adantr P m 0 P pCnt 0 ! = 0
52 36 46 51 3eqtr4rd P m 0 P pCnt 0 ! = k = 1 m 0 P k
53 52 ralrimiva P m 0 P pCnt 0 ! = k = 1 m 0 P k
54 nn0z n 0 n
55 54 adantr n 0 P n
56 uzid n n n
57 peano2uz n n n + 1 n
58 55 56 57 3syl n 0 P n + 1 n
59 uzss n + 1 n n + 1 n
60 ssralv n + 1 n m n P pCnt n ! = k = 1 m n P k m n + 1 P pCnt n ! = k = 1 m n P k
61 58 59 60 3syl n 0 P m n P pCnt n ! = k = 1 m n P k m n + 1 P pCnt n ! = k = 1 m n P k
62 oveq1 P pCnt n ! = k = 1 m n P k P pCnt n ! + P pCnt n + 1 = k = 1 m n P k + P pCnt n + 1
63 simpll n 0 P m n + 1 n 0
64 facp1 n 0 n + 1 ! = n ! n + 1
65 63 64 syl n 0 P m n + 1 n + 1 ! = n ! n + 1
66 65 oveq2d n 0 P m n + 1 P pCnt n + 1 ! = P pCnt n ! n + 1
67 simplr n 0 P m n + 1 P
68 faccl n 0 n !
69 nnz n ! n !
70 nnne0 n ! n ! 0
71 69 70 jca n ! n ! n ! 0
72 63 68 71 3syl n 0 P m n + 1 n ! n ! 0
73 nn0p1nn n 0 n + 1
74 nnz n + 1 n + 1
75 nnne0 n + 1 n + 1 0
76 74 75 jca n + 1 n + 1 n + 1 0
77 63 73 76 3syl n 0 P m n + 1 n + 1 n + 1 0
78 pcmul P n ! n ! 0 n + 1 n + 1 0 P pCnt n ! n + 1 = P pCnt n ! + P pCnt n + 1
79 67 72 77 78 syl3anc n 0 P m n + 1 P pCnt n ! n + 1 = P pCnt n ! + P pCnt n + 1
80 66 79 eqtr2d n 0 P m n + 1 P pCnt n ! + P pCnt n + 1 = P pCnt n + 1 !
81 63 adantr n 0 P m n + 1 k 1 m n 0
82 81 nn0zd n 0 P m n + 1 k 1 m n
83 prmnn P P
84 83 ad2antlr n 0 P m n + 1 P
85 nnexpcl P k 0 P k
86 84 39 85 syl2an n 0 P m n + 1 k 1 m P k
87 fldivp1 n P k n + 1 P k n P k = if P k n + 1 1 0
88 82 86 87 syl2anc n 0 P m n + 1 k 1 m n + 1 P k n P k = if P k n + 1 1 0
89 elfzuz k 1 m k 1
90 63 73 syl n 0 P m n + 1 n + 1
91 67 90 pccld n 0 P m n + 1 P pCnt n + 1 0
92 91 nn0zd n 0 P m n + 1 P pCnt n + 1
93 elfz5 k 1 P pCnt n + 1 k 1 P pCnt n + 1 k P pCnt n + 1
94 89 92 93 syl2anr n 0 P m n + 1 k 1 m k 1 P pCnt n + 1 k P pCnt n + 1
95 simpllr n 0 P m n + 1 k 1 m P
96 81 73 syl n 0 P m n + 1 k 1 m n + 1
97 96 nnzd n 0 P m n + 1 k 1 m n + 1
98 39 adantl n 0 P m n + 1 k 1 m k 0
99 pcdvdsb P n + 1 k 0 k P pCnt n + 1 P k n + 1
100 95 97 98 99 syl3anc n 0 P m n + 1 k 1 m k P pCnt n + 1 P k n + 1
101 94 100 bitr2d n 0 P m n + 1 k 1 m P k n + 1 k 1 P pCnt n + 1
102 101 ifbid n 0 P m n + 1 k 1 m if P k n + 1 1 0 = if k 1 P pCnt n + 1 1 0
103 88 102 eqtrd n 0 P m n + 1 k 1 m n + 1 P k n P k = if k 1 P pCnt n + 1 1 0
104 103 sumeq2dv n 0 P m n + 1 k = 1 m n + 1 P k n P k = k = 1 m if k 1 P pCnt n + 1 1 0
105 fzfid n 0 P m n + 1 1 m Fin
106 63 nn0red n 0 P m n + 1 n
107 peano2re n n + 1
108 106 107 syl n 0 P m n + 1 n + 1
109 108 adantr n 0 P m n + 1 k 1 m n + 1
110 109 86 nndivred n 0 P m n + 1 k 1 m n + 1 P k
111 110 flcld n 0 P m n + 1 k 1 m n + 1 P k
112 111 zcnd n 0 P m n + 1 k 1 m n + 1 P k
113 106 adantr n 0 P m n + 1 k 1 m n
114 113 86 nndivred n 0 P m n + 1 k 1 m n P k
115 114 flcld n 0 P m n + 1 k 1 m n P k
116 115 zcnd n 0 P m n + 1 k 1 m n P k
117 105 112 116 fsumsub n 0 P m n + 1 k = 1 m n + 1 P k n P k = k = 1 m n + 1 P k k = 1 m n P k
118 fzfi 1 m Fin
119 91 nn0red n 0 P m n + 1 P pCnt n + 1
120 eluzelz m n + 1 m
121 120 adantl n 0 P m n + 1 m
122 121 zred n 0 P m n + 1 m
123 prmuz2 P P 2
124 123 ad2antlr n 0 P m n + 1 P 2
125 90 nnnn0d n 0 P m n + 1 n + 1 0
126 bernneq3 P 2 n + 1 0 n + 1 < P n + 1
127 124 125 126 syl2anc n 0 P m n + 1 n + 1 < P n + 1
128 119 108 letrid n 0 P m n + 1 P pCnt n + 1 n + 1 n + 1 P pCnt n + 1
129 128 ord n 0 P m n + 1 ¬ P pCnt n + 1 n + 1 n + 1 P pCnt n + 1
130 90 nnzd n 0 P m n + 1 n + 1
131 pcdvdsb P n + 1 n + 1 0 n + 1 P pCnt n + 1 P n + 1 n + 1
132 67 130 125 131 syl3anc n 0 P m n + 1 n + 1 P pCnt n + 1 P n + 1 n + 1
133 84 125 nnexpcld n 0 P m n + 1 P n + 1
134 133 nnzd n 0 P m n + 1 P n + 1
135 dvdsle P n + 1 n + 1 P n + 1 n + 1 P n + 1 n + 1
136 134 90 135 syl2anc n 0 P m n + 1 P n + 1 n + 1 P n + 1 n + 1
137 133 nnred n 0 P m n + 1 P n + 1
138 137 108 lenltd n 0 P m n + 1 P n + 1 n + 1 ¬ n + 1 < P n + 1
139 136 138 sylibd n 0 P m n + 1 P n + 1 n + 1 ¬ n + 1 < P n + 1
140 132 139 sylbid n 0 P m n + 1 n + 1 P pCnt n + 1 ¬ n + 1 < P n + 1
141 129 140 syld n 0 P m n + 1 ¬ P pCnt n + 1 n + 1 ¬ n + 1 < P n + 1
142 127 141 mt4d n 0 P m n + 1 P pCnt n + 1 n + 1
143 eluzle m n + 1 n + 1 m
144 143 adantl n 0 P m n + 1 n + 1 m
145 119 108 122 142 144 letrd n 0 P m n + 1 P pCnt n + 1 m
146 eluz P pCnt n + 1 m m P pCnt n + 1 P pCnt n + 1 m
147 92 121 146 syl2anc n 0 P m n + 1 m P pCnt n + 1 P pCnt n + 1 m
148 145 147 mpbird n 0 P m n + 1 m P pCnt n + 1
149 fzss2 m P pCnt n + 1 1 P pCnt n + 1 1 m
150 148 149 syl n 0 P m n + 1 1 P pCnt n + 1 1 m
151 sumhash 1 m Fin 1 P pCnt n + 1 1 m k = 1 m if k 1 P pCnt n + 1 1 0 = 1 P pCnt n + 1
152 118 150 151 sylancr n 0 P m n + 1 k = 1 m if k 1 P pCnt n + 1 1 0 = 1 P pCnt n + 1
153 hashfz1 P pCnt n + 1 0 1 P pCnt n + 1 = P pCnt n + 1
154 91 153 syl n 0 P m n + 1 1 P pCnt n + 1 = P pCnt n + 1
155 152 154 eqtrd n 0 P m n + 1 k = 1 m if k 1 P pCnt n + 1 1 0 = P pCnt n + 1
156 104 117 155 3eqtr3d n 0 P m n + 1 k = 1 m n + 1 P k k = 1 m n P k = P pCnt n + 1
157 105 112 fsumcl n 0 P m n + 1 k = 1 m n + 1 P k
158 105 116 fsumcl n 0 P m n + 1 k = 1 m n P k
159 119 recnd n 0 P m n + 1 P pCnt n + 1
160 157 158 159 subaddd n 0 P m n + 1 k = 1 m n + 1 P k k = 1 m n P k = P pCnt n + 1 k = 1 m n P k + P pCnt n + 1 = k = 1 m n + 1 P k
161 156 160 mpbid n 0 P m n + 1 k = 1 m n P k + P pCnt n + 1 = k = 1 m n + 1 P k
162 80 161 eqeq12d n 0 P m n + 1 P pCnt n ! + P pCnt n + 1 = k = 1 m n P k + P pCnt n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
163 62 162 syl5ib n 0 P m n + 1 P pCnt n ! = k = 1 m n P k P pCnt n + 1 ! = k = 1 m n + 1 P k
164 163 ralimdva n 0 P m n + 1 P pCnt n ! = k = 1 m n P k m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
165 61 164 syld n 0 P m n P pCnt n ! = k = 1 m n P k m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
166 165 ex n 0 P m n P pCnt n ! = k = 1 m n P k m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
167 166 a2d n 0 P m n P pCnt n ! = k = 1 m n P k P m n + 1 P pCnt n + 1 ! = k = 1 m n + 1 P k
168 8 16 24 32 53 167 nn0ind N 0 P m N P pCnt N ! = k = 1 m N P k
169 168 imp N 0 P m N P pCnt N ! = k = 1 m N P k
170 oveq2 m = M 1 m = 1 M
171 170 sumeq1d m = M k = 1 m N P k = k = 1 M N P k
172 171 eqeq2d m = M P pCnt N ! = k = 1 m N P k P pCnt N ! = k = 1 M N P k
173 172 rspcv M N m N P pCnt N ! = k = 1 m N P k P pCnt N ! = k = 1 M N P k
174 169 173 syl5 M N N 0 P P pCnt N ! = k = 1 M N P k
175 174 3impib M N N 0 P P pCnt N ! = k = 1 M N P k
176 175 3com12 N 0 M N P P pCnt N ! = k = 1 M N P k