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 e. NN0 /\ M e. ( ZZ>= ` N ) /\ P e. Prime ) -> ( P pCnt ( ! ` N ) ) = sum_ k e. ( 1 ... M ) ( |_ ` ( N / ( P ^ k ) ) ) )

Proof

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