let a, b be Real; 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; ( (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
; ( ((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; verum