let a, b be Real; :: thesis: ( |.(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 ) ; :: thesis: ( a is Integer or [\a/] + 1 >= b )
assume A2: ( a is not Integer & [\a/] + 1 < b ) ; :: thesis: 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 A6: ( |.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| > |.(a - b).| / 2 ) ; :: thesis: contradiction
(1 + [\a/]) - [\a/] < b - [\a/] by A2, XREAL_1:14;
then (|.(a - [\a/]).| * |.(b - [\a/]).|) * (|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).|) > (|.(a - b).| / 2) * (|.(a - b).| / 2) by A6, A3, XREAL_1:98;
hence contradiction by A5; :: thesis: verum
end;
suppose A6: ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 ) ; :: thesis: contradiction
a6: a - ([\a/] + 1) < 0 by a3, XREAL_1:49;
b - ([\a/] + 1) > 0 by A2, XREAL_1:50;
then (|.(a - [\a/]).| * |.(b - [\a/]).|) * (|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).|) > (|.(a - b).| / 2) * (|.(a - b).| / 2) by a6, XREAL_1:98, A6;
hence contradiction by A5; :: thesis: verum
end;
suppose ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| > |.(a - b).| / 2 ) ; :: thesis: contradiction
hence contradiction by Th23, A5; :: thesis: verum
end;
suppose SS: ( |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 & |.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 ) ; :: thesis: contradiction
A6: ([\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; :: thesis: verum
end;
end;