Metamath Proof Explorer

Theorem rpvmasum

Description: The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to log x / phi ( x ) + O(1) . Equation 9.4.3 of Shapiro, p. 375. (Contributed by Mario Carneiro, 2-May-2016) (Proof shortened by Mario Carneiro, 26-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.u 
|- U = ( Unit ` Z )
rpvmasum.b 
|- ( ph -> A e. U )
rpvmasum.t 
|- T = ( `' L " { A } )
Assertion rpvmasum 
|- ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 
 |-  Z = ( Z/nZ ` N )
2 rpvmasum.l 
 |-  L = ( ZRHom ` Z )
3 rpvmasum.a 
 |-  ( ph -> N e. NN )
4 rpvmasum.u 
 |-  U = ( Unit ` Z )
5 rpvmasum.b 
 |-  ( ph -> A e. U )
6 rpvmasum.t 
 |-  T = ( `' L " { A } )
7 3 adantr 
 |-  ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> N e. NN )
8 eqid 
 |-  ( DChr ` N ) = ( DChr ` N )
9 eqid 
 |-  ( Base ` ( DChr ` N ) ) = ( Base ` ( DChr ` N ) )
10 eqid 
 |-  ( 0g ` ( DChr ` N ) ) = ( 0g ` ( DChr ` N ) )
11 2fveq3 
 |-  ( m = n -> ( y ` ( L ` m ) ) = ( y ` ( L ` n ) ) )
12 id 
 |-  ( m = n -> m = n )
13 11 12 oveq12d 
 |-  ( m = n -> ( ( y ` ( L ` m ) ) / m ) = ( ( y ` ( L ` n ) ) / n ) )
14 13 cbvsumv 
 |-  sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = sum_ n e. NN ( ( y ` ( L ` n ) ) / n )
15 14 eqeq1i 
 |-  ( sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 <-> sum_ n e. NN ( ( y ` ( L ` n ) ) / n ) = 0 )
16 15 rabbii 
 |-  { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ n e. NN ( ( y ` ( L ` n ) ) / n ) = 0 }
17 simpr 
 |-  ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } )
18 1 2 7 8 9 10 16 17 dchrisum0 
 |-  -. ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } )
19 18 imnani 
 |-  ( ph -> -. f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } )
20 19 eq0rdv 
 |-  ( ph -> { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = (/) )
21 20 fveq2d 
 |-  ( ph -> ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) = ( # ` (/) ) )
22 hash0 
 |-  ( # ` (/) ) = 0
23 21 22 eqtrdi 
 |-  ( ph -> ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) = 0 )
24 23 oveq2d 
 |-  ( ph -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = ( 1 - 0 ) )
25 1m0e1 
 |-  ( 1 - 0 ) = 1
26 24 25 eqtrdi 
 |-  ( ph -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = 1 )
27 26 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) = 1 )
28 27 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) = ( ( log ` x ) x. 1 ) )
29 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
30 29 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. RR )
31 30 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( log ` x ) e. CC )
32 31 mulid1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. 1 ) = ( log ` x ) )
33 28 32 eqtrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) = ( log ` x ) )
34 33 oveq2d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) = ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) )
35 34 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) ) = ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) )
36 eqid 
 |-  { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } = { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 }
37 18 pm2.21i 
 |-  ( ( ph /\ f e. { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) -> A = ( 1r ` Z ) )
38 1 2 3 8 9 10 36 4 5 6 37 rpvmasum2 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( ( log ` x ) x. ( 1 - ( # ` { y e. ( ( Base ` ( DChr ` N ) ) \ { ( 0g ` ( DChr ` N ) ) } ) | sum_ m e. NN ( ( y ` ( L ` m ) ) / m ) = 0 } ) ) ) ) ) e. O(1) )
39 35 38 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> ( ( ( phi ` N ) x. sum_ n e. ( ( 1 ... ( |_ ` x ) ) i^i T ) ( ( Lam ` n ) / n ) ) - ( log ` x ) ) ) e. O(1) )