let a, e be Real; :: thesis: for b, c, d being non negative Real st a <= (b * c) * d & d < e / ((2 * b) * |.c.|) holds
a <= e / 2
let b, c, d be non negative Real; :: thesis: ( a <= (b * c) * d & d < e / ((2 * b) * |.c.|) implies a <= e / 2 )
assume that
A1: a <= (b * c) * d and
A2: d < e / ((2 * b) * |.c.|) ; :: thesis: a <= e / 2
A3: ( 0 < b & 0 < c ) by A2, Th05;
A4: (b * c) * d <= (b * c) * (e / ((2 * b) * |.c.|)) by A2, XREAL_1:64;
(b * c) * (e / ((2 * b) * |.c.|)) = (b * c) * (e / ((2 * b) * c)) by ABSVALUE:def 1
.= (b * c) * (e / (2 * (b * c)))
.= e / 2 by A3, Th06 ;
hence a <= e / 2 by A4, A1, XXREAL_0:2; :: thesis: verum