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/] <= 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 ) ; :: thesis: ( a is Integer or [\a/] <= b )
assume that
A1: a is not Integer and
A2: [\a/] > b ; :: thesis: 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 ) ; :: thesis: contradiction
A8: b - [\a/] < 0 by A2, XREAL_1:49;
(|.(a - [\a/]).| * |.(b - [\a/]).|) * (|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).|) > (|.(a - b).| / 2) * (|.(a - b).| / 2) by A3, A8, XREAL_1:98, A5;
hence contradiction by a5; :: thesis: verum
end;
suppose A5: ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 ) ; :: thesis: contradiction
A4: ((|.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| <= (|.(a - b).| ^2) / 4 by A1, A2, INT_1:26, Th25, S2;
a6: a - ([\a/] + 1) < 0 by XREAL_1:49, S2;
b - ([\a/] + 1) < 0 by XREAL_1:49, S;
then (|.(a - [\a/]).| * |.(b - [\a/]).|) * (|.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).|) > (|.(a - b).| / 2) * (|.(a - b).| / 2) by A5, a6, XREAL_1:98;
hence contradiction by A4; :: thesis: verum
end;
suppose A5: ( |.(a - [\a/]).| * |.(b - [\a/]).| > |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| > |.(a - b).| / 2 ) ; :: thesis: contradiction
((|.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).| <= (|.(a - b).| ^2) / 4 by A1, A2, S2, INT_1:26, Th25;
hence contradiction by Th23, A5; :: thesis: verum
end;
suppose A5: ( |.(a - [\a/]).| * |.(b - [\a/]).| = |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| = |.(a - b).| / 2 ) ; :: thesis: contradiction
A10: |.(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; :: thesis: verum
end;
end;