let a1, a2, b1, b2, c1, c2 be Element of REAL ; :: thesis: 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; :: thesis: ( |.((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 ; :: 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 & |.((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
proof
assume (a1 * (denominator q1)) + (b1 * (numerator q1)) = 0 ; :: thesis: contradiction
then (- (numerator q1)) * b1 = a1 * (denominator q1) ;
then (- (numerator q1)) / (denominator q1) = a1 / b1 by A22, XCMPLX_1:94;
hence contradiction by A2; :: thesis: verum
end;
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
proof
per cases ( |.(((((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 A20;
suppose |.(((((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 ; :: thesis: |.(((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
then ((|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).|) * (1 / (|.((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 / 4) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) by A42, XREAL_1:64;
then A48: |.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).| <= (1 / 4) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) by XCMPLX_1:109, A23, A7;
(|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) * (1 / 4) <= ((|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) * (1 / 4) by XREAL_1:64, A49;
then A67: |.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).| <= ((|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) * (1 / 4) by A48, XXREAL_0:2;
((|.b1.| / ((denominator q1) * (sqrt 5))) * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) * (1 / 4) < |.((a1 * b2) - (a2 * b1)).| * (1 / 4) by XREAL_1:68, A66;
hence |.(((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 by A67, XXREAL_0:2; :: thesis: verum
end;
suppose |.(((((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 ; :: thesis: |.(((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
then ((|.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).|) * (1 / (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|))) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) < (|.(((((a1 * r) + (b1 * s)) + c1) / ((a1 * (denominator q1)) + (b1 * (numerator q1)))) - ((((a2 * r) + (b2 * s)) + c2) / ((a2 * (denominator q1)) + (b2 * (numerator q1))))).| / 2) * (|.((a1 * (denominator q1)) + (b1 * (numerator q1))).| * |.((a2 * (denominator q1)) + (b2 * (numerator q1))).|) by A23, A7, A42, XREAL_1:68;
then |.(((a1 * (r - (u * (denominator q1)))) + (b1 * (s - (u * (numerator q1))))) + c1).| * |.(((a2 * (r - (u * (denominator q1)))) + (b2 * (s - (u * (numerator q1))))) + c2).| < ((1 / 2) * |.((a1 * b2) - (a2 * b1)).|) * |.((((denominator q1) * s) - ((numerator q1) * r)) + rh0).| by XCMPLX_1:109, A23, A7, A73;
hence |.(((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 by A75, XXREAL_0:2; :: thesis: verum
end;
end;
end;
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; :: thesis: verum