:: by Yasushige Watase

::

:: Received November 29, 2017

:: Copyright (c) 2017-2021 Association of Mizar Users

theorem Th18: :: DIOPHAN2:1

for r1, r2, r3 being non negative Real holds

( not r1 * r2 <= r3 or r1 <= sqrt r3 or r2 <= sqrt r3 )

( not r1 * r2 <= r3 or r1 <= sqrt r3 or r2 <= sqrt r3 )

proof end;

theorem Th15: :: DIOPHAN2:4

for i1, j1 being Integer st i1,j1 are_coprime holds

ex s, t being Integer st (s * i1) + (t * j1) = 1

ex s, t being Integer st (s * i1) + (t * j1) = 1

proof end;

sqrt 5 > sqrt (2 ^2)

by SQUARE_1:27;

then SQRT2: 2 < sqrt 5

by SQUARE_1:22;

then SQRT3: 1 / (sqrt 5) < 1 / 2

by XREAL_1:76;

theorem Th1: :: DIOPHAN2:5

for s being Real st 1 < s & s + (1 / s) < sqrt 5 holds

( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )

( s < ((sqrt 5) + 1) / 2 & 1 / s > ((sqrt 5) - 1) / 2 )

proof end;

theorem Th8: :: DIOPHAN2:6

for m1 being Nat

for i1 being Integer

for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds

( i1 = numerator q & m1 = denominator q )

for i1 being Integer

for q being Rational st q = i1 / m1 & m1 <> 0 & i1,m1 are_coprime holds

( i1 = numerator q & m1 = denominator q )

proof end;

:: deftheorem defines ZeroPointSet DIOPHAN2:def 1 :

for f being Function holds ZeroPointSet f = (dom f) \ (support f);

for f being Function holds ZeroPointSet f = (dom f) \ (support f);

theorem Th13: :: DIOPHAN2:7

for f being Function

for o1, o2 being object holds

( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )

for o1, o2 being object holds

( o1 in ZeroPointSet f iff ( o1 in dom f & f . o1 = 0 ) )

proof end;

registration

let r be irrational Real;

let n be Nat;

coherence

( (c_d r) . n is positive & (c_d r) . n is natural )

end;
let n be Nat;

coherence

( (c_d r) . n is positive & (c_d r) . n is natural )

proof end;

:: Approximation an irrational by its simple continued fraction

theorem Th3: :: DIOPHAN2:8

for r being irrational Real

for n being Nat st n > 1 & |.(r - (((c_n r) . n) / ((c_d r) . n))).| >= 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) holds

sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n)))

for n being Nat st n > 1 & |.(r - (((c_n r) . n) / ((c_d r) . n))).| >= 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) & |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| >= 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) holds

sqrt 5 > (((c_d r) . (n + 1)) / ((c_d r) . n)) + (1 / (((c_d r) . (n + 1)) / ((c_d r) . n)))

proof end;

theorem Th4: :: DIOPHAN2:9

for n being Nat

for cn, cd being Integer

for r being irrational Real st cn = (c_n r) . n & cd = (c_d r) . n holds

cn,cd are_coprime

for cn, cd being Integer

for r being irrational Real st cn = (c_n r) . n & cd = (c_d r) . n holds

cn,cd are_coprime

proof end;

::Hardy&Wright Th196

theorem Th5: :: DIOPHAN2:10

for n being Nat

for r being irrational Real holds

( not n > 1 or |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) or |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) or |.(r - (((c_n r) . (n + 2)) / ((c_d r) . (n + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 2)) |^ 2)) )

for r being irrational Real holds

( not n > 1 or |.(r - (((c_n r) . n) / ((c_d r) . n))).| < 1 / ((sqrt 5) * (((c_d r) . n) |^ 2)) or |.(r - (((c_n r) . (n + 1)) / ((c_d r) . (n + 1)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 1)) |^ 2)) or |.(r - (((c_n r) . (n + 2)) / ((c_d r) . (n + 2)))).| < 1 / ((sqrt 5) * (((c_d r) . (n + 2)) |^ 2)) )

proof end;

definition

let r be irrational Real;

{ p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } is Subset of RAT

end;
func HWZSet r -> Subset of RAT equals :: DIOPHAN2:def 2

{ p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;

coherence { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;

{ p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } is Subset of RAT

proof end;

:: deftheorem defines HWZSet DIOPHAN2:def 2 :

for r being irrational Real holds HWZSet r = { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;

for r being irrational Real holds HWZSet r = { p where p is Rational : |.(r - p).| < 1 / ((sqrt 5) * ((denominator p) |^ 2)) } ;

definition

let r be irrational Real;

{ x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } is Subset of NAT

end;
func HWZSet1 r -> Subset of NAT equals :: DIOPHAN2:def 3

{ x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } ;

coherence { x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } ;

{ x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } is Subset of NAT

proof end;

:: deftheorem defines HWZSet1 DIOPHAN2:def 3 :

for r being irrational Real holds HWZSet1 r = { x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } ;

for r being irrational Real holds HWZSet1 r = { x where x is Nat : ex p being Rational st

( p in HWZSet r & x = denominator p ) } ;

definition

ex b_{1} being Function of RAT,NAT st

for x being Rational holds b_{1} . x = denominator x

for b_{1}, b_{2} being Function of RAT,NAT st ( for x being Rational holds b_{1} . x = denominator x ) & ( for x being Rational holds b_{2} . x = denominator x ) holds

b_{1} = b_{2}
end;

func TRANQN -> Function of RAT,NAT means :Def3A: :: DIOPHAN2:def 4

for x being Rational holds it . x = denominator x;

existence for x being Rational holds it . x = denominator x;

ex b

for x being Rational holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def3A defines TRANQN DIOPHAN2:def 4 :

for b_{1} being Function of RAT,NAT holds

( b_{1} = TRANQN iff for x being Rational holds b_{1} . x = denominator x );

for b

( b

theorem :: DIOPHAN2:14

for r being irrational Real holds { q where q is Rational : |.(r - q).| < 1 / ((sqrt 5) * ((denominator q) |^ 2)) } is infinite

proof end;

definition

let a0, b0, c0 be Real;

ex b_{1} being Function of [:INT,INT:],REAL st

for x, y being Integer holds b_{1} . (x,y) = ((a0 * x) + (b0 * y)) + c0

for b_{1}, b_{2} being Function of [:INT,INT:],REAL st ( for x, y being Integer holds b_{1} . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) & ( for x, y being Integer holds b_{2} . (x,y) = ((a0 * x) + (b0 * y)) + c0 ) holds

b_{1} = b_{2}

end;
func LF (a0,b0,c0) -> Function of [:INT,INT:],REAL means :Def4: :: DIOPHAN2:def 5

for x, y being Integer holds it . (x,y) = ((a0 * x) + (b0 * y)) + c0;

existence for x, y being Integer holds it . (x,y) = ((a0 * x) + (b0 * y)) + c0;

ex b

for x, y being Integer holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def4 defines LF DIOPHAN2:def 5 :

for a0, b0, c0 being Real

for b_{4} being Function of [:INT,INT:],REAL holds

( b_{4} = LF (a0,b0,c0) iff for x, y being Integer holds b_{4} . (x,y) = ((a0 * x) + (b0 * y)) + c0 );

for a0, b0, c0 being Real

for b

( b

:: lemma 2.1 of chapter 2 p16 of Niven[1]

theorem Th16: :: DIOPHAN2:15

for rh0 being Element of REAL

for p, q being Integer st p,q are_coprime holds

ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

for p, q being Integer st p,q are_coprime holds

ex x, y being Element of INT st |.(((p * x) - (q * y)) + rh0).| <= 1 / 2

proof end;

theorem Th17: :: DIOPHAN2:16

for b being Real

for n being Integer st n <= b & b <= n + 1 holds

|.(n - b).| * |.((n + 1) - b).| <= 1 / 4

for n being Integer st n <= b & b <= n + 1 holds

|.(n - b).| * |.((n + 1) - b).| <= 1 / 4

proof end;

theorem Th21: :: DIOPHAN2:17

for a being Real

for n being Integer st a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) holds

|.(a - n).| < 1

for n being Integer st a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) holds

|.(a - n).| < 1

proof end;

theorem Th22: :: DIOPHAN2:18

for a, b being Real

for n being Integer st |.(n - a).| * |.((n + 1) - a).| <= 1 / 4 & |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 & not |.(n - a).| * |.(n - b).| <= 1 / 4 holds

|.((n + 1) - a).| * |.((n + 1) - b).| <= 1 / 4

for n being Integer st |.(n - a).| * |.((n + 1) - a).| <= 1 / 4 & |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 & not |.(n - a).| * |.(n - b).| <= 1 / 4 holds

|.((n + 1) - a).| * |.((n + 1) - b).| <= 1 / 4

proof end;

theorem Th23: :: DIOPHAN2:19

for a, b being Real

for n being Integer holds

( not ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 or |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 )

for n being Integer holds

( not ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 or |.(a - n).| * |.(b - n).| <= |.(a - b).| / 2 or |.((a - n) - 1).| * |.((b - n) - 1).| <= |.(a - b).| / 2 )

proof end;

theorem Th24: :: DIOPHAN2:20

for a, b being Real

for n being Integer st (n - b) * ((n + 1) - a) > 0 & (a - n) * ((n + 1) - b) > 0 holds

( ((n - b) * ((n + 1) - a)) + ((a - n) * ((n + 1) - b)) = a - b & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )

for n being Integer st (n - b) * ((n + 1) - a) > 0 & (a - n) * ((n + 1) - b) > 0 holds

( ((n - b) * ((n + 1) - a)) + ((a - n) * ((n + 1) - b)) = a - b & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )

proof end;

::b< n< a< n+1 => |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4

theorem Th25: :: DIOPHAN2:21

for a, b being Real

for n being Integer st b < n & n < a & a < n + 1 holds

((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4

for n being Integer st b < n & n < a & a < n + 1 holds

((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4

proof end;

theorem Th26: :: DIOPHAN2:22

for a, b being Real

for n being Integer st (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 holds

( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )

for n being Integer st (n - a) * ((n + 1) - b) > 0 & (b - n) * ((n + 1) - a) > 0 holds

( ((n - a) * ((n + 1) - b)) + ((b - n) * ((n + 1) - a)) = b - a & ((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4 )

proof end;

:: n <a<n+1 <b => |.a-n.|*|.b-n.|*|.a-n-1.|*|.b-n-1.|<=|.a-b.|^2/4

theorem Th27: :: DIOPHAN2:23

for a, b being Real

for n being Integer st n + 1 < b & n < a & a < n + 1 holds

((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4

for n being Integer st n + 1 < b & n < a & a < n + 1 holds

((|.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).| <= (|.(a - b).| ^2) / 4

proof end;

theorem Th28: :: DIOPHAN2:24

for a, b being Real st a is not Integer & [\a/] <= b & b <= [\a/] + 1 holds

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| <= 1 / 4 )

proof end;

theorem Th32: :: DIOPHAN2:25

for a, b being Real st |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 & a is not Integer holds

[\a/] <= b

[\a/] <= b

proof end;

theorem Th33: :: DIOPHAN2:26

for a, b being Real st a is not Integer & [\a/] > b holds

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )

proof end;

theorem Th37: :: DIOPHAN2:27

for a, b being Real st |.(a - [\a/]).| * |.(b - [\a/]).| >= |.(a - b).| / 2 & |.(a - ([\a/] + 1)).| * |.(b - ([\a/] + 1)).| >= |.(a - b).| / 2 & a is not Integer holds

[\a/] + 1 >= b

[\a/] + 1 >= b

proof end;

theorem Th39: :: DIOPHAN2:28

for a, b being Real st a is not Integer & [\a/] + 1 < b holds

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )

ex u being Integer st

( |.(a - u).| < 1 & |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 )

proof end;

:: lemma 2.2 of chapter 2 p16 of Niven

theorem Th41: :: DIOPHAN2:29

for a, b being Real ex u being Integer st

( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

( |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).| <= 1 / 4 or |.(a - u).| * |.(b - u).| < |.(a - b).| / 2 ) )

proof end;

theorem Th42: :: DIOPHAN2:30

for r being irrational Real

for r1 being non negative Real ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r )

for r1 being non negative Real ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r )

proof end;

theorem Th43: :: DIOPHAN2:31

for a1, a2, b1, b2 being Element of REAL

for q, q1 being Element of RAT st |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 holds

(a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0

for q, q1 being Element of RAT st |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & (a2 * (denominator q)) + (b2 * (numerator q)) = 0 holds

(a2 * (denominator q1)) + (b2 * (numerator q1)) <> 0

proof end;

theorem Th44: :: DIOPHAN2:32

for r being irrational Real

for a1, a2, b1, b2 being Element of REAL

for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

for a1, a2, b1, b2 being Element of REAL

for r1 being non negative Real st |.((a1 * b2) - (a2 * b1)).| <> 0 holds

ex q being Element of RAT st

( denominator q > [\r1/] + 1 & q in HWZSet r & (a2 * (denominator q)) + (b2 * (numerator q)) <> 0 )

proof end;

theorem Th45: :: DIOPHAN2:33

for a1, b1 being Real

for n1, d1 being Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) holds

ex d being Real st

( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )

for n1, d1 being Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < 1 / ((sqrt 5) * (d1 |^ 2)) holds

ex d being Real st

( n1 / d1 = (- (a1 / b1)) + (d / (d1 |^ 2)) & |.d.| < 1 / (sqrt 5) )

proof end;

:: Theorem 2.3 of chapter 2 p18 of Niven[1]

theorem Th46: :: DIOPHAN2:34

for a1, a2, b1, b2, c1, c2 being 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 )

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 )

proof end;

theorem Th47: :: DIOPHAN2:35

for a1, a2, b1, b2, c1, c2 being Element of REAL

for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational holds

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 )

for eps being positive Real st |.((a1 * b2) - (a2 * b1)).| <> 0 & a2 / b2 is irrational holds

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 )

proof end;

theorem Th48: :: DIOPHAN2:36

for a1, a2, b1, b2, c1, c2 being Element of REAL st ZeroPointSet (LF (a1,b1,c1)) <> {} 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

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 end;

theorem Th49: :: DIOPHAN2:37

for a1, a2, b1, b2, c1, c2 being Element of REAL st ZeroPointSet (LF (a2,b2,c2)) <> {} 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

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 end;

theorem Th50: :: DIOPHAN2:38

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 <> 0 & a1 / b1 is rational 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

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 end;

theorem Th51: :: DIOPHAN2:39

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & a2 / b2 is rational 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

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 end;

theorem Th52: :: DIOPHAN2:40

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 = 0 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

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 end;

::Hardy&Wright Th455

theorem :: DIOPHAN2:41

for a1, a2, b1, b2, c1, c2 being Element of REAL st |.((a1 * b2) - (a2 * b1)).| <> 0 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

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 end;