let a1, a2, b1, b2, c1, c2 be Element of REAL ; ( |.((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
; 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
; verum