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