let r be Real; :: thesis: ( r > 0 implies ( log (number_e,r) <= r - 1 & ( r = 1 implies log (number_e,r) = r - 1 ) & ( log (number_e,r) = r - 1 implies r = 1 ) & ( r <> 1 implies log (number_e,r) < r - 1 ) & ( log (number_e,r) < r - 1 implies r <> 1 ) ) )
assume A1: r > 0 ; :: thesis: ( log (number_e,r) <= r - 1 & ( r = 1 implies log (number_e,r) = r - 1 ) & ( log (number_e,r) = r - 1 implies r = 1 ) & ( r <> 1 implies log (number_e,r) < r - 1 ) & ( log (number_e,r) < r - 1 implies r <> 1 ) )
then r in { g where g is Real : 0 < g } ;
then r in right_open_halfline 0 by XXREAL_1:230;
then log (number_e,r) = ln . r by TAYLOR_1:def 2;
hence ( log (number_e,r) <= r - 1 & ( r = 1 implies log (number_e,r) = r - 1 ) & ( log (number_e,r) = r - 1 implies r = 1 ) & ( r <> 1 implies log (number_e,r) < r - 1 ) & ( log (number_e,r) < r - 1 implies r <> 1 ) ) by A1, Th2; :: thesis: verum