let n be non zero Nat; ln . (n + 1) < Harmonic n
set A = [.1,(n + 1).];
0 + 1 <= n + 1
by XREAL_1:31;
then reconsider A = [.1,(n + 1).] as non empty closed_interval Subset of REAL by MEASURE5:def 3, XXREAL_1:1;
WA:
A = ['1,(n + 1)']
by XREAL_1:31, INTEGRA5:def 3;
reconsider Z = right_open_halfline 0 as open Subset of REAL ;
N1:
not 0 in Z
by XXREAL_1:4;
A1:
A c= Z
set f = id Z;
NN: dom ((id Z) ^) =
(dom (id Z)) \ ((id Z) " {0})
by RFUNCT_1:def 2
.=
Z \ {}
by Counter0, N1
.=
Z
;
B1:
lower_bound A = 1
by XREAL_1:31, XXREAL_2:25;
B2:
upper_bound A = n + 1
by XREAL_1:31, XXREAL_2:29;
((id Z) ^) | A is continuous
by ContCut, A1, N1;
then KL: integral (((id Z) ^),A) =
(ln . (upper_bound A)) - (ln . (lower_bound A))
by A1, TAYLOR_1:18, NN, INTEGRA9:61
.=
(ln . (n + 1)) - (1 - 1)
by ENTROPY1:2, B1, B2
.=
ln . (n + 1)
;
set g = (id Z) ^ ;
defpred S1[ Nat] means integral (((id Z) ^),1,($1 + 1)) < Harmonic $1;
reconsider AA = ['1,(1 + 1)'] as non empty closed_interval Subset of REAL ;
AA = [.1,(1 + 1).]
by INTEGRA5:def 3;
then
integral (((id Z) ^),AA) < 1 / 1
by Diesel3;
then I1:
S1[1]
by Harm1, INTEGRA5:def 4;
I2:
for k being non zero Nat st S1[k] holds
S1[k + 1]
proof
let k be non
zero Nat;
( S1[k] implies S1[k + 1] )
assume s0:
S1[
k]
;
S1[k + 1]
set a = 1;
set b =
(k + 1) + 1;
set c =
k + 1;
W0:
1
<= (k + 1) + 1
by XREAL_1:31;
Za:
[.1,((k + 1) + 1).] c= ].0,+infty.[
by XXREAL_1:249;
then W3:
['1,((k + 1) + 1)'] c= dom ((id Z) ^)
by XREAL_1:31, INTEGRA5:def 3, NN;
set B =
['1,((k + 1) + 1)'];
['1,((k + 1) + 1)'] c= Z
by Za, INTEGRA5:def 3, XREAL_1:31;
then v1:
((id Z) ^) | ['1,((k + 1) + 1)'] is
continuous
by ContCut, N1;
then W2:
(id Z) ^ is_integrable_on ['1,((k + 1) + 1)']
by INTEGRA5:11, W3;
W4:
((id Z) ^) | ['1,((k + 1) + 1)'] is
bounded
by INTEGRA5:10, W3, v1;
( 1
<= k + 1 &
k + 1
<= (k + 1) + 1 )
by XREAL_1:31;
then
k + 1
in [.1,((k + 1) + 1).]
by XXREAL_1:1;
then
k + 1
in ['1,((k + 1) + 1)']
by XREAL_1:31, INTEGRA5:def 3;
then W1:
integral (
((id Z) ^),1,
((k + 1) + 1))
= (integral (((id Z) ^),1,(k + 1))) + (integral (((id Z) ^),(k + 1),((k + 1) + 1)))
by W0, W2, W3, W4, INTEGRA6:17;
set AB =
['(k + 1),((k + 1) + 1)'];
['(k + 1),((k + 1) + 1)'] = [.(k + 1),((k + 1) + 1).]
by INTEGRA5:def 3, NAT_1:11;
then
integral (
((id Z) ^),
['(k + 1),((k + 1) + 1)'])
< 1
/ (k + 1)
by Diesel3;
then
integral (
((id Z) ^),
(k + 1),
((k + 1) + 1))
< 1
/ (k + 1)
by NAT_1:11, INTEGRA5:def 4;
then
(integral (((id Z) ^),1,(k + 1))) + (integral (((id Z) ^),(k + 1),((k + 1) + 1))) < (Harmonic k) + (1 / (k + 1))
by s0, XREAL_1:8;
hence
S1[
k + 1]
by Harmon1, W1;
verum
end;
KK:
for n being non zero Nat holds S1[n]
from NAT_1:sch 10(I1, I2);
integral (((id Z) ^),1,(n + 1)) < Harmonic n
by KK;
hence
ln . (n + 1) < Harmonic n
by KL, INTEGRA5:def 4, WA, XREAL_1:31; verum