Metamath Proof Explorer

Theorem dchrvmasumlem3

Description: Lemma for dchrvmasum . (Contributed by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses rpvmasum.z 
|- Z = ( Z/nZ ` N )
rpvmasum.l 
|- L = ( ZRHom ` Z )
rpvmasum.a 
|- ( ph -> N e. NN )
rpvmasum.g 
|- G = ( DChr ` N )
rpvmasum.d 
|- D = ( Base ` G )
rpvmasum.1 
|- .1. = ( 0g ` G )
dchrisum.b 
|- ( ph -> X e. D )
dchrisum.n1 
|- ( ph -> X =/= .1. )
dchrvmasum.f 
|- ( ( ph /\ m e. RR+ ) -> F e. CC )
dchrvmasum.g 
|- ( m = ( x / d ) -> F = K )
dchrvmasum.c 
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrvmasum.t 
|- ( ph -> T e. CC )
dchrvmasum.1 
|- ( ( ph /\ m e. ( 3 [,) +oo ) ) -> ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )
dchrvmasum.r 
|- ( ph -> R e. RR )
dchrvmasum.2 
|- ( ph -> A. m e. ( 1 [,) 3 ) ( abs ` ( F - T ) ) <_ R )
Assertion dchrvmasumlem3 
|- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) 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.g 
 |-  G = ( DChr ` N )
5 rpvmasum.d 
 |-  D = ( Base ` G )
6 rpvmasum.1 
 |-  .1. = ( 0g ` G )
7 dchrisum.b 
 |-  ( ph -> X e. D )
8 dchrisum.n1 
 |-  ( ph -> X =/= .1. )
9 dchrvmasum.f 
 |-  ( ( ph /\ m e. RR+ ) -> F e. CC )
10 dchrvmasum.g 
 |-  ( m = ( x / d ) -> F = K )
11 dchrvmasum.c 
 |-  ( ph -> C e. ( 0 [,) +oo ) )
12 dchrvmasum.t 
 |-  ( ph -> T e. CC )
13 dchrvmasum.1 
 |-  ( ( ph /\ m e. ( 3 [,) +oo ) ) -> ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )
14 dchrvmasum.r 
 |-  ( ph -> R e. RR )
15 dchrvmasum.2 
 |-  ( ph -> A. m e. ( 1 [,) 3 ) ( abs ` ( F - T ) ) <_ R )
16 1red 
 |-  ( ph -> 1 e. RR )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 dchrvmasumlem2 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) e. O(1) )
18 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
19 10 eleq1d 
 |-  ( m = ( x / d ) -> ( F e. CC <-> K e. CC ) )
20 9 ralrimiva 
 |-  ( ph -> A. m e. RR+ F e. CC )
21 20 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> A. m e. RR+ F e. CC )
22 simpr 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR+ )
23 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
24 23 nnrpd 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. RR+ )
25 rpdivcl 
 |-  ( ( x e. RR+ /\ d e. RR+ ) -> ( x / d ) e. RR+ )
26 22 24 25 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR+ )
27 19 21 26 rspcdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> K e. CC )
28 12 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
29 27 28 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( K - T ) e. CC )
30 29 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( K - T ) ) e. RR )
31 23 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
32 30 31 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( K - T ) ) / d ) e. RR )
33 18 32 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) e. RR )
34 7 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
35 elfzelz 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. ZZ )
36 35 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. ZZ )
37 4 1 5 2 34 36 dchrzrhcl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC )
38 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
39 31 38 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. ZZ )
40 39 zred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. RR )
41 40 31 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. RR )
42 41 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
43 37 42 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
44 43 29 mulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) e. CC )
45 18 44 fsumcl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) e. CC )
46 45 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) e. RR )
47 33 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) e. CC )
48 47 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) e. RR )
49 44 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) e. RR )
50 18 49 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) e. RR )
51 18 44 fsumabs 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) )
52 43 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) e. RR )
53 31 nnrecred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. RR )
54 29 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( K - T ) ) )
55 37 42 absmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) = ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) )
56 37 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) e. RR )
57 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
58 42 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) e. RR )
59 37 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( X ` ( L ` d ) ) ) )
60 42 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( mmu ` d ) / d ) ) )
61 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
62 3 nnnn0d 
 |-  ( ph -> N e. NN0 )
63 1 61 2 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
64 62 63 syl 
 |-  ( ph -> L : ZZ -onto-> ( Base ` Z ) )
65 fof 
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
66 64 65 syl 
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> L : ZZ --> ( Base ` Z ) )
68 67 36 ffvelrnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` d ) e. ( Base ` Z ) )
69 4 5 1 61 34 68 dchrabs2 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) <_ 1 )
70 40 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. CC )
71 31 nncnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. CC )
72 31 nnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d =/= 0 )
73 70 71 72 absdivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) )
74 31 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ )
75 74 rprege0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( d e. RR /\ 0 <_ d ) )
76 absid 
 |-  ( ( d e. RR /\ 0 <_ d ) -> ( abs ` d ) = d )
77 75 76 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` d ) = d )
78 77 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) )
79 73 78 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) )
80 70 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) e. RR )
81 mule1 
 |-  ( d e. NN -> ( abs ` ( mmu ` d ) ) <_ 1 )
82 31 81 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) <_ 1 )
83 80 57 74 82 lediv1dd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / d ) <_ ( 1 / d ) )
84 79 83 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) <_ ( 1 / d ) )
85 56 57 58 53 59 60 69 84 lemul12ad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) <_ ( 1 x. ( 1 / d ) ) )
86 53 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. CC )
87 86 mulid2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( 1 / d ) ) = ( 1 / d ) )
88 85 87 breqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) <_ ( 1 / d ) )
89 55 88 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) <_ ( 1 / d ) )
90 52 53 30 54 89 lemul1ad 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( K - T ) ) ) <_ ( ( 1 / d ) x. ( abs ` ( K - T ) ) ) )
91 43 29 absmuld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) = ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( K - T ) ) ) )
92 30 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( K - T ) ) e. CC )
93 92 71 72 divrec2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( K - T ) ) / d ) = ( ( 1 / d ) x. ( abs ` ( K - T ) ) ) )
94 90 91 93 3brtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ ( ( abs ` ( K - T ) ) / d ) )
95 18 49 32 94 fsumle 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) )
96 46 50 33 51 95 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) )
97 33 leabsd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) <_ ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) )
98 46 33 48 96 97 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) )
99 98 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) <_ ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) )
100 16 17 33 45 99 o1le 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( K - T ) ) ) e. O(1) )