Metamath Proof Explorer


Theorem harmonicbnd4

Description: The asymptotic behavior of sum_ m <_ A , 1 / m = log A + gamma + O ( 1 / A ) . (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Assertion harmonicbnd4
|- ( A e. RR+ -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 fzfid
 |-  ( A e. RR+ -> ( 1 ... ( |_ ` A ) ) e. Fin )
2 elfznn
 |-  ( m e. ( 1 ... ( |_ ` A ) ) -> m e. NN )
3 2 adantl
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( |_ ` A ) ) ) -> m e. NN )
4 3 nnrecred
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( |_ ` A ) ) ) -> ( 1 / m ) e. RR )
5 1 4 fsumrecl
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. RR )
6 5 recnd
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) e. CC )
7 relogcl
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
8 7 recnd
 |-  ( A e. RR+ -> ( log ` A ) e. CC )
9 emre
 |-  gamma e. RR
10 9 a1i
 |-  ( A e. RR+ -> gamma e. RR )
11 10 recnd
 |-  ( A e. RR+ -> gamma e. CC )
12 6 8 11 subsub4d
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - gamma ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) )
13 12 fveq2d
 |-  ( A e. RR+ -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - gamma ) ) = ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) )
14 rpreccl
 |-  ( A e. RR+ -> ( 1 / A ) e. RR+ )
15 14 rpred
 |-  ( A e. RR+ -> ( 1 / A ) e. RR )
16 resubcl
 |-  ( ( gamma e. RR /\ ( 1 / A ) e. RR ) -> ( gamma - ( 1 / A ) ) e. RR )
17 9 15 16 sylancr
 |-  ( A e. RR+ -> ( gamma - ( 1 / A ) ) e. RR )
18 rprege0
 |-  ( A e. RR+ -> ( A e. RR /\ 0 <_ A ) )
19 flge0nn0
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
20 18 19 syl
 |-  ( A e. RR+ -> ( |_ ` A ) e. NN0 )
21 nn0p1nn
 |-  ( ( |_ ` A ) e. NN0 -> ( ( |_ ` A ) + 1 ) e. NN )
22 20 21 syl
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. NN )
23 22 nnrpd
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. RR+ )
24 relogcl
 |-  ( ( ( |_ ` A ) + 1 ) e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) e. RR )
25 23 24 syl
 |-  ( A e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) e. RR )
26 5 25 resubcld
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. RR )
27 5 7 resubcld
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) e. RR )
28 22 nnrecred
 |-  ( A e. RR+ -> ( 1 / ( ( |_ ` A ) + 1 ) ) e. RR )
29 fzfid
 |-  ( A e. RR+ -> ( 1 ... ( ( |_ ` A ) + 1 ) ) e. Fin )
30 elfznn
 |-  ( m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) -> m e. NN )
31 30 adantl
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ) -> m e. NN )
32 31 nnrecred
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ) -> ( 1 / m ) e. RR )
33 29 32 fsumrecl
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) e. RR )
34 33 25 resubcld
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. RR )
35 harmonicbnd
 |-  ( ( ( |_ ` A ) + 1 ) e. NN -> ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( gamma [,] 1 ) )
36 22 35 syl
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( gamma [,] 1 ) )
37 1re
 |-  1 e. RR
38 9 37 elicc2i
 |-  ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( gamma [,] 1 ) <-> ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. RR /\ gamma <_ ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) /\ ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ 1 ) )
39 38 simp2bi
 |-  ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( gamma [,] 1 ) -> gamma <_ ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
40 36 39 syl
 |-  ( A e. RR+ -> gamma <_ ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
41 rpre
 |-  ( A e. RR+ -> A e. RR )
42 fllep1
 |-  ( A e. RR -> A <_ ( ( |_ ` A ) + 1 ) )
43 41 42 syl
 |-  ( A e. RR+ -> A <_ ( ( |_ ` A ) + 1 ) )
44 rpregt0
 |-  ( A e. RR+ -> ( A e. RR /\ 0 < A ) )
45 22 nnred
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. RR )
46 22 nngt0d
 |-  ( A e. RR+ -> 0 < ( ( |_ ` A ) + 1 ) )
47 lerec
 |-  ( ( ( A e. RR /\ 0 < A ) /\ ( ( ( |_ ` A ) + 1 ) e. RR /\ 0 < ( ( |_ ` A ) + 1 ) ) ) -> ( A <_ ( ( |_ ` A ) + 1 ) <-> ( 1 / ( ( |_ ` A ) + 1 ) ) <_ ( 1 / A ) ) )
48 44 45 46 47 syl12anc
 |-  ( A e. RR+ -> ( A <_ ( ( |_ ` A ) + 1 ) <-> ( 1 / ( ( |_ ` A ) + 1 ) ) <_ ( 1 / A ) ) )
49 43 48 mpbid
 |-  ( A e. RR+ -> ( 1 / ( ( |_ ` A ) + 1 ) ) <_ ( 1 / A ) )
50 10 28 34 15 40 49 le2subd
 |-  ( A e. RR+ -> ( gamma - ( 1 / A ) ) <_ ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) )
51 33 recnd
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) e. CC )
52 25 recnd
 |-  ( A e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) e. CC )
53 28 recnd
 |-  ( A e. RR+ -> ( 1 / ( ( |_ ` A ) + 1 ) ) e. CC )
54 51 52 53 sub32d
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) = ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
55 nnuz
 |-  NN = ( ZZ>= ` 1 )
56 22 55 eleqtrdi
 |-  ( A e. RR+ -> ( ( |_ ` A ) + 1 ) e. ( ZZ>= ` 1 ) )
57 32 recnd
 |-  ( ( A e. RR+ /\ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ) -> ( 1 / m ) e. CC )
58 oveq2
 |-  ( m = ( ( |_ ` A ) + 1 ) -> ( 1 / m ) = ( 1 / ( ( |_ ` A ) + 1 ) ) )
59 56 57 58 fsumm1
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) = ( sum_ m e. ( 1 ... ( ( ( |_ ` A ) + 1 ) - 1 ) ) ( 1 / m ) + ( 1 / ( ( |_ ` A ) + 1 ) ) ) )
60 20 nn0cnd
 |-  ( A e. RR+ -> ( |_ ` A ) e. CC )
61 ax-1cn
 |-  1 e. CC
62 pncan
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC ) -> ( ( ( |_ ` A ) + 1 ) - 1 ) = ( |_ ` A ) )
63 60 61 62 sylancl
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) - 1 ) = ( |_ ` A ) )
64 63 oveq2d
 |-  ( A e. RR+ -> ( 1 ... ( ( ( |_ ` A ) + 1 ) - 1 ) ) = ( 1 ... ( |_ ` A ) ) )
65 64 sumeq1d
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( ( ( |_ ` A ) + 1 ) - 1 ) ) ( 1 / m ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )
66 65 oveq1d
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( ( ( |_ ` A ) + 1 ) - 1 ) ) ( 1 / m ) + ( 1 / ( ( |_ ` A ) + 1 ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) + ( 1 / ( ( |_ ` A ) + 1 ) ) ) )
67 59 66 eqtrd
 |-  ( A e. RR+ -> sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) + ( 1 / ( ( |_ ` A ) + 1 ) ) ) )
68 6 53 67 mvrraddd
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) = sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) )
69 68 oveq1d
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
70 54 69 eqtrd
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( ( |_ ` A ) + 1 ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) - ( 1 / ( ( |_ ` A ) + 1 ) ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
71 50 70 breqtrd
 |-  ( A e. RR+ -> ( gamma - ( 1 / A ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
72 logleb
 |-  ( ( A e. RR+ /\ ( ( |_ ` A ) + 1 ) e. RR+ ) -> ( A <_ ( ( |_ ` A ) + 1 ) <-> ( log ` A ) <_ ( log ` ( ( |_ ` A ) + 1 ) ) ) )
73 23 72 mpdan
 |-  ( A e. RR+ -> ( A <_ ( ( |_ ` A ) + 1 ) <-> ( log ` A ) <_ ( log ` ( ( |_ ` A ) + 1 ) ) ) )
74 43 73 mpbid
 |-  ( A e. RR+ -> ( log ` A ) <_ ( log ` ( ( |_ ` A ) + 1 ) ) )
75 7 25 5 74 lesub2dd
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) )
76 17 26 27 71 75 letrd
 |-  ( A e. RR+ -> ( gamma - ( 1 / A ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) )
77 27 15 resubcld
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - ( 1 / A ) ) e. RR )
78 15 recnd
 |-  ( A e. RR+ -> ( 1 / A ) e. CC )
79 6 8 78 subsub4d
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - ( 1 / A ) ) = ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + ( 1 / A ) ) ) )
80 7 15 readdcld
 |-  ( A e. RR+ -> ( ( log ` A ) + ( 1 / A ) ) e. RR )
81 id
 |-  ( A e. RR+ -> A e. RR+ )
82 23 81 relogdivd
 |-  ( A e. RR+ -> ( log ` ( ( ( |_ ` A ) + 1 ) / A ) ) = ( ( log ` ( ( |_ ` A ) + 1 ) ) - ( log ` A ) ) )
83 rerpdivcl
 |-  ( ( ( ( |_ ` A ) + 1 ) e. RR /\ A e. RR+ ) -> ( ( ( |_ ` A ) + 1 ) / A ) e. RR )
84 45 83 mpancom
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) / A ) e. RR )
85 37 a1i
 |-  ( A e. RR+ -> 1 e. RR )
86 85 15 readdcld
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) e. RR )
87 15 reefcld
 |-  ( A e. RR+ -> ( exp ` ( 1 / A ) ) e. RR )
88 61 a1i
 |-  ( A e. RR+ -> 1 e. CC )
89 rpcnne0
 |-  ( A e. RR+ -> ( A e. CC /\ A =/= 0 ) )
90 divdir
 |-  ( ( ( |_ ` A ) e. CC /\ 1 e. CC /\ ( A e. CC /\ A =/= 0 ) ) -> ( ( ( |_ ` A ) + 1 ) / A ) = ( ( ( |_ ` A ) / A ) + ( 1 / A ) ) )
91 60 88 89 90 syl3anc
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) / A ) = ( ( ( |_ ` A ) / A ) + ( 1 / A ) ) )
92 reflcl
 |-  ( A e. RR -> ( |_ ` A ) e. RR )
93 41 92 syl
 |-  ( A e. RR+ -> ( |_ ` A ) e. RR )
94 rerpdivcl
 |-  ( ( ( |_ ` A ) e. RR /\ A e. RR+ ) -> ( ( |_ ` A ) / A ) e. RR )
95 93 94 mpancom
 |-  ( A e. RR+ -> ( ( |_ ` A ) / A ) e. RR )
96 flle
 |-  ( A e. RR -> ( |_ ` A ) <_ A )
97 41 96 syl
 |-  ( A e. RR+ -> ( |_ ` A ) <_ A )
98 rpcn
 |-  ( A e. RR+ -> A e. CC )
99 98 mulid1d
 |-  ( A e. RR+ -> ( A x. 1 ) = A )
100 97 99 breqtrrd
 |-  ( A e. RR+ -> ( |_ ` A ) <_ ( A x. 1 ) )
101 ledivmul
 |-  ( ( ( |_ ` A ) e. RR /\ 1 e. RR /\ ( A e. RR /\ 0 < A ) ) -> ( ( ( |_ ` A ) / A ) <_ 1 <-> ( |_ ` A ) <_ ( A x. 1 ) ) )
102 93 85 44 101 syl3anc
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) / A ) <_ 1 <-> ( |_ ` A ) <_ ( A x. 1 ) ) )
103 100 102 mpbird
 |-  ( A e. RR+ -> ( ( |_ ` A ) / A ) <_ 1 )
104 95 85 15 103 leadd1dd
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) / A ) + ( 1 / A ) ) <_ ( 1 + ( 1 / A ) ) )
105 91 104 eqbrtrd
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) / A ) <_ ( 1 + ( 1 / A ) ) )
106 efgt1p
 |-  ( ( 1 / A ) e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) )
107 14 106 syl
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) )
108 86 87 107 ltled
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) <_ ( exp ` ( 1 / A ) ) )
109 84 86 87 105 108 letrd
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) / A ) <_ ( exp ` ( 1 / A ) ) )
110 rpdivcl
 |-  ( ( ( ( |_ ` A ) + 1 ) e. RR+ /\ A e. RR+ ) -> ( ( ( |_ ` A ) + 1 ) / A ) e. RR+ )
111 23 110 mpancom
 |-  ( A e. RR+ -> ( ( ( |_ ` A ) + 1 ) / A ) e. RR+ )
112 15 rpefcld
 |-  ( A e. RR+ -> ( exp ` ( 1 / A ) ) e. RR+ )
113 111 112 logled
 |-  ( A e. RR+ -> ( ( ( ( |_ ` A ) + 1 ) / A ) <_ ( exp ` ( 1 / A ) ) <-> ( log ` ( ( ( |_ ` A ) + 1 ) / A ) ) <_ ( log ` ( exp ` ( 1 / A ) ) ) ) )
114 109 113 mpbid
 |-  ( A e. RR+ -> ( log ` ( ( ( |_ ` A ) + 1 ) / A ) ) <_ ( log ` ( exp ` ( 1 / A ) ) ) )
115 15 relogefd
 |-  ( A e. RR+ -> ( log ` ( exp ` ( 1 / A ) ) ) = ( 1 / A ) )
116 114 115 breqtrd
 |-  ( A e. RR+ -> ( log ` ( ( ( |_ ` A ) + 1 ) / A ) ) <_ ( 1 / A ) )
117 82 116 eqbrtrrd
 |-  ( A e. RR+ -> ( ( log ` ( ( |_ ` A ) + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) )
118 25 7 15 lesubadd2d
 |-  ( A e. RR+ -> ( ( ( log ` ( ( |_ ` A ) + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) <-> ( log ` ( ( |_ ` A ) + 1 ) ) <_ ( ( log ` A ) + ( 1 / A ) ) ) )
119 117 118 mpbid
 |-  ( A e. RR+ -> ( log ` ( ( |_ ` A ) + 1 ) ) <_ ( ( log ` A ) + ( 1 / A ) ) )
120 25 80 5 119 lesub2dd
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + ( 1 / A ) ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
121 79 120 eqbrtrd
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - ( 1 / A ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) )
122 harmonicbnd3
 |-  ( ( |_ ` A ) e. NN0 -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) )
123 20 122 syl
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) )
124 0re
 |-  0 e. RR
125 124 9 elicc2i
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) <-> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. RR /\ 0 <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) /\ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ gamma ) )
126 125 simp3bi
 |-  ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) e. ( 0 [,] gamma ) -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ gamma )
127 123 126 syl
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` ( ( |_ ` A ) + 1 ) ) ) <_ gamma )
128 77 26 10 121 127 letrd
 |-  ( A e. RR+ -> ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - ( 1 / A ) ) <_ gamma )
129 27 15 10 lesubaddd
 |-  ( A e. RR+ -> ( ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - ( 1 / A ) ) <_ gamma <-> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) <_ ( gamma + ( 1 / A ) ) ) )
130 128 129 mpbid
 |-  ( A e. RR+ -> ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) <_ ( gamma + ( 1 / A ) ) )
131 27 10 15 absdifled
 |-  ( A e. RR+ -> ( ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - gamma ) ) <_ ( 1 / A ) <-> ( ( gamma - ( 1 / A ) ) <_ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) /\ ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) <_ ( gamma + ( 1 / A ) ) ) ) )
132 76 130 131 mpbir2and
 |-  ( A e. RR+ -> ( abs ` ( ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( log ` A ) ) - gamma ) ) <_ ( 1 / A ) )
133 13 132 eqbrtrrd
 |-  ( A e. RR+ -> ( abs ` ( sum_ m e. ( 1 ... ( |_ ` A ) ) ( 1 / m ) - ( ( log ` A ) + gamma ) ) ) <_ ( 1 / A ) )