let r be Real; :: thesis: ( r > 0 implies ( ln . r <= r - 1 & ( r = 1 implies ln . r = r - 1 ) & ( ln . r = r - 1 implies r = 1 ) & ( r <> 1 implies ln . r < r - 1 ) & ( ln . r < r - 1 implies r <> 1 ) ) )
set Z2 = ].0,1.[;
set Z1 = right_open_halfline 1;
reconsider f2 = log_ number_e as PartFunc of REAL,REAL ;
deffunc H₁( Real) -> Element of REAL = $1 - 1;
defpred S₁[ set ] means $1 in REAL ;
set Z = right_open_halfline 0;
A1: 1 in right_open_halfline 0 by XXREAL_1:235;
1 in { g where g is Real : 0 < g } ;
then A2: 1 in right_open_halfline 0 by XXREAL_1:230;
consider f1 being PartFunc of REAL,REAL such that
A3: ( ( for r being Real holds
( r in dom f1 iff S₁[r] ) ) & ( for r being Real st r in dom f1 holds
f1 . r = H₁(r) ) ) from SEQ_1:sch 3();
dom f1 is Subset of REAL by RELAT_1:def 18;
then A4: dom f1 = REAL by A3, FDIFF_1:1;
A5: for r being Real st r in right_open_halfline 0 holds
f1 . r = (1 * r) + (- 1)

proof

let r be Real; :: thesis: ( r in right_open_halfline 0 implies f1 . r = (1 * r) + (- 1) )
assume r in right_open_halfline 0 ; :: thesis: f1 . r = (1 * r) + (- 1)
f1 . r = r - 1 by A3;
hence f1 . r = (1 * r) + (- 1) ; :: thesis: verum

end;

then A6: f1 is_differentiable_on right_open_halfline 0 by A4, FDIFF_1:23;
set f = f1 - f2;
A7: number_e <> 1 by TAYLOR_1:11;
assume A8: r > 0 ; :: thesis: ( ln . r <= r - 1 & ( r = 1 implies ln . r = r - 1 ) & ( ln . r = r - 1 implies r = 1 ) & ( r <> 1 implies ln . r < r - 1 ) & ( ln . r < r - 1 implies r <> 1 ) )
dom f2 = right_open_halfline 0 by TAYLOR_1:def 2;
then A9: dom (f1 - f2) = (right_open_halfline 0) /\ REAL by A4, VALUED_1:12
.= right_open_halfline 0 by XBOOLE_1:28 ;
A10: for x being Real st x > 0 holds
(f1 - f2) . x = (x - 1) - (ln . x)

proof

let x be Real; :: thesis: ( x > 0 implies (f1 - f2) . x = (x - 1) - (ln . x) )
assume x > 0 ; :: thesis: (f1 - f2) . x = (x - 1) - (ln . x)
then x in { g where g is Real : 0 < g } ;
then A11: x in dom (f1 - f2) by A9, XXREAL_1:230;
(f1 - f2) . x = (f1 . x) - (f2 . x) by A11, VALUED_1:13;
hence (f1 - f2) . x = (x - 1) - (ln . x) by A3; :: thesis: verum

end;

then A12: (f1 - f2) . 1 = (1 - 1) - (ln . 1)
.= - (log (number_e,1)) by A2, TAYLOR_1:def 2
.= - 0 by A7, POWER:51, TAYLOR_1:11
.= 0 ;
A13: f1 is_differentiable_on right_open_halfline 0 by A4, A5, FDIFF_1:23;

A14: now :: thesis: for r being Real st r in right_open_halfline 0 holds
diff (f1,r) = 1

let r be Real; :: thesis: ( r in right_open_halfline 0 implies diff (f1,r) = 1 )
assume A15: r in right_open_halfline 0 ; :: thesis: diff (f1,r) = 1
thus diff (f1,r) = (f1 `| (right_open_halfline 0)) . r by A13, A15, FDIFF_1:def 7
.= 1 by A4, A5, A15, FDIFF_1:23 ; :: thesis: verum

end;

A16: ( f1 - f2 is_differentiable_on right_open_halfline 0 & ( for r being Real st r in right_open_halfline 0 holds
diff ((f1 - f2),r) = 1 - (1 / r) ) )

proof

thus A17: f1 - f2 is_differentiable_on right_open_halfline 0 by A9, A6, FDIFF_1:19, TAYLOR_1:18; :: thesis: for r being Real st r in right_open_halfline 0 holds
diff ((f1 - f2),r) = 1 - (1 / r)

hereby :: thesis: verum

let r be Real; :: thesis: ( r in right_open_halfline 0 implies diff ((f1 - f2),r) = 1 - (1 / r) )
assume A18: r in right_open_halfline 0 ; :: thesis: diff ((f1 - f2),r) = 1 - (1 / r)
((f1 - f2) `| (right_open_halfline 0)) . r = (diff (f1,r)) - (diff (f2,r)) by A9, A6, A18, FDIFF_1:19, TAYLOR_1:18
.= 1 - (diff (f2,r)) by A14, A18
.= 1 - (1 / r) by A18, TAYLOR_1:18 ;
hence diff ((f1 - f2),r) = 1 - (1 / r) by A17, A18, FDIFF_1:def 7; :: thesis: verum

end;

end;

then A19: (f1 - f2) | (right_open_halfline 0) is continuous by FDIFF_1:25;
A20: right_open_halfline 1 c= right_open_halfline 0 by XXREAL_1:46;
A21: for r being Real st r in right_open_halfline 1 holds
diff ((f1 - f2),r) > 0

proof

let r be Real; :: thesis: ( r in right_open_halfline 1 implies diff ((f1 - f2),r) > 0 )
assume A22: r in right_open_halfline 1 ; :: thesis: diff ((f1 - f2),r) > 0
r in { g where g is Real : 1 < g } by A22, XXREAL_1:230;
then A23: ex g1 being Real st
( g1 = r & 1 < g1 ) ;
diff ((f1 - f2),r) = 1 - (1 / r) by A16, A20, A22;
hence diff ((f1 - f2),r) > 0 by A23, XREAL_1:50, XREAL_1:212; :: thesis: verum

end;

A24: for r being Real st r in right_open_halfline 1 holds
(f1 - f2) . r > 0

proof

assume ex r being Real st
( r in right_open_halfline 1 & not (f1 - f2) . r > 0 ) ; :: thesis: contradiction
then consider r1 being Real such that
A25: r1 in right_open_halfline 1 and
A26: (f1 - f2) . r1 <= 0 ;
A27: [.1,r1.] c= dom (f1 - f2) by A1, A9, A20, A25, XXREAL_2:def 12;
r1 in { g where g is Real : 1 < g } by A25, XXREAL_1:230;
then A28: ex g1 being Real st
( g1 = r1 & 1 < g1 ) ;
A29: f1 - f2 is_differentiable_on ].1,r1.[ by A16, FDIFF_1:26, XXREAL_1:247;
A30: (f1 - f2) | [.1,r1.] is continuous by A19, FCONT_1:16, XXREAL_1:249;

per cases ( (f1 - f2) . r1 = 0 or (f1 - f2) . r1 < 0 ) by A26;

suppose (f1 - f2) . r1 = 0 ; :: thesis: contradiction

then consider r2 being Real such that
A31: r2 in ].1,r1.[ and
A32: diff ((f1 - f2),r2) = 0 by A12, A28, A30, A29, A27, ROLLE:1;
ex g1 being Real st
( g1 = r2 & 1 < g1 & g1 < r1 ) by A31;
then r2 in { g where g is Real : 1 < g } ;
then r2 in right_open_halfline 1 by XXREAL_1:230;
hence contradiction by A21, A32; :: thesis: verum

end;

suppose A33: (f1 - f2) . r1 < 0 ; :: thesis: contradiction

consider r3 being Real such that
A34: r3 in ].1,r1.[ and
A35: diff ((f1 - f2),r3) = (((f1 - f2) . r1) - ((f1 - f2) . 1)) / (r1 - 1) by A28, A30, A29, A27, ROLLE:3;
ex g1 being Real st
( g1 = r3 & 1 < g1 & g1 < r1 ) by A34;
then r3 in { g where g is Real : 1 < g } ;
then A36: r3 in right_open_halfline 1 by XXREAL_1:230;
r1 - 1 > 0 by A28, XREAL_1:50;
hence contradiction by A12, A21, A33, A35, A36; :: thesis: verum

end;

end;

end;

A37: for r being Real st r > 1 holds
(f1 - f2) . r > 0

proof

let r be Real; :: thesis: ( r > 1 implies (f1 - f2) . r > 0 )
assume r > 1 ; :: thesis: (f1 - f2) . r > 0
then r in { g where g is Real : 1 < g } ;
then r in right_open_halfline 1 by XXREAL_1:230;
hence (f1 - f2) . r > 0 by A24; :: thesis: verum

end;

A38: ].0,1.[ c= right_open_halfline 0 by XXREAL_1:247;
A39: for r being Real st r in ].0,1.[ holds
diff ((f1 - f2),r) < 0

proof

let r be Real; :: thesis: ( r in ].0,1.[ implies diff ((f1 - f2),r) < 0 )
assume A40: r in ].0,1.[ ; :: thesis: diff ((f1 - f2),r) < 0
then ex g1 being Real st
( g1 = r & 0 < g1 & g1 < 1 ) ;
then A41: 1 < 1 / r by XREAL_1:187;
diff ((f1 - f2),r) = 1 - (1 / r) by A16, A38, A40;
hence diff ((f1 - f2),r) < 0 by A41, XREAL_1:49; :: thesis: verum

end;

A42: for r being Real st r in ].0,1.[ holds
(f1 - f2) . r > 0

proof

assume ex r being Real st
( r in ].0,1.[ & not (f1 - f2) . r > 0 ) ; :: thesis: contradiction
then consider r1 being Real such that
A43: r1 in ].0,1.[ and
A44: (f1 - f2) . r1 <= 0 ;
A45: [.r1,1.] c= dom (f1 - f2) by A1, A9, A38, A43, XXREAL_2:def 12;
A46: ex g1 being Real st
( g1 = r1 & 0 < g1 & g1 < 1 ) by A43;
then A47: (f1 - f2) | [.r1,1.] is continuous by A19, FCONT_1:16, XXREAL_1:249;
A48: f1 - f2 is_differentiable_on ].r1,1.[ by A16, A46, FDIFF_1:26, XXREAL_1:247;

per cases ( (f1 - f2) . r1 = 0 or (f1 - f2) . r1 < 0 ) by A44;

suppose (f1 - f2) . r1 = 0 ; :: thesis: contradiction

then consider r2 being Real such that
A49: r2 in ].r1,1.[ and
A50: diff ((f1 - f2),r2) = 0 by A12, A46, A47, A45, A48, ROLLE:1;
ex g1 being Real st
( g1 = r2 & r1 < g1 & g1 < 1 ) by A49;
then r2 in { g where g is Real : ( 0 < g & g < 1 ) } by A46;
hence contradiction by A39, A50; :: thesis: verum

end;

suppose A51: (f1 - f2) . r1 < 0 ; :: thesis: contradiction

A52: 1 - r1 > 0 by A46, XREAL_1:50;
consider r3 being Real such that
A53: r3 in ].r1,1.[ and
A54: diff ((f1 - f2),r3) = (((f1 - f2) . 1) - ((f1 - f2) . r1)) / (1 - r1) by A46, A47, A45, A48, ROLLE:3;
ex g1 being Real st
( g1 = r3 & r1 < g1 & g1 < 1 ) by A53;
then r3 in ].0,1.[ by A46;
hence contradiction by A12, A39, A51, A54, A52; :: thesis: verum

end;

end;

end;

A55: for r being Real st r > 0 & r < 1 holds
(f1 - f2) . r > 0

proof

let r be Real; :: thesis: ( r > 0 & r < 1 implies (f1 - f2) . r > 0 )
assume that
A56: r > 0 and
A57: r < 1 ; :: thesis: (f1 - f2) . r > 0
r in { g where g is Real : ( 0 < g & g < 1 ) } by A56, A57;
hence (f1 - f2) . r > 0 by A42; :: thesis: verum

end;

for r being Real st r > 0 holds
(f1 - f2) . r >= 0

proof

let r be Real; :: thesis: ( r > 0 implies (f1 - f2) . r >= 0 )
assume A58: r > 0 ; :: thesis: (f1 - f2) . r >= 0

per cases ( r < 1 or r = 1 or r > 1 ) by XXREAL_0:1;

suppose r < 1 ; :: thesis: (f1 - f2) . r >= 0

hence (f1 - f2) . r >= 0 by A55, A58; :: thesis: verum

end;

suppose r = 1 ; :: thesis: (f1 - f2) . r >= 0

hence (f1 - f2) . r >= 0 by A12; :: thesis: verum

end;

suppose r > 1 ; :: thesis: (f1 - f2) . r >= 0

hence (f1 - f2) . r >= 0 by A37; :: thesis: verum

end;

end;

end;

then (f1 - f2) . r >= 0 by A8;
then (r - 1) - (ln . r) >= 0 by A10, A8;
then (r - 1) - 0 >= ln . r by XREAL_1:11;
hence ln . r <= r - 1 ; :: thesis: ( ( r = 1 implies ln . r = r - 1 ) & ( ln . r = r - 1 implies r = 1 ) & ( r <> 1 implies ln . r < r - 1 ) & ( ln . r < r - 1 implies r <> 1 ) )
thus A59: ( r = 1 iff ln . r = r - 1 ) :: thesis: ( r <> 1 iff ln . r < r - 1 )

proof

hereby :: thesis: ( ln . r = r - 1 implies r = 1 )

assume r = 1 ; :: thesis: ln . r = r - 1
then (r - 1) - (ln . r) = 0 by A10, A12;
hence ln . r = r - 1 ; :: thesis: verum

end;

assume ln . r = r - 1 ; :: thesis: r = 1
then A60: (r - 1) - (ln . r) = 0 ;
assume A61: r <> 1 ; :: thesis: contradiction

per cases ( r < 1 or r > 1 ) by A61, XXREAL_0:1;

suppose r < 1 ; :: thesis: contradiction

then (f1 - f2) . r > 0 by A55, A8;
hence contradiction by A10, A8, A60; :: thesis: verum

end;

suppose A62: r > 1 ; :: thesis: contradiction

then (f1 - f2) . r > 0 by A37;
hence contradiction by A10, A60, A62; :: thesis: verum

end;

end;

end;

thus ( r <> 1 iff ln . r < r - 1 ) :: thesis: verum

proof

hereby :: thesis: ( ln . r < r - 1 implies r <> 1 )

assume r <> 1 ; :: thesis: ln . r < r - 1
then A63: ( r - 1 > 0 or 1 - r > 0 ) by XREAL_1:55;

per cases ( r < 1 or r > 1 ) by A63, XREAL_1:47;

suppose r < 1 ; :: thesis: ln . r < r - 1

then (f1 - f2) . r > 0 by A55, A8;
then (r - 1) - (ln . r) > 0 by A10, A8;
hence ln . r < r - 1 by XREAL_1:47; :: thesis: verum

end;

suppose A64: r > 1 ; :: thesis: ln . r < r - 1

then (f1 - f2) . r > 0 by A37;
then (r - 1) - (ln . r) > 0 by A10, A64;
hence ln . r < r - 1 by XREAL_1:47; :: thesis: verum

end;

end;

end;

assume A65: ln . r < r - 1 ; :: thesis: r <> 1
assume r = 1 ; :: thesis: contradiction
hence contradiction by A59, A65; :: thesis: verum

end;