let x, y be Real; ( number_e < x & x <= y implies x / (log (2,x)) <= y / (log (2,y)) )
assume AS:
( number_e < x & x <= y )
; x / (log (2,x)) <= y / (log (2,y))
consider f being PartFunc of REAL,REAL such that
A11:
right_open_halfline number_e = dom f
and
A12:
for x being Real st x in dom f holds
f . x = x / (log (2,x))
and
f is_differentiable_on right_open_halfline number_e
and
for x0 being Real st x0 in right_open_halfline number_e holds
0 <= diff (f,x0)
and
A15:
f is non-decreasing
by LMC31H2;
number_e < y
by AS, XXREAL_0:2;
then
( x in { g where g is Real : number_e < g } & y in { g where g is Real : number_e < g } )
by AS;
then A3:
( x in dom f & y in dom f )
by A11, XXREAL_1:230;
then A4:
f . x <= f . y
by AS, A15, VALUED_0:def 15;
f . x = x / (log (2,x))
by A12, A3;
hence
x / (log (2,x)) <= y / (log (2,y))
by A4, A12, A3; verum