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