diophan2.miz



    begin

    reserve r1,r2,r3 for non negative Real;

    reserve n,m1 for Nat;

    reserve s for Real;

    reserve cn,cd,i1,j1 for Integer;

    reserve r for irrational Real;

    reserve q for Rational;

    theorem :: DIOPHAN2:1

    

     Th18: (r1 * r2) <= r3 implies r1 <= ( sqrt r3) or r2 <= ( sqrt r3)

    proof

      assume that

       A1: (r1 * r2) <= r3 and

       A2: not (r1 <= ( sqrt r3) or r2 <= ( sqrt r3));

      ( sqrt r3) >= 0 by SQUARE_1:def 2;

      then (( sqrt r3) ^2 ) < (r1 * r2) by A2, XREAL_1: 96;

      hence contradiction by A1, SQUARE_1:def 2;

    end;

    theorem :: DIOPHAN2:2

    

     Th19: ( sqrt (r1 * r2)) = ((r1 + r2) / 2) iff r1 = r2

    proof

      hereby

        assume

         A1: ( sqrt (r1 * r2)) = ((r1 + r2) / 2);

        

         A2: ((( sqrt (r1 * r2)) * 2) ^2 ) = ((( sqrt (r1 * r2)) ^2 ) * (2 ^2 ))

        .= ((r1 * r2) * 4) by SQUARE_1:def 2

        .= ((4 * r1) * r2);

         0 = (((r1 + r2) ^2 ) - ((( sqrt (r1 * r2)) * 2) ^2 )) by A1

        .= ((r1 - r2) ^2 ) by A2;

        then (r1 - r2) = 0 ;

        hence r1 = r2;

      end;

      assume

       A3: r1 = r2;

      

      then ( sqrt (r1 * r2)) = (( sqrt r1) ^2 ) by SQUARE_1: 29

      .= ((r1 + r2) / 2) by A3, SQUARE_1:def 2;

      hence ( sqrt (r1 * r2)) = ((r1 + r2) / 2);

    end;

    theorem :: DIOPHAN2:3

    

     Th20: (r1 * r2) = (((r1 + r2) / 2) ^2 ) iff r1 = r2

    proof

      hereby

        assume (r1 * r2) = (((r1 + r2) / 2) ^2 );

        then ( sqrt (r1 * r2)) = ((r1 + r2) / 2) by SQUARE_1: 22;

        hence r1 = r2 by Th19;

      end;

      thus thesis;

    end;

    theorem :: DIOPHAN2:4

    

     Th15: for i1, j1 st (i1,j1) are_coprime holds ex s,t be Integer st ((s * i1) + (t * j1)) = 1

    proof

      let i1, j1;

      assume

       A1: (i1,j1) are_coprime ;

      then

       B1: (j1 gcd i1) = 1 by INT_2:def 3;

      per cases ;

        suppose i1 >= 0 & j1 >= 0 ;

        then i1 in NAT & j1 in NAT by INT_1: 3;

        hence thesis by A1, EULER_1: 10;

      end;

        suppose

         A3: i1 >= 0 & j1 < 0 ;

        set j2 = ( - j1);

        i1 in NAT & j2 in NAT by A3, INT_1: 3;

        then

        reconsider i1, j2 as Nat;

        (i1 gcd j2) = ( |.i1.| gcd |.( - j1).|)

        .= (i1 gcd |.j1.|) by COMPLEX1: 52

        .= 1 by B1, INT_6: 14;

        then

        consider s,t be Integer such that

         A5: ((s * i1) + (t * j2)) = 1 by EULER_1: 10, INT_2:def 3;

        ((s * i1) + (( - t) * j1)) = 1 by A5;

        hence thesis;

      end;

        suppose

         A6: i1 < 0 & j1 >= 0 ;

        set i2 = ( - i1);

        i2 in NAT & j1 in NAT by A6, INT_1: 3;

        then

        reconsider i2, j1 as Nat;

        (i2 gcd j1) = ( |.( - i1).| gcd |.j1.|)

        .= ( |.i1.| gcd j1) by COMPLEX1: 52

        .= 1 by B1, INT_6: 14;

        then

        consider s,t be Integer such that

         A8: ((s * i2) + (t * j1)) = 1 by EULER_1: 10, INT_2:def 3;

        ((( - s) * i1) + (t * j1)) = 1 by A8;

        hence thesis;

      end;

        suppose

         A9: i1 < 0 & j1 < 0 ;

        set i2 = ( - i1), j2 = ( - j1);

        i2 in NAT & j2 in NAT by A9, INT_1: 3;

        then

        reconsider i2, j2 as Nat;

        (i2 gcd j2) = ( |.( - i1).| gcd |.( - j1).|)

        .= ( |.i1.| gcd |.( - j1).|) by COMPLEX1: 52

        .= ( |.i1.| gcd |.j1.|) by COMPLEX1: 52

        .= ( |.i1.| gcd j1) by INT_6: 14

        .= 1 by B1, INT_6: 14;

        then

        consider s,t be Integer such that

         A11: ((s * i2) + (t * j2)) = 1 by EULER_1: 10, INT_2:def 3;

        ((( - s) * i1) + (( - t) * j1)) = 1 by A11;

        hence thesis;

      end;

    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 :: DIOPHAN2:5

    

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

    proof

      assume that

       A1: 1 < s and

       A2: (s + (1 / s)) < ( sqrt 5);

      

       A4: (( - (1 * ( sqrt 5))) ^2 ) = ((( - 1) ^2 ) * (( sqrt 5) ^2 ))

      .= 5 by SQUARE_1:def 2;

      (s * (s + (1 / s))) < (s * ( sqrt 5)) by A1, A2, XREAL_1: 68;

      then ((s * s) + ((s * 1) / s)) < (s * ( sqrt 5));

      then ((s * s) + 1) < (s * ( sqrt 5)) by A1, XCMPLX_0:def 7;

      then

       A5: (((s * s) + 1) - (s * ( sqrt 5))) < ((s * ( sqrt 5)) - (s * ( sqrt 5))) by XREAL_1: 14;

      set a = 1, b = ( - ( sqrt 5)), c = 1;

      

       A7: (((a * (s ^2 )) + (b * s)) + c) < 0 by A5;

      

       A6: ( delta (1,( - ( sqrt 5)),1)) = ((( - ( sqrt 5)) ^2 ) - ((4 * 1) * 1)) by QUIN_1:def 1

      .= 1 by A4;

      then ((( - b) + ( sqrt ( delta (a,b,c)))) / (2 * a)) = ((( sqrt 5) + 1) / 2) by SQUARE_1: 18;

      then

       A8: s < ((( sqrt 5) + 1) / 2) by A7, A6, QUIN_1: 26;

      (( sqrt 5) - 1) <> 0 by SQRT2;

      then

       A9: ((( sqrt 5) - 1) / (( sqrt 5) - 1)) = 1 by XCMPLX_1: 60;

      (1 / ((( sqrt 5) + 1) / 2)) = ((2 / (( sqrt 5) + 1)) * ((( sqrt 5) - 1) / (( sqrt 5) - 1))) by A9, XCMPLX_1: 57

      .= ((2 * (( sqrt 5) - 1)) / ((( sqrt 5) + 1) * (( sqrt 5) - 1))) by XCMPLX_1: 76

      .= ((2 * (( sqrt 5) - 1)) / ((( sqrt 5) ^2 ) - 1))

      .= ((2 * (( sqrt 5) - 1)) / (5 - 1)) by SQUARE_1:def 2

      .= ((( sqrt 5) - 1) / 2);

      hence thesis by A1, A8, XREAL_1: 88;

    end;

    theorem :: DIOPHAN2:6

    

     Th8: q = (i1 / m1) & m1 <> 0 & (i1,m1) are_coprime implies i1 = ( numerator q) & m1 = ( denominator q)

    proof

      assume that

       A1: q = (i1 / m1) and

       A2: m1 <> 0 and

       A3: (i1,m1) are_coprime ;

      

       A4: (i1 gcd m1) = 1 by A3, INT_2:def 3;

      ex m be Nat st i1 = (( numerator q) * m) & m1 = (( denominator q) * m) by A1, A2, RAT_1: 27;

      then

      consider m be Nat such that

       A5: i1 = (m * ( numerator q)) and

       A6: m1 = (m * ( denominator q));

      

       A7: m divides i1 by A5;

      

       A8: m divides m1 by A6;

      m divides 1 by A4, A7, A8, INT_2:def 2;

      then m = 1 by WSIERP_1: 15;

      hence thesis by A6, A5;

    end;

    definition

      let f be Function;

      :: DIOPHAN2:def1

      func ZeroPointSet f -> set equals (( dom f) \ ( support f));

      correctness ;

    end

    theorem :: DIOPHAN2:7

    

     Th13: for f be Function, o1,o2 be object holds o1 in ( ZeroPointSet f) iff o1 in ( dom f) & (f . o1) = 0

    proof

      let f be Function, o1,o2 be object;

      hereby

        assume

         A1: o1 in ( ZeroPointSet f);

        then not o1 in ( support f) by XBOOLE_0:def 5;

        hence o1 in ( dom f) & (f . o1) = 0 by PRE_POLY:def 7, A1;

      end;

      assume that

       A1: o1 in ( dom f) and

       A2: (f . o1) = 0 ;

       not o1 in ( support f) by A2, PRE_POLY:def 7;

      hence thesis by A1, XBOOLE_0:def 5;

    end;

    begin

    registration

      let r be irrational Real;

      let n be Nat;

      cluster (( c_d r) . n) -> positive natural;

      coherence

      proof

        (( c_d r) . n) >= 1 & (( c_d r) . n) in NAT by DIOPHAN1: 7, REAL_3: 50;

        hence thesis;

      end;

    end

    theorem :: DIOPHAN2:8

    

     Th3: for r, n 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

      let r, n;

      set s5 = ( sqrt 5);

      assume that

       A2: n > 1 and

       A3: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| >= (1 / (( sqrt 5) * ((( c_d r) . n) |^ 2))) and

       A4: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| >= (1 / (( sqrt 5) * ((( c_d r) . (n + 1)) |^ 2)));

      ( |.(r - ((( c_n r) . n) / (( c_d r) . n))).| + |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).|) = |.(((( c_n r) . n) / (( c_d r) . n)) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| by A2, DIOPHAN1: 17;

      then

       A6: |.(((( c_n r) . n) / (( c_d r) . n)) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| >= ((1 / (s5 * ((( c_d r) . n) |^ 2))) + (1 / (s5 * ((( c_d r) . (n + 1)) |^ 2)))) by A3, A4, XREAL_1: 7;

      

       A7: for n holds (( c_d r) . n) <> 0 ;

      

       A8: |.(((( c_n r) . n) / (( c_d r) . n)) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| = |.(((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((( c_n r) . n) / (( c_d r) . n))).| by COMPLEX1: 60;

      (1 / |.((( c_d r) . (n + 1)) * (( c_d r) . n)).|) = (1 * (((( c_d r) . (n + 1)) * (( c_d r) . n)) " ));

      then (((( c_d r) . (n + 1)) * (( c_d r) . n)) " ) >= ((1 / (s5 * ((( c_d r) . n) |^ 2))) + (1 / (s5 * ((( c_d r) . (n + 1)) |^ 2)))) by A6, A7, A8, REAL_3: 69;

      then

       A10: (((( c_d r) . (n + 1)) * (( c_d r) . n)) * (((( c_d r) . (n + 1)) * (( c_d r) . n)) " )) >= (((( c_d r) . (n + 1)) * (( c_d r) . n)) * ((1 / (s5 * ((( c_d r) . n) |^ 2))) + (1 / (s5 * ((( c_d r) . (n + 1)) |^ 2))))) by XREAL_1: 64;

      ((( c_d r) . n) |^ 2) = ((( c_d r) . n) * (( c_d r) . n)) by WSIERP_1: 1;

      

      then

       A15: (((( c_d r) . (n + 1)) * (( c_d r) . n)) / (s5 * ((( c_d r) . n) |^ 2))) = (((( c_d r) . (n + 1)) * (( c_d r) . n)) * ((s5 " ) * (((( c_d r) . n) * (( c_d r) . n)) " ))) by XCMPLX_1: 204

      .= (((( c_d r) . (n + 1)) * (( c_d r) . n)) * ((s5 " ) * (((( c_d r) . n) " ) * ((( c_d r) . n) " )))) by XCMPLX_1: 204

      .= ((((s5 " ) * (( c_d r) . (n + 1))) * ((( c_d r) . n) * ((( c_d r) . n) " ))) * ((( c_d r) . n) " ))

      .= ((((s5 " ) * (( c_d r) . (n + 1))) * 1) * ((( c_d r) . n) " )) by XCMPLX_0:def 7

      .= (((s5 " ) * (( c_d r) . (n + 1))) * ((( c_d r) . n) " ));

      ((( c_d r) . (n + 1)) |^ 2) = ((( c_d r) . (n + 1)) * (( c_d r) . (n + 1))) by WSIERP_1: 1;

      

      then ((((( c_d r) . (n + 1)) * (( c_d r) . n)) * 1) / (s5 * ((( c_d r) . (n + 1)) |^ 2))) = (((( c_d r) . (n + 1)) * (( c_d r) . n)) * ((s5 " ) * (((( c_d r) . (n + 1)) * (( c_d r) . (n + 1))) " ))) by XCMPLX_1: 204

      .= (((( c_d r) . (n + 1)) * (( c_d r) . n)) * ((s5 " ) * (((( c_d r) . (n + 1)) " ) * ((( c_d r) . (n + 1)) " )))) by XCMPLX_1: 204

      .= ((((( sqrt 5) " ) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) * ((( c_d r) . (n + 1)) " ))) * ((( c_d r) . (n + 1)) " ))

      .= ((((( sqrt 5) " ) * (( c_d r) . n)) * 1) * ((( c_d r) . (n + 1)) " )) by XCMPLX_0:def 7

      .= (((( sqrt 5) " ) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " ));

      then

       A17: 1 >= ((((( sqrt 5) " ) * (( c_d r) . (n + 1))) * ((( c_d r) . n) " )) + (((s5 " ) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " ))) by A15, A10, XCMPLX_0:def 7;

       0 < ( sqrt 5) by SQUARE_1: 20, SQUARE_1: 27;

      then

       A18: (s5 * 1) >= (s5 * ((((s5 " ) * (( c_d r) . (n + 1))) * ((( c_d r) . n) " )) + (((s5 " ) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " )))) by A17, XREAL_1: 64;

      

       A20: (s5 * ((((s5 " ) * (( c_d r) . (n + 1))) * ((( c_d r) . n) " )) + (((s5 " ) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " )))) = ((((s5 * (s5 " )) * (( c_d r) . (n + 1))) * ((( c_d r) . n) " )) + (((s5 * (s5 " )) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " )))

      .= (((1 * (( c_d r) . (n + 1))) * ((( c_d r) . n) " )) + (((s5 * (s5 " )) * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " ))) by SQRT2, XCMPLX_0:def 7

      .= (((( c_d r) . (n + 1)) * ((( c_d r) . n) " )) + ((1 * (( c_d r) . n)) * ((( c_d r) . (n + 1)) " ))) by SQRT2, XCMPLX_0:def 7

      .= (((( c_d r) . (n + 1)) / (( c_d r) . n)) + ((( c_d r) . n) / (( c_d r) . (n + 1))));

      s5 <> (((( c_d r) . (n + 1)) / (( c_d r) . n)) + ((( c_d r) . n) / (( c_d r) . (n + 1)))) by PEPIN: 59, IRRAT_1: 1;

      then s5 > (((( c_d r) . (n + 1)) / (( c_d r) . n)) + ((( c_d r) . n) / (( c_d r) . (n + 1)))) by A18, A20, XXREAL_0: 1;

      hence thesis by XCMPLX_1: 213;

    end;

    theorem :: DIOPHAN2:9

    

     Th4: cn = (( c_n r) . n) & cd = (( c_d r) . n) implies (cn,cd) are_coprime

    proof

      set cd2 = (( c_d r) . (n + 1));

      set cn2 = (( c_n r) . (n + 1));

      assume that

       A1: cn = (( c_n r) . n) and

       A2: cd = (( c_d r) . n);

      

       A6: ((cn2 * cd) - (cn * cd2)) = (( - 1) |^ n) by A1, A2, REAL_3: 64;

      assume

       A5: not (cn,cd) are_coprime ;

      consider cn0,cd0 be Integer such that

       A7: cn = ((cn gcd cd) * cn0) and

       A8: cd = ((cn gcd cd) * cd0) and (cn0,cd0) are_coprime by A2, INT_2: 23;

      (cn gcd cd) >= ( 0 + 1) by A2, INT_1: 7;

      then

       A9: (cn gcd cd) > 1 by A5, INT_2:def 3, XXREAL_0: 1;

      

       A10: (( - 1) |^ n) = ((cn gcd cd) * ((cn2 * cd0) - (cn0 * cd2))) by A7, A6, A8;

      

       A11: 1 = |.(( - 1) |^ n).| by SERIES_2: 1

      .= ( |.(cn gcd cd).| * |.((cn2 * cd0) - (cn0 * cd2)).|) by COMPLEX1: 65, A10

      .= ((cn gcd cd) * |.((cn2 * cd0) - (cn0 * cd2)).|);

      ((cn gcd cd) " ) < 1 by A9, XREAL_1: 212;

      then |.((cn2 * cd0) - (cn0 * cd2)).| < 1 by A11, XCMPLX_1: 210;

      then |.((cn2 * cd0) - (cn0 * cd2)).| = 0 by NAT_1: 14;

      hence contradiction by A11;

    end;

    theorem :: DIOPHAN2:10

    

     Th5: n > 1 implies |.(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

      assume that

       A2: n > 1 and

       A3: not ( |.(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))));

      

       A4: ( sqrt 5) > (((( c_d r) . (n + 1)) / (( c_d r) . n)) + (1 / ((( c_d r) . (n + 1)) / (( c_d r) . n)))) by A2, A3, Th3;

      set m = (n + 1);

      m > (1 + 1) by A2, XREAL_1: 8;

      then m > 1 by XXREAL_0: 2;

      then

       A7: ( sqrt 5) > (((( c_d r) . (m + 1)) / (( c_d r) . m)) + (1 / ((( c_d r) . (m + 1)) / (( c_d r) . m)))) by A3, Th3;

      

       A10: ((( c_d r) . (n + 2)) / (( c_d r) . (n + 1))) = ((((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) / (( c_d r) . m)) by REAL_3:def 6

      .= (((( scf r) . (n + 2)) * ((( c_d r) . (n + 1)) * ((( c_d r) . m) " ))) + ((( c_d r) . n) / (( c_d r) . (n + 1))))

      .= (((( scf r) . (n + 2)) * 1) + ((( c_d r) . n) / (( c_d r) . m))) by XCMPLX_0:def 7

      .= ((( scf r) . (n + 2)) + (((( c_d r) . m) / (( c_d r) . n)) " )) by XCMPLX_1: 213;

      ((( c_d r) . (n + 2)) / (( c_d r) . m)) > ((( c_d r) . m) / (( c_d r) . m)) by XREAL_1: 74, DIOPHAN1: 8;

      then

       A11: ((( c_d r) . (n + 2)) / (( c_d r) . (n + 1))) > 1 by XCMPLX_1: 60;

      set m1 = (n - 1);

      ((( c_d r) . (m1 + 2)) / (( c_d r) . (m1 + 1))) > ((( c_d r) . (m1 + 1)) / (( c_d r) . (m1 + 1))) by XREAL_1: 74, A2, DIOPHAN1: 8;

      then ((( c_d r) . ((n - 1) + 2)) / (( c_d r) . ((n - 1) + 1))) > 1 by XCMPLX_1: 60;

      then

       A13: (1 / ((( c_d r) . (n + 1)) / (( c_d r) . n))) > ((( sqrt 5) - 1) / 2) by A4, Th1;

      (( scf r) . ((n + 1) + 1)) > 0 by DIOPHAN1: 5;

      then (( scf r) . (n + 2)) >= ( 0 + 1) by INT_1: 7;

      then ((( scf r) . (n + 2)) + (1 / ((( c_d r) . (n + 1)) / (( c_d r) . n)))) > (1 + ((( sqrt 5) - 1) / 2)) by A13, XREAL_1: 8;

      hence contradiction by A7, A10, A11, Th1;

    end;

    definition

      let r;

      :: DIOPHAN2:def2

      func HWZSet (r) -> Subset of RAT equals { p where p be Rational : |.(r - p).| < (1 / (( sqrt 5) * (( denominator p) |^ 2))) };

      coherence

      proof

        defpred P[ Rational] means |.(r - $1).| < (1 / (( sqrt 5) * (( denominator $1) |^ 2)));

        { p where p be Rational : P[p] } c= RAT

        proof

          let y be object;

          assume y in { p where p be Rational : P[p] };

          then ex r be Rational st y = r & P[r];

          hence thesis by RAT_1:def 2;

        end;

        hence thesis;

      end;

    end

    definition

      let r;

      :: DIOPHAN2:def3

      func HWZSet1 (r) -> Subset of NAT equals { x where x be Nat : ex p be Rational st p in ( HWZSet r) & x = ( denominator p) };

      coherence

      proof

        defpred P[ Nat] means ex p be Rational st p in ( HWZSet r) & $1 = ( denominator p);

        { x where x be Nat : P[x] } c= NAT

        proof

          let y be object;

          assume y in { x where x be Nat : P[x] };

          then ex x be Nat st y = x & P[x];

          hence thesis by ORDINAL1:def 12;

        end;

        hence thesis;

      end;

    end

    definition

      :: DIOPHAN2:def4

      func TRANQN -> Function of RAT , NAT means

      : Def3A: for x be Rational holds (it . x) = ( denominator x);

      existence

      proof

        defpred P[ Element of RAT , Element of NAT ] means $2 = ( denominator $1);

        

         A1: for x be Element of RAT holds ex y be Element of NAT st P[x, y]

        proof

          let x be Element of RAT ;

          ( denominator x) in NAT by ORDINAL1:def 12;

          hence thesis;

        end;

        consider f be Function of RAT , NAT such that

         A2: for x be Element of RAT holds P[x, (f . x)] from FUNCT_2:sch 3( A1);

        take f;

        let x be Rational;

        x in RAT by RAT_1:def 2;

        hence thesis by A2;

      end;

      uniqueness

      proof

        let f,g be Function of RAT , NAT ;

        assume that

         A3: for x be Rational holds (f . x) = ( denominator x) and

         A4: for x be Rational holds (g . x) = ( denominator x);

        now

          let x be Element of RAT ;

          (f . x) = ( denominator x) by A3;

          hence (f . x) = (g . x) by A4;

        end;

        hence thesis;

      end;

    end

    theorem :: DIOPHAN2:11

    

     Th6: ( TRANQN .: ( HWZSet r)) = ( HWZSet1 r)

    proof

      thus ( TRANQN .: ( HWZSet r)) c= ( HWZSet1 r)

      proof

        let y be object;

        assume

         A2: y in ( TRANQN .: ( HWZSet r));

        consider p be object such that

         A3: p in ( dom TRANQN ) and

         A4: p in ( HWZSet r) and

         A5: y = ( TRANQN . p) by A2, FUNCT_1:def 6;

        consider q be Element of RAT such that

         A6: q = p by A3;

        y = ( denominator q) by Def3A, A5, A6;

        hence thesis by A4, A6;

      end;

      let y be object;

      assume y in ( HWZSet1 r);

      then

      consider y1 be Nat such that

       A11: y1 = y and

       A12: ex p be Rational st p in ( HWZSet r) & y1 = ( denominator p);

      consider p be Rational such that

       A13: p in ( HWZSet r) & y1 = ( denominator p) by A12;

      

       A14: ( dom TRANQN ) = RAT by FUNCT_2:def 1;

      y1 = ( TRANQN . p) by Def3A, A13;

      hence thesis by A11, A13, A14, FUNCT_1:def 6;

    end;

    theorem :: DIOPHAN2:12

    

     Th7: ( HWZSet r) is finite implies ( HWZSet1 r) is finite

    proof

      ( TRANQN .: ( HWZSet r)) = ( HWZSet1 r) by Th6;

      hence thesis;

    end;

    registration

      let r;

      cluster ( HWZSet1 r) -> non empty;

      coherence

      proof

        set n = 2;

        per cases by Th5;

          suppose

           A3: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| < (1 / (( sqrt 5) * ((( c_d r) . n) |^ 2)));

          set q1 = (( c_n r) . n);

          reconsider q2 = (( c_d r) . n) as Element of INT by NUMBERS: 17, REAL_3: 50;

          set q = (q1 / q2);

          

           A5: (q1,q2) are_coprime by Th4;

           |.(r - q).| < (1 / (( sqrt 5) * (( denominator q) |^ 2))) by Th8, A3, A5;

          then q in ( HWZSet r);

          then ( denominator q) in ( HWZSet1 r);

          hence thesis by XBOOLE_0:def 1;

        end;

          suppose

           A8: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| < (1 / (( sqrt 5) * ((( c_d r) . (n + 1)) |^ 2)));

          set q1 = (( c_n r) . (n + 1));

          reconsider q2 = (( c_d r) . (n + 1)) as Element of INT by NUMBERS: 17, REAL_3: 50;

          set q = (q1 / q2);

          (q1,q2) are_coprime by Th4;

          then q1 = ( numerator q) & q2 = ( denominator q) by Th8;

          then q in ( HWZSet r) by A8;

          then ( denominator q) in ( HWZSet1 r);

          hence thesis by XBOOLE_0:def 1;

        end;

          suppose

           A14: |.(r - ((( c_n r) . (n + 2)) / (( c_d r) . (n + 2)))).| < (1 / (( sqrt 5) * ((( c_d r) . (n + 2)) |^ 2)));

          set q1 = (( c_n r) . (n + 2));

          reconsider q2 = (( c_d r) . (n + 2)) as Element of INT by NUMBERS: 17, REAL_3: 50;

          set q = (q1 / q2);

          (q1,q2) are_coprime by Th4;

          then |.(r - q).| < (1 / (( sqrt 5) * (( denominator q) |^ 2))) by Th8, A14;

          then q in ( HWZSet r);

          then ( denominator q) in ( HWZSet1 r);

          hence thesis by XBOOLE_0:def 1;

        end;

      end;

    end

    theorem :: DIOPHAN2:13

    

     Th10: for h be Nat st h in ( HWZSet1 r) holds h > 0

    proof

      let h be Nat;

      assume h in ( HWZSet1 r);

      then ex h1 be Nat st h1 = h & ex p be Rational st p in ( HWZSet r) & h1 = ( denominator p);

      hence thesis;

    end;

    registration

      let r;

      cluster ( HWZSet1 r) -> infinite;

      coherence

      proof

        assume ( HWZSet1 r) is finite;

        then

        reconsider HWS1 = ( HWZSet1 r) as finite non empty Subset of NAT ;

        reconsider j = ( max HWS1) as Element of NAT by ORDINAL1:def 12;

        HWS1 c= REAL by NUMBERS: 19;

        then

        reconsider HWS1 as non empty Subset of ExtREAL by NUMBERS: 31, XBOOLE_1: 1;

        

         A4: for s be Element of HWS1 holds j >= s & j > 0

        proof

          let s be Element of HWS1;

          

           A5: s in HWS1 by SUBSET_1:def 1;

          then j >= s by XXREAL_2: 4;

          hence thesis by A5, Th10;

        end;

        set n = (j + 1);

        per cases by Th5, A4, XREAL_1: 29;

          suppose

           A7: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| < (1 / (( sqrt 5) * ((( c_d r) . n) |^ 2)));

          set q1 = (( c_n r) . n);

          set q2 = (( c_d r) . n);

          set q = (q1 / q2);

          

           A9: (q1,q2) are_coprime by Th4;

          q1 = ( numerator q) & q2 = ( denominator q) by Th8, A9;

          then q in ( HWZSet r) by A7;

          then ( denominator q) in ( HWZSet1 r);

          then

           A14: q2 in ( HWZSet1 r) by Th8, A9;

          

           A15: q2 >= (j + 1) by DIOPHAN1: 9;

          (j + 1) > j by XREAL_1: 29;

          then q2 > j by A15, XXREAL_0: 2;

          hence contradiction by A4, A14;

        end;

          suppose

           A17: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| < (1 / (( sqrt 5) * ((( c_d r) . (n + 1)) |^ 2)));

          set q1 = (( c_n r) . (n + 1));

          set q2 = (( c_d r) . (n + 1));

          set q = (q1 / q2);

          

           A19: (q1,q2) are_coprime by Th4;

          then

           A20: q1 = ( numerator q) & q2 = ( denominator q) by Th8;

           |.(r - q).| < (1 / (( sqrt 5) * (( denominator q) |^ 2))) by A17, Th8, A19;

          then q in ( HWZSet r);

          then q2 in ( HWZSet1 r) by A20;

          then

           A23: q2 <= j by A4;

          

           A24: q2 >= (j + 2) by DIOPHAN1: 9;

          (j + 2) > j by XREAL_1: 29;

          hence contradiction by A23, A24, XXREAL_0: 2;

        end;

          suppose

           A26: |.(r - ((( c_n r) . (n + 2)) / (( c_d r) . (n + 2)))).| < (1 / (( sqrt 5) * ((( c_d r) . (n + 2)) |^ 2)));

          set q1 = (( c_n r) . (n + 2));

          set q2 = (( c_d r) . (n + 2));

          set q = (q1 / q2);

          

           A28: (q1,q2) are_coprime by Th4;

          then

           A29: q1 = ( numerator q) & q2 = ( denominator q) by Th8;

           |.(r - q).| < (1 / (( sqrt 5) * (( denominator q) |^ 2))) by Th8, A28, A26;

          then q in ( HWZSet r);

          then q2 in ( HWZSet1 r) by A29;

          then

           A33: q2 <= j by A4;

          

           A34: q2 >= (j + 3) by DIOPHAN1: 9;

          (j + 3) > j by XREAL_1: 29;

          hence contradiction by A33, A34, XXREAL_0: 2;

        end;

      end;

    end

    ::$Notion-Name

    theorem :: DIOPHAN2:14

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

    proof

      let r;

      ( HWZSet1 r) is infinite;

      hence thesis by Th7;

    end;

    reserve c0,c1,c2,u,a0,b0 for Real;

    definition

      let a0,b0,c0 be Real;

      :: DIOPHAN2:def5

      func LF (a0,b0,c0) -> Function of [: INT , INT :], REAL means

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

      existence

      proof

        defpred P[ Integer, Integer, set] means $3 = (((a0 * $1) + (b0 * $2)) + c0);

        

         A1: for x,y be Element of INT holds ex z be Element of REAL st P[x, y, z]

        proof

          let x,y be Element of INT ;

          (((a0 * x) + (b0 * y)) + c0) in REAL by XREAL_0:def 1;

          hence thesis;

        end;

        consider f be Function of [: INT , INT :], REAL such that

         A3: for x,y be Element of INT holds P[x, y, (f . (x,y))] from BINOP_1:sch 3( A1);

        take f;

        let x,y be Integer;

        x in INT & y in INT by INT_1:def 2;

        hence thesis by A3;

      end;

      uniqueness

      proof

        let F1,F2 be Function of [: INT , INT :], REAL ;

        assume that

         A4: for x,y be Integer holds (F1 . (x,y)) = (((a0 * x) + (b0 * y)) + c0) and

         A5: for x,y be Integer holds (F2 . (x,y)) = (((a0 * x) + (b0 * y)) + c0);

        now

          let x,y be Element of INT ;

          

          thus (F1 . (x,y)) = (((a0 * x) + (b0 * y)) + c0) by A4

          .= (F2 . (x,y)) by A5;

        end;

        hence thesis by BINOP_1: 2;

      end;

    end

    begin

    theorem :: DIOPHAN2:15

    

     Th16: for rh0 be Element of REAL , p,q be Integer st (p,q) are_coprime holds ex x,y be Element of INT st |.(((p * x) - (q * y)) + rh0).| <= (1 / 2)

    proof

      let rh0 be Element of REAL ;

      let p,q be Integer;

      assume

       A1: (p,q) are_coprime ;

      consider b be Element of INT such that

       A2: |.(rh0 - b).| <= (1 / 2) by GAUSSINT: 48;

      consider s,t be Integer such that

       A3: ((s * p) + (t * q)) = 1 by A1, Th15;

      

       A4: (b * ((s * p) + (t * q))) = b by A3;

      set x = ( - (b * s)), y = (b * t);

      

       X: x in INT & y in INT by INT_1:def 2;

      (((p * x) - (q * y)) + rh0) = (rh0 - b) by A4;

      hence thesis by A2, X;

    end;

    reserve a,b for Real;

    reserve n for Integer;

    theorem :: DIOPHAN2:16

    

     Th17: n <= b & b <= (n + 1) implies ( |.(n - b).| * |.((n + 1) - b).|) <= (1 / 4)

    proof

      assume that

       A1: n <= b and

       A2: b <= (n + 1);

      set x = (b - n), y = ((n + 1) - b);

      x >= 0 by A1, XREAL_1: 48;

      

      then

       A4: |.(n - b).| = ( - ( - x)) by ABSVALUE: 30

      .= x;

      

       A5: (x + y) = 1;

      ( |.(n - b).| * |.((n + 1) - b).|) = (x * y) by A4, A2, XREAL_1: 48, ABSVALUE:def 1;

      hence thesis by A5, SERIES_3: 18;

    end;

    theorem :: DIOPHAN2:17

    

     Th21: not a is Integer & (n = [\a/] or n = ( [\a/] + 1)) implies |.(a - n).| < 1

    proof

      assume

       A1: not a is Integer & (n = [\a/] or n = ( [\a/] + 1));

      per cases by A1;

        suppose

         A2: n = [\a/];

        then

         A3: (a - n) > 0 by A1, INT_1: 26, XREAL_1: 50;

        (a - [\a/]) < ((1 + [\a/]) - [\a/]) by INT_1: 29, XREAL_1: 14;

        hence thesis by A2, A3, ABSVALUE:def 1;

      end;

        suppose

         A5: n = ( [\a/] + 1);

        then

         A6: (a - n) < 0 by INT_1: 29, XREAL_1: 49;

         [\a/] < [/a\] by A1, INT_1: 35;

        then n = [/a\] by A5, INT_1: 41;

        then n < (a + 1) by INT_1:def 7;

        then

         A8: (n - a) < 1 by XREAL_1: 19;

         |.(a - n).| = ( - (a - n)) by A6, ABSVALUE:def 1;

        hence thesis by A8;

      end;

    end;

    theorem :: DIOPHAN2:18

    

     Th22: ( |.(n - a).| * |.((n + 1) - a).|) <= (1 / 4) & ( |.(n - b).| * |.((n + 1) - b).|) <= (1 / 4) implies ( |.(n - a).| * |.(n - b).|) <= (1 / 4) or ( |.((n + 1) - a).| * |.((n + 1) - b).|) <= (1 / 4)

    proof

      assume

       A1: ( |.(n - a).| * |.((n + 1) - a).|) <= (1 / 4) & ( |.(n - b).| * |.((n + 1) - b).|) <= (1 / 4);

      set r1 = |.(n - a).|, r2 = |.(n - b).|, s1 = |.((n + 1) - a).|, s2 = |.((n + 1) - b).|;

      

       A2: ((r1 * s1) * (r2 * s2)) <= ((1 / 4) * (1 / 4)) by A1, XREAL_1: 66;

      set r3 = (r1 * r2), r4 = (s1 * s2), r5 = ((1 / 4) * (1 / 4));

      

       A3: ( sqrt r5) = (( sqrt (1 / 4)) ^2 ) by SQUARE_1: 29

      .= (1 / 4) by SQUARE_1:def 2;

      (r3 * r4) <= r5 by A2;

      hence thesis by A3, Th18;

    end;

    theorem :: DIOPHAN2:19

    

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

    proof

      assume

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

      set r1 = |.(a - n).|, r2 = |.(b - n).|, s1 = |.((a - n) - 1).|, s2 = |.((b - n) - 1).|;

      set t = (a - b);

      set r0 = ( |.(a - b).| / 2);

      set r3 = (r1 * r2), r4 = (s1 * s2);

      

       A3: ( sqrt (( |.(a - b).| ^2 ) / 4)) = ( sqrt (( |.(a - b).| / 2) * ( |.(a - b).| / 2)))

      .= (( sqrt r0) ^2 ) by SQUARE_1: 29

      .= r0 by SQUARE_1:def 2;

      (r3 * r4) <= (( |.(a - b).| ^2 ) / 4) by A1;

      hence thesis by A3, Th18;

    end;

    theorem :: DIOPHAN2:20

    

     Th24: ((n - b) * ((n + 1) - a)) > 0 & ((a - n) * ((n + 1) - b)) > 0 implies (((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

      assume that

       A1: ((n - b) * ((n + 1) - a)) > 0 and

       A2: ((a - n) * ((n + 1) - b)) > 0 ;

      set s = ((n - b) * ((n + 1) - a));

      set t = ((a - n) * ((n + 1) - b));

      

       A3: ( sqrt (s * t)) <= ((s + t) / 2) by A1, A2, SERIES_3: 2;

      

       A4: (( sqrt (s * t)) ^2 ) = (s * t) by A1, A2, SQUARE_1:def 2;

      

       A5: ( sqrt (s * t)) >= 0 by A1, A2, SQUARE_1:def 2;

      

       A6: s = |.s.| by A1, COMPLEX1: 43

      .= ( |.(n - b).| * |.((n + 1) - a).|) by COMPLEX1: 65;

      

       A7: t = |.t.| by A2, COMPLEX1: 43

      .= ( |.(a - n).| * |.((n + 1) - b).|) by COMPLEX1: 65;

      

       A9: |.(n - b).| = |.( - (n - b)).| by COMPLEX1: 52

      .= |.(b - n).|;

      

       A10: |.((n + 1) - a).| = |.( - ((n + 1) - a)).| by COMPLEX1: 52

      .= |.((a - n) - 1).|;

      

       A11: |.((n + 1) - b).| = |.( - ((n + 1) - b)).| by COMPLEX1: 52

      .= |.((b - n) - 1).|;

      

       A12: (s * t) = (( |.(n - b).| * |.((n + 1) - a).|) * ( |.(a - n).| * |.((n + 1) - b).|)) by A7, A6

      .= ((( |.(a - n).| * |.(b - n).|) * |.((a - n) - 1).|) * |.((b - n) - 1).|) by A11, A10, A9;

      (((a - b) / 2) ^2 ) = (((a - b) ^2 ) / (2 ^2 )) by XCMPLX_1: 76

      .= (( |.(a - b).| ^2 ) / 4) by COMPLEX1: 75;

      hence thesis by A3, A4, A5, A12, SQUARE_1: 15;

    end;

    theorem :: DIOPHAN2:21

    

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

    proof

      assume that

       A1: n > b and

       A2: n < a & a < (n + 1);

      

       A3: (n - b) > 0 by A1, XREAL_1: 50;

      

       A4: ((n + 1) - a) > 0 by A2, XREAL_1: 50;

      

       A5: (a - n) > 0 by A2, XREAL_1: 50;

      

       A6: ((n - b) + 1) > 0 by A3;

      

       A7: ((n - b) * ((n + 1) - a)) > 0 by A3, A4;

      ((a - n) * ((n + 1) - b)) > 0 by A5, A6;

      hence thesis by A7, Th24;

    end;

    theorem :: DIOPHAN2:22

    

     Th26: ((n - a) * ((n + 1) - b)) > 0 & ((b - n) * ((n + 1) - a)) > 0 implies (((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

      assume that

       A1: ((n - a) * ((n + 1) - b)) > 0 and

       A2: ((b - n) * ((n + 1) - a)) > 0 ;

      set s = ((n - a) * ((n + 1) - b));

      set t = ((b - n) * ((n + 1) - a));

      

       A3: ( sqrt (s * t)) <= ((s + t) / 2) by A1, A2, SERIES_3: 2;

      

       A4: (( sqrt (s * t)) ^2 ) = (s * t) by A1, A2, SQUARE_1:def 2;

      

       A5: ( sqrt (s * t)) >= 0 by A1, A2, SQUARE_1:def 2;

      

       A6: s = |.s.| by A1, COMPLEX1: 43

      .= ( |.(n - a).| * |.((n + 1) - b).|) by COMPLEX1: 65;

      

       A7: t = |.t.| by A2, COMPLEX1: 43

      .= ( |.(b - n).| * |.((n + 1) - a).|) by COMPLEX1: 65;

      

       A8: |.(n - a).| = |.( - (n - a)).| by COMPLEX1: 52

      .= |.(a - n).|;

      

       A9: |.((n + 1) - b).| = |.( - ((n + 1) - b)).| by COMPLEX1: 52

      .= |.((b - n) - 1).|;

      

       A10: |.((n + 1) - a).| = |.( - ((n + 1) - a)).| by COMPLEX1: 52

      .= |.((a - n) - 1).|;

      

       A11: (s * t) = (( |.(n - a).| * |.((n + 1) - b).|) * ( |.(b - n).| * |.((n + 1) - a).|)) by A7, A6

      .= ((( |.(b - n).| * |.(a - n).|) * |.((b - n) - 1).|) * |.((a - n) - 1).|) by A10, A9, A8;

      ((b - a) ^2 ) = ( |.(b - a).| ^2 ) by COMPLEX1: 75

      .= ( |.(a - b).| ^2 ) by COMPLEX1: 60;

      then (((b - a) / 2) ^2 ) = (( |.(a - b).| ^2 ) / 4);

      hence thesis by A3, A4, A5, A11, SQUARE_1: 15;

    end;

    theorem :: DIOPHAN2:23

    

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

    proof

      assume

       A2: (n + 1) < b & n < a & a < (n + 1);

      then

       A3: ((n + 1) - b) < 0 by XREAL_1: 49;

      

       A4: (n - a) < 0 by A2, XREAL_1: 49;

      

       A5: ((1 + n) - n) < (b - n) by A2, XREAL_1: 14;

      

       A6: ((n + 1) - a) > 0 by A2, XREAL_1: 50;

      

       A7: ((n - a) * ((n + 1) - b)) > 0 by A3, A4;

      ((b - n) * ((n + 1) - a)) > 0 by A5, A6;

      hence thesis by A7, Th26;

    end;

    theorem :: DIOPHAN2:24

    

     Th28: not a is Integer & [\a/] <= b & b <= ( [\a/] + 1) implies ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) <= (1 / 4)

    proof

      assume that

       A1: not a is Integer and

       A2: [\a/] <= b & b <= ( [\a/] + 1);

      set n = [\a/];

      

       A3: n < a by A1, INT_1: 26;

      (a - 1) < n by INT_1:def 6;

      then a < (n + 1) by XREAL_1: 19;

      then

       A6: ( |.(n - a).| * |.((n + 1) - a).|) <= (1 / 4) by Th17, A3;

      ( |.(n - b).| * |.((n + 1) - b).|) <= (1 / 4) by Th17, A2;

      per cases by Th22, A6;

        suppose

         A8: ( |.(n - a).| * |.(n - b).|) <= (1 / 4);

        set u = n;

        

         A10: |.(a - u).| < 1 by A1, Th21;

        ( |.(u - a).| * |.(u - b).|) = ( |.(a - u).| * |.(u - b).|) by COMPLEX1: 60

        .= ( |.(a - u).| * |.(b - u).|) by COMPLEX1: 60;

        hence thesis by A10, A8;

      end;

        suppose

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

        set u = (n + 1);

        

         A14: |.(a - u).| < 1 by A1, Th21;

        ( |.(u - a).| * |.(u - b).|) = ( |.(a - u).| * |.(u - b).|) by COMPLEX1: 60

        .= ( |.(a - u).| * |.(b - u).|) by COMPLEX1: 60;

        hence thesis by A14, A12;

      end;

    end;

    theorem :: DIOPHAN2:25

    

     Th32: ( |.(a - [\a/]).| * |.(b - [\a/]).|) >= ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) >= ( |.(a - b).| / 2) implies a is Integer or [\a/] <= b

    proof

      set u = [\a/];

      set v = ( [\a/] + 1);

      assume

       A5: ( |.(a - [\a/]).| * |.(b - [\a/]).|) >= ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) >= ( |.(a - b).| / 2);

      assume that

       A1: not a is Integer and

       A2: [\a/] > b;

      

       A3: (a - [\a/]) > 0 by A1, INT_1: 26, XREAL_1: 50;

      

       A4: (a - 1) < [\a/] by INT_1:def 6;

      

       S: ( [\a/] + 1) > b by A2, XREAL_1: 40;

      then

       A6: (( [\a/] + 1) - b) > 0 by XREAL_1: 50;

      

       A8: ( [\a/] - b) > 0 by A2, XREAL_1: 50;

      

       A9: (( [\a/] + 1) - a) > 0 by A4, XREAL_1: 19, XREAL_1: 50;

      

       S2: a < ( [\a/] + 1) by A4, XREAL_1: 19;

      then

       a5: ((( |.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).|) <= (( |.(a - b).| ^2 ) / 4) by A1, A2, INT_1: 26, Th25;

      per cases by A5, XXREAL_0: 1;

        suppose

         A5: ( |.(a - [\a/]).| * |.(b - [\a/]).|) = ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) > ( |.(a - b).| / 2);

        

         A8: (b - [\a/]) < 0 by A2, XREAL_1: 49;

        (( |.(a - [\a/]).| * |.(b - [\a/]).|) * ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|)) > (( |.(a - b).| / 2) * ( |.(a - b).| / 2)) by A3, A8, XREAL_1: 98, A5;

        hence contradiction by a5;

      end;

        suppose

         A5: ( |.(a - [\a/]).| * |.(b - [\a/]).|) > ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) = ( |.(a - b).| / 2);

        

         A4: ((( |.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).|) <= (( |.(a - b).| ^2 ) / 4) by A1, A2, INT_1: 26, Th25, S2;

        

         a6: (a - ( [\a/] + 1)) < 0 by XREAL_1: 49, S2;

        (b - ( [\a/] + 1)) < 0 by XREAL_1: 49, S;

        then (( |.(a - [\a/]).| * |.(b - [\a/]).|) * ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|)) > (( |.(a - b).| / 2) * ( |.(a - b).| / 2)) by A5, a6, XREAL_1: 98;

        hence contradiction by A4;

      end;

        suppose

         A5: ( |.(a - [\a/]).| * |.(b - [\a/]).|) > ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) > ( |.(a - b).| / 2);

        ((( |.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).|) <= (( |.(a - b).| ^2 ) / 4) by A1, A2, S2, INT_1: 26, Th25;

        hence thesis by Th23, A5;

      end;

        suppose

         A5: ( |.(a - [\a/]).| * |.(b - [\a/]).|) = ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) = ( |.(a - b).| / 2);

        

         A10: ( |.(a - u).| * |.(u - b).|) = ( |.(a - u).| * |.( - (u - b)).|) by COMPLEX1: 52

        .= ( |.(a - b).| / 2) by A5;

        

         A11: ( |.(a - u).| * |.(u - b).|) = ( |.(a - u).| * |.( - (u - b)).|) by COMPLEX1: 52

        .= ( |.(a - v).| * |.(b - v).|) by A5;

        

         A13: ((a - u) * ((u + 1) - b)) = |.((a - u) * ((u + 1) - b)).| by A6, A3, ABSVALUE:def 1

        .= ( |.(a - u).| * |.((u + 1) - b).|) by COMPLEX1: 65;

        

         a14: ((u - b) * ((u + 1) - a)) = |.((u - b) * ((u + 1) - a)).| by A8, A9, ABSVALUE:def 1

        .= ( |.(u - b).| * |.((u + 1) - a).|) by COMPLEX1: 65;

        then

         A14: (( |.(a - u).| * |.((u + 1) - b).|) + ( |.(u - b).| * |.((u + 1) - a).|)) = |.(a - b).| by A13;

        

         A15: ((( |.(a - u).| * |.(u - b).|) * |.((a - u) - 1).|) * |.((b - u) - 1).|) = (( |.(a - u).| * |.(u - b).|) * ( |.((a - u) - 1).| * |.((b - u) - 1).|))

        .= (((( |.(a - u).| * |.((u + 1) - b).|) + ( |.(u - b).| * |.((u + 1) - a).|)) / 2) ^2 ) by A13, a14, A10, A11;

        set r1 = ( |.(a - u).| * |.((u + 1) - b).|);

        set r2 = ( |.(u - b).| * |.((u + 1) - a).|);

        

         A17: |.((u + 1) - a).| = |.( - ((u + 1) - a)).| by COMPLEX1: 52

        .= |.((a - u) - 1).|;

        

         A18: |.((u + 1) - b).| = |.( - ((u + 1) - b)).| by COMPLEX1: 52

        .= |.((b - u) - 1).|;

        (r1 * r2) = (((r1 + r2) / 2) ^2 ) by A15, A18, A17;

        then

         A19: r1 = r2 by Th20;

        

         A23: ( |.((u + 1) - b).| - |.(u - b).|) = ((( |.((u + 1) - b).| * |.(a - u).|) - ( |.(u - b).| * |.(a - u).|)) / |.(a - u).|) by A3, XCMPLX_1: 129

        .= 0 by A10, A14, A19;

        ( |.((u + 1) - b).| - |.(u - b).|) = (((u + 1) - b) - |.(u - b).|) by A6, ABSVALUE:def 1

        .= (((u + 1) - b) - (u - b)) by A8, ABSVALUE:def 1

        .= 1;

        hence contradiction by A23;

      end;

    end;

    theorem :: DIOPHAN2:26

    

     Th33: not a is Integer & [\a/] > b implies ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2)

    proof

      assume that

       A1: not a is Integer and

       A2: [\a/] > b;

      assume

       A3: for u be Integer st |.(a - u).| < 1 holds ( |.(a - u).| * |.(b - u).|) >= ( |.(a - b).| / 2);

      set u = [\a/], v = (u + 1);

      

       A4: |.(a - u).| < 1 by A1, Th21;

       |.(a - v).| < 1 by A1, Th21;

      then ( |.(a - u).| * |.(b - u).|) >= ( |.(a - b).| / 2) & ( |.(a - v).| * |.(b - v).|) >= ( |.(a - b).| / 2) by A3, A4;

      hence thesis by A1, A2, Th32;

    end;

    theorem :: DIOPHAN2:27

    

     Th37: ( |.(a - [\a/]).| * |.(b - [\a/]).|) >= ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) >= ( |.(a - b).| / 2) implies a is Integer or ( [\a/] + 1) >= b

    proof

      set u = [\a/], v = (u + 1);

      assume

       AA: ( |.(a - [\a/]).| * |.(b - [\a/]).|) >= ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) >= ( |.(a - b).| / 2);

      assume

       A2: not a is Integer & ( [\a/] + 1) < b;

      then

       A3: (a - [\a/]) > 0 by INT_1: 26, XREAL_1: 50;

      

       A4: (a - 1) < [\a/] by INT_1:def 6;

      then

       a3: a < ( [\a/] + 1) by XREAL_1: 19;

      then

       A5: ((( |.(a - [\a/]).| * |.(b - [\a/]).|) * |.((a - [\a/]) - 1).|) * |.((b - [\a/]) - 1).|) <= (( |.(a - b).| ^2 ) / 4) by A2, INT_1: 26, Th27;

      per cases by XXREAL_0: 1, AA;

        suppose

         A6: ( |.(a - [\a/]).| * |.(b - [\a/]).|) = ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) > ( |.(a - b).| / 2);

        ((1 + [\a/]) - [\a/]) < (b - [\a/]) by A2, XREAL_1: 14;

        then (( |.(a - [\a/]).| * |.(b - [\a/]).|) * ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|)) > (( |.(a - b).| / 2) * ( |.(a - b).| / 2)) by A6, A3, XREAL_1: 98;

        hence thesis by A5;

      end;

        suppose

         A6: ( |.(a - [\a/]).| * |.(b - [\a/]).|) > ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) = ( |.(a - b).| / 2);

        

         a6: (a - ( [\a/] + 1)) < 0 by a3, XREAL_1: 49;

        (b - ( [\a/] + 1)) > 0 by A2, XREAL_1: 50;

        then (( |.(a - [\a/]).| * |.(b - [\a/]).|) * ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|)) > (( |.(a - b).| / 2) * ( |.(a - b).| / 2)) by a6, XREAL_1: 98, A6;

        hence thesis by A5;

      end;

        suppose ( |.(a - [\a/]).| * |.(b - [\a/]).|) > ( |.(a - b).| / 2) & ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) > ( |.(a - b).| / 2);

        hence thesis by Th23, A5;

      end;

        suppose

         SS: ( |.(a - ( [\a/] + 1)).| * |.(b - ( [\a/] + 1)).|) = ( |.(a - b).| / 2) & ( |.(a - [\a/]).| * |.(b - [\a/]).|) = ( |.(a - b).| / 2);

        

         A6: (( [\a/] + 1) - b) < 0 by A2, XREAL_1: 49;

        

         A7: ( [\a/] - a) < 0 by A2, INT_1: 26, XREAL_1: 49;

        

         A8: ((1 + [\a/]) - [\a/]) < (b - [\a/]) by A2, XREAL_1: 14;

        

         A9: (( [\a/] + 1) - a) > 0 by A4, XREAL_1: 19, XREAL_1: 50;

        

         A11: ((u - a) * ((u + 1) - b)) = |.((u - a) * ((u + 1) - b)).| by A6, A7, ABSVALUE:def 1

        .= ( |.(u - a).| * |.((u + 1) - b).|) by COMPLEX1: 65

        .= ( |.( - (u - a)).| * |.((u + 1) - b).|) by COMPLEX1: 52

        .= ( |.(a - u).| * |.((u + 1) - b).|);

        ((b - u) * ((u + 1) - a)) = |.((b - u) * ((u + 1) - a)).| by A8, A9, ABSVALUE:def 1

        .= ( |.(b - u).| * |.((u + 1) - a).|) by COMPLEX1: 65;

        

        then

         A12: (( |.(a - u).| * |.((u + 1) - b).|) + ( |.(b - u).| * |.((u + 1) - a).|)) = |.(b - a).| by A11

        .= |.( - (b - a)).| by COMPLEX1: 52

        .= |.(a - b).|;

        set r1 = ( |.(a - u).| * |.((u + 1) - b).|);

        set r2 = ( |.(b - u).| * |.((u + 1) - a).|);

        

         A16: |.((u + 1) - a).| = |.( - ((u + 1) - a)).| by COMPLEX1: 52

        .= |.((a - u) - 1).|;

        

         A17: |.((u + 1) - b).| = |.( - ((u + 1) - b)).| by COMPLEX1: 52

        .= |.((b - u) - 1).|;

        ((( |.(a - u).| * |.(b - u).|) * |.((a - u) - 1).|) * |.((b - u) - 1).|) = (( |.(a - u).| * |.(b - u).|) * ( |.((a - u) - 1).| * |.((b - u) - 1).|))

        .= (((r1 + r2) / 2) ^2 ) by A12, SS;

        then (r1 * r2) = (((r1 + r2) / 2) ^2 ) by A17, A16;

        then

         A18: r1 = r2 by Th20;

        

         A22: ( |.((u + 1) - b).| - |.(b - u).|) = ((( |.((u + 1) - b).| * |.(a - u).|) - ( |.(b - u).| * |.(a - u).|)) / |.(a - u).|) by A3, XCMPLX_1: 129

        .= 0 by A12, A18, SS;

        ( |.((u + 1) - b).| - |.(b - u).|) = (( - ((u + 1) - b)) - |.(b - u).|) by A2, XREAL_1: 49, ABSVALUE:def 1

        .= (( - ((u + 1) - b)) - (b - u)) by A8, ABSVALUE:def 1

        .= ( - 1);

        hence contradiction by A22;

      end;

    end;

    theorem :: DIOPHAN2:28

    

     Th39: not a is Integer & ( [\a/] + 1) < b implies ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2)

    proof

      assume that

       A1: not a is Integer and

       A2: ( [\a/] + 1) < b;

      assume

       A3: not ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2);

      set u = [\a/], v = (u + 1);

      

       A4: |.(a - u).| < 1 by A1, Th21;

       |.(a - v).| < 1 by A1, Th21;

      then

       b1: ( |.(a - v).| * |.(b - v).|) >= ( |.(a - b).| / 2) by A3;

      ( |.(a - u).| * |.(b - u).|) >= ( |.(a - b).| / 2) by A3, A4;

      hence thesis by A1, A2, Th37, b1;

    end;

    theorem :: DIOPHAN2:29

    

     Th41: ex u be Integer st |.(a - u).| < 1 & (( |.(a - u).| * |.(b - u).|) <= (1 / 4) or ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2))

    proof

      per cases ;

        suppose

         A: a in INT ;

        ( |.(a - a).| * |.(b - a).|) = 0 ;

        hence thesis by A;

      end;

        suppose not a in INT ;

        then

         A5: not a is integer;

        per cases ;

          suppose [\a/] <= b & b <= ( [\a/] + 1);

          then ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) <= (1 / 4) by Th28, A5;

          hence thesis;

        end;

          suppose b < [\a/];

          then ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2) by Th33, A5;

          hence thesis;

        end;

          suppose ( [\a/] + 1) < b;

          then ex u be Integer st |.(a - u).| < 1 & ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2) by Th39, A5;

          hence thesis;

        end;

      end;

    end;

    reserve a1,a2,b1,b2,c1,c2 for Element of REAL ;

    reserve eps for positive Real;

    reserve r1 for non negative Real;

    reserve q,q1 for Element of RAT ;

    theorem :: DIOPHAN2:30

    

     Th42: ex q be Element of RAT st ( denominator q) > ( [\r1/] + 1) & q in ( HWZSet r)

    proof

       0 < ( [\r1/] + 1) by INT_1: 29;

      then

      reconsider m = ( [\r1/] + 1) as Nat;

      ex n st n in ( HWZSet1 r) & n > m

      proof

        assume

         A1: not ex n st n in ( HWZSet1 r) & n > m;

        

         A2: for n st n in ( HWZSet1 r) holds n in ( Seg m)

        proof

          let n;

          assume

           A3: n in ( HWZSet1 r);

          then n > 0 by Th10;

          then

           A4: (n + 0 ) >= 1 by NAT_1: 19;

          n <= m by A1, A3;

          hence thesis by A4;

        end;

        ( Seg m) c= ( Segm (m + 1)) by AFINSQ_1: 3;

        then ( HWZSet1 r) c= ( Segm (m + 1)) by A2;

        hence thesis;

      end;

      then

      consider n such that

       A8: n in ( HWZSet1 r) and

       A9: n > m;

      ex n1 be Nat st n1 = n & ex p be Rational st p in ( HWZSet r) & n1 = ( denominator p) by A8;

      hence thesis by A9;

    end;

    theorem :: DIOPHAN2:31

    

     Th43: |.((a1 * b2) - (a2 * b1)).| <> 0 & q <> q1 & ((a2 * ( denominator q)) + (b2 * ( numerator q))) = 0 implies ((a2 * ( denominator q1)) + (b2 * ( numerator q1))) <> 0

    proof

      assume that

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and

       A2: q <> q1 and

       A3: ((a2 * ( denominator q)) + (b2 * ( numerator q))) = 0 ;

      

       A5: (( - a2) * ( denominator q)) = (( numerator q) * b2) by A3;

      per cases by A1;

        suppose

         A4: a2 <> 0 & b2 <> 0 ;

        assume ((a2 * ( denominator q1)) + (b2 * ( numerator q1))) = 0 ;

        then

         A7: (( - a2) * ( denominator q1)) = (b2 * ( numerator q1));

        q = (( numerator q) / ( denominator q)) by RAT_1: 15

        .= (( - a2) / b2) by A4, A5, XCMPLX_1: 94

        .= (( numerator q1) / ( denominator q1)) by A4, A7, XCMPLX_1: 94

        .= q1 by RAT_1: 15;

        hence contradiction by A2;

      end;

        suppose a2 <> 0 & b2 = 0 ;

        hence thesis;

      end;

        suppose

         A10: a2 = 0 & b2 <> 0 ;

        assume

         A11: ((a2 * ( denominator q1)) + (b2 * ( numerator q1))) = 0 ;

        q = 0 by A3, A10

        .= q1 by A10, A11;

        hence contradiction by A2;

      end;

    end;

    theorem :: DIOPHAN2:32

    

     Th44: for a1, a2, b1, b2, r1 st |.((a1 * b2) - (a2 * b1)).| <> 0 holds ex q be Element of RAT st ( denominator q) > ( [\r1/] + 1) & q in ( HWZSet r) & ((a2 * ( denominator q)) + (b2 * ( numerator q))) <> 0

    proof

      let a1, a2, b1, b2, r1;

      assume

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 ;

      consider q be Element of RAT such that

       A2: ( denominator q) > ( [\r1/] + 1) and

       A3: q in ( HWZSet r) by Th42;

      per cases ;

        suppose ((a2 * ( denominator q)) + (b2 * ( numerator q))) <> 0 ;

        hence thesis by A2, A3;

      end;

        suppose

         A5: ((a2 * ( denominator q)) + (b2 * ( numerator q))) = 0 ;

        consider q1 be Element of RAT such that

         A6: ( denominator q1) > ( [\( denominator q)/] + 1) and

         A7: q1 in ( HWZSet r) by Th42;

        ( denominator q1) > ( denominator q) by A6, INT_1: 29, XXREAL_0: 2;

        then

         A8: ( denominator q1) > ( [\r1/] + 1) by A2, XXREAL_0: 2;

        q1 <> q by A6, INT_1: 29;

        then ((a2 * ( denominator q1)) + (b2 * ( numerator q1))) <> 0 by A1, A5, Th43;

        hence thesis by A7, A8;

      end;

    end;

    theorem :: DIOPHAN2:33

    

     Th45: for a1,b1 be Real, n1,d1 be Integer st d1 > 0 & |.((a1 / b1) + (n1 / d1)).| < (1 / (( sqrt 5) * (d1 |^ 2))) holds ex d be Real st (n1 / d1) = (( - (a1 / b1)) + (d / (d1 |^ 2))) & |.d.| < (1 / ( sqrt 5))

    proof

      let a1,b1 be Real, n1,d1 be Integer;

      assume that

       A1: d1 > 0 and

       A2: |.((a1 / b1) + (n1 / d1)).| < (1 / (( sqrt 5) * (d1 |^ 2)));

      set d = (((a1 / b1) + (n1 / d1)) * (d1 |^ 2));

      (d / (d1 |^ 2)) = ((a1 / b1) + (n1 / d1)) by A1, XCMPLX_1: 89;

      then

       A4: (( - (a1 / b1)) + (d / (d1 |^ 2))) = (n1 / d1);

      

       A5: |.d.| = ( |.((a1 / b1) + (n1 / d1)).| * |.(d1 |^ 2).|) by COMPLEX1: 65

      .= ( |.((a1 / b1) + (n1 / d1)).| * (d1 |^ 2));

      ((1 / (( sqrt 5) * (d1 |^ 2))) * (d1 |^ 2)) = (((1 / ( sqrt 5)) * (1 / (d1 |^ 2))) * (d1 |^ 2)) by XCMPLX_1: 102

      .= (1 / ( sqrt 5)) by A1, XCMPLX_1: 109;

      hence thesis by A4, A1, A2, XREAL_1: 68, A5;

    end;

    theorem :: DIOPHAN2:34

    

     Th46: |.((a1 * b2) - (a2 * b1)).| <> 0 & (a1 / b1) is irrational implies ex x,y be 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

      set Delta = |.((a1 * b2) - (a2 * b1)).|;

      assume that

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and

       A2: (a1 / b1) is irrational;

      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).| / Delta))) as non negative Real by SQRT2, XXREAL_0:def 10;

      consider q1 be 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: d1 > r1 by A7, INT_1: 29, XXREAL_0: 2;

      ( |.b1.| / (( sqrt 5) * eps)) <= r1 by XXREAL_0: 25;

      then ( |.b1.| / (( sqrt 5) * eps)) < (1 * d1) by A8, XXREAL_0: 2;

      then ( |.b1.| / d1) < (1 * (( sqrt 5) * eps)) by SQRT2, XREAL_1: 113;

      then (( |.b1.| / d1) * 1) < (eps * ( sqrt 5));

      then (( |.b1.| / d1) / ( sqrt 5)) < (eps / 1) by SQRT2, XREAL_1: 106;

      then

       A11: ( |.b1.| / (d1 * ( sqrt 5))) < eps by XCMPLX_1: 78;

      ( |.(b1 * b2).| / Delta) <= r1 by XXREAL_0: 25;

      then ( |.(b1 * b2).| / Delta) < (1 * d1) by A8, XXREAL_0: 2;

      then

       A13: ( |.(b1 * b2).| / d1) < (1 * Delta) by XREAL_1: 113, A1;

      (d1 + 0 ) >= 1 by NAT_1: 19;

      then (1 / d1) <= 1 by XREAL_1: 183;

      then

       A16: (( |.(b1 * b2).| / d1) * (1 / d1)) <= ( |.(b1 * b2).| / d1) by XREAL_1: 153;

      (( |.(b1 * b2).| / d1) * (1 / d1)) = (( |.(b1 * b2).| * 1) / (d1 * d1)) by XCMPLX_1: 76

      .= ( |.(b1 * b2).| / (d1 |^ 2)) by WSIERP_1: 1;

      then

       A17: ( |.(b1 * b2).| / (d1 |^ 2)) < Delta by A13, A16, XXREAL_0: 2;

      reconsider rh0 = (((d1 * ((c1 * a2) - (c2 * a1))) + (n1 * ((c1 * b2) - (c2 * b1)))) / ((a2 * b1) - (a1 * b2))) as Element of REAL by XREAL_0:def 1;

      (d1,n1) are_coprime by WSIERP_1: 22;

      then

      consider s,r be Element of INT such that

       A19: |.(((d1 * s) - (n1 * r)) + rh0).| <= (1 / 2) by Th16;

      set h = n1, k = d1;

      set a = ((((a1 * r) + (b1 * s)) + c1) / ((a1 * k) + (b1 * h))), b = ((((a2 * r) + (b2 * s)) + c2) / ((a2 * k) + (b2 * h)));

      consider u be Integer such that

       A20: |.(a - u).| < 1 & (( |.(a - u).| * |.(b - u).|) <= (1 / 4) or ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2)) by Th41;

      set x = (r - (u * k)), y = (s - (u * h));

      t in IRRAT by SUBSET_1:def 1;

      then

       A22: b1 <> 0 ;

      

       A23: ((a1 * k) + (b1 * h)) <> 0

      proof

        assume ((a1 * k) + (b1 * h)) = 0 ;

        then (( - n1) * b1) = (a1 * d1);

        then (( - n1) / d1) = (a1 / b1) by A22, XCMPLX_1: 94;

        hence contradiction by A2;

      end;

      

       A26: (a - u) = ((((((a1 * x) + (b1 * y)) + c1) / ((a1 * k) + (b1 * h))) + ((u * ((a1 * k) + (b1 * h))) / ((a1 * k) + (b1 * h)))) - u)

      .= ((((((a1 * x) + (b1 * y)) + c1) / ((a1 * k) + (b1 * h))) + (u * 1)) - u) by A23, XCMPLX_1: 89

      .= ((((a1 * x) + (b1 * y)) + c1) / ((a1 * k) + (b1 * h)));

      then

       A27: ( |.(((a1 * x) + (b1 * y)) + c1).| / |.((a1 * k) + (b1 * h)).|) < 1 by A20, COMPLEX1: 67;

      (( |.(((a1 * x) + (b1 * y)) + c1).| / |.((a1 * k) + (b1 * h)).|) * |.((a1 * k) + (b1 * h)).|) = (( |.(((a1 * x) + (b1 * y)) + c1).| * (1 / |.((a1 * k) + (b1 * h)).|)) * |.((a1 * k) + (b1 * h)).|)

      .= |.(((a1 * x) + (b1 * y)) + c1).| by A23, XCMPLX_1: 109;

      then

       A30: |.(((a1 * x) + (b1 * y)) + c1).| < (1 * |.((a1 * k) + (b1 * h)).|) by XREAL_1: 68, A27, A23;

      consider q be 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) + (n1 / d1)).| by RAT_1: 15

      .= |.(((a1 * d1) + (n1 * b1)) / (b1 * d1)).| by A22, XCMPLX_1: 116

      .= ( |.((a1 * d1) + (n1 * b1)).| / |.(b1 * d1).|) by COMPLEX1: 67;

      then

       A36: ( |.((a1 * d1) + (n1 * b1)).| / 1) < ((1 / (( sqrt 5) * (d1 |^ 2))) * |.(b1 * d1).|) by A32, A33, A22, XREAL_1: 113;

      set S1 = (1 / ( sqrt 5));

      

       A37: (1 / (( sqrt 5) * (d1 |^ 2))) = (S1 * (1 / (d1 |^ 2))) by XCMPLX_1: 102

      .= (S1 * (1 / (d1 * d1))) by WSIERP_1: 1

      .= (S1 * ((1 / d1) * (1 / d1))) by XCMPLX_1: 102

      .= ((S1 * (1 / d1)) * (1 / d1));

       |.(b1 * d1).| = ( |.d1.| * |.b1.|) by COMPLEX1: 65

      .= (d1 * |.b1.|);

      

      then

       A39: ((1 / (( sqrt 5) * (d1 |^ 2))) * |.(b1 * d1).|) = (((S1 * (1 / d1)) * ((1 / d1) * d1)) * |.b1.|) by A37

      .= (((S1 * (1 / d1)) * 1) * |.b1.|) by XCMPLX_1: 106

      .= ((1 / (( sqrt 5) * d1)) * |.b1.|) by XCMPLX_1: 102

      .= ( |.b1.| / (d1 * ( sqrt 5)));

      then

       A40: |.((a1 * d1) + (b1 * n1)).| < eps by A36, A11, XXREAL_0: 2;

      

       A41: (b - u) = ((((((a2 * x) + (b2 * y)) + c2) / ((a2 * k) + (b2 * h))) + ((u * ((a2 * k) + (b2 * h))) / ((a2 * k) + (b2 * h)))) - u)

      .= ((((((a2 * x) + (b2 * y)) + c2) / ((a2 * k) + (b2 * h))) + (u * 1)) - u) by A7, XCMPLX_1: 89

      .= ((((a2 * x) + (b2 * y)) + c2) / ((a2 * k) + (b2 * h)));

      set u1 = (((a1 * x) + (b1 * y)) + c1), u2 = (((a2 * x) + (b2 * y)) + c2), v1 = ((a1 * k) + (b1 * h)), v2 = ((a2 * k) + (b2 * h));

      

       A42: ( |.(a - u).| * |.(b - u).|) = (( |.u1.| / |.v1.|) * |.(u2 / v2).|) by COMPLEX1: 67, A41, A26

      .= (( |.u1.| / |.v1.|) * ( |.u2.| / |.v2.|)) by COMPLEX1: 67

      .= (( |.u1.| * |.u2.|) / ( |.v1.| * |.v2.|)) by XCMPLX_1: 76;

      

       A43: |.(t - q).| = |.( - ((a1 / b1) + q1)).| by A32

      .= |.((a1 / b1) + q1).| by COMPLEX1: 52

      .= |.((a1 / b1) + (n1 / d1)).| by RAT_1: 15;

      consider d be Real such that

       A44: (n1 / d1) = (( - (a1 / b1)) + (d / (d1 |^ 2))) and

       A45: |.d.| < S1 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

      .= (Delta / |.b1.|) by COMPLEX1: 67;

      

       A52: (( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) = (( |.b1.| * (1 / (d1 * ( sqrt 5)))) * |.((a2 * d1) + (b2 * n1)).|)

      .= (( |.b1.| * ((1 / d1) * (1 / ( sqrt 5)))) * |.((a2 * d1) + (b2 * n1)).|) by XCMPLX_1: 102

      .= (( |.b1.| * S1) * ( |.(1 / d1).| * |.((a2 * d1) + (b2 * n1)).|))

      .= (( |.b1.| * S1) * |.((1 / d1) * ((a2 * d1) + (b2 * n1))).|) by COMPLEX1: 65

      .= (( |.b1.| * S1) * |.(((a2 * d1) * (1 / d1)) + ((b2 * n1) * (1 / d1))).|)

      .= (( |.b1.| * S1) * |.(a2 + (b2 * (n1 / d1))).|) by XCMPLX_1: 107

      .= (( |.b1.| * S1) * |.((a2 + (b2 * ( - (a1 / b1)))) + (b2 * (d / (d1 |^ 2)))).|) by A44;

      

       A54: ((( |.b1.| * S1) * Delta) / |.b1.|) = ((( |.b1.| * (1 / |.b1.|)) * (1 / ( sqrt 5))) * Delta)

      .= (Delta / ( sqrt 5)) by A22, XCMPLX_1: 106;

      

       A55: (( |.b1.| * S1) * |.(b2 * (d / (d1 |^ 2))).|) = (S1 * ( |.b1.| * |.(b2 * (d / (d1 |^ 2))).|))

      .= (S1 * |.(b1 * (b2 * (d / (d1 |^ 2)))).|) by COMPLEX1: 65

      .= (S1 * |.(d * ((b1 * b2) / (d1 |^ 2))).|)

      .= (S1 * ( |.d.| * |.((b1 * b2) / (d1 |^ 2)).|)) by COMPLEX1: 65

      .= (S1 * ( |.d.| * ( |.(b1 * b2).| / |.(d1 |^ 2).|))) by COMPLEX1: 67

      .= ((S1 * |.d.|) * ( |.(b1 * b2).| / (d1 |^ 2)));

      

       A49: ( |.v1.| * |.v2.|) <= (( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) by A36, A39, XREAL_1: 64;

      

       A57: (( |.b1.| * S1) * |.(b2 * (d / (d1 |^ 2))).|) <= (Delta * ((1 / ( sqrt 5)) * |.d.|)) by A55, A17, SQRT2, XREAL_1: 64;

      (( |.b1.| * (1 / ( sqrt 5))) * ((Delta / |.b1.|) + |.(b2 * (d / (d1 |^ 2))).|)) = ((Delta / ( sqrt 5)) + (( |.b1.| * (1 / ( sqrt 5))) * |.(b2 * (d / (d1 |^ 2))).|)) by A54;

      then

       A59: (( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) <= ((Delta / ( sqrt 5)) + (( |.b1.| * (1 / ( sqrt 5))) * |.(b2 * (d / (d1 |^ 2))).|)) by A52, SQRT2, A51, COMPLEX1: 56, XREAL_1: 64;

      

       A60: ((Delta / ( sqrt 5)) + (( |.b1.| * (1 / ( sqrt 5))) * |.(b2 * (d / (d1 |^ 2))).|)) <= ((Delta / ( sqrt 5)) + (Delta * ((1 / ( sqrt 5)) * |.d.|))) by XREAL_1: 6, A57;

      

       A61: (( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) <= (Delta * ((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 (S1 * |.d.|) < (1 / 5) by A45, XREAL_1: 68;

      then (S1 + (S1 * |.d.|)) < ((1 / 5) + (1 / 2)) by SQRT3, XREAL_1: 8;

      then (S1 + (S1 * |.d.|)) < 1 by XXREAL_0: 2;

      then ((S1 + (S1 * |.d.|)) * Delta) < (1 * Delta) by A1, XREAL_1: 68;

      then

       A66: (( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) < Delta by A61, XXREAL_0: 2;

      

       A71: (a - b) = ((((((a1 * r) + (b1 * s)) + c1) * ((a2 * k) + (b2 * h))) - ((((a2 * r) + (b2 * s)) + c2) * ((a1 * k) + (b1 * h)))) / (((a1 * k) + (b1 * h)) * ((a2 * k) + (b2 * h)))) by XCMPLX_1: 130, A7, A23;

      (((((a1 * r) + (b1 * s)) + c1) * ((a2 * k) + (b2 * h))) - ((((a2 * r) + (b2 * s)) + c2) * ((a1 * k) + (b1 * h)))) = ((((a1 * b2) - (a2 * b1)) * ((r * h) - (s * k))) + (((k * ((c1 * a2) - (c2 * a1))) + (h * ((c1 * b2) - (c2 * b1)))) * 1))

      .= ((((a1 * b2) - (a2 * b1)) * ((r * h) - (s * k))) + (((k * ((c1 * a2) - (c2 * a1))) + (h * ((c1 * b2) - (c2 * b1)))) * ((1 / ((a2 * b1) - (a1 * b2))) * ((a2 * b1) - (a1 * b2))))) by A4, XCMPLX_1: 106

      .= (((a2 * b1) - (a1 * b2)) * (((k * s) - (h * r)) + rh0));

      

      then |.(a - b).| = ( |.( - (((a1 * b2) - (a2 * b1)) * (((k * s) - (h * r)) + rh0))).| / |.(v1 * v2).|) by COMPLEX1: 67, A71

      .= ( |.(((a1 * b2) - (a2 * b1)) * (((k * s) - (h * r)) + rh0)).| / |.(v1 * v2).|) by COMPLEX1: 52

      .= (( |.((a1 * b2) - (a2 * b1)).| * |.(((k * s) - (h * r)) + rh0).|) / |.(v1 * v2).|) by COMPLEX1: 65

      .= ((Delta * |.(((k * s) - (h * r)) + rh0).|) / ( |.v1.| * |.v2.|)) by COMPLEX1: 65;

      

      then

       A73: (((1 / 2) * |.(a - b).|) * ( |.v1.| * |.v2.|)) = (((((1 / 2) * Delta) * |.(((k * s) - (h * r)) + rh0).|) / ( |.v1.| * |.v2.|)) * ( |.v1.| * |.v2.|))

      .= (((1 / 2) * Delta) * |.(((k * s) - (h * r)) + rh0).|) by XCMPLX_1: 87, A23, A7;

      

       A75: (((1 / 2) * Delta) * |.(((k * s) - (h * r)) + rh0).|) <= (((1 / 2) * Delta) * (1 / 2)) by A19, XREAL_1: 64;

      

       A46: ( |.u1.| * |.u2.|) < (Delta / 4)

      proof

        per cases by A20;

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

          then ((( |.u1.| * |.u2.|) * (1 / ( |.v1.| * |.v2.|))) * ( |.v1.| * |.v2.|)) <= ((1 / 4) * ( |.v1.| * |.v2.|)) by A42, XREAL_1: 64;

          then

           A48: ( |.u1.| * |.u2.|) <= ((1 / 4) * ( |.v1.| * |.v2.|)) by XCMPLX_1: 109, A23, A7;

          (( |.v1.| * |.v2.|) * (1 / 4)) <= ((( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) * (1 / 4)) by XREAL_1: 64, A49;

          then

           A67: ( |.u1.| * |.u2.|) <= ((( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) * (1 / 4)) by A48, XXREAL_0: 2;

          ((( |.b1.| / (d1 * ( sqrt 5))) * |.v2.|) * (1 / 4)) < (Delta * (1 / 4)) by XREAL_1: 68, A66;

          hence thesis by A67, XXREAL_0: 2;

        end;

          suppose ( |.(a - u).| * |.(b - u).|) < ( |.(a - b).| / 2);

          then ((( |.u1.| * |.u2.|) * (1 / ( |.v1.| * |.v2.|))) * ( |.v1.| * |.v2.|)) < (( |.(a - b).| / 2) * ( |.v1.| * |.v2.|)) by A23, A7, A42, XREAL_1: 68;

          then ( |.u1.| * |.u2.|) < (((1 / 2) * Delta) * |.(((k * s) - (h * r)) + rh0).|) by XCMPLX_1: 109, A23, A7, A73;

          hence thesis by A75, XXREAL_0: 2;

        end;

      end;

      

       I: x in INT & y in INT by INT_1:def 2;

      

       A77: (( LF (a1,b1,c1)) . (x,y)) = u1 & (( LF (a2,b2,c2)) . (x,y)) = u2 by Def4;

       |.u1.| < eps by A30, A40, XXREAL_0: 2;

      hence thesis by I, A77, A46;

    end;

    theorem :: DIOPHAN2:35

    

     Th47: |.((a1 * b2) - (a2 * b1)).| <> 0 & (a2 / b2) is irrational implies ex x,y be 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

       |.((a2 * b1) - (a1 * b2)).| = |.( - ((a1 * b2) - (a2 * b1))).|

      .= |.((a1 * b2) - (a2 * b1)).| by COMPLEX1: 52;

      hence thesis by Th46;

    end;

    theorem :: DIOPHAN2:36

    

     Th48: ( ZeroPointSet ( LF (a1,b1,c1))) <> {} implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      assume ( ZeroPointSet ( LF (a1,b1,c1))) <> {} ;

      then

      consider p be object such that

       A2: p in ( ZeroPointSet ( LF (a1,b1,c1))) by XBOOLE_0:def 1;

      (( LF (a1,b1,c1)) . p) = 0 & p in ( dom ( LF (a1,b1,c1))) by A2, Th13;

      then

      consider p1,p2 be object such that

       A4: p1 in INT & p2 in INT & p = [p1, p2] by ZFMISC_1:def 2;

      reconsider x = p1, y = p2 as Element of INT by A4;

      (( LF (a1,b1,c1)) . (x,y)) = 0 by A2, Th13, A4;

      then ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4);

      hence thesis;

    end;

    theorem :: DIOPHAN2:37

    

     Th49: ( ZeroPointSet ( LF (a2,b2,c2))) <> {} implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      assume ( ZeroPointSet ( LF (a2,b2,c2))) <> {} ;

      then

      consider p be object such that

       A2: p in ( ZeroPointSet ( LF (a2,b2,c2))) by XBOOLE_0:def 1;

      (( LF (a2,b2,c2)) . p) = 0 & p in ( dom ( LF (a2,b2,c2))) by A2, Th13;

      then

      consider p1,p2 be object such that

       A4: p1 in INT & p2 in INT & p = [p1, p2] by ZFMISC_1:def 2;

      reconsider x = p1, y = p2 as Element of INT by A4;

      (( LF (a2,b2,c2)) . (x,y)) = 0 by A2, Th13, A4;

      then ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4);

      hence thesis;

    end;

    theorem :: DIOPHAN2:38

    

     Th50: |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 <> 0 & (a1 / b1) is rational implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      set Delta = |.((a1 * b2) - (a2 * b1)).|;

      assume that

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and

       A2: b1 <> 0 and

       A3: (a1 / b1) is rational;

      reconsider r1 = (a1 / b1) as Rational by A3;

      set n1 = ( numerator r1);

      set d1 = ( denominator r1);

      reconsider t0 = (b1 / d1) as non zero Real by A2;

      

       A5: b1 = (t0 * d1) by XCMPLX_1: 87;

      

       A6: a1 = ((a1 / b1) * b1) by A2, XCMPLX_1: 87

      .= ((n1 / d1) * b1) by RAT_1: 15

      .= (((n1 / d1) * d1) * t0) by A5

      .= (t0 * n1) 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 be Element of INT such that

       A8: |.(((n1 * x0) - (d1 * y0)) + rh0).| <= (1 / 2) by Th16, WSIERP_1: 22;

      reconsider x = x0, y = ( - y0) as Element of INT by INT_1:def 2;

      (t0 * (((n1 * x) - (d1 * y0)) + rh0)) = (((a1 * x) + ((t0 * d1) * ( - 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.| * |.(((n1 * x0) - (d1 * 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 be 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 + (d1 * s)), y1 = (y - (n1 * 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 * d1) - (b1 * n1)) * 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 * d1) - (b2 * n1)) * s))

      .= ((((a2 * x) + (b2 * y)) + c2) + (((a2 * d1) - (b2 * n1)) * ((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))).|

      .= Delta by COMPLEX1: 52;

      then ( |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| / Delta) <= (1 / 2) by COMPLEX1: 67, A16;

      then (( |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| / Delta) * Delta) <= ((1 / 2) * Delta) by XREAL_1: 64;

      then

       A18: |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * s)).| <= ((1 / 2) * Delta) by A1, XCMPLX_1: 87;

       |.((t0 * (((a2 * x) + (b2 * y)) + c2)) + (((a2 * b1) - (b2 * a1)) * ((s * t0) / t0))).| <= ((1 / 2) * Delta) by A18, XCMPLX_1: 89;

      then |.(t0 * ((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0)))).| <= ((1 / 2) * Delta);

      then

       A20: ( |.t0.| * |.((((a2 * x) + (b2 * y)) + c2) + (((a2 * b1) - (b2 * a1)) * (s / t0))).|) <= ((1 / 2) * Delta) 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) * Delta) / |.t0.|) by A14, A20, XREAL_1: 72;

      (( |.t0.| * (1 / 2)) * (((1 / 2) * Delta) / |.t0.|)) = ( |.t0.| * (((1 / 4) * Delta) / |.t0.|))

      .= (Delta / 4) by XCMPLX_1: 87;

      then ( |.(( LF (a1,b1,c1)) . (x1,y1)).| * |.(( LF (a2,b2,c2)) . (x1,y1)).|) <= (Delta / 4) by A23, A24, XREAL_1: 66;

      hence thesis;

    end;

    theorem :: DIOPHAN2:39

    

     Th51: |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & (a2 / b2) is rational implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      assume

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 & b2 <> 0 & (a2 / b2) is rational;

      

       A4: |.((a2 * b1) - (a1 * b2)).| = |.( - ((a1 * b2) - (a2 * b1))).|

      .= |.((a1 * b2) - (a2 * b1)).| by COMPLEX1: 52;

      then ex x,y be Element of INT st ( |.(( LF (a2,b2,c2)) . (x,y)).| * |.(( LF (a1,b1,c1)) . (x,y)).|) <= ( |.((a2 * b1) - (a1 * b2)).| / 4) by A1, Th50;

      hence thesis by A4;

    end;

    theorem :: DIOPHAN2:40

    

     Th52: |.((a1 * b2) - (a2 * b1)).| <> 0 & b1 = 0 implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      set Delta = |.((a1 * b2) - (a2 * b1)).|;

      assume that

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 and

       A2: b1 = 0 ;

      

       A4: b2 <> 0 by A1, A2;

      per cases ;

        suppose

         A5: (a2 / b2) is irrational & ( ZeroPointSet ( LF (a2,b2,c2))) = {} ;

        for eps holds ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

        proof

          let eps;

          ex x,y be 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 thesis;

        end;

        hence thesis;

      end;

        suppose ( ZeroPointSet ( LF (a2,b2,c2))) <> {} ;

        hence thesis by Th49;

      end;

        suppose (a2 / b2) is rational & ( ZeroPointSet ( LF (a2,b2,c2))) = {} ;

        hence thesis by A1, A4, Th51;

      end;

    end;

    theorem :: DIOPHAN2:41

     |.((a1 * b2) - (a2 * b1)).| <> 0 implies ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

    proof

      assume

       A1: |.((a1 * b2) - (a2 * b1)).| <> 0 ;

      per cases ;

        suppose

         A2: (a1 / b1) is irrational & ( ZeroPointSet ( LF (a1,b1,c1))) = {} ;

        for eps holds ex x,y be Element of INT st ( |.(( LF (a1,b1,c1)) . (x,y)).| * |.(( LF (a2,b2,c2)) . (x,y)).|) <= ( |.((a1 * b2) - (a2 * b1)).| / 4)

        proof

          let eps;

          ex x,y be 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 A1, A2, Th46;

          hence thesis;

        end;

        hence thesis;

      end;

        suppose ( ZeroPointSet ( LF (a1,b1,c1))) <> {} ;

        hence thesis by Th48;

      end;

        suppose (a1 / b1) is rational & ( ZeroPointSet ( LF (a1,b1,c1))) = {} ;

        hence thesis by A1, Th52, Th50;

      end;

    end;