Metamath Proof Explorer


Theorem dchrvmasumlem

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.16 of Shapiro, p. 379. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z
|- Z = ( Z/nZ ` N )
rpvmasum.l
|- L = ( ZRHom ` Z )
rpvmasum.a
|- ( ph -> N e. NN )
dchrmusum.g
|- G = ( DChr ` N )
dchrmusum.d
|- D = ( Base ` G )
dchrmusum.1
|- .1. = ( 0g ` G )
dchrmusum.b
|- ( ph -> X e. D )
dchrmusum.n1
|- ( ph -> X =/= .1. )
dchrmusum.f
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrmusum.c
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrmusum.t
|- ( ph -> seq 1 ( + , F ) ~~> T )
dchrmusum.2
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
Assertion dchrvmasumlem
|- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) 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 dchrmusum.g
 |-  G = ( DChr ` N )
5 dchrmusum.d
 |-  D = ( Base ` G )
6 dchrmusum.1
 |-  .1. = ( 0g ` G )
7 dchrmusum.b
 |-  ( ph -> X e. D )
8 dchrmusum.n1
 |-  ( ph -> X =/= .1. )
9 dchrmusum.f
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10 dchrmusum.c
 |-  ( ph -> C e. ( 0 [,) +oo ) )
11 dchrmusum.t
 |-  ( ph -> seq 1 ( + , F ) ~~> T )
12 dchrmusum.2
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
13 1 2 3 4 5 6 7 8 9 10 11 12 dchrisumn0
 |-  ( ph -> T =/= 0 )
14 13 adantr
 |-  ( ( ph /\ x e. RR+ ) -> T =/= 0 )
15 ifnefalse
 |-  ( T =/= 0 -> if ( T = 0 , ( log ` x ) , 0 ) = 0 )
16 14 15 syl
 |-  ( ( ph /\ x e. RR+ ) -> if ( T = 0 , ( log ` x ) , 0 ) = 0 )
17 16 oveq2d
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( T = 0 , ( log ` x ) , 0 ) ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + 0 ) )
18 fzfid
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
19 7 ad2antrr
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
20 elfzelz
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
21 20 adantl
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ )
22 4 1 5 2 19 21 dchrzrhcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` n ) ) e. CC )
23 elfznn
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
24 23 adantl
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
25 vmacl
 |-  ( n e. NN -> ( Lam ` n ) e. RR )
26 nndivre
 |-  ( ( ( Lam ` n ) e. RR /\ n e. NN ) -> ( ( Lam ` n ) / n ) e. RR )
27 25 26 mpancom
 |-  ( n e. NN -> ( ( Lam ` n ) / n ) e. RR )
28 24 27 syl
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. RR )
29 28 recnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( Lam ` n ) / n ) e. CC )
30 22 29 mulcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
31 18 30 fsumcl
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) e. CC )
32 31 addid1d
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + 0 ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
33 17 32 eqtrd
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( T = 0 , ( log ` x ) , 0 ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) )
34 33 mpteq2dva
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( T = 0 , ( log ` x ) , 0 ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) )
35 1 2 3 4 5 6 7 8 9 10 11 12 dchrvmasumif
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) + if ( T = 0 , ( log ` x ) , 0 ) ) ) e. O(1) )
36 34 35 eqeltrrd
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( Lam ` n ) / n ) ) ) e. O(1) )