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 ffvelcdmda 
 |-  ( ( 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 mullidd 
 |-  ( ( ( 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 ffvelcdmd 
 |-  ( ( ( 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 ffvelcdm 
 |-  ( ( 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 mullidd 
 |-  ( ( ( 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) )