let a1, a2, b1, b2, c1, c2 be Element of REAL ; ( |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 = 0 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
; 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
A4:
b2 <> 0
by A1, A2;
per cases
( ( a2 / b2 is irrational & ZeroPointSet (LF (a2,b2,c2)) = {} ) or ZeroPointSet (LF (a2,b2,c2)) <> {} or ( a2 / b2 is rational & ZeroPointSet (LF (a2,b2,c2)) = {} ) )
;
suppose A5:
(
a2 / b2 is
irrational &
ZeroPointSet (LF (a2,b2,c2)) = {} )
;
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
for
eps being
positive Real 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
proof
let eps be
positive Real;
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
ex
x,
y being
Element of
INT st
(
|.((LF (a2,b2,c2)) . (x,y)).| * |.((LF (a1,b1,c1)) . (x,y)).| < |.((a1 * b2) - (a2 * b1)).| / 4 &
|.((LF (a2,b2,c2)) . (x,y)).| < eps )
by A1, A5, Th47;
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
end; 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