This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dchrvmasumlem2

Description: Lemma for dchrvmasum . (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. )
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 dchrvmasumlem2 
|- ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) 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 elrege0 
 |-  ( C e. ( 0 [,) +oo ) <-> ( C e. RR /\ 0 <_ C ) )
18 11 17 sylib 
 |-  ( ph -> ( C e. RR /\ 0 <_ C ) )
19 18 simpld 
 |-  ( ph -> C e. RR )
20 19 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> C e. RR )
21 fzfid 
 |-  ( ( ph /\ x e. RR+ ) -> ( 1 ... ( |_ ` x ) ) e. Fin )
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 26 relogcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / d ) ) e. RR )
28 22 adantr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR+ )
29 27 28 rerpdivcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / d ) ) / x ) e. RR )
30 21 29 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) e. RR )
31 20 30 remulcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) e. RR )
32 3nn 
 |-  3 e. NN
33 nnrp 
 |-  ( 3 e. NN -> 3 e. RR+ )
34 relogcl 
 |-  ( 3 e. RR+ -> ( log ` 3 ) e. RR )
35 32 33 34 mp2b 
 |-  ( log ` 3 ) e. RR
36 1re 
 |-  1 e. RR
37 35 36 readdcli 
 |-  ( ( log ` 3 ) + 1 ) e. RR
38 remulcl 
 |-  ( ( R e. RR /\ ( ( log ` 3 ) + 1 ) e. RR ) -> ( R x. ( ( log ` 3 ) + 1 ) ) e. RR )
39 14 37 38 sylancl 
 |-  ( ph -> ( R x. ( ( log ` 3 ) + 1 ) ) e. RR )
40 39 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> ( R x. ( ( log ` 3 ) + 1 ) ) e. RR )
41 rpssre 
 |-  RR+ C_ RR
42 19 recnd 
 |-  ( ph -> C e. CC )
43 o1const 
 |-  ( ( RR+ C_ RR /\ C e. CC ) -> ( x e. RR+ |-> C ) e. O(1) )
44 41 42 43 sylancr 
 |-  ( ph -> ( x e. RR+ |-> C ) e. O(1) )
45 logfacrlim2 
 |-  ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) ~~>r 1
46 rlimo1 
 |-  ( ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) ~~>r 1 -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) e. O(1) )
47 45 46 mp1i 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) e. O(1) )
48 20 30 44 47 o1mul2 
 |-  ( ph -> ( x e. RR+ |-> ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) ) e. O(1) )
49 39 recnd 
 |-  ( ph -> ( R x. ( ( log ` 3 ) + 1 ) ) e. CC )
50 o1const 
 |-  ( ( RR+ C_ RR /\ ( R x. ( ( log ` 3 ) + 1 ) ) e. CC ) -> ( x e. RR+ |-> ( R x. ( ( log ` 3 ) + 1 ) ) ) e. O(1) )
51 41 49 50 sylancr 
 |-  ( ph -> ( x e. RR+ |-> ( R x. ( ( log ` 3 ) + 1 ) ) ) e. O(1) )
52 31 40 48 51 o1add2 
 |-  ( ph -> ( x e. RR+ |-> ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) ) e. O(1) )
53 31 40 readdcld 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) e. RR )
54 10 eleq1d 
 |-  ( m = ( x / d ) -> ( F e. CC <-> K e. CC ) )
55 9 ralrimiva 
 |-  ( ph -> A. m e. RR+ F e. CC )
56 55 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> A. m e. RR+ F e. CC )
57 54 56 26 rspcdva 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> K e. CC )
58 12 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> T e. CC )
59 57 58 subcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( K - T ) e. CC )
60 59 abscld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( K - T ) ) e. RR )
61 23 adantl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. NN )
62 60 61 nndivred 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( abs ` ( K - T ) ) / d ) e. RR )
63 21 62 fsumrecl 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) e. RR )
64 63 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) e. CC )
65 61 nnrpd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. RR+ )
66 59 absge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( abs ` ( K - T ) ) )
67 60 65 66 divge0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( abs ` ( K - T ) ) / d ) )
68 21 62 67 fsumge0 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) )
69 63 68 absidd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) )
70 69 63 eqeltrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) e. RR )
71 53 recnd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) e. CC )
72 71 abscld 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) ) e. RR )
73 3re 
 |-  3 e. RR
74 73 a1i 
 |-  ( ( ph /\ x e. RR+ ) -> 3 e. RR )
75 1le3 
 |-  1 <_ 3
76 74 75 jctir 
 |-  ( ( ph /\ x e. RR+ ) -> ( 3 e. RR /\ 1 <_ 3 ) )
77 14 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> R e. RR )
78 36 rexri 
 |-  1 e. RR*
79 73 rexri 
 |-  3 e. RR*
80 1lt3 
 |-  1 < 3
81 lbico1 
 |-  ( ( 1 e. RR* /\ 3 e. RR* /\ 1 < 3 ) -> 1 e. ( 1 [,) 3 ) )
82 78 79 80 81 mp3an 
 |-  1 e. ( 1 [,) 3 )
83 0red 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> 0 e. RR )
84 elico2 
 |-  ( ( 1 e. RR /\ 3 e. RR* ) -> ( m e. ( 1 [,) 3 ) <-> ( m e. RR /\ 1 <_ m /\ m < 3 ) ) )
85 36 79 84 mp2an 
 |-  ( m e. ( 1 [,) 3 ) <-> ( m e. RR /\ 1 <_ m /\ m < 3 ) )
86 85 simp1bi 
 |-  ( m e. ( 1 [,) 3 ) -> m e. RR )
87 0red 
 |-  ( m e. ( 1 [,) 3 ) -> 0 e. RR )
88 1red 
 |-  ( m e. ( 1 [,) 3 ) -> 1 e. RR )
89 0lt1 
 |-  0 < 1
90 89 a1i 
 |-  ( m e. ( 1 [,) 3 ) -> 0 < 1 )
91 85 simp2bi 
 |-  ( m e. ( 1 [,) 3 ) -> 1 <_ m )
92 87 88 86 90 91 ltletrd 
 |-  ( m e. ( 1 [,) 3 ) -> 0 < m )
93 86 92 elrpd 
 |-  ( m e. ( 1 [,) 3 ) -> m e. RR+ )
94 12 adantr 
 |-  ( ( ph /\ m e. RR+ ) -> T e. CC )
95 9 94 subcld 
 |-  ( ( ph /\ m e. RR+ ) -> ( F - T ) e. CC )
96 95 abscld 
 |-  ( ( ph /\ m e. RR+ ) -> ( abs ` ( F - T ) ) e. RR )
97 93 96 sylan2 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> ( abs ` ( F - T ) ) e. RR )
98 14 adantr 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> R e. RR )
99 95 absge0d 
 |-  ( ( ph /\ m e. RR+ ) -> 0 <_ ( abs ` ( F - T ) ) )
100 93 99 sylan2 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> 0 <_ ( abs ` ( F - T ) ) )
101 15 r19.21bi 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> ( abs ` ( F - T ) ) <_ R )
102 83 97 98 100 101 letrd 
 |-  ( ( ph /\ m e. ( 1 [,) 3 ) ) -> 0 <_ R )
103 102 ralrimiva 
 |-  ( ph -> A. m e. ( 1 [,) 3 ) 0 <_ R )
104 biidd 
 |-  ( m = 1 -> ( 0 <_ R <-> 0 <_ R ) )
105 104 rspcv 
 |-  ( 1 e. ( 1 [,) 3 ) -> ( A. m e. ( 1 [,) 3 ) 0 <_ R -> 0 <_ R ) )
106 82 103 105 mpsyl 
 |-  ( ph -> 0 <_ R )
107 106 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> 0 <_ R )
108 77 107 jca 
 |-  ( ( ph /\ x e. RR+ ) -> ( R e. RR /\ 0 <_ R ) )
109 60 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( K - T ) ) e. CC )
110 19 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. RR )
111 110 29 remulcld 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C x. ( ( log ` ( x / d ) ) / x ) ) e. RR )
112 18 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C e. RR /\ 0 <_ C ) )
113 log1 
 |-  ( log ` 1 ) = 0
114 61 nncnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d e. CC )
115 114 mullidd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) = d )
116 rpre 
 |-  ( x e. RR+ -> x e. RR )
117 116 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> x e. RR )
118 fznnfl 
 |-  ( x e. RR -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) )
119 117 118 syl 
 |-  ( ( ph /\ x e. RR+ ) -> ( d e. ( 1 ... ( |_ ` x ) ) <-> ( d e. NN /\ d <_ x ) ) )
120 119 simplbda 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> d <_ x )
121 115 120 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 x. d ) <_ x )
122 1red 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR )
123 116 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> x e. RR )
124 122 123 65 lemuldivd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( 1 x. d ) <_ x <-> 1 <_ ( x / d ) ) )
125 121 124 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 <_ ( x / d ) )
126 1rp 
 |-  1 e. RR+
127 126 a1i 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 1 e. RR+ )
128 127 26 logled 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( 1 <_ ( x / d ) <-> ( log ` 1 ) <_ ( log ` ( x / d ) ) ) )
129 125 128 mpbid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` 1 ) <_ ( log ` ( x / d ) ) )
130 113 129 eqbrtrrid 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( log ` ( x / d ) ) )
131 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
132 131 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. RR /\ 0 < x ) )
133 divge0 
 |-  ( ( ( ( log ` ( x / d ) ) e. RR /\ 0 <_ ( log ` ( x / d ) ) ) /\ ( x e. RR /\ 0 < x ) ) -> 0 <_ ( ( log ` ( x / d ) ) / x ) )
134 27 130 132 133 syl21anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( ( log ` ( x / d ) ) / x ) )
135 mulge0 
 |-  ( ( ( C e. RR /\ 0 <_ C ) /\ ( ( ( log ` ( x / d ) ) / x ) e. RR /\ 0 <_ ( ( log ` ( x / d ) ) / x ) ) ) -> 0 <_ ( C x. ( ( log ` ( x / d ) ) / x ) ) )
136 112 29 134 135 syl12anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> 0 <_ ( C x. ( ( log ` ( x / d ) ) / x ) ) )
137 absidm 
 |-  ( ( K - T ) e. CC -> ( abs ` ( abs ` ( K - T ) ) ) = ( abs ` ( K - T ) ) )
138 59 137 syl 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( abs ` ( abs ` ( K - T ) ) ) = ( abs ` ( K - T ) ) )
139 138 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( abs ` ( abs ` ( K - T ) ) ) = ( abs ` ( K - T ) ) )
140 10 fvoveq1d 
 |-  ( m = ( x / d ) -> ( abs ` ( F - T ) ) = ( abs ` ( K - T ) ) )
141 fveq2 
 |-  ( m = ( x / d ) -> ( log ` m ) = ( log ` ( x / d ) ) )
142 id 
 |-  ( m = ( x / d ) -> m = ( x / d ) )
143 141 142 oveq12d 
 |-  ( m = ( x / d ) -> ( ( log ` m ) / m ) = ( ( log ` ( x / d ) ) / ( x / d ) ) )
144 143 oveq2d 
 |-  ( m = ( x / d ) -> ( C x. ( ( log ` m ) / m ) ) = ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) )
145 140 144 breq12d 
 |-  ( m = ( x / d ) -> ( ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) <-> ( abs ` ( K - T ) ) <_ ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) ) )
146 13 ralrimiva 
 |-  ( ph -> A. m e. ( 3 [,) +oo ) ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )
147 146 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> A. m e. ( 3 [,) +oo ) ( abs ` ( F - T ) ) <_ ( C x. ( ( log ` m ) / m ) ) )
148 nndivre 
 |-  ( ( x e. RR /\ d e. NN ) -> ( x / d ) e. RR )
149 117 23 148 syl2an 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x / d ) e. RR )
150 149 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( x / d ) e. RR )
151 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> 3 <_ ( x / d ) )
152 elicopnf 
 |-  ( 3 e. RR -> ( ( x / d ) e. ( 3 [,) +oo ) <-> ( ( x / d ) e. RR /\ 3 <_ ( x / d ) ) ) )
153 73 152 ax-mp 
 |-  ( ( x / d ) e. ( 3 [,) +oo ) <-> ( ( x / d ) e. RR /\ 3 <_ ( x / d ) ) )
154 150 151 153 sylanbrc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( x / d ) e. ( 3 [,) +oo ) )
155 145 147 154 rspcdva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( abs ` ( K - T ) ) <_ ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) )
156 27 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / d ) ) e. CC )
157 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
158 157 ad2antlr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( x e. CC /\ x =/= 0 ) )
159 65 rpcnne0d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( d e. CC /\ d =/= 0 ) )
160 divdiv2 
 |-  ( ( ( log ` ( x / d ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) /\ ( d e. CC /\ d =/= 0 ) ) -> ( ( log ` ( x / d ) ) / ( x / d ) ) = ( ( ( log ` ( x / d ) ) x. d ) / x ) )
161 156 158 159 160 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / d ) ) / ( x / d ) ) = ( ( ( log ` ( x / d ) ) x. d ) / x ) )
162 div23 
 |-  ( ( ( log ` ( x / d ) ) e. CC /\ d e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( log ` ( x / d ) ) x. d ) / x ) = ( ( ( log ` ( x / d ) ) / x ) x. d ) )
163 156 114 158 162 syl3anc 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( ( log ` ( x / d ) ) x. d ) / x ) = ( ( ( log ` ( x / d ) ) / x ) x. d ) )
164 161 163 eqtrd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / d ) ) / ( x / d ) ) = ( ( ( log ` ( x / d ) ) / x ) x. d ) )
165 164 oveq2d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) = ( C x. ( ( ( log ` ( x / d ) ) / x ) x. d ) ) )
166 42 ad2antrr 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> C e. CC )
167 29 recnd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / d ) ) / x ) e. CC )
168 166 167 114 mulassd 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( ( C x. ( ( log ` ( x / d ) ) / x ) ) x. d ) = ( C x. ( ( ( log ` ( x / d ) ) / x ) x. d ) ) )
169 165 168 eqtr4d 
 |-  ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) -> ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) = ( ( C x. ( ( log ` ( x / d ) ) / x ) ) x. d ) )
170 169 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( C x. ( ( log ` ( x / d ) ) / ( x / d ) ) ) = ( ( C x. ( ( log ` ( x / d ) ) / x ) ) x. d ) )
171 155 170 breqtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( abs ` ( K - T ) ) <_ ( ( C x. ( ( log ` ( x / d ) ) / x ) ) x. d ) )
172 139 171 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ 3 <_ ( x / d ) ) -> ( abs ` ( abs ` ( K - T ) ) ) <_ ( ( C x. ( ( log ` ( x / d ) ) / x ) ) x. d ) )
173 138 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( abs ` ( abs ` ( K - T ) ) ) = ( abs ` ( K - T ) ) )
174 140 breq1d 
 |-  ( m = ( x / d ) -> ( ( abs ` ( F - T ) ) <_ R <-> ( abs ` ( K - T ) ) <_ R ) )
175 15 ad3antrrr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> A. m e. ( 1 [,) 3 ) ( abs ` ( F - T ) ) <_ R )
176 149 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( x / d ) e. RR )
177 125 adantr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> 1 <_ ( x / d ) )
178 simpr 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( x / d ) < 3 )
179 elico2 
 |-  ( ( 1 e. RR /\ 3 e. RR* ) -> ( ( x / d ) e. ( 1 [,) 3 ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) /\ ( x / d ) < 3 ) ) )
180 36 79 179 mp2an 
 |-  ( ( x / d ) e. ( 1 [,) 3 ) <-> ( ( x / d ) e. RR /\ 1 <_ ( x / d ) /\ ( x / d ) < 3 ) )
181 176 177 178 180 syl3anbrc 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( x / d ) e. ( 1 [,) 3 ) )
182 174 175 181 rspcdva 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( abs ` ( K - T ) ) <_ R )
183 173 182 eqbrtrd 
 |-  ( ( ( ( ph /\ x e. RR+ ) /\ d e. ( 1 ... ( |_ ` x ) ) ) /\ ( x / d ) < 3 ) -> ( abs ` ( abs ` ( K - T ) ) ) <_ R )
184 22 76 108 109 111 136 172 183 fsumharmonic 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) <_ ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( C x. ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) )
185 42 adantr 
 |-  ( ( ph /\ x e. RR+ ) -> C e. CC )
186 21 185 167 fsummulc2 
 |-  ( ( ph /\ x e. RR+ ) -> ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) ( C x. ( ( log ` ( x / d ) ) / x ) ) )
187 186 oveq1d 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) ( C x. ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) )
188 184 187 breqtrrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) <_ ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) )
189 53 leabsd 
 |-  ( ( ph /\ x e. RR+ ) -> ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) <_ ( abs ` ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) ) )
190 70 53 72 188 189 letrd 
 |-  ( ( ph /\ x e. RR+ ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) <_ ( abs ` ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) ) )
191 190 adantrr 
 |-  ( ( ph /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) <_ ( abs ` ( ( C x. sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / d ) ) / x ) ) + ( R x. ( ( log ` 3 ) + 1 ) ) ) ) )
192 16 52 53 64 191 o1le 
 |-  ( ph -> ( x e. RR+ |-> sum_ d e. ( 1 ... ( |_ ` x ) ) ( ( abs ` ( K - T ) ) / d ) ) e. O(1) )