let a1, a2, b1, b2, c1, c2 be Element of REAL ; for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a1 / b1 is irrational holds
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 & |.((LF (a1,b1,c1)) . (x,y)).| < eps )
let eps be positive Real; ( |.((a1 * b2) - (a2 * b1)).| <> 0 & a1 / b1 is irrational 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 & |.((LF (a1,b1,c1)) . (x,y)).| < eps ) )
set Delta = |.((a1 * b2) - (a2 * b1)).|;
assume that
A1:
|.((a1 * b2) - (a2 * b1)).| <> 0
and
A2:
a1 / b1 is irrational
; 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 & |.((LF (a1,b1,c1)) . (x,y)).| < eps )
reconsider t = - (a1 / b1) as Element of IRRAT by A2, BORSUK_5:17;
A4:
(a2 * b1) - (a1 * b2) <> 0
by A1;
reconsider r1 = max ((|.b1.| / ((sqrt 5) * eps)),(|.(b1 * b2).| / |.((a1 * b2) - (a2 * b1)).|)) as non negative Real by SQRT2, XXREAL_0:def 10;
consider q1 being Element of RAT such that
A7:
( denominator q1 > [\r1/] + 1 & q1 in HWZSet t & (a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0 )
by A1, Th44;
set n1 = numerator q1;
set d1 = denominator q1;
A8:
denominator q1 > r1
by A7, INT_1:29, XXREAL_0:2;
|.b1.| / ((sqrt 5) * eps) <= r1
by XXREAL_0:25;
then
|.b1.| / ((sqrt 5) * eps) < 1 * (denominator q1)
by A8, XXREAL_0:2;
then
|.b1.| / (denominator q1) < 1 * ((sqrt 5) * eps)
by SQRT2, XREAL_1:113;
then
(|.b1.| / (denominator q1)) * 1 < eps * (sqrt 5)
;
then
(|.b1.| / (denominator q1)) / (sqrt 5) < eps / 1
by SQRT2, XREAL_1:106;
then A11:
|.b1.| / ((denominator q1) * (sqrt 5)) < eps
by XCMPLX_1:78;
|.(b1 * b2).| / |.((a1 * b2) - (a2 * b1)).| <= r1
by XXREAL_0:25;
then
|.(b1 * b2).| / |.((a1 * b2) - (a2 * b1)).| < 1 * (denominator q1)
by A8, XXREAL_0:2;
then A13:
|.(b1 * b2).| / (denominator q1) < 1 * |.((a1 * b2) - (a2 * b1)).|
by XREAL_1:113, A1;
(denominator q1) + 0 >= 1
by NAT_1:19;
then
1 / (denominator q1) <= 1
by XREAL_1:183;
then A16:
(|.(b1 * b2).| / (denominator q1)) * (1 / (denominator q1)) <= |.(b1 * b2).| / (denominator q1)
by XREAL_1:153;
(|.(b1 * b2).| / (denominator q1)) * (1 / (denominator q1)) =
(|.(b1 * b2).| * 1) / ((denominator q1) * (denominator q1))
by XCMPLX_1:76
.=
|.(b1 * b2).| / ((denominator q1) |^ 2)
by WSIERP_1:1
;
then A17:
|.(b1 * b2).| / ((denominator q1) |^ 2) < |.((a1 * b2) - (a2 * b1)).|
by A13, A16, XXREAL_0:2;
reconsider rh0 = (((denominator q1) * ((c1 * a2) - (c2 * a1))) + ((numerator q1) * ((c1 * b2) - (c2 * b1)))) / ((a2 * b1) - (a1 * b2)) as Element of REAL by XREAL_0:def 1;
denominator q1, numerator q1 are_coprime
by WSIERP_1:22;
then consider s, r being Element of INT such that
A19:
|.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).| <= 1 / 2
by Th16;
set h = numerator q1;
set k = denominator q1;
set a = (((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)));
set b = (((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)));
consider u being Integer such that
A20:
( |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - u).| < 1 & ( |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - u).| * |.(((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - u).| <= 1 / 4 or |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - u).| * |.(((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - u).| < |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1))))).| / 2 ) )
by Th41;
set x = r - (u * (denominator q1));
set y = s - (u * (numerator q1));
t in IRRAT
by SUBSET_1:def 1;
then A22:
b1 <> 0
;
A23:
(a1 * (denominator q1)) + (b1 * (numerator q1)) <> 0
A26: ((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - u =
(((((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) + ((u * ((a1 * (denominator q1)) + (b1 * (numerator q1)))) / ((a1 * (denominator q1)) + (b1 * (numerator q1))))) - u
.=
(((((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) + (u * 1)) - u
by A23, XCMPLX_1:89
.=
(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))
;
then A27:
|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| / |.((a1 * (denominator q1)) + (b1 * (numerator q1))).| < 1
by A20, COMPLEX1:67;
(|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| / |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|) * |.((a1 * (denominator q1)) + (b1 * (numerator q1))).| =
(|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * (1 / |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|)) * |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|
.=
|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).|
by A23, XCMPLX_1:109
;
then A30:
|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| < 1 * |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|
by XREAL_1:68, A27, A23;
consider q being Rational such that
A32:
q1 = q
and
A33:
|.(t - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2))
by A7;
|.(t - q).| =
|.(- ((a1 / b1) + q1)).|
by A32
.=
|.((a1 / b1) + q1).|
by COMPLEX1:52
.=
|.((a1 / b1) + ((numerator q1) / (denominator q1))).|
by RAT_1:15
.=
|.(((a1 * (denominator q1)) + ((numerator q1) * b1)) / (b1 * (denominator q1))).|
by A22, XCMPLX_1:116
.=
|.((a1 * (denominator q1)) + ((numerator q1) * b1)).| / |.(b1 * (denominator q1)).|
by COMPLEX1:67
;
then A36:
|.((a1 * (denominator q1)) + ((numerator q1) * b1)).| / 1 < (1 / ((sqrt 5) * ((denominator q1) |^ 2))) * |.(b1 * (denominator q1)).|
by A32, A33, A22, XREAL_1:113;
set S1 = 1 / (sqrt 5);
A37: 1 / ((sqrt 5) * ((denominator q1) |^ 2)) =
(1 / (sqrt 5)) * (1 / ((denominator q1) |^ 2))
by XCMPLX_1:102
.=
(1 / (sqrt 5)) * (1 / ((denominator q1) * (denominator q1)))
by WSIERP_1:1
.=
(1 / (sqrt 5)) * ((1 / (denominator q1)) * (1 / (denominator q1)))
by XCMPLX_1:102
.=
((1 / (sqrt 5)) * (1 / (denominator q1))) * (1 / (denominator q1))
;
|.(b1 * (denominator q1)).| =
|.(denominator q1).| * |.b1.|
by COMPLEX1:65
.=
(denominator q1) * |.b1.|
;
then A39: (1 / ((sqrt 5) * ((denominator q1) |^ 2))) * |.(b1 * (denominator q1)).| =
(((1 / (sqrt 5)) * (1 / (denominator q1))) * ((1 / (denominator q1)) * (denominator q1))) * |.b1.|
by A37
.=
(((1 / (sqrt 5)) * (1 / (denominator q1))) * 1) * |.b1.|
by XCMPLX_1:106
.=
(1 / ((sqrt 5) * (denominator q1))) * |.b1.|
by XCMPLX_1:102
.=
|.b1.| / ((denominator q1) * (sqrt 5))
;
then A40:
|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| < eps
by A36, A11, XXREAL_0:2;
A41: ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - u =
(((((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) + ((u * ((a2 * (denominator q1)) + (b2 * (numerator q1)))) / ((a2 * (denominator q1)) + (b2 * (numerator q1))))) - u
.=
(((((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) + (u * 1)) - u
by A7, XCMPLX_1:89
.=
(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))
;
set u1 = ((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1;
set u2 = ((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2;
set v1 = (a1 * (denominator q1)) + (b1 * (numerator q1));
set v2 = (a2 * (denominator q1)) + (b2 * (numerator q1));
A42: |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - u).| * |.(((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - u).| =
(|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| / |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|) * |.((((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))).|
by COMPLEX1:67, A41, A26
.=
(|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| / |.((a1 * (denominator q1)) + (b1 * (numerator q1))).|) * (|.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).| / |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)
by COMPLEX1:67
.=
(|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).|) / (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)
by XCMPLX_1:76
;
A43: |.(t - q).| =
|.(- ((a1 / b1) + q1)).|
by A32
.=
|.((a1 / b1) + q1).|
by COMPLEX1:52
.=
|.((a1 / b1) + ((numerator q1) / (denominator q1))).|
by RAT_1:15
;
consider d being Real such that
A44:
(numerator q1) / (denominator q1) = (- (a1 / b1)) + (d / ((denominator q1) |^ 2))
and
A45:
|.d.| < 1 / (sqrt 5)
by A33, A32, A43, Th45;
b1 / b1 = 1
by A22, XCMPLX_1:60;
then A51: |.(a2 + (b2 * (- (a1 / b1)))).| =
|.((a2 * (b1 / b1)) - ((b2 * a1) * (1 / b1))).|
.=
|.(- (((a1 * b2) - (a2 * b1)) / b1)).|
.=
|.(((a1 * b2) - (a2 * b1)) / b1).|
by COMPLEX1:52
.=
|.((a1 * b2) - (a2 * b1)).| / |.b1.|
by COMPLEX1:67
;
A52: (|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).| =
(|.b1.| * (1 / ((denominator q1) * (sqrt 5)))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|
.=
(|.b1.| * ((1 / (denominator q1)) * (1 / (sqrt 5)))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|
by XCMPLX_1:102
.=
(|.b1.| * (1 / (sqrt 5))) * (|.(1 / (denominator q1)).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)
.=
(|.b1.| * (1 / (sqrt 5))) * |.((1 / (denominator q1)) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))).|
by COMPLEX1:65
.=
(|.b1.| * (1 / (sqrt 5))) * |.(((a2 * (denominator q1)) * (1 / (denominator q1))) + ((b2 * (numerator q1)) * (1 / (denominator q1)))).|
.=
(|.b1.| * (1 / (sqrt 5))) * |.(a2 + (b2 * ((numerator q1) / (denominator q1)))).|
by XCMPLX_1:107
.=
(|.b1.| * (1 / (sqrt 5))) * |.((a2 + (b2 * (- (a1 / b1)))) + (b2 * (d / ((denominator q1) |^ 2)))).|
by A44
;
A54: ((|.b1.| * (1 / (sqrt 5))) * |.((a1 * b2) - (a2 * b1)).|) / |.b1.| =
((|.b1.| * (1 / |.b1.|)) * (1 / (sqrt 5))) * |.((a1 * b2) - (a2 * b1)).|
.=
|.((a1 * b2) - (a2 * b1)).| / (sqrt 5)
by A22, XCMPLX_1:106
;
A55: (|.b1.| * (1 / (sqrt 5))) * |.(b2 * (d / ((denominator q1) |^ 2))).| =
(1 / (sqrt 5)) * (|.b1.| * |.(b2 * (d / ((denominator q1) |^ 2))).|)
.=
(1 / (sqrt 5)) * |.(b1 * (b2 * (d / ((denominator q1) |^ 2)))).|
by COMPLEX1:65
.=
(1 / (sqrt 5)) * |.(d * ((b1 * b2) / ((denominator q1) |^ 2))).|
.=
(1 / (sqrt 5)) * (|.d.| * |.((b1 * b2) / ((denominator q1) |^ 2)).|)
by COMPLEX1:65
.=
(1 / (sqrt 5)) * (|.d.| * (|.(b1 * b2).| / |.((denominator q1) |^ 2).|))
by COMPLEX1:67
.=
((1 / (sqrt 5)) * |.d.|) * (|.(b1 * b2).| / ((denominator q1) |^ 2))
;
A49:
|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).| <= (|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|
by A36, A39, XREAL_1:64;
A57:
(|.b1.| * (1 / (sqrt 5))) * |.(b2 * (d / ((denominator q1) |^ 2))).| <= |.((a1 * b2) - (a2 * b1)).| * ((1 / (sqrt 5)) * |.d.|)
by A55, A17, SQRT2, XREAL_1:64;
(|.b1.| * (1 / (sqrt 5))) * ((|.((a1 * b2) - (a2 * b1)).| / |.b1.|) + |.(b2 * (d / ((denominator q1) |^ 2))).|) = (|.((a1 * b2) - (a2 * b1)).| / (sqrt 5)) + ((|.b1.| * (1 / (sqrt 5))) * |.(b2 * (d / ((denominator q1) |^ 2))).|)
by A54;
then A59:
(|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).| <= (|.((a1 * b2) - (a2 * b1)).| / (sqrt 5)) + ((|.b1.| * (1 / (sqrt 5))) * |.(b2 * (d / ((denominator q1) |^ 2))).|)
by A52, SQRT2, A51, COMPLEX1:56, XREAL_1:64;
A60:
(|.((a1 * b2) - (a2 * b1)).| / (sqrt 5)) + ((|.b1.| * (1 / (sqrt 5))) * |.(b2 * (d / ((denominator q1) |^ 2))).|) <= (|.((a1 * b2) - (a2 * b1)).| / (sqrt 5)) + (|.((a1 * b2) - (a2 * b1)).| * ((1 / (sqrt 5)) * |.d.|))
by XREAL_1:6, A57;
A61:
(|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).| <= |.((a1 * b2) - (a2 * b1)).| * ((1 / (sqrt 5)) + ((1 / (sqrt 5)) * |.d.|))
by A59, A60, XXREAL_0:2;
(1 / (sqrt 5)) * (1 / (sqrt 5)) =
1 / ((sqrt 5) ^2)
by XCMPLX_1:102
.=
1 / 5
by SQUARE_1:def 2
;
then
(1 / (sqrt 5)) * |.d.| < 1 / 5
by A45, XREAL_1:68;
then
(1 / (sqrt 5)) + ((1 / (sqrt 5)) * |.d.|) < (1 / 5) + (1 / 2)
by SQRT3, XREAL_1:8;
then
(1 / (sqrt 5)) + ((1 / (sqrt 5)) * |.d.|) < 1
by XXREAL_0:2;
then
((1 / (sqrt 5)) + ((1 / (sqrt 5)) * |.d.|)) * |.((a1 * b2) - (a2 * b1)).| < 1 * |.((a1 * b2) - (a2 * b1)).|
by A1, XREAL_1:68;
then A66:
(|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).| < |.((a1 * b2) - (a2 * b1)).|
by A61, XXREAL_0:2;
A71:
((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1)))) = (((((a1 * r) + (b1 * s)) + c1) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) * ((a1 * (denominator q1)) + (b1 * (numerator q1))))) / (((a1 * (denominator q1)) + (b1 * (numerator q1))) * ((a2 * (denominator q1)) + (b2 * (numerator q1))))
by XCMPLX_1:130, A7, A23;
((((a1 * r) + (b1 * s)) + c1) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) * ((a1 * (denominator q1)) + (b1 * (numerator q1)))) =
(((a1 * b2) - (a2 * b1)) * ((r * (numerator q1)) - (s * (denominator q1)))) + ((((denominator q1) * ((c1 * a2) - (c2 * a1))) + ((numerator q1) * ((c1 * b2) - (c2 * b1)))) * 1)
.=
(((a1 * b2) - (a2 * b1)) * ((r * (numerator q1)) - (s * (denominator q1)))) + ((((denominator q1) * ((c1 * a2) - (c2 * a1))) + ((numerator q1) * ((c1 * b2) - (c2 * b1)))) * ((1 / ((a2 * b1) - (a1 * b2))) * ((a2 * b1) - (a1 * b2))))
by A4, XCMPLX_1:106
.=
((a2 * b1) - (a1 * b2)) * ((((denominator q1) * s) - ((numerator q1) * r)) + rh0)
;
then |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1))))).| =
|.(- (((a1 * b2) - (a2 * b1)) * ((((denominator q1) * s) - ((numerator q1) * r)) + rh0))).| / |.(((a1 * (denominator q1)) + (b1 * (numerator q1))) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))).|
by COMPLEX1:67, A71
.=
|.(((a1 * b2) - (a2 * b1)) * ((((denominator q1) * s) - ((numerator q1) * r)) + rh0)).| / |.(((a1 * (denominator q1)) + (b1 * (numerator q1))) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))).|
by COMPLEX1:52
.=
(|.((a1 * b2) - (a2 * b1)).| * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).|) / |.(((a1 * (denominator q1)) + (b1 * (numerator q1))) * ((a2 * (denominator q1)) + (b2 * (numerator q1)))).|
by COMPLEX1:65
.=
(|.((a1 * b2) - (a2 * b1)).| * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).|) / (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)
by COMPLEX1:65
;
then A73: ((1 / 2) * |.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1))))).|) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) =
((((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).|) / (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|)
.=
((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).|
by XCMPLX_1:87, A23, A7
;
A75:
((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).| <= ((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) * (1 / 2)
by A19, XREAL_1:64;
A46:
|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).| < |.((a1 * b2) - (a2 * b1)).| / 4
I:
( r - (u * (denominator q1)) in INT & s - (u * (numerator q1)) in INT )
by INT_1:def 2;
A77:
( (LF (a1,b1,c1)) . ((r - (u * (denominator q1))),(s - (u * (numerator q1)))) = ((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1 & (LF (a2,b2,c2)) . ((r - (u * (denominator q1))),(s - (u * (numerator q1)))) = ((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2 )
by Def4;
|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| < eps
by A30, A40, XXREAL_0:2;
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 & |.((LF (a1,b1,c1)) . (x,y)).| < eps )
by I, A77, A46; verum