let x, y be Real; :: thesis: ( number_e < x & x <= y implies x / (log (2,x)) <= y / (log (2,y)) )

assume AS: ( number_e < x & x <= y ) ; :: thesis: 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; :: thesis: verum

assume AS: ( number_e < x & x <= y ) ; :: thesis: 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; :: thesis: verum