Metamath Proof Explorer

Theorem vmasum

Description: The sum of the von Mangoldt function over the divisors of n . Equation 9.2.4 of Shapiro, p. 328 and theorem 2.10 in ApostolNT p. 32. (Contributed by Mario Carneiro, 15-Apr-2016)

Ref Expression
Assertion vmasum 
|- ( A e. NN -> sum_ n e. { x e. NN | x || A } ( Lam ` n ) = ( log ` A ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( n = ( p ^ k ) -> ( Lam ` n ) = ( Lam ` ( p ^ k ) ) )
2 fzfid 
 |-  ( A e. NN -> ( 1 ... A ) e. Fin )
3 dvdsssfz1 
 |-  ( A e. NN -> { x e. NN | x || A } C_ ( 1 ... A ) )
4 2 3 ssfid 
 |-  ( A e. NN -> { x e. NN | x || A } e. Fin )
5 ssrab2 
 |-  { x e. NN | x || A } C_ NN
6 5 a1i 
 |-  ( A e. NN -> { x e. NN | x || A } C_ NN )
7 inss1 
 |-  ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A )
8 ssfi 
 |-  ( ( ( 1 ... A ) e. Fin /\ ( ( 1 ... A ) i^i Prime ) C_ ( 1 ... A ) ) -> ( ( 1 ... A ) i^i Prime ) e. Fin )
9 2 7 8 sylancl 
 |-  ( A e. NN -> ( ( 1 ... A ) i^i Prime ) e. Fin )
10 pccl 
 |-  ( ( p e. Prime /\ A e. NN ) -> ( p pCnt A ) e. NN0 )
11 10 ancoms 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( p pCnt A ) e. NN0 )
12 11 nn0zd 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( p pCnt A ) e. ZZ )
13 fznn 
 |-  ( ( p pCnt A ) e. ZZ -> ( k e. ( 1 ... ( p pCnt A ) ) <-> ( k e. NN /\ k <_ ( p pCnt A ) ) ) )
14 12 13 syl 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( k e. ( 1 ... ( p pCnt A ) ) <-> ( k e. NN /\ k <_ ( p pCnt A ) ) ) )
15 14 anbi2d 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( ( p e. ( 1 ... A ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( p e. ( 1 ... A ) /\ ( k e. NN /\ k <_ ( p pCnt A ) ) ) ) )
16 an12 
 |-  ( ( p e. ( 1 ... A ) /\ ( k e. NN /\ k <_ ( p pCnt A ) ) ) <-> ( k e. NN /\ ( p e. ( 1 ... A ) /\ k <_ ( p pCnt A ) ) ) )
17 prmz 
 |-  ( p e. Prime -> p e. ZZ )
18 17 adantl 
 |-  ( ( A e. NN /\ p e. Prime ) -> p e. ZZ )
19 iddvdsexp 
 |-  ( ( p e. ZZ /\ k e. NN ) -> p || ( p ^ k ) )
20 18 19 sylan 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> p || ( p ^ k ) )
21 17 ad2antlr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> p e. ZZ )
22 prmnn 
 |-  ( p e. Prime -> p e. NN )
23 22 adantl 
 |-  ( ( A e. NN /\ p e. Prime ) -> p e. NN )
24 nnnn0 
 |-  ( k e. NN -> k e. NN0 )
25 nnexpcl 
 |-  ( ( p e. NN /\ k e. NN0 ) -> ( p ^ k ) e. NN )
26 23 24 25 syl2an 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( p ^ k ) e. NN )
27 26 nnzd 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( p ^ k ) e. ZZ )
28 nnz 
 |-  ( A e. NN -> A e. ZZ )
29 28 ad2antrr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> A e. ZZ )
30 dvdstr 
 |-  ( ( p e. ZZ /\ ( p ^ k ) e. ZZ /\ A e. ZZ ) -> ( ( p || ( p ^ k ) /\ ( p ^ k ) || A ) -> p || A ) )
31 21 27 29 30 syl3anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p || ( p ^ k ) /\ ( p ^ k ) || A ) -> p || A ) )
32 20 31 mpand 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p ^ k ) || A -> p || A ) )
33 simpll 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> A e. NN )
34 dvdsle 
 |-  ( ( p e. ZZ /\ A e. NN ) -> ( p || A -> p <_ A ) )
35 21 33 34 syl2anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( p || A -> p <_ A ) )
36 32 35 syld 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p ^ k ) || A -> p <_ A ) )
37 22 ad2antlr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> p e. NN )
38 fznn 
 |-  ( A e. ZZ -> ( p e. ( 1 ... A ) <-> ( p e. NN /\ p <_ A ) ) )
39 38 baibd 
 |-  ( ( A e. ZZ /\ p e. NN ) -> ( p e. ( 1 ... A ) <-> p <_ A ) )
40 29 37 39 syl2anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( p e. ( 1 ... A ) <-> p <_ A ) )
41 36 40 sylibrd 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p ^ k ) || A -> p e. ( 1 ... A ) ) )
42 41 pm4.71rd 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p ^ k ) || A <-> ( p e. ( 1 ... A ) /\ ( p ^ k ) || A ) ) )
43 breq1 
 |-  ( x = ( p ^ k ) -> ( x || A <-> ( p ^ k ) || A ) )
44 43 elrab3 
 |-  ( ( p ^ k ) e. NN -> ( ( p ^ k ) e. { x e. NN | x || A } <-> ( p ^ k ) || A ) )
45 26 44 syl 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p ^ k ) e. { x e. NN | x || A } <-> ( p ^ k ) || A ) )
46 simplr 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> p e. Prime )
47 24 adantl 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> k e. NN0 )
48 pcdvdsb 
 |-  ( ( p e. Prime /\ A e. ZZ /\ k e. NN0 ) -> ( k <_ ( p pCnt A ) <-> ( p ^ k ) || A ) )
49 46 29 47 48 syl3anc 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( k <_ ( p pCnt A ) <-> ( p ^ k ) || A ) )
50 49 anbi2d 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p e. ( 1 ... A ) /\ k <_ ( p pCnt A ) ) <-> ( p e. ( 1 ... A ) /\ ( p ^ k ) || A ) ) )
51 42 45 50 3bitr4rd 
 |-  ( ( ( A e. NN /\ p e. Prime ) /\ k e. NN ) -> ( ( p e. ( 1 ... A ) /\ k <_ ( p pCnt A ) ) <-> ( p ^ k ) e. { x e. NN | x || A } ) )
52 51 pm5.32da 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( ( k e. NN /\ ( p e. ( 1 ... A ) /\ k <_ ( p pCnt A ) ) ) <-> ( k e. NN /\ ( p ^ k ) e. { x e. NN | x || A } ) ) )
53 16 52 syl5bb 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( ( p e. ( 1 ... A ) /\ ( k e. NN /\ k <_ ( p pCnt A ) ) ) <-> ( k e. NN /\ ( p ^ k ) e. { x e. NN | x || A } ) ) )
54 15 53 bitrd 
 |-  ( ( A e. NN /\ p e. Prime ) -> ( ( p e. ( 1 ... A ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( k e. NN /\ ( p ^ k ) e. { x e. NN | x || A } ) ) )
55 54 pm5.32da 
 |-  ( A e. NN -> ( ( p e. Prime /\ ( p e. ( 1 ... A ) /\ k e. ( 1 ... ( p pCnt A ) ) ) ) <-> ( p e. Prime /\ ( k e. NN /\ ( p ^ k ) e. { x e. NN | x || A } ) ) ) )
56 elin 
 |-  ( p e. ( ( 1 ... A ) i^i Prime ) <-> ( p e. ( 1 ... A ) /\ p e. Prime ) )
57 56 anbi1i 
 |-  ( ( p e. ( ( 1 ... A ) i^i Prime ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( ( p e. ( 1 ... A ) /\ p e. Prime ) /\ k e. ( 1 ... ( p pCnt A ) ) ) )
58 anass 
 |-  ( ( ( p e. ( 1 ... A ) /\ p e. Prime ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( p e. ( 1 ... A ) /\ ( p e. Prime /\ k e. ( 1 ... ( p pCnt A ) ) ) ) )
59 an12 
 |-  ( ( p e. ( 1 ... A ) /\ ( p e. Prime /\ k e. ( 1 ... ( p pCnt A ) ) ) ) <-> ( p e. Prime /\ ( p e. ( 1 ... A ) /\ k e. ( 1 ... ( p pCnt A ) ) ) ) )
60 57 58 59 3bitri 
 |-  ( ( p e. ( ( 1 ... A ) i^i Prime ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( p e. Prime /\ ( p e. ( 1 ... A ) /\ k e. ( 1 ... ( p pCnt A ) ) ) ) )
61 anass 
 |-  ( ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. { x e. NN | x || A } ) <-> ( p e. Prime /\ ( k e. NN /\ ( p ^ k ) e. { x e. NN | x || A } ) ) )
62 55 60 61 3bitr4g 
 |-  ( A e. NN -> ( ( p e. ( ( 1 ... A ) i^i Prime ) /\ k e. ( 1 ... ( p pCnt A ) ) ) <-> ( ( p e. Prime /\ k e. NN ) /\ ( p ^ k ) e. { x e. NN | x || A } ) ) )
63 6 sselda 
 |-  ( ( A e. NN /\ n e. { x e. NN | x || A } ) -> n e. NN )
64 vmacl 
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
65 63 64 syl 
 |-  ( ( A e. NN /\ n e. { x e. NN | x || A } ) -> ( Lam ` n ) e. RR )
66 65 recnd 
 |-  ( ( A e. NN /\ n e. { x e. NN | x || A } ) -> ( Lam ` n ) e. CC )
67 simprr 
 |-  ( ( A e. NN /\ ( n e. { x e. NN | x || A } /\ ( Lam ` n ) = 0 ) ) -> ( Lam ` n ) = 0 )
68 1 4 6 9 62 66 67 fsumvma 
 |-  ( A e. NN -> sum_ n e. { x e. NN | x || A } ( Lam ` n ) = sum_ p e. ( ( 1 ... A ) i^i Prime ) sum_ k e. ( 1 ... ( p pCnt A ) ) ( Lam ` ( p ^ k ) ) )
69 elinel2 
 |-  ( p e. ( ( 1 ... A ) i^i Prime ) -> p e. Prime )
70 69 ad2antlr 
 |-  ( ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) /\ k e. ( 1 ... ( p pCnt A ) ) ) -> p e. Prime )
71 elfznn 
 |-  ( k e. ( 1 ... ( p pCnt A ) ) -> k e. NN )
72 71 adantl 
 |-  ( ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) /\ k e. ( 1 ... ( p pCnt A ) ) ) -> k e. NN )
73 vmappw 
 |-  ( ( p e. Prime /\ k e. NN ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
74 70 72 73 syl2anc 
 |-  ( ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) /\ k e. ( 1 ... ( p pCnt A ) ) ) -> ( Lam ` ( p ^ k ) ) = ( log ` p ) )
75 74 sumeq2dv 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( p pCnt A ) ) ( Lam ` ( p ^ k ) ) = sum_ k e. ( 1 ... ( p pCnt A ) ) ( log ` p ) )
76 fzfid 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( 1 ... ( p pCnt A ) ) e. Fin )
77 69 22 syl 
 |-  ( p e. ( ( 1 ... A ) i^i Prime ) -> p e. NN )
78 77 adantl 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. NN )
79 78 nnrpd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> p e. RR+ )
80 79 relogcld 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` p ) e. RR )
81 80 recnd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( log ` p ) e. CC )
82 fsumconst 
 |-  ( ( ( 1 ... ( p pCnt A ) ) e. Fin /\ ( log ` p ) e. CC ) -> sum_ k e. ( 1 ... ( p pCnt A ) ) ( log ` p ) = ( ( # ` ( 1 ... ( p pCnt A ) ) ) x. ( log ` p ) ) )
83 76 81 82 syl2anc 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( p pCnt A ) ) ( log ` p ) = ( ( # ` ( 1 ... ( p pCnt A ) ) ) x. ( log ` p ) ) )
84 69 11 sylan2 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( p pCnt A ) e. NN0 )
85 hashfz1 
 |-  ( ( p pCnt A ) e. NN0 -> ( # ` ( 1 ... ( p pCnt A ) ) ) = ( p pCnt A ) )
86 84 85 syl 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( # ` ( 1 ... ( p pCnt A ) ) ) = ( p pCnt A ) )
87 86 oveq1d 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> ( ( # ` ( 1 ... ( p pCnt A ) ) ) x. ( log ` p ) ) = ( ( p pCnt A ) x. ( log ` p ) ) )
88 75 83 87 3eqtrd 
 |-  ( ( A e. NN /\ p e. ( ( 1 ... A ) i^i Prime ) ) -> sum_ k e. ( 1 ... ( p pCnt A ) ) ( Lam ` ( p ^ k ) ) = ( ( p pCnt A ) x. ( log ` p ) ) )
89 88 sumeq2dv 
 |-  ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) sum_ k e. ( 1 ... ( p pCnt A ) ) ( Lam ` ( p ^ k ) ) = sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) )
90 pclogsum 
 |-  ( A e. NN -> sum_ p e. ( ( 1 ... A ) i^i Prime ) ( ( p pCnt A ) x. ( log ` p ) ) = ( log ` A ) )
91 68 89 90 3eqtrd 
 |-  ( A e. NN -> sum_ n e. { x e. NN | x || A } ( Lam ` n ) = ( log ` A ) )