let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: ( |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 <> 0 & a1 / b1 is rational implies ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4 )
set Delta = |.((a1 * b2) - (a2 * b1)).|;
assume that
A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and
A2: b1 <> 0 and
A3: a1 / b1 is rational ; :: thesis: ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4
reconsider r1 = a1 / b1 as Rational by A3;
set n1 = numerator r1;
set d1 = denominator r1;
reconsider t0 = b1 / (denominator r1) as non zero Real by A2;
A5: b1 = t0 * (denominator r1) by XCMPLX_1:87;
A6: a1 = (a1 / b1) * b1 by A2, XCMPLX_1:87
.= ((numerator r1) / (denominator r1)) * b1 by RAT_1:15
.= (((numerator r1) / (denominator r1)) * (denominator r1)) * t0 by A5
.= t0 * (numerator r1) by XCMPLX_1:87 ;
reconsider rh0 = c1 / t0 as Element of REAL by XREAL_0:def 1;
A7: c1 = rh0 * t0 by XCMPLX_1:87;
consider x0, y0 being Element of INT such that
A8: |.((((numerator r1) * x0) - ((denominator r1) * y0)) + rh0).| <= 1 / 2 by Th16, WSIERP_1:22;
reconsider x = x0, y = - y0 as Element of INT by INT_1:def 2;
t0 * ((((numerator r1) * x) - ((denominator r1) * y0)) + rh0) = ((a1 * x) + ((t0 * (denominator r1)) * (- y0))) + (rh0 * t0) by A6
.= ((a1 * x) + (b1 * y)) + (rh0 * t0) by XCMPLX_1:87
.= (LF (a1,b1,c1)) . (x,y) by A7, Def4 ;
then A9: |.((LF (a1,b1,c1)) . (x,y)).| = |.t0.| * |.((((numerator r1) * x0) - ((denominator r1) * y0)) + rh0).| by COMPLEX1:65;
reconsider r = - ((t0 * (((a2 * x) + (b2 * y)) + c2)) / ((a2 * b1) - (b2 * a1))) as Element of REAL by XREAL_0:def 1;
consider s being Element of INT such that
A11: |.(r - s).| <= 1 / 2 by GAUSSINT:48;
A12: |.((- ((t0 * (((a2 * x) + (b2 * y)) + c2)) / ((a2 * b1) - (b2 * a1)))) - s).| = |.(- (((t0 * (((a2 * x) + (b2 * y)) + c2)) / ((a2 * b1) - (b2 * a1))) + s)).|
.= |.(((t0 * (((a2 * x) + (b2 * y)) + c2)) / ((a2 * b1) - (b2 * a1))) + s).| by COMPLEX1:52 ;
reconsider x1 = x + ((denominator r1) * s), y1 = y - ((numerator r1) * s) as Element of INT by INT_1:def 2;
(LF (a1,b1,c1)) . (x1,y1) = ((a1 * x1) + (b1 * y1)) + c1 by Def4
.= (((a1 * x) + (b1 * y)) + c1) + (((a1 * (denominator r1)) - (b1 * (numerator r1))) * s)
.= (LF (a1,b1,c1)) . (x,y) by Def4, A6, A5 ;
then A24: |.((LF (a1,b1,c1)) . (x1,y1)).| <= |.t0.| * (1 / 2) by A9, A8, XREAL_1:64;
A14: (LF (a2,b2,c2)) . (x1,y1) = ((a2 * x1) + (b2 * y1)) + c2 by Def4
.= (((a2 * x) + (b2 * y)) + c2) + (((a2 * (denominator r1)) - (b2 * (numerator r1))) * s)
.= (((a2 * x) + (b2 * y)) + c2) + (((a2 * (denominator r1)) - (b2 * (numerator r1))) * ((s * t0) / t0)) by XCMPLX_1:89
.= (((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0)) by A6, A5 ;
(a2 * b1) - (b2 * a1) <> 0 by A1;
then A16: |.(((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)) / ((a2 * b1) - (b2 * a1))).| <= 1 / 2 by A11, A12, XCMPLX_1:113;
|.((a2 * b1) - (b2 * a1)).| = |.(- ((a1 * b2) - (a2 * b1))).|
.= |.((a1 * b2) - (a2 * b1)).| by COMPLEX1:52 ;
then |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| / |.((a1 * b2) - (a2 * b1)).| <= 1 / 2 by COMPLEX1:67, A16;
then (|.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| / |.((a1 * b2) - (a2 * b1)).|) * |.((a1 * b2) - (a2 * b1)).| <= (1 / 2) * |.((a1 * b2) - (a2 * b1)).| by XREAL_1:64;
then A18: |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| <= (1 / 2) * |.((a1 * b2) - (a2 * b1)).| by A1, XCMPLX_1:87;
|.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * ((s * t0) / t0))).| <= (1 / 2) * |.((a1 * b2) - (a2 * b1)).| by A18, XCMPLX_1:89;
then |.(t0 * ((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0)))).| <= (1 / 2) * |.((a1 * b2) - (a2 * b1)).| ;
then A20: |.t0.| * |.((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0))).| <= (1 / 2) * |.((a1 * b2) - (a2 * b1)).| by COMPLEX1:65;
(|.t0.| * |.((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0))).|) / |.t0.| = ((1 / |.t0.|) * |.t0.|) * |.((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0))).|
.= 1 * |.((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0))).| by XCMPLX_1:106 ;
then A23: |.((LF (a2,b2,c2)) . (x1,y1)).| <= ((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) / |.t0.| by A14, A20, XREAL_1:72;
(|.t0.| * (1 / 2)) * (((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) / |.t0.|) = |.t0.| * (((1 / 4) * |.((a1 * b2) - (a2 * b1)).|) / |.t0.|)
.= |.((a1 * b2) - (a2 * b1)).| / 4 by XCMPLX_1:87 ;
then |.((LF (a1,b1,c1)) . (x1,y1)).| * |.((LF (a2,b2,c2)) . (x1,y1)).| <= |.((a1 * b2) - (a2 * b1)).| / 4 by A23, A24, XREAL_1:66;
hence ex x, y being Element of INT st |.((LF (a1,b1,c1)) . (x,y)).| * |.((LF (a2,b2,c2)) . (x,y)).| <= |.((a1 * b2) - (a2 * b1)).| / 4 ; :: thesis: verum