Metamath Proof Explorer

Theorem dchrmusumlem

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 dchrmusumlem 
|- ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` 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 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
14 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
15 elfzelz 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
16 15 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ )
17 4 1 5 2 14 16 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` n ) ) e. CC )
18 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
19 18 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
20 mucl 
 |-  ( n e. NN -> ( mmu ` n ) e. ZZ )
21 19 20 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. ZZ )
22 21 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` n ) e. RR )
23 22 19 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. RR )
24 23 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` n ) / n ) e. CC )
25 17 24 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) e. CC )
26 13 25 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) e. CC )
27 climcl 
 |-  ( seq 1 ( + , F ) ~~> T -> T e. CC )
28 11 27 syl 
 |-  ( ph -> T e. CC )
29 28 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> T e. CC )
30 26 29 mulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) e. CC )
31 1 2 3 4 5 6 7 8 9 10 11 12 dchrisumn0 
 |-  ( ph -> T =/= 0 )
32 31 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> T =/= 0 )
33 30 29 32 divrecd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) / T ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) x. ( 1 / T ) ) )
34 26 29 32 divcan4d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) / T ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) )
35 33 34 eqtr3d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) x. ( 1 / T ) ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) )
36 35 mpteq2dva 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) x. ( 1 / T ) ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) ) )
37 28 31 reccld 
 |-  ( ph -> ( 1 / T ) e. CC )
38 37 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 / T ) e. CC )
39 1 2 3 4 5 6 7 8 9 10 11 12 dchrmusum2 
 |-  ( ph -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) ) e. O(1) )
40 rpssre 
 |-  RR+ C_ RR
41 o1const 
 |-  ( ( RR+ C_ RR /\ ( 1 / T ) e. CC ) -> ( x e. RR+ |-> ( 1 / T ) ) e. O(1) )
42 40 37 41 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( 1 / T ) ) e. O(1) )
43 30 38 39 42 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) x. T ) x. ( 1 / T ) ) ) e. O(1) )
44 36 43 eqeltrrd 
 |-  ( ph -> ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` n ) ) x. ( ( mmu ` n ) / n ) ) ) e. O(1) )