let a, b be Real; ( |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 & a is not Integer implies [\a/] + 1 >= b )
set u = [\a/];
set v = [\a/] + 1;
assume AA:
( |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 )
; ( a is Integer or [\a/] + 1 >= b )
assume A2:
( a is not Integer & [\a/] + 1 < b )
; contradiction
then A3:
a - [\a/] > 0
by INT_1:26, XREAL_1:50;
A4:
a - 1 < [\a/]
by INT_1:def 6;
then a3:
a < [\a/] + 1
by XREAL_1:19;
then A5:
((|.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| <= (|.(a - b).| ^2) / 4
by A2, INT_1:26, Th27;
per cases
( ( |.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| > |.(a - b).| / 2 ) or ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 ) or ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| > |.(a - b).| / 2 ) or ( |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 & |.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 ) )
by XXREAL_0:1, AA;
suppose SS:
(
|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 &
|.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 )
;
contradictionA6:
([\a/] + 1) - b < 0
by A2, XREAL_1:49;
A7:
[\a/] - a < 0
by A2, INT_1:26, XREAL_1:49;
A8:
(1 + [\a/]) - [\a/] < b - [\a/]
by A2, XREAL_1:14;
A9:
([\a/] + 1) - a > 0
by A4, XREAL_1:19, XREAL_1:50;
A11:
([\a/] - a) * (([\a/] + 1) - b) =
|.(([\a/] - a) * (([\a/] + 1) - b)).|
by A6, A7, ABSVALUE:def 1
.=
|.([\a/] - a).| * |.(([\a/] + 1) - b).|
by COMPLEX1:65
.=
|.(- ([\a/] - a)).| * |.(([\a/] + 1) - b).|
by COMPLEX1:52
.=
|.(a - [\a/]).| * |.(([\a/] + 1) - b).|
;
(b - [\a/]) * (([\a/] + 1) - a) =
|.((b - [\a/]) * (([\a/] + 1) - a)).|
by A8, A9, ABSVALUE:def 1
.=
|.(b - [\a/]).| * |.(([\a/] + 1) - a).|
by COMPLEX1:65
;
then A12:
(|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.(b - [\a/]).| * |.(([\a/] + 1) - a).|) =
|.(b - a).|
by A11
.=
|.(- (b - a)).|
by COMPLEX1:52
.=
|.(a - b).|
;
set r1 =
|.(a - [\a/]).| * |.(([\a/] + 1) - b).|;
set r2 =
|.(b - [\a/]).| * |.(([\a/] + 1) - a).|;
A16:
|.(([\a/] + 1) - a).| =
|.(- (([\a/] + 1) - a)).|
by COMPLEX1:52
.=
|.((a - [\a/]) - 1).|
;
A17:
|.(([\a/] + 1) - b).| =
|.(- (([\a/] + 1) - b)).|
by COMPLEX1:52
.=
|.((b - [\a/]) - 1).|
;
((|.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| =
(|.(a - [\a/]).| * |.(b - [\a/]).|) * (|.((a - [\a/]) - 1).| * |.((b - [\a/]) - 1).|)
.=
(((|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.(b - [\a/]).| * |.(([\a/] + 1) - a).|)) / 2) ^2
by A12, SS
;
then
(|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) * (|.(b - [\a/]).| * |.(([\a/] + 1) - a).|) = (((|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.(b - [\a/]).| * |.(([\a/] + 1) - a).|)) / 2) ^2
by A17, A16;
then A18:
|.(a - [\a/]).| * |.(([\a/] + 1) - b).| = |.(b - [\a/]).| * |.(([\a/] + 1) - a).|
by Th20;
A22:
|.(([\a/] + 1) - b).| - |.(b - [\a/]).| =
((|.(([\a/] + 1) - b).| * |.(a - [\a/]).|) - (|.(b - [\a/]).| * |.(a - [\a/]).|)) / |.(a - [\a/]).|
by A3, XCMPLX_1:129
.=
0
by A12, A18, SS
;
|.(([\a/] + 1) - b).| - |.(b - [\a/]).| =
(- (([\a/] + 1) - b)) - |.(b - [\a/]).|
by A2, XREAL_1:49, ABSVALUE:def 1
.=
(- (([\a/] + 1) - b)) - (b - [\a/])
by A8, ABSVALUE:def 1
.=
- 1
;
hence
contradiction
by A22;
verum end; end;