let n be non zero Nat; :: thesis: 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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in Z )
assume a1: x in A ; :: thesis: x in Z
then reconsider xx = x as Real ;
( 1 <= xx & xx <= n + 1 ) by a1, XXREAL_1:1;
hence x in Z by XXREAL_1:235; :: thesis: verum

end;

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 S₁[ 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: S₁[1] by Harm1, INTEGRA5:def 4;
I2: for k being non zero Nat st S₁[k] holds
S₁[k + 1]

proof

let k be non zero Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume s0: S₁[k] ; :: thesis: S₁[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 S₁[k + 1] by Harmon1, W1; :: thesis: verum

end;

KK: for n being non zero Nat holds S₁[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; :: thesis: verum