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