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/] <= b )
set u = [\a/];
set v = [\a/] + 1;
assume A5:
( |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 )
; ( a is Integer or [\a/] <= b )
assume that
A1:
a is not Integer
and
A2:
[\a/] > b
; contradiction
A3:
a - [\a/] > 0
by A1, INT_1:26, XREAL_1:50;
A4:
a - 1 < [\a/]
by INT_1:def 6;
S:
[\a/] + 1 > b
by A2, XREAL_1:40;
then A6:
([\a/] + 1) - b > 0
by XREAL_1:50;
A8:
[\a/] - b > 0
by A2, XREAL_1:50;
A9:
([\a/] + 1) - a > 0
by A4, XREAL_1:19, XREAL_1:50;
S2:
a < [\a/] + 1
by A4, XREAL_1:19;
then a5:
((|.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| <= (|.(a - b).| ^2) / 4
by A1, A2, INT_1:26, Th25;
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/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 ) )
by A5, XXREAL_0:1;
suppose A5:
(
|.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 &
|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 )
;
contradictionA10:
|.(a - [\a/]).| * |.([\a/] - b).| =
|.(a - [\a/]).| * |.(- ([\a/] - b)).|
by COMPLEX1:52
.=
|.(a - b).| / 2
by A5
;
A11:
|.(a - [\a/]).| * |.([\a/] - b).| =
|.(a - [\a/]).| * |.(- ([\a/] - b)).|
by COMPLEX1:52
.=
|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).|
by A5
;
A13:
(a - [\a/]) * (([\a/] + 1) - b) =
|.((a - [\a/]) * (([\a/] + 1) - b)).|
by A6, A3, ABSVALUE:def 1
.=
|.(a - [\a/]).| * |.(([\a/] + 1) - b).|
by COMPLEX1:65
;
a14:
([\a/] - b) * (([\a/] + 1) - a) =
|.(([\a/] - b) * (([\a/] + 1) - a)).|
by A8, A9, ABSVALUE:def 1
.=
|.([\a/] - b).| * |.(([\a/] + 1) - a).|
by COMPLEX1:65
;
then A14:
(|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.([\a/] - b).| * |.(([\a/] + 1) - a).|) = |.(a - b).|
by A13;
A15:
((|.(a - [\a/]).| * |.([\a/] - b).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| =
(|.(a - [\a/]).| * |.([\a/] - b).|) * (|.((a - [\a/]) - 1).| * |.((b - [\a/]) - 1).|)
.=
(((|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.([\a/] - b).| * |.(([\a/] + 1) - a).|)) / 2) ^2
by A13, a14, A10, A11
;
set r1 =
|.(a - [\a/]).| * |.(([\a/] + 1) - b).|;
set r2 =
|.([\a/] - b).| * |.(([\a/] + 1) - a).|;
A17:
|.(([\a/] + 1) - a).| =
|.(- (([\a/] + 1) - a)).|
by COMPLEX1:52
.=
|.((a - [\a/]) - 1).|
;
A18:
|.(([\a/] + 1) - b).| =
|.(- (([\a/] + 1) - b)).|
by COMPLEX1:52
.=
|.((b - [\a/]) - 1).|
;
(|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) * (|.([\a/] - b).| * |.(([\a/] + 1) - a).|) = (((|.(a - [\a/]).| * |.(([\a/] + 1) - b).|) + (|.([\a/] - b).| * |.(([\a/] + 1) - a).|)) / 2) ^2
by A15, A18, A17;
then A19:
|.(a - [\a/]).| * |.(([\a/] + 1) - b).| = |.([\a/] - b).| * |.(([\a/] + 1) - a).|
by Th20;
A23:
|.(([\a/] + 1) - b).| - |.([\a/] - b).| =
((|.(([\a/] + 1) - b).| * |.(a - [\a/]).|) - (|.([\a/] - b).| * |.(a - [\a/]).|)) / |.(a - [\a/]).|
by A3, XCMPLX_1:129
.=
0
by A10, A14, A19
;
|.(([\a/] + 1) - b).| - |.([\a/] - b).| =
(([\a/] + 1) - b) - |.([\a/] - b).|
by A6, ABSVALUE:def 1
.=
(([\a/] + 1) - b) - ([\a/] - b)
by A8, ABSVALUE:def 1
.=
1
;
hence
contradiction
by A23;
verum end; end;