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 ) )