let a, b be Real; :: thesis: for n being Integer st (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 holds
( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )
let n be Integer; :: thesis: ( (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 implies ( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 ) )
assume that
A1: (n - a) * ((n + 1) - b) > 0 and
A2: (b - n) * ((n + 1) - a) > 0 ; :: thesis: ( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )
set s = (n - a) * ((n + 1) - b);
set t = (b - n) * ((n + 1) - a);
A3: sqrt (((n - a) * ((n + 1) - b)) * ((b - n) * ((n + 1) - a))) <= (((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a))) / 2 by A1, A2, SERIES_3:2;
A4: (sqrt (((n - a) * ((n + 1) - b)) * ((b - n) * ((n + 1) - a)))) ^2 = ((n - a) * ((n + 1) - b)) * ((b - n) * ((n + 1) - a)) by A1, A2, SQUARE_1:def 2;
A5: sqrt (((n - a) * ((n + 1) - b)) * ((b - n) * ((n + 1) - a))) >= 0 by A1, A2, SQUARE_1:def 2;
A6: (n - a) * ((n + 1) - b) = |.((n - a) * ((n + 1) - b)).| by A1, COMPLEX1:43
.= |.(n - a).| * |.((n + 1) - b).| by COMPLEX1:65 ;
A7: (b - n) * ((n + 1) - a) = |.((b - n) * ((n + 1) - a)).| by A2, COMPLEX1:43
.= |.(b - n).| * |.((n + 1) - a).| by COMPLEX1:65 ;
A8: |.(n - a).| = |.(- (n - a)).| by COMPLEX1:52
.= |.(a - n).| ;
A9: |.((n + 1) - b).| = |.(- ((n + 1) - b)).| by COMPLEX1:52
.= |.((b - n) - 1).| ;
A10: |.((n + 1) - a).| = |.(- ((n + 1) - a)).| by COMPLEX1:52
.= |.((a - n) - 1).| ;
A11: ((n - a) * ((n + 1) - b)) * ((b - n) * ((n + 1) - a)) = (|.(n - a).| * |.((n + 1) - b).|) * (|.(b - n).| * |.((n + 1) - a).|) by A7, A6
.= ((|.(b - n).| * |.(a - n).|) * |.((b - n) - 1).|) * |.((a - n) - 1).| by A10, A9, A8 ;
(b - a) ^2 = |.(b - a).| ^2 by COMPLEX1:75
.= |.(a - b).| ^2 by COMPLEX1:60 ;
then ((b - a) / 2) ^2 = (|.(a - b).| ^2) / 4 ;
hence ( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 ) by A3, A4, A5, A11, SQUARE_1:15; :: thesis: verum