let a, b be Real; :: thesis: for n being Integer st b < n & n < a & a < n + 1 holds
((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
let n be Integer; :: thesis: ( b < n & n < a & a < n + 1 implies ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )
assume that
A1: n > b and
A2: ( n < a & a < n + 1 ) ; :: thesis: ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4
A3: n - b > 0 by A1, XREAL_1:50;
A4: (n + 1) - a > 0 by A2, XREAL_1:50;
A5: a - n > 0 by A2, XREAL_1:50;
A6: (n - b) + 1 > 0 by A3;
A7: (n - b) * ((n + 1) - a) > 0 by A3, A4;
(a - n) * ((n + 1) - b) > 0 by A5, A6;
hence ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 by A7, Th24; :: thesis: verum