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 Z = right_open_halfline 0 ;
Z: 1 in right_open_halfline 0 by XXREAL_1:235;
defpred S₁[ set ] means $1 in REAL ;
deffunc H₁( Real) -> Element of REAL = $1 - 1;
consider f1 being PartFunc of REAL ,REAL such that
A1: ( ( 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 A2: dom f1 = REAL by A1, FDIFF_1:1;
defpred S₂[ set ] means $1 in right_open_halfline 0 ;
deffunc H₂( Real) -> Element of REAL = ln . $1;
reconsider f2 = log_ number_e as PartFunc of REAL ,REAL ;
A3: dom f2 = right_open_halfline 0 by TAYLOR_1:def 2;
defpred S₃[ set ] means $1 in right_open_halfline 0 ;
deffunc H₃( Real) -> Element of REAL = ($1 - 1) - (ln . $1);
set f = f1 - f2;
A4: dom (f1 - f2) = (right_open_halfline 0 ) /\ REAL by A2, A3, VALUED_1:12
.= right_open_halfline 0 by XBOOLE_1:28 ;
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 A1, A2;
hence f1 . r = (1 * r) + (- 1) ; :: thesis: verum

end;

A6: ( f1 is_differentiable_on right_open_halfline 0 & ( for r being Real st r in right_open_halfline 0 holds
diff f1,r = 1 ) )

proof

A7: ( f1 is_differentiable_on right_open_halfline 0 & ( for r being Real st r in right_open_halfline 0 holds
(f1 `| (right_open_halfline 0 )) . r = 1 ) ) by A2, A5, FDIFF_1:31;

now

let r be Real; :: thesis: ( r in right_open_halfline 0 implies diff f1,r = 1 )
assume A8: r in right_open_halfline 0 ; :: thesis: diff f1,r = 1
thus diff f1,r = (f1 `| (right_open_halfline 0 )) . r by A7, A8, FDIFF_1:def 8
.= 1 by A2, A5, A8, FDIFF_1:31 ; :: thesis: verum

end;

hence ( f1 is_differentiable_on right_open_halfline 0 & ( for r being Real st r in right_open_halfline 0 holds
diff f1,r = 1 ) ) by A2, A5, FDIFF_1:31; :: thesis: verum

end;

A9: ( 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 A10: f1 - f2 is_differentiable_on right_open_halfline 0 by A4, A6, FDIFF_1:27, 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 A11: 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 A4, A6, A11, FDIFF_1:27, TAYLOR_1:18
.= 1 - (diff f2,r) by A6, A11
.= 1 - (1 / r) by A11, TAYLOR_1:18 ;
hence diff (f1 - f2),r = 1 - (1 / r) by A10, A11, FDIFF_1:def 8; :: thesis: verum

end;

end;

1 in { g where g is Real : 0 < g } ;
then A12: 1 in right_open_halfline 0 by XXREAL_1:230;
A13: ( number_e > 0 & number_e <> 1 ) by TAYLOR_1:11;
A14: 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 A15: x > 0 ; :: thesis: (f1 - f2) . x = (x - 1) - (ln . x)
x in { g where g is Real : 0 < g } by A15;
then A16: x in dom (f1 - f2) by A4, XXREAL_1:230;
then A17: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13;
x in (dom f1) /\ (dom f2) by A16, VALUED_1:12;
then ( x in dom f1 & x in dom f2 ) by XBOOLE_0:def 4;
hence (f1 - f2) . x = (x - 1) - (ln . x) by A1, A17; :: thesis: verum

end;

then A18: (f1 - f2) . 1 = (1 - 1) - (ln . 1)
.= - (log number_e ,1) by A12, TAYLOR_1:def 2
.= - 0 by A13, POWER:59
.= 0 ;
set Z1 = right_open_halfline 1;
A19: right_open_halfline 1 c= right_open_halfline 0 by XXREAL_1:46;
A20: f1 - f2 is_differentiable_on right_open_halfline 1 by A9, FDIFF_1:34, 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 C23: ex g1 being Real st
( g1 = r & 1 < g1 ) ;
diff (f1 - f2),r = 1 - (1 / r) by A9, A19, A22;
hence diff (f1 - f2),r > 0 by C23, XREAL_1:52, XREAL_1:214; :: thesis: verum

end;

set Z2 = ].0 ,1.[;
A24: ].0 ,1.[ c= right_open_halfline 0 by XXREAL_1:247;
A25: f1 - f2 is_differentiable_on ].0 ,1.[ by A9, FDIFF_1:34, XXREAL_1:247;
A26: 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 A27: r in ].0 ,1.[ ; :: thesis: diff (f1 - f2),r < 0
then ex g1 being Real st
( g1 = r & 0 < g1 & g1 < 1 ) ;
then A28: 1 < 1 / r by XREAL_1:189;
diff (f1 - f2),r = 1 - (1 / r) by A9, A24, A27;
hence diff (f1 - f2),r < 0 by A28, XREAL_1:51; :: thesis: verum

end;

A29: ( (f1 - f2) | (right_open_halfline 0 ) is continuous & (f1 - f2) | (right_open_halfline 1) is continuous & (f1 - f2) | ].0 ,1.[ is continuous ) by A9, A20, A25, FDIFF_1:33;
A30: 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
A31: ( r1 in right_open_halfline 1 & (f1 - f2) . r1 <= 0 ) ;
r1 in { g where g is Real : 1 < g } by A31, XXREAL_1:230;
then A32: ex g1 being Real st
( g1 = r1 & 1 < g1 ) ;
A33: (f1 - f2) | [.1,r1.] is continuous by A29, FCONT_1:17, XXREAL_1:249;
A34: f1 - f2 is_differentiable_on ].1,r1.[ by A9, FDIFF_1:34, XXREAL_1:247;
y: [.1,r1.] c= dom (f1 - f2) by A19, A31, A4, Z, XXREAL_2:def 12;

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

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

then consider r2 being Real such that
A35: ( r2 in ].1,r1.[ & diff (f1 - f2),r2 = 0 ) by A18, A32, A33, A34, y, ROLLE:1;
ex g1 being Real st
( g1 = r2 & 1 < g1 & g1 < r1 ) by A35;
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, A35; :: thesis: verum

end;

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

consider r3 being Real such that
A37: ( r3 in ].1,r1.[ & diff (f1 - f2),r3 = (((f1 - f2) . r1) - ((f1 - f2) . 1)) / (r1 - 1) ) by A32, A33, A34, y, ROLLE:3;
ex g1 being Real st
( g1 = r3 & 1 < g1 & g1 < r1 ) by A37;
then r3 in { g where g is Real : 1 < g } ;
then A38: r3 in right_open_halfline 1 by XXREAL_1:230;
r1 - 1 > 0 by A32, XREAL_1:52;
hence contradiction by A21, A38, A18, A36, A37; :: thesis: verum

end;

end;

end;

A39: 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
A40: ( r1 in ].0 ,1.[ & (f1 - f2) . r1 <= 0 ) ;
A41: ex g1 being Real st
( g1 = r1 & 0 < g1 & g1 < 1 ) by A40;
then A42: (f1 - f2) | [.r1,1.] is continuous by A29, FCONT_1:17, XXREAL_1:249;
y: [.r1,1.] c= dom (f1 - f2) by A24, A40, A4, Z, XXREAL_2:def 12;
A43: f1 - f2 is_differentiable_on ].r1,1.[ by A9, A41, FDIFF_1:34, XXREAL_1:247;

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

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

then consider r2 being Real such that
A44: ( r2 in ].r1,1.[ & diff (f1 - f2),r2 = 0 ) by A18, A41, A42, A43, y, ROLLE:1;
ex g1 being Real st
( g1 = r2 & r1 < g1 & g1 < 1 ) by A44;
then r2 in { g where g is Real : ( 0 < g & g < 1 ) } by A41;
hence contradiction by A26, A44; :: thesis: verum

end;

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

consider r3 being Real such that
A46: ( r3 in ].r1,1.[ & diff (f1 - f2),r3 = (((f1 - f2) . 1) - ((f1 - f2) . r1)) / (1 - r1) ) by A41, A42, A43, y, ROLLE:3;
ex g1 being Real st
( g1 = r3 & r1 < g1 & g1 < 1 ) by A46;
then A47: r3 in ].0 ,1.[ by A41;
1 - r1 > 0 by A41, XREAL_1:52;
hence contradiction by A26, A47, A46, A18, A45; :: thesis: verum

end;

end;

end;

A49: 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 A50: ( r > 0 & r < 1 ) ; :: thesis: (f1 - f2) . r > 0
r in { g where g is Real : ( 0 < g & g < 1 ) } by A50;
hence (f1 - f2) . r > 0 by A39; :: thesis: verum

end;

A51: 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 A52: r > 1 ; :: thesis: (f1 - f2) . r > 0
r in { g where g is Real : 1 < g } by A52;
then r in right_open_halfline 1 by XXREAL_1:230;
hence (f1 - f2) . r > 0 by A30; :: thesis: verum

end;

A53: 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 A54: 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 A49, A54; :: thesis: verum

end;

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

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

end;

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

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

end;

end;

end;

assume A55: 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 ) )
then (f1 - f2) . r >= 0 by A53;
then (r - 1) - (ln . r) >= 0 by A14, A55;
then (r - 1) - 0 >= ln . r by XREAL_1:13;
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 A56: ( 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 A14, A18;
hence ln . r = r - 1 ; :: thesis: verum

end;

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

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

suppose r < 1 ; :: thesis: contradiction

then (f1 - f2) . r > 0 by A49, A55;
hence contradiction by A14, A55, A57; :: thesis: verum

end;

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

then (f1 - f2) . r > 0 by A51;
hence contradiction by A14, A57, A59; :: 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 A60: ( r - 1 > 0 or 1 - r > 0 ) by XREAL_1:57;

per cases ( r < 1 or r > 1 ) by A60, XREAL_1:49;

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

then (f1 - f2) . r > 0 by A49, A55;
then (r - 1) - (ln . r) > 0 by A14, A55;
hence ln . r < r - 1 by XREAL_1:49; :: thesis: verum

end;

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

then (f1 - f2) . r > 0 by A51;
then (r - 1) - (ln . r) > 0 by A14, A61;
hence ln . r < r - 1 by XREAL_1:49; :: thesis: verum

end;

end;

end;

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

end;