Metamath Proof Explorer


Theorem dchrmusum2

Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by n , is bounded, provided that T =/= 0 . Lemma 9.4.2 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-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. )
dchrisumn0.f
|- F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
dchrisumn0.c
|- ( ph -> C e. ( 0 [,) +oo ) )
dchrisumn0.t
|- ( ph -> seq 1 ( + , F ) ~~> T )
dchrisumn0.1
|- ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
Assertion dchrmusum2
|- ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. 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 dchrisumn0.f
 |-  F = ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) )
10 dchrisumn0.c
 |-  ( ph -> C e. ( 0 [,) +oo ) )
11 dchrisumn0.t
 |-  ( ph -> seq 1 ( + , F ) ~~> T )
12 dchrisumn0.1
 |-  ( ph -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
13 rpssre
 |-  RR+ C_ RR
14 ax-1cn
 |-  1 e. CC
15 o1const
 |-  ( ( RR+ C_ RR /\ 1 e. CC ) -> ( x e. RR+ |-> 1 ) e. O(1) )
16 13 14 15 mp2an
 |-  ( x e. RR+ |-> 1 ) e. O(1)
17 16 a1i
 |-  ( ph -> ( x e. RR+ |-> 1 ) e. O(1) )
18 14 a1i
 |-  ( ( ph /\ x e. RR+ ) -> 1 e. CC )
19 fzfid
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
20 7 ad2antrr
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
21 elfzelz
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. ZZ )
22 21 adantl
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. ZZ )
23 4 1 5 2 20 22 dchrzrhcl
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC )
24 elfznn
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
25 24 adantl
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
26 mucl
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
27 26 zred
 |-  ( d e. NN -> ( mmu ` d ) e. RR )
28 nndivre
 |-  ( ( ( mmu ` d ) e. RR /\ d e. NN ) -> ( ( mmu ` d ) / d ) e. RR )
29 27 28 mpancom
 |-  ( d e. NN -> ( ( mmu ` d ) / d ) e. RR )
30 25 29 syl
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. RR )
31 30 recnd
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
32 23 31 mulcld
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
33 19 32 fsumcl
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
34 climcl
 |-  ( seq 1 ( + , F ) ~~> T -> T e. CC )
35 11 34 syl
 |-  ( ph -> T e. CC )
36 35 adantr
 |-  ( ( ph /\ x e. RR+ ) -> T e. CC )
37 33 36 mulcld
 |-  ( ( ph /\ x e. RR+ ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC )
38 13 a1i
 |-  ( ph -> RR+ C_ RR )
39 subcl
 |-  ( ( 1 e. CC /\ ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. CC )
40 14 37 39 sylancr
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. CC )
41 1red
 |-  ( ph -> 1 e. RR )
42 elrege0
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
43 10 42 sylib
 |-  ( ph -> ( C e. RR /\ 0 <_ C ) )
44 43 simpld
 |-  ( ph -> C e. RR )
45 fzfid
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
46 32 adantlrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) e. CC )
47 nnuz
 |-  NN = ( ZZ>= ` 1 )
48 1zzd
 |-  ( ph -> 1 e. ZZ )
49 7 adantr
 |-  ( ( ph /\ m e. NN ) -> X e. D )
50 nnz
 |-  ( m e. NN -> m e. ZZ )
51 50 adantl
 |-  ( ( ph /\ m e. NN ) -> m e. ZZ )
52 4 1 5 2 49 51 dchrzrhcl
 |-  ( ( ph /\ m e. NN ) -> ( X ` ( L ` m ) ) e. CC )
53 nncn
 |-  ( m e. NN -> m e. CC )
54 53 adantl
 |-  ( ( ph /\ m e. NN ) -> m e. CC )
55 nnne0
 |-  ( m e. NN -> m =/= 0 )
56 55 adantl
 |-  ( ( ph /\ m e. NN ) -> m =/= 0 )
57 52 54 56 divcld
 |-  ( ( ph /\ m e. NN ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
58 2fveq3
 |-  ( a = m -> ( X ` ( L ` a ) ) = ( X ` ( L ` m ) ) )
59 id
 |-  ( a = m -> a = m )
60 58 59 oveq12d
 |-  ( a = m -> ( ( X ` ( L ` a ) ) / a ) = ( ( X ` ( L ` m ) ) / m ) )
61 60 cbvmptv
 |-  ( a e. NN |-> ( ( X ` ( L ` a ) ) / a ) ) = ( m e. NN |-> ( ( X ` ( L ` m ) ) / m ) )
62 9 61 eqtri
 |-  F = ( m e. NN |-> ( ( X ` ( L ` m ) ) / m ) )
63 57 62 fmptd
 |-  ( ph -> F : NN --> CC )
64 63 ffvelrnda
 |-  ( ( ph /\ m e. NN ) -> ( F ` m ) e. CC )
65 47 48 64 serf
 |-  ( ph -> seq 1 ( + , F ) : NN --> CC )
66 65 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> seq 1 ( + , F ) : NN --> CC )
67 simprl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
68 67 rpred
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR )
69 nndivre
 |-  ( ( x e. RR /\ d e. NN ) -> ( x / d ) e. RR )
70 68 24 69 syl2an
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR )
71 24 adantl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
72 71 nncnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. CC )
73 72 mulid2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) = d )
74 fznnfl
 |-  ( x e. RR -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) )
75 68 74 syl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) )
76 75 simplbda
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d <_ x )
77 73 76 eqbrtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) <_ x )
78 1red
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
79 68 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
80 71 nnrpd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ )
81 78 79 80 lemuldivd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. d ) <_ x <-> 1 <_ ( x / d ) ) )
82 77 81 mpbid
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / d ) )
83 flge1nn
 |-  ( ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) -> ( |_ ` ( x / d ) ) e. NN )
84 70 82 83 syl2anc
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / d ) ) e. NN )
85 66 84 ffvelrnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) e. CC )
86 46 85 mulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) e. CC )
87 35 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
88 46 87 mulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) e. CC )
89 45 86 88 fsumsub
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) )
90 46 85 87 subdid
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) = ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) )
91 90 sumeq2dv
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) )
92 7 ad3antrrr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> X e. D )
93 21 ad2antlr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. ZZ )
94 elfzelz
 |-  ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. ZZ )
95 94 adantl
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. ZZ )
96 4 1 5 2 92 93 95 dchrzrhmul
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` ( d x. m ) ) ) = ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) )
97 96 oveq1d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) )
98 23 adantlrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` d ) ) e. CC )
99 98 adantr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` d ) ) e. CC )
100 72 adantr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. CC )
101 4 1 5 2 92 95 dchrzrhcl
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( X ` ( L ` m ) ) e. CC )
102 elfznn
 |-  ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. NN )
103 102 adantl
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. NN )
104 103 nncnd
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. CC )
105 71 nnne0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d =/= 0 )
106 105 adantr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d =/= 0 )
107 103 nnne0d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m =/= 0 )
108 99 100 101 104 106 107 divmuldivd
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( X ` ( L ` m ) ) ) / ( d x. m ) ) )
109 97 108 eqtr4d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) = ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) )
110 109 oveq2d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
111 71 26 syl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. ZZ )
112 111 zcnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( mmu ` d ) e. CC )
113 112 adantr
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( mmu ` d ) e. CC )
114 99 100 106 divcld
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` d ) ) / d ) e. CC )
115 101 104 107 divcld
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
116 113 114 115 mulassd
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( mmu ` d ) x. ( ( ( X ` ( L ` d ) ) / d ) x. ( ( X ` ( L ` m ) ) / m ) ) ) )
117 113 99 100 106 div12d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) = ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) )
118 117 oveq1d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( ( mmu ` d ) x. ( ( X ` ( L ` d ) ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
119 110 116 118 3eqtr2d
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
120 119 sumeq2dv
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
121 fzfid
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 ... ( |_ ` ( x / d ) ) ) e. Fin )
122 simpll
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ph )
123 122 102 57 syl2an
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( X ` ( L ` m ) ) / m ) e. CC )
124 121 46 123 fsummulc2
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( X ` ( L ` m ) ) / m ) ) )
125 ovex
 |-  ( ( X ` ( L ` m ) ) / m ) e. _V
126 60 9 125 fvmpt
 |-  ( m e. NN -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) )
127 103 126 syl
 |-  ( ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( F ` m ) = ( ( X ` ( L ` m ) ) / m ) )
128 84 47 eleqtrdi
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( |_ ` ( x / d ) ) e. ( ZZ>= ` 1 ) )
129 127 128 123 fsumser
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) = ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) )
130 129 oveq2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( X ` ( L ` m ) ) / m ) ) = ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) )
131 120 124 130 3eqtr2rd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) )
132 131 sumeq2dv
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) )
133 2fveq3
 |-  ( n = ( d x. m ) -> ( X ` ( L ` n ) ) = ( X ` ( L ` ( d x. m ) ) ) )
134 id
 |-  ( n = ( d x. m ) -> n = ( d x. m ) )
135 133 134 oveq12d
 |-  ( n = ( d x. m ) -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) )
136 135 oveq2d
 |-  ( n = ( d x. m ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) )
137 elrabi
 |-  ( d e. { y e. NN | y || n } -> d e. NN )
138 137 ad2antll
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. NN )
139 138 26 syl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. ZZ )
140 139 zcnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. CC )
141 7 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
142 elfzelz
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. ZZ )
143 142 adantl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. ZZ )
144 4 1 5 2 141 143 dchrzrhcl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( X ` ( L ` n ) ) e. CC )
145 fz1ssnn
 |-  ( 1 ... ( |_ ` x ) ) C_ NN
146 145 a1i
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 ... ( |_ ` x ) ) C_ NN )
147 146 sselda
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. NN )
148 147 nncnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n e. CC )
149 147 nnne0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> n =/= 0 )
150 144 148 149 divcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( X ` ( L ` n ) ) / n ) e. CC )
151 150 adantrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( X ` ( L ` n ) ) / n ) e. CC )
152 140 151 mulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) e. CC )
153 136 68 152 dvdsflsumcom
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( X ` ( L ` ( d x. m ) ) ) / ( d x. m ) ) ) )
154 2fveq3
 |-  ( n = 1 -> ( X ` ( L ` n ) ) = ( X ` ( L ` 1 ) ) )
155 id
 |-  ( n = 1 -> n = 1 )
156 154 155 oveq12d
 |-  ( n = 1 -> ( ( X ` ( L ` n ) ) / n ) = ( ( X ` ( L ` 1 ) ) / 1 ) )
157 simprr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
158 flge1nn
 |-  ( ( x e. RR /\ 1 <_ x ) -> ( |_ ` x ) e. NN )
159 68 157 158 syl2anc
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN )
160 159 47 eleqtrdi
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. ( ZZ>= ` 1 ) )
161 eluzfz1
 |-  ( ( |_ ` x ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
162 160 161 syl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. ( 1 ... ( |_ ` x ) ) )
163 156 45 146 162 150 musumsum
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( X ` ( L ` n ) ) / n ) ) = ( ( X ` ( L ` 1 ) ) / 1 ) )
164 132 153 163 3eqtr2d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) = ( ( X ` ( L ` 1 ) ) / 1 ) )
165 4 1 5 2 7 dchrzrh1
 |-  ( ph -> ( X ` ( L ` 1 ) ) = 1 )
166 165 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( X ` ( L ` 1 ) ) = 1 )
167 166 oveq1d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( X ` ( L ` 1 ) ) / 1 ) = ( 1 / 1 ) )
168 1div1e1
 |-  ( 1 / 1 ) = 1
169 167 168 eqtrdi
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( X ` ( L ` 1 ) ) / 1 ) = 1 )
170 164 169 eqtr2d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) )
171 35 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> T e. CC )
172 45 171 46 fsummulc1
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) )
173 170 172 oveq12d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) ) - sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) )
174 89 91 173 3eqtr4rd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) )
175 174 fveq2d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) = ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) )
176 85 87 subcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) e. CC )
177 46 176 mulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. CC )
178 45 177 fsumcl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. CC )
179 178 abscld
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR )
180 177 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR )
181 45 180 fsumrecl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) e. RR )
182 44 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> C e. RR )
183 45 177 fsumabs
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) )
184 reflcl
 |-  ( x e. RR -> ( |_ ` x ) e. RR )
185 68 184 syl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. RR )
186 185 182 remulcld
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( |_ ` x ) x. C ) e. RR )
187 186 67 rerpdivcld
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) e. RR )
188 182 67 rerpdivcld
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C / x ) e. RR )
189 188 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) e. RR )
190 46 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) e. RR )
191 71 nnrecred
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. RR )
192 176 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) e. RR )
193 80 rpred
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR )
194 189 193 remulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C / x ) x. d ) e. RR )
195 46 absge0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) )
196 176 absge0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) )
197 98 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) e. RR )
198 31 adantlrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( mmu ` d ) / d ) e. CC )
199 198 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) e. RR )
200 98 absge0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( X ` ( L ` d ) ) ) )
201 198 absge0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( ( mmu ` d ) / d ) ) )
202 eqid
 |-  ( Base ` Z ) = ( Base ` Z )
203 7 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> X e. D )
204 3 nnnn0d
 |-  ( ph -> N e. NN0 )
205 1 202 2 znzrhfo
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Z ) )
206 fof
 |-  ( L : ZZ -onto-> ( Base ` Z ) -> L : ZZ --> ( Base ` Z ) )
207 204 205 206 3syl
 |-  ( ph -> L : ZZ --> ( Base ` Z ) )
208 207 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> L : ZZ --> ( Base ` Z ) )
209 ffvelrn
 |-  ( ( L : ZZ --> ( Base ` Z ) /\ d e. ZZ ) -> ( L ` d ) e. ( Base ` Z ) )
210 208 21 209 syl2an
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( L ` d ) e. ( Base ` Z ) )
211 4 5 1 202 203 210 dchrabs2
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( X ` ( L ` d ) ) ) <_ 1 )
212 112 72 105 absdivd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) )
213 80 rprege0d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( d e. RR /\ 0 <_ d ) )
214 absid
 |-  ( ( d e. RR /\ 0 <_ d ) -> ( abs ` d ) = d )
215 213 214 syl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` d ) = d )
216 215 oveq2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / ( abs ` d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) )
217 212 216 eqtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) = ( ( abs ` ( mmu ` d ) ) / d ) )
218 112 abscld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) e. RR )
219 mule1
 |-  ( d e. NN -> ( abs ` ( mmu ` d ) ) <_ 1 )
220 71 219 syl
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( mmu ` d ) ) <_ 1 )
221 218 78 80 220 lediv1dd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( mmu ` d ) ) / d ) <_ ( 1 / d ) )
222 217 221 eqbrtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( mmu ` d ) / d ) ) <_ ( 1 / d ) )
223 197 78 199 191 200 201 211 222 lemul12ad
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) <_ ( 1 x. ( 1 / d ) ) )
224 98 198 absmuld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) = ( ( abs ` ( X ` ( L ` d ) ) ) x. ( abs ` ( ( mmu ` d ) / d ) ) ) )
225 191 recnd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) e. CC )
226 225 mulid2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. ( 1 / d ) ) = ( 1 / d ) )
227 226 eqcomd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 / d ) = ( 1 x. ( 1 / d ) ) )
228 223 224 227 3brtr4d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) <_ ( 1 / d ) )
229 2fveq3
 |-  ( y = ( x / d ) -> ( seq 1 ( + , F ) ` ( |_ ` y ) ) = ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) )
230 229 fvoveq1d
 |-  ( y = ( x / d ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) = ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) )
231 oveq2
 |-  ( y = ( x / d ) -> ( C / y ) = ( C / ( x / d ) ) )
232 230 231 breq12d
 |-  ( y = ( x / d ) -> ( ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) <-> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( C / ( x / d ) ) ) )
233 12 ad2antrr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` y ) ) - T ) ) <_ ( C / y ) )
234 1re
 |-  1 e. RR
235 elicopnf
 |-  ( 1 e. RR -> ( ( x / d ) e. ( 1 [,) +oo ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) ) )
236 234 235 ax-mp
 |-  ( ( x / d ) e. ( 1 [,) +oo ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) ) )
237 70 82 236 sylanbrc
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. ( 1 [,) +oo ) )
238 232 233 237 rspcdva
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( C / ( x / d ) ) )
239 182 recnd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> C e. CC )
240 239 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. CC )
241 rpcnne0
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
242 241 ad2antrl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. CC /\ x =/= 0 ) )
243 242 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
244 divdiv2
 |-  ( ( C e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( d e. CC /\ d =/= 0 ) ) -> ( C / ( x / d ) ) = ( ( C x. d ) / x ) )
245 240 243 72 105 244 syl112anc
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( x / d ) ) = ( ( C x. d ) / x ) )
246 div23
 |-  ( ( C e. CC /\ d e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( C x. d ) / x ) = ( ( C / x ) x. d ) )
247 240 72 243 246 syl3anc
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C x. d ) / x ) = ( ( C / x ) x. d ) )
248 245 247 eqtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / ( x / d ) ) = ( ( C / x ) x. d ) )
249 238 248 breqtrd
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) <_ ( ( C / x ) x. d ) )
250 190 191 192 194 195 196 228 249 lemul12ad
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( ( 1 / d ) x. ( ( C / x ) x. d ) ) )
251 46 176 absmuld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) = ( ( abs ` ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) ) x. ( abs ` ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) )
252 188 recnd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C / x ) e. CC )
253 252 adantr
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) e. CC )
254 253 72 105 divcan4d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( C / x ) x. d ) / d ) = ( C / x ) )
255 253 72 mulcld
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C / x ) x. d ) e. CC )
256 255 72 105 divrec2d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( C / x ) x. d ) / d ) = ( ( 1 / d ) x. ( ( C / x ) x. d ) ) )
257 254 256 eqtr3d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C / x ) = ( ( 1 / d ) x. ( ( C / x ) x. d ) ) )
258 250 251 257 3brtr4d
 |-  ( ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( C / x ) )
259 45 180 189 258 fsumle
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) )
260 159 nnnn0d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. NN0 )
261 hashfz1
 |-  ( ( |_ ` x ) e. NN0 -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
262 260 261 syl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( # ` ( 1 ... ( |_ ` x ) ) ) = ( |_ ` x ) )
263 262 oveq1d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) = ( ( |_ ` x ) x. ( C / x ) ) )
264 fsumconst
 |-  ( ( ( 1 ... ( |_ ` x ) ) e. Fin /\ ( C / x ) e. CC ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) )
265 45 252 264 syl2anc
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( # ` ( 1 ... ( |_ ` x ) ) ) x. ( C / x ) ) )
266 159 nncnd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) e. CC )
267 divass
 |-  ( ( ( |_ ` x ) e. CC /\ C e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( |_ ` x ) x. C ) / x ) = ( ( |_ ` x ) x. ( C / x ) ) )
268 266 239 242 267 syl3anc
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) = ( ( |_ ` x ) x. ( C / x ) ) )
269 263 265 268 3eqtr4d
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( C / x ) = ( ( ( |_ ` x ) x. C ) / x ) )
270 259 269 breqtrd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ ( ( ( |_ ` x ) x. C ) / x ) )
271 43 adantr
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( C e. RR /\ 0 <_ C ) )
272 flle
 |-  ( x e. RR -> ( |_ ` x ) <_ x )
273 68 272 syl
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( |_ ` x ) <_ x )
274 lemul1a
 |-  ( ( ( ( |_ ` x ) e. RR /\ x e. RR /\ ( C e. RR /\ 0 <_ C ) ) /\ ( |_ ` x ) <_ x ) -> ( ( |_ ` x ) x. C ) <_ ( x x. C ) )
275 185 68 271 273 274 syl31anc
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( |_ ` x ) x. C ) <_ ( x x. C ) )
276 186 182 67 ledivmuld
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( |_ ` x ) x. C ) / x ) <_ C <-> ( ( |_ ` x ) x. C ) <_ ( x x. C ) ) )
277 275 276 mpbird
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( |_ ` x ) x. C ) / x ) <_ C )
278 181 187 182 270 277 letrd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( abs ` ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ C )
279 179 181 182 183 278 letrd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. ( ( seq 1 ( + , F ) ` ( |_ ` ( x / d ) ) ) - T ) ) ) <_ C )
280 175 279 eqbrtrd
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) <_ C )
281 38 40 41 44 280 elo1d
 |-  ( ph -> ( x e. RR+ |-> ( 1 - ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) ) e. O(1) )
282 18 37 281 o1dif
 |-  ( ph -> ( ( x e. RR+ |-> 1 ) e. O(1) <-> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. O(1) ) )
283 17 282 mpbid
 |-  ( ph -> ( x e. RR+ |-> ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( X ` ( L ` d ) ) x. ( ( mmu ` d ) / d ) ) x. T ) ) e. O(1) )