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) )