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