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 = In (($1 - 1),REAL);
defpred S₁[ object ] 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 Element of REAL holds
( r in dom f1 iff S₁[r] ) ) & ( for r being Element of REAL st r in dom f1 holds
f1 . r = H₁(r) ) ) from SEQ_1:sch 3();
A4: for r being Real holds
( r in dom f1 iff S₁[r] ) by XREAL_0:def 1, A3;
dom f1 is Subset of REAL by RELAT_1:def 18;
then A5: dom f1 = REAL by A4, FDIFF_1:1;
A6: 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)
reconsider r = r as Element of REAL by XREAL_0:def 1;
f1 . r = H₁(r) by A3;
hence f1 . r = (1 * r) + (- 1) ; :: thesis: verum

end;

then A7: f1 is_differentiable_on right_open_halfline 0 by A5, FDIFF_1:23;
set f = f1 - f2;
A8: number_e <> 1 by TAYLOR_1:11;
assume A9: 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 A10: dom (f1 - f2) = (right_open_halfline 0) /\ REAL by A5, VALUED_1:12
.= right_open_halfline 0 by XBOOLE_1:28 ;
A11: for x being Element of REAL st x > 0 holds
(f1 - f2) . x = (x - 1) - (ln . x)

proof

let x be Element of 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 A12: x in dom (f1 - f2) by A10, XXREAL_1:230;
(f1 - f2) . x = (f1 . x) - (f2 . x) by A12, VALUED_1:13
.= H₁(x) - (f2 . x) by A3 ;
hence (f1 - f2) . x = (x - 1) - (ln . x) ; :: thesis: verum

end;

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

A15: 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 A16: r in right_open_halfline 0 ; :: thesis: diff (f1,r) = 1
thus diff (f1,r) = (f1 `| (right_open_halfline 0)) . r by A14, A16, FDIFF_1:def 7
.= 1 by A5, A6, A16, FDIFF_1:23 ; :: thesis: verum

end;

A17: ( 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 A18: f1 - f2 is_differentiable_on right_open_halfline 0 by A10, A7, 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 A19: 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 A10, A7, A19, FDIFF_1:19, TAYLOR_1:18
.= 1 - (diff (f2,r)) by A15, A19
.= 1 - (1 / r) by A19, TAYLOR_1:18 ;
hence diff ((f1 - f2),r) = 1 - (1 / r) by A18, A19, FDIFF_1:def 7; :: thesis: verum

end;

end;

then A20: (f1 - f2) | (right_open_halfline 0) is continuous by FDIFF_1:25;
A21: right_open_halfline 1 c= right_open_halfline 0 by XXREAL_1:46;
A22: 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 A23: r in right_open_halfline 1 ; :: thesis: diff ((f1 - f2),r) > 0
r in { g where g is Real : 1 < g } by A23, XXREAL_1:230;
then A24: ex g1 being Real st
( g1 = r & 1 < g1 ) ;
diff ((f1 - f2),r) = 1 - (1 / r) by A17, A21, A23;
hence diff ((f1 - f2),r) > 0 by A24, XREAL_1:50, XREAL_1:212; :: thesis: verum

end;

A25: 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
A26: r1 in right_open_halfline 1 and
A27: (f1 - f2) . r1 <= 0 ;
A28: [.1,r1.] c= dom (f1 - f2) by A1, A10, A21, A26, XXREAL_2:def 12;
r1 in { g where g is Real : 1 < g } by A26, XXREAL_1:230;
then A29: ex g1 being Real st
( g1 = r1 & 1 < g1 ) ;
A30: f1 - f2 is_differentiable_on ].1,r1.[ by A17, FDIFF_1:26, XXREAL_1:247;
A31: (f1 - f2) | [.1,r1.] is continuous by A20, FCONT_1:16, XXREAL_1:249;

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

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

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

end;

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

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

end;

end;

end;

A38: 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 A25; :: thesis: verum

end;

A39: ].0,1.[ c= right_open_halfline 0 by XXREAL_1:247;
A40: 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 A41: r in ].0,1.[ ; :: thesis: diff ((f1 - f2),r) < 0
then ex g1 being Real st
( g1 = r & 0 < g1 & g1 < 1 ) ;
then A42: 1 < 1 / r by XREAL_1:187;
diff ((f1 - f2),r) = 1 - (1 / r) by A17, A39, A41;
hence diff ((f1 - f2),r) < 0 by A42, XREAL_1:49; :: thesis: verum

end;

A43: 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
A44: r1 in ].0,1.[ and
A45: (f1 - f2) . r1 <= 0 ;
A46: [.r1,1.] c= dom (f1 - f2) by A1, A10, A39, A44, XXREAL_2:def 12;
A47: ex g1 being Real st
( g1 = r1 & 0 < g1 & g1 < 1 ) by A44;
then A48: (f1 - f2) | [.r1,1.] is continuous by A20, FCONT_1:16, XXREAL_1:249;
A49: f1 - f2 is_differentiable_on ].r1,1.[ by A17, A47, FDIFF_1:26, XXREAL_1:247;

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

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

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

end;

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

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

end;

end;

end;

A56: 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
A57: r > 0 and
A58: r < 1 ; :: thesis: (f1 - f2) . r > 0
r in { g where g is Real : ( 0 < g & g < 1 ) } by A57, A58;
hence (f1 - f2) . r > 0 by A43; :: thesis: verum

end;

reconsider rr = r as Element of REAL by XREAL_0:def 1;
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 A59: 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 A56, A59; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

then (f1 - f2) . r >= 0 by A9;
then (r - 1) - (ln . rr) >= 0 by A11, A9;
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 A60: ( 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 . rr) = 0 by A11, A13;
hence ln . r = r - 1 ; :: thesis: verum

end;

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

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

suppose r < 1 ; :: thesis: contradiction

then (f1 - f2) . rr > 0 by A56, A9;
hence contradiction by A11, A9, A61; :: thesis: verum

end;

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

then (f1 - f2) . rr > 0 by A38;
hence contradiction by A11, A61, A63; :: 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 A64: ( r - 1 > 0 or 1 - r > 0 ) by XREAL_1:55;

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

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

then (f1 - f2) . r > 0 by A56, A9;
then (r - 1) - (ln . rr) > 0 by A11, A9;
hence ln . r < r - 1 by XREAL_1:47; :: thesis: verum

end;

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

then (f1 - f2) . r > 0 by A38;
then (r - 1) - (ln . rr) > 0 by A11, A65;
hence ln . r < r - 1 by XREAL_1:47; :: thesis: verum

end;

end;

end;

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

end;