Metamath Proof Explorer

Theorem mulog2sumlem1

Description: Asymptotic formula for sum_ n <_ x , log ( x / n ) / n = ( 1 / 2 ) log ^ 2 ( x ) + gamma x. log x - L + O ( log x / x ) , with explicit constants. Equation 10.2.7 of Shapiro, p. 407. (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses logdivsum.1 
|- F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
mulog2sumlem.1 
|- ( ph -> F ~~>r L )
mulog2sumlem1.2 
|- ( ph -> A e. RR+ )
mulog2sumlem1.3 
|- ( ph -> _e <_ A )
Assertion mulog2sumlem1 
|- ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) <_ ( 2 x. ( ( log ` A ) / A ) ) )

Proof

Step Hyp Ref Expression
1 logdivsum.1 
 |-  F = ( y e. RR+ |-> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) )
2 mulog2sumlem.1 
 |-  ( ph -> F ~~>r L )
3 mulog2sumlem1.2 
 |-  ( ph -> A e. RR+ )
4 mulog2sumlem1.3 
 |-  ( ph -> _e <_ A )
5 fzfid 
 |-  ( ph -> ( 1 ... ( |_ ` A ) ) e. Fin )
6 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
7 6 nnrpd 
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. RR+ )
8 rpdivcl 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( A / m ) e. RR+ )
9 3 7 8 syl2an 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( A / m ) e. RR+ )
10 9 relogcld 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / m ) ) e. RR )
11 6 adantl 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. NN )
12 10 11 nndivred 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` ( A / m ) ) / m ) e. RR )
13 5 12 fsumrecl 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) e. RR )
14 3 relogcld 
 |-  ( ph -> ( log ` A ) e. RR )
15 14 resqcld 
 |-  ( ph -> ( ( log ` A ) ^ 2 ) e. RR )
16 15 rehalfcld 
 |-  ( ph -> ( ( ( log ` A ) ^ 2 ) / 2 ) e. RR )
17 emre 
 |-  gamma e. RR
18 remulcl 
 |-  ( ( gamma e. RR /\ ( log ` A ) e. RR ) -> ( gamma x. ( log ` A ) ) e. RR )
19 17 14 18 sylancr 
 |-  ( ph -> ( gamma x. ( log ` A ) ) e. RR )
20 rpsup 
 |-  sup ( RR+ , RR* , < ) = +oo
21 20 a1i 
 |-  ( ph -> sup ( RR+ , RR* , < ) = +oo )
22 1 logdivsum 
 |-  ( F : RR+ --> RR /\ F e. dom ~~>r /\ ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) ) )
23 22 simp1i 
 |-  F : RR+ --> RR
24 23 a1i 
 |-  ( ph -> F : RR+ --> RR )
25 24 feqmptd 
 |-  ( ph -> F = ( x e. RR+ |-> ( F ` x ) ) )
26 25 2 eqbrtrrd 
 |-  ( ph -> ( x e. RR+ |-> ( F ` x ) ) ~~>r L )
27 23 ffvelcdmi 
 |-  ( x e. RR+ -> ( F ` x ) e. RR )
28 27 adantl 
 |-  ( ( ph /\ x e. RR+ ) -> ( F ` x ) e. RR )
29 21 26 28 rlimrecl 
 |-  ( ph -> L e. RR )
30 19 29 resubcld 
 |-  ( ph -> ( ( gamma x. ( log ` A ) ) - L ) e. RR )
31 16 30 readdcld 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) e. RR )
32 13 31 resubcld 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) e. RR )
33 32 recnd 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) e. CC )
34 33 abscld 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) e. RR )
35 rerpdivcl 
 |-  ( ( ( log ` A ) e. RR /\ m e. RR+ ) -> ( ( log ` A ) / m ) e. RR )
36 14 7 35 syl2an 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` A ) / m ) e. RR )
37 36 recnd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` A ) / m ) e. CC )
38 5 37 fsumcl 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) e. CC )
39 14 recnd 
 |-  ( ph -> ( log ` A ) e. CC )
40 readdcl 
 |-  ( ( ( log ` A ) e. RR /\ gamma e. RR ) -> ( ( log ` A ) + gamma ) e. RR )
41 14 17 40 sylancl 
 |-  ( ph -> ( ( log ` A ) + gamma ) e. RR )
42 41 recnd 
 |-  ( ph -> ( ( log ` A ) + gamma ) e. CC )
43 39 42 mulcld 
 |-  ( ph -> ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) e. CC )
44 38 43 subcld 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) e. CC )
45 44 abscld 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) e. RR )
46 11 nnrpd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. RR+ )
47 46 relogcld 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` m ) e. RR )
48 47 11 nndivred 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` m ) / m ) e. RR )
49 48 recnd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` m ) / m ) e. CC )
50 5 49 fsumcl 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) e. CC )
51 16 recnd 
 |-  ( ph -> ( ( ( log ` A ) ^ 2 ) / 2 ) e. CC )
52 29 recnd 
 |-  ( ph -> L e. CC )
53 51 52 addcld 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) e. CC )
54 50 53 subcld 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) e. CC )
55 54 abscld 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) e. RR )
56 45 55 readdcld 
 |-  ( ph -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) + ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) e. RR )
57 2re 
 |-  2 e. RR
58 14 3 rerpdivcld 
 |-  ( ph -> ( ( log ` A ) / A ) e. RR )
59 remulcl 
 |-  ( ( 2 e. RR /\ ( ( log ` A ) / A ) e. RR ) -> ( 2 x. ( ( log ` A ) / A ) ) e. RR )
60 57 58 59 sylancr 
 |-  ( ph -> ( 2 x. ( ( log ` A ) / A ) ) e. RR )
61 relogdiv 
 |-  ( ( A e. RR+ /\ m e. RR+ ) -> ( log ` ( A / m ) ) = ( ( log ` A ) - ( log ` m ) ) )
62 3 7 61 syl2an 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` ( A / m ) ) = ( ( log ` A ) - ( log ` m ) ) )
63 62 oveq1d 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` ( A / m ) ) / m ) = ( ( ( log ` A ) - ( log ` m ) ) / m ) )
64 39 adantr 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` A ) e. CC )
65 47 recnd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( log ` m ) e. CC )
66 46 rpcnne0d 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( m e. CC /\ m =/= 0 ) )
67 divsubdir 
 |-  ( ( ( log ` A ) e. CC /\ ( log ` m ) e. CC /\ ( m e. CC /\ m =/= 0 ) ) -> ( ( ( log ` A ) - ( log ` m ) ) / m ) = ( ( ( log ` A ) / m ) - ( ( log ` m ) / m ) ) )
68 64 65 66 67 syl3anc 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( ( log ` A ) - ( log ` m ) ) / m ) = ( ( ( log ` A ) / m ) - ( ( log ` m ) / m ) ) )
69 63 68 eqtrd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` ( A / m ) ) / m ) = ( ( ( log ` A ) / m ) - ( ( log ` m ) / m ) ) )
70 69 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( ( log ` A ) / m ) - ( ( log ` m ) / m ) ) )
71 5 37 49 fsumsub 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( ( log ` A ) / m ) - ( ( log ` m ) / m ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) ) )
72 70 71 eqtrd 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) ) )
73 remulcl 
 |-  ( ( ( log ` A ) e. RR /\ gamma e. RR ) -> ( ( log ` A ) x. gamma ) e. RR )
74 14 17 73 sylancl 
 |-  ( ph -> ( ( log ` A ) x. gamma ) e. RR )
75 16 74 readdcld 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) e. RR )
76 75 recnd 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) e. CC )
77 76 51 pncand 
 |-  ( ph -> ( ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) = ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) )
78 17 recni 
 |-  gamma e. CC
79 78 a1i 
 |-  ( ph -> gamma e. CC )
80 39 39 79 adddid 
 |-  ( ph -> ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) = ( ( ( log ` A ) x. ( log ` A ) ) + ( ( log ` A ) x. gamma ) ) )
81 15 recnd 
 |-  ( ph -> ( ( log ` A ) ^ 2 ) e. CC )
82 81 2halvesd 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) = ( ( log ` A ) ^ 2 ) )
83 39 sqvald 
 |-  ( ph -> ( ( log ` A ) ^ 2 ) = ( ( log ` A ) x. ( log ` A ) ) )
84 82 83 eqtrd 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) = ( ( log ` A ) x. ( log ` A ) ) )
85 84 oveq1d 
 |-  ( ph -> ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) + ( ( log ` A ) x. gamma ) ) = ( ( ( log ` A ) x. ( log ` A ) ) + ( ( log ` A ) x. gamma ) ) )
86 74 recnd 
 |-  ( ph -> ( ( log ` A ) x. gamma ) e. CC )
87 51 51 86 add32d 
 |-  ( ph -> ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) + ( ( log ` A ) x. gamma ) ) = ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
88 80 85 87 3eqtr2d 
 |-  ( ph -> ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) = ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
89 88 oveq1d 
 |-  ( ph -> ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) = ( ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) + ( ( ( log ` A ) ^ 2 ) / 2 ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
90 mulcom 
 |-  ( ( gamma e. CC /\ ( log ` A ) e. CC ) -> ( gamma x. ( log ` A ) ) = ( ( log ` A ) x. gamma ) )
91 78 39 90 sylancr 
 |-  ( ph -> ( gamma x. ( log ` A ) ) = ( ( log ` A ) x. gamma ) )
92 91 oveq2d 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( gamma x. ( log ` A ) ) ) = ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( log ` A ) x. gamma ) ) )
93 77 89 92 3eqtr4rd 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( gamma x. ( log ` A ) ) ) = ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
94 93 oveq1d 
 |-  ( ph -> ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( gamma x. ( log ` A ) ) ) - L ) = ( ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) - L ) )
95 91 86 eqeltrd 
 |-  ( ph -> ( gamma x. ( log ` A ) ) e. CC )
96 51 95 52 addsubassd 
 |-  ( ph -> ( ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( gamma x. ( log ` A ) ) ) - L ) = ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) )
97 43 51 52 subsub4d 
 |-  ( ph -> ( ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) - L ) = ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) )
98 94 96 97 3eqtr3d 
 |-  ( ph -> ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) = ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) )
99 72 98 oveq12d 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) ) - ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) )
100 38 50 43 53 sub4d 
 |-  ( ph -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) ) - ( ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) )
101 99 100 eqtrd 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) = ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) )
102 101 fveq2d 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) = ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) )
103 44 54 abs2dif2d 
 |-  ( ph -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) - ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) <_ ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) + ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) )
104 102 103 eqbrtrd 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) <_ ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) + ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) )
105 harmonicbnd4 
 |-  ( A e. RR+ -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) )
106 3 105 syl 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) )
107 11 nnrecred 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / m ) e. RR )
108 5 107 fsumrecl 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. RR )
109 108 41 resubcld 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) e. RR )
110 109 recnd 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) e. CC )
111 110 abscld 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) e. RR )
112 3 rprecred 
 |-  ( ph -> ( 1 / A ) e. RR )
113 0red 
 |-  ( ph -> 0 e. RR )
114 1red 
 |-  ( ph -> 1 e. RR )
115 0lt1 
 |-  0 < 1
116 115 a1i 
 |-  ( ph -> 0 < 1 )
117 loge 
 |-  ( log ` _e ) = 1
118 epr 
 |-  _e e. RR+
119 logleb 
 |-  ( ( _e e. RR+ /\ A e. RR+ ) -> ( _e <_ A <-> ( log ` _e ) <_ ( log ` A ) ) )
120 118 3 119 sylancr 
 |-  ( ph -> ( _e <_ A <-> ( log ` _e ) <_ ( log ` A ) ) )
121 4 120 mpbid 
 |-  ( ph -> ( log ` _e ) <_ ( log ` A ) )
122 117 121 eqbrtrrid 
 |-  ( ph -> 1 <_ ( log ` A ) )
123 113 114 14 116 122 ltletrd 
 |-  ( ph -> 0 < ( log ` A ) )
124 lemul2 
 |-  ( ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) e. RR /\ ( 1 / A ) e. RR /\ ( ( log ` A ) e. RR /\ 0 < ( log ` A ) ) ) -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) <-> ( ( log ` A ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) <_ ( ( log ` A ) x. ( 1 / A ) ) ) )
125 111 112 14 123 124 syl112anc 
 |-  ( ph -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) <-> ( ( log ` A ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) <_ ( ( log ` A ) x. ( 1 / A ) ) ) )
126 106 125 mpbid 
 |-  ( ph -> ( ( log ` A ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) <_ ( ( log ` A ) x. ( 1 / A ) ) )
127 46 rpcnd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. CC )
128 46 rpne0d 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m =/= 0 )
129 64 127 128 divrecd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( ( log ` A ) / m ) = ( ( log ` A ) x. ( 1 / m ) ) )
130 129 sumeq2dv 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) x. ( 1 / m ) ) )
131 107 recnd 
 |-  ( ( ph /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / m ) e. CC )
132 5 39 131 fsummulc2 
 |-  ( ph -> ( ( log ` A ) x. sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) x. ( 1 / m ) ) )
133 130 132 eqtr4d 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) = ( ( log ` A ) x. sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) ) )
134 133 oveq1d 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) = ( ( ( log ` A ) x. sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) )
135 5 131 fsumcl 
 |-  ( ph -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. CC )
136 39 135 42 subdid 
 |-  ( ph -> ( ( log ` A ) x. ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) = ( ( ( log ` A ) x. sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) )
137 134 136 eqtr4d 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) = ( ( log ` A ) x. ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) )
138 137 fveq2d 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) = ( abs ` ( ( log ` A ) x. ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) )
139 135 42 subcld 
 |-  ( ph -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) e. CC )
140 39 139 absmuld 
 |-  ( ph -> ( abs ` ( ( log ` A ) x. ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) = ( ( abs ` ( log ` A ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) )
141 113 14 123 ltled 
 |-  ( ph -> 0 <_ ( log ` A ) )
142 14 141 absidd 
 |-  ( ph -> ( abs ` ( log ` A ) ) = ( log ` A ) )
143 142 oveq1d 
 |-  ( ph -> ( ( abs ` ( log ` A ) ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) = ( ( log ` A ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) )
144 138 140 143 3eqtrd 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) = ( ( log ` A ) x. ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) ) )
145 3 rpcnd 
 |-  ( ph -> A e. CC )
146 3 rpne0d 
 |-  ( ph -> A =/= 0 )
147 39 145 146 divrecd 
 |-  ( ph -> ( ( log ` A ) / A ) = ( ( log ` A ) x. ( 1 / A ) ) )
148 126 144 147 3brtr4d 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) <_ ( ( log ` A ) / A ) )
149 fveq2 
 |-  ( i = m -> ( log ` i ) = ( log ` m ) )
150 id 
 |-  ( i = m -> i = m )
151 149 150 oveq12d 
 |-  ( i = m -> ( ( log ` i ) / i ) = ( ( log ` m ) / m ) )
152 151 cbvsumv 
 |-  sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) = sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m )
153 fveq2 
 |-  ( y = A -> ( |_ ` y ) = ( |_ ` A ) )
154 153 oveq2d 
 |-  ( y = A -> ( 1 ... ( |_ ` y ) ) = ( 1 ... ( |_ ` A ) ) )
155 154 sumeq1d 
 |-  ( y = A -> sum_ m e. ( 1 ... ( |_ ` y ) ) ( ( log ` m ) / m ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) )
156 152 155 eqtrid 
 |-  ( y = A -> sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) )
157 fveq2 
 |-  ( y = A -> ( log ` y ) = ( log ` A ) )
158 157 oveq1d 
 |-  ( y = A -> ( ( log ` y ) ^ 2 ) = ( ( log ` A ) ^ 2 ) )
159 158 oveq1d 
 |-  ( y = A -> ( ( ( log ` y ) ^ 2 ) / 2 ) = ( ( ( log ` A ) ^ 2 ) / 2 ) )
160 156 159 oveq12d 
 |-  ( y = A -> ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( log ` i ) / i ) - ( ( ( log ` y ) ^ 2 ) / 2 ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
161 ovex 
 |-  ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) e. _V
162 160 1 161 fvmpt 
 |-  ( A e. RR+ -> ( F ` A ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
163 3 162 syl 
 |-  ( ph -> ( F ` A ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) )
164 163 oveq1d 
 |-  ( ph -> ( ( F ` A ) - L ) = ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) - L ) )
165 50 51 52 subsub4d 
 |-  ( ph -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( log ` A ) ^ 2 ) / 2 ) ) - L ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) )
166 164 165 eqtrd 
 |-  ( ph -> ( ( F ` A ) - L ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) )
167 166 fveq2d 
 |-  ( ph -> ( abs ` ( ( F ` A ) - L ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) )
168 22 simp3i 
 |-  ( ( F ~~>r L /\ A e. RR+ /\ _e <_ A ) -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) )
169 2 3 4 168 syl3anc 
 |-  ( ph -> ( abs ` ( ( F ` A ) - L ) ) <_ ( ( log ` A ) / A ) )
170 167 169 eqbrtrrd 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) <_ ( ( log ` A ) / A ) )
171 45 55 58 58 148 170 le2addd 
 |-  ( ph -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) + ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) <_ ( ( ( log ` A ) / A ) + ( ( log ` A ) / A ) ) )
172 58 recnd 
 |-  ( ph -> ( ( log ` A ) / A ) e. CC )
173 172 2timesd 
 |-  ( ph -> ( 2 x. ( ( log ` A ) / A ) ) = ( ( ( log ` A ) / A ) + ( ( log ` A ) / A ) ) )
174 171 173 breqtrrd 
 |-  ( ph -> ( ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` A ) / m ) - ( ( log ` A ) x. ( ( log ` A ) + gamma ) ) ) ) + ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` m ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + L ) ) ) ) <_ ( 2 x. ( ( log ` A ) / A ) ) )
175 34 56 60 104 174 letrd 
 |-  ( ph -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( ( log ` ( A / m ) ) / m ) - ( ( ( ( log ` A ) ^ 2 ) / 2 ) + ( ( gamma x. ( log ` A ) ) - L ) ) ) ) <_ ( 2 x. ( ( log ` A ) / A ) ) )