diophan1.miz



    begin

    reserve i,j,k,m,n,m1,n1 for Nat;

    reserve a,r,r1,r2 for Real;

    reserve m0,cn,cd for Integer;

    reserve x1,x2,o for object;

    theorem :: DIOPHAN1:1

    

     Th1: r = (( rfs r) . 0 ) & r = ((( scf r) . 0 ) + (1 / (( rfs r) . 1))) & (( rfs r) . n) = ((( scf r) . n) + (1 / (( rfs r) . (n + 1))))

    proof

      

       A1: (( rfs r) . 1) = (( rfs r) . ( 0 + 1))

      .= (1 / ( frac (( rfs r) . 0 ))) by REAL_3:def 3;

      

       A2: ( frac (( rfs r) . 0 )) = ( frac r) by REAL_3:def 3

      .= (r - (( scf r) . 0 )) by REAL_3: 35;

      

       A4: ( frac (( rfs r) . n)) = ((( rfs r) . n) - [\(( rfs r) . n)/]) by INT_1:def 8;

      (1 / (( rfs r) . (n + 1))) = (1 / (1 / ( frac (( rfs r) . n)))) by REAL_3:def 3

      .= ( frac (( rfs r) . n));

      

      then ((( scf r) . n) + (1 / (( rfs r) . (n + 1)))) = (((( scf r) . n) + (( rfs r) . n)) - [\(( rfs r) . n)/]) by A4

      .= (((( scf r) . n) + (( rfs r) . n)) - (( scf r) . n)) by REAL_3:def 4

      .= (( rfs r) . n);

      hence thesis by REAL_3:def 3, A2, A1;

    end;

    theorem :: DIOPHAN1:2

    

     Th2: r is irrational implies (( rfs r) . n) is irrational

    proof

      assume

       A1: r is irrational;

      set rn = (( rfs r) . n);

      

       A3: (( scf rn) . 0 ) = [\(( rfs rn) . 0 )/] by REAL_3:def 4

      .= [\(( rfs r) . n)/] by REAL_3:def 3

      .= (( scf r) . n) by REAL_3:def 4;

      

       A4: (( scf rn) . m) = (( scf r) . (n + m)) & (( rfs rn) . m) = (( rfs r) . (n + m))

      proof

        defpred P[ Nat] means (( scf rn) . $1) = (( scf r) . (n + $1)) & (( rfs rn) . $1) = (( rfs r) . (n + $1));

        

         A5: P[ 0 ] by REAL_3:def 3, A3;

        

         A6: for m be Nat st P[m] holds P[(m + 1)]

        proof

          let m be Nat;

          assume

           A7: P[m];

          

           A9: (( rfs rn) . (m + 1)) = (1 / ( frac (( rfs rn) . m))) by REAL_3:def 3

          .= (( rfs r) . ((n + m) + 1)) by A7, REAL_3:def 3;

          (( scf rn) . (m + 1)) = [\(( rfs rn) . (m + 1))/] by REAL_3:def 4

          .= (( scf r) . ((n + m) + 1)) by A9, REAL_3:def 4;

          hence thesis by A9;

        end;

        for m be Nat holds P[m] from NAT_1:sch 2( A5, A6);

        hence thesis;

      end;

      assume

       A10: (( rfs r) . n) is rational;

      consider n1 such that

       A12: for m1 st m1 >= n1 holds (( scf rn) . m1) = 0 by A10, REAL_3: 42;

      

       A13: for m1 st m1 >= n1 holds (( scf r) . (n + m1)) = 0

      proof

        let m1;

        assume

         A14: m1 >= n1;

        (( scf r) . (n + m1)) = (( scf rn) . m1) by A4

        .= 0 by A12, A14;

        hence thesis;

      end;

      for m st m >= (n1 + n) holds (( scf r) . m) = 0

      proof

        let m;

        assume

         A15: m >= (n1 + n);

        

         A16: (m - n) >= ((n1 + n) - n) by A15, XREAL_1: 9;

        (m - n) in NAT by A16, INT_1: 3;

        then

        reconsider l = (m - n) as Nat;

        (( scf r) . (n + l)) = 0 by A13, A16;

        hence thesis;

      end;

      hence contradiction by A1, REAL_3: 42;

    end;

    theorem :: DIOPHAN1:3

    

     Th3: r is irrational implies (( rfs r) . n) <> 0 & ((( rfs r) . 1) * (( rfs r) . 2)) <> 0 & (((( scf r) . 1) * (( rfs r) . 2)) + 1) <> 0

    proof

      assume

       A1: r is irrational;

      

       A2: (( rfs r) . n) <> 0

      proof

        assume (( rfs r) . n) = 0 ;

        then

        consider n1 be Nat such that

         A4: (( rfs r) . n1) = 0 ;

        n1 <= m implies (( scf r) . m) = 0 by A4, REAL_3: 28;

        hence contradiction by A1, REAL_3: 42;

      end;

      

       A5: (( rfs r) . 1) <> 0 & (( rfs r) . 2) <> 0 by A1, Th2;

      (( rfs r) . 1) = ((( scf r) . 1) + (1 / (( rfs r) . (1 + 1)))) by Th1;

      

      then ((( rfs r) . 1) * (( rfs r) . 2)) = (((( scf r) . 1) * (( rfs r) . 2)) + ((1 / (( rfs r) . 2)) * (( rfs r) . 2)))

      .= (((( scf r) . 1) * (( rfs r) . 2)) + 1) by XCMPLX_1: 106, A5;

      hence thesis by A2, A5;

    end;

    theorem :: DIOPHAN1:4

    

     Th4: r is irrational implies (( scf r) . n) < (( rfs r) . n) & (( rfs r) . n) < ((( scf r) . n) + 1) & 1 < (( rfs r) . (n + 1))

    proof

      assume r is irrational;

      then

       A2: not (( rfs r) . n) is integer by Th2;

      

       A3: (1 / (( rfs r) . (n + 1))) = (1 / (1 / ( frac (( rfs r) . n)))) by REAL_3:def 3

      .= ( frac (( rfs r) . n));

      

       A4: (1 / (( rfs r) . (n + 1))) > 0 by A2, A3, INT_1: 46;

      

       A5: (( rfs r) . n) = ((( scf r) . n) + (1 / (( rfs r) . (n + 1)))) by Th1;

      

       A6: (((( rfs r) . n) - (( scf r) . n)) + (( scf r) . n)) > ( 0 + (( scf r) . n)) by A2, A3, A5, INT_1: 46, XREAL_1: 8;

      (1 " ) < (((( rfs r) . (n + 1)) " ) " ) by A3, INT_1: 43, A4, XREAL_1: 88;

      hence thesis by A6, A5, A3, INT_1: 43, XREAL_1: 8;

    end;

    theorem :: DIOPHAN1:5

    

     Th5: r is irrational implies 0 < (( scf r) . (n + 1))

    proof

      assume

       A1: r is irrational;

      

       A2: ((( rfs r) . (n + 1)) - 1) > (1 - 1) by A1, Th4, XREAL_1: 14;

      (( rfs r) . (n + 1)) < ((( scf r) . (n + 1)) + 1) by A1, Th4;

      then ((( rfs r) . (n + 1)) - 1) < (((( scf r) . (n + 1)) + 1) - 1) by XREAL_1: 14;

      hence thesis by A2;

    end;

    

     Th6: for n holds (( c_n r) . n) is Integer

    proof

      defpred P[ Nat] means (( c_n r) . $1) is Integer;

      

       A1: for n be Nat st P[n] & P[(n + 1)] holds P[(n + 2)]

      proof

        let n be Nat;

        assume that

         A2: (( c_n r) . n) is Integer and

         A3: (( c_n r) . (n + 1)) is Integer;

        (( c_n r) . (n + 2)) = (((( scf r) . (n + 2)) * (( c_n r) . (n + 1))) + (( c_n r) . n)) by REAL_3:def 5;

        hence thesis by A2, A3;

      end;

      

       A5: P[1]

      proof

        (( c_n r) . 1) = (((( scf r) . 1) * (( scf r) . 0 )) + 1) by REAL_3:def 5;

        hence thesis;

      end;

      

       A6: P[ 0 ]

      proof

        (( c_n r) . 0 ) = (( scf r) . 0 ) by REAL_3:def 5;

        hence thesis;

      end;

      for n be Nat holds P[n] from FIB_NUM:sch 1( A6, A5, A1);

      hence thesis;

    end;

    registration

      let r, n;

      cluster (( c_n r) . n) -> integer;

      coherence by Th6;

    end

    theorem :: DIOPHAN1:6

    

     Th7: r is irrational implies for n holds (( c_d r) . (n + 1)) >= (( c_d r) . n)

    proof

      assume

       A1: r is irrational;

      defpred P[ Nat] means (( c_d r) . $1) <= (( c_d r) . ($1 + 1));

      

       A2: P[ 0 ]

      proof

        

         A3: (( c_d r) . 0 ) = 1 by REAL_3:def 6;

        (( rfs r) . ( 0 + 1)) > 1 by A1, Th4;

        then ((( rfs r) . 1) - 1) > (1 - 1) by XREAL_1: 14;

        then [\(( rfs r) . 1)/] > 0 by INT_1:def 6;

        then (( scf r) . 1) > 0 by REAL_3:def 4;

        then ( 0 + 1) <= (( scf r) . 1) by INT_1: 7;

        hence thesis by A3, REAL_3:def 6;

      end;

      

       A8: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume P[n];

        

         A9: ((( 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) . (n + 1))) by REAL_3:def 6

        .= ((((( scf r) . (n + 2)) - 1) * (( c_d r) . (n + 1))) + (( c_d r) . n));

        

         A10: (( scf r) . (n + 2)) = [\(( rfs r) . (n + 2))/] by REAL_3:def 4;

        (( rfs r) . ((n + 1) + 1)) > 1 by A1, Th4;

        then ((( rfs r) . (n + 2)) - 1) > (1 - 1) by XREAL_1: 14;

        then (( scf r) . (n + 2)) > 0 by A10, INT_1:def 6;

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

        then

         A12: ((( scf r) . (n + 2)) - 1) >= (1 - 1) by XREAL_1: 13;

        (( c_d r) . (n + 1)) >= 0 & (( c_d r) . n) >= 0 by REAL_3: 51;

        then (((( c_d r) . (n + 2)) - (( c_d r) . (n + 1))) + (( c_d r) . (n + 1))) >= ( 0 + (( c_d r) . (n + 1))) by A9, A12, XREAL_1: 6;

        hence thesis;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A8);

      hence thesis;

    end;

    theorem :: DIOPHAN1:7

    

     Th8: r is irrational implies (( c_d r) . n) >= 1

    proof

      assume

       A1: r is irrational;

      defpred P[ Nat] means (( c_d r) . $1) >= 1;

      

       A2: P[ 0 ] by REAL_3:def 6;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: P[n];

        (( c_d r) . (n + 1)) >= (( c_d r) . n) by A1, Th7;

        hence thesis by A4, XXREAL_0: 2;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: DIOPHAN1:8

    r is irrational implies (( c_d r) . (n + 2)) > (( c_d r) . (n + 1))

    proof

      assume

       A1: r is irrational;

      then

       A2: (( scf r) . ((n + 1) + 1)) > 0 by Th5;

      

       A3: (n + 2) >= ( 0 + 1) by XREAL_1: 8;

      

       A4: (( c_d r) . (n + 2)) = (((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) by REAL_3:def 6;

      (( c_d r) . n) > 0 by A1, Th8;

      then

       A5: ((( c_d r) . (n + 2)) - 0 ) > ((((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) - (( c_d r) . n)) by A4, XREAL_1: 15;

      (( c_d r) . (n + 1)) >= 1 by A1, Th8;

      then ((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) >= (( c_d r) . (n + 1)) by A2, A3, REAL_3: 40, XREAL_1: 151;

      hence thesis by A5, XXREAL_0: 2;

    end;

    theorem :: DIOPHAN1:9

    

     Th10: r is irrational implies (( c_d r) . n) >= n

    proof

      assume

       A1: r is irrational;

      defpred P[ Nat] means (( c_d r) . $1) >= $1;

      

       A2: P[ 0 ] by REAL_3:def 6;

      

       A3: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A4: P[n];

        set m = (n - 1);

        per cases ;

          suppose n = 0 ;

          hence thesis by A1, Th8;

        end;

          suppose n > 0 ;

          then

          reconsider m as Nat;

          

           A7: (( scf r) . ((m + 1) + 1)) > 0 by A1, Th5;

          

           A8: (m + 2) >= ( 0 + 1) by XREAL_1: 8;

          (( c_d r) . (m + 1)) >= 1 by A1, Th8;

          then

           A9: ((( scf r) . (m + 2)) * (( c_d r) . (m + 1))) >= (( c_d r) . (m + 1)) by A7, A8, REAL_3: 40, XREAL_1: 151;

          (((( scf r) . (m + 2)) * (( c_d r) . (m + 1))) + (( c_d r) . m)) >= ((( c_d r) . (m + 1)) + (( c_d r) . m)) by A9, XREAL_1: 6;

          then

           A12: (( c_d r) . (m + 2)) >= ((( c_d r) . (m + 1)) + (( c_d r) . m)) by REAL_3:def 6;

          

           A13: ((( c_d r) . (m + 1)) + (( c_d r) . m)) >= (n + (( c_d r) . m)) by A4, XREAL_1: 6;

          (n + (( c_d r) . m)) >= (n + 1) by A1, Th8, XREAL_1: 6;

          then ((( c_d r) . (m + 1)) + (( c_d r) . m)) >= (n + 1) by A13, XXREAL_0: 2;

          hence thesis by A12, XXREAL_0: 2;

        end;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A3);

      hence thesis;

    end;

    theorem :: DIOPHAN1:10

    cn = (( c_n r) . n) & cd = (( c_d r) . n) & cn <> 0 implies (cn,cd) are_coprime

    proof

      (( c_d r) . (n + 1)) in NAT by REAL_3: 50;

      then

      reconsider cd2 = (( c_d r) . (n + 1)) as Integer;

      reconsider cn2 = (( c_n r) . (n + 1)) as Integer;

      assume that

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

       A3: cd = (( c_d r) . n) and

       A4: cn <> 0 ;

      assume

       A5: not ((cn,cd) are_coprime );

      

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

      consider cn0,cd0 be Integer such that

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

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

      (cn gcd cd) <> 0 by A4, INT_2: 5;

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

      then

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

      

       A12: (( - 1) |^ n) = (((cn2 * (cn gcd cd)) * cd0) - (cn * cd2)) by A6, A9

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

      

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

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

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

      .= ((cn gcd cd) * |.((cn2 * cd0) - (cn0 * cd2)).|) by ABSVALUE:def 1;

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

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

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

      hence contradiction by A13;

    end;

    theorem :: DIOPHAN1:11

    

     Th12: r is irrational implies (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) > 0 & (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) - (( c_d r) . n)) > 0

    proof

      assume

       A1: r is irrational;

      then

       A2: (( c_d r) . (n + 1)) >= 1 by Th8;

      (( rfs r) . ((n + 1) + 1)) > 1 by A1, Th4;

      then

       A4: ((( rfs r) . (n + 2)) * (( c_d r) . (n + 1))) > (1 * (( c_d r) . (n + 1))) by A2, XREAL_1: 68;

      then

       A5: ((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) > 1 by A2, XXREAL_0: 2;

      

       A6: ((( c_d r) . n) + 1) >= (1 + 1) by A1, Th8, XREAL_1: 6;

      (( c_d r) . (n + 1)) >= (( c_d r) . n) by A1, Th7;

      then ((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) > (( c_d r) . n) by A4, XXREAL_0: 2;

      then (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) - (( c_d r) . n)) > ((( c_d r) . n) - (( c_d r) . n)) by XREAL_1: 14;

      hence thesis by A5, A6, XREAL_1: 6;

    end;

    theorem :: DIOPHAN1:12

    

     Th13: r is irrational implies ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) > 0

    proof

      assume

       A1: r is irrational;

      then

       A2: (( c_d r) . (n + 1)) >= 1 by Th8;

      (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) > 0 by A1, Th12;

      hence thesis by A2;

    end;

    theorem :: DIOPHAN1:13

    

     Th14: r is irrational implies r = ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))

    proof

      assume

       A1: r is irrational;

      defpred P[ Nat] means r = ((((( c_n r) . ($1 + 1)) * (( rfs r) . ($1 + 2))) + (( c_n r) . $1)) / (((( c_d r) . ($1 + 1)) * (( rfs r) . ($1 + 2))) + (( c_d r) . $1)));

      

       A2: P[ 0 ]

      proof

        

         A3: (( rfs r) . 1) = ((( scf r) . 1) + (1 / (( rfs r) . (1 + 1)))) by Th1;

        

         A4: (((( c_n r) . 1) * (( rfs r) . 2)) + (( c_n r) . 0 )) = (((((( scf r) . 1) * (( scf r) . 0 )) + 1) * (( rfs r) . 2)) + (( c_n r) . 0 )) by REAL_3:def 5

        .= (((((( scf r) . 1) * (( scf r) . 0 )) + 1) * (( rfs r) . 2)) + (( scf r) . 0 )) by REAL_3:def 5

        .= (((( scf r) . 0 ) * (((( scf r) . 1) * (( rfs r) . 2)) + 1)) + (( rfs r) . 2));

        

         A5: (((( c_d r) . 1) * (( rfs r) . 2)) + (( c_d r) . 0 )) = (((( scf r) . 1) * (( rfs r) . 2)) + (( c_d r) . 0 )) by REAL_3:def 6

        .= (((( scf r) . 1) * (( rfs r) . 2)) + 1) by REAL_3:def 6;

        

         A6: (( rfs r) . 2) <> 0 & (((( scf r) . 1) * (( rfs r) . 2)) + 1) <> 0 by A1, Th3;

        ((((( c_n r) . 1) * (( rfs r) . 2)) + (( c_n r) . 0 )) / (((( c_d r) . 1) * (( rfs r) . 2)) + (( c_d r) . 0 ))) = ((((( scf r) . 0 ) * (((( scf r) . 1) * (( rfs r) . 2)) + 1)) + (( rfs r) . 2)) / (((( c_d r) . 1) * (( rfs r) . 2)) + (( c_d r) . 0 ))) by A4

        .= (((( scf r) . 0 ) * ((((( scf r) . 1) * (( rfs r) . 2)) + 1) / (((( scf r) . 1) * (( rfs r) . 2)) + 1))) + ((( rfs r) . 2) / (((( scf r) . 1) * (( rfs r) . 2)) + 1))) by A5

        .= (((( scf r) . 0 ) * 1) + ((( rfs r) . 2) / (((( scf r) . 1) * (( rfs r) . 2)) + 1))) by A6, XCMPLX_1: 60

        .= ((( scf r) . 0 ) + (((( rfs r) . 2) / (( rfs r) . 2)) / ((((( scf r) . 1) * (( rfs r) . 2)) + 1) / (( rfs r) . 2)))) by A6, XCMPLX_1: 55

        .= ((( scf r) . 0 ) + (1 / ((((( scf r) . 1) * (( rfs r) . 2)) + 1) / (( rfs r) . 2)))) by A6, XCMPLX_1: 60

        .= ((( scf r) . 0 ) + (1 / (((( scf r) . 1) * ((( rfs r) . 2) / (( rfs r) . 2))) + (1 / (( rfs r) . 2)))))

        .= ((( scf r) . 0 ) + (1 / (((( scf r) . 1) * 1) + (1 / (( rfs r) . 2))))) by A1, Th3, XCMPLX_1: 60

        .= r by Th1, A3;

        hence thesis;

      end;

      

       A7: for n be Nat st P[n] holds P[(n + 1)]

      proof

        let n be Nat;

        assume

         A8: P[n];

        

         A9: (( rfs r) . (n + 2)) = ((( scf r) . (n + 2)) + (1 / (( rfs r) . ((n + 2) + 1)))) by Th1

        .= ((( scf r) . (n + 2)) + (1 / (( rfs r) . (n + 3))));

        

         A10: 1 = ((( rfs r) . (n + 3)) / (( rfs r) . (n + 3))) by A1, Th3, XCMPLX_1: 60;

        

         A11: (((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) = (((( c_n r) . (n + 1)) * ((( scf r) . (n + 2)) + (1 / (( rfs r) . (n + 3))))) + (( c_n r) . n)) by A9

        .= ((((( scf r) . (n + 2)) * (( c_n r) . (n + 1))) + (( c_n r) . n)) + ((( c_n r) . (n + 1)) * (1 / (( rfs r) . (n + 3)))))

        .= ((( c_n r) . (n + 2)) + ((( c_n r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) by REAL_3:def 5;

        

         A12: (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) = (((( c_d r) . (n + 1)) * ((( scf r) . (n + 2)) + (1 / (( rfs r) . (n + 3))))) + (( c_d r) . n)) by A9

        .= ((((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) + ((( c_d r) . (n + 1)) * (1 / (( rfs r) . (n + 3)))))

        .= ((( c_d r) . (n + 2)) + ((( c_d r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) by REAL_3:def 6;

        r = ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) by A8

        .= (((( c_n r) . (n + 2)) + ((( c_n r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) / ((( c_d r) . (n + 2)) + ((( c_d r) . (n + 1)) * (1 / (( rfs r) . (n + 3)))))) by A11, A12

        .= ((((( c_n r) . (n + 2)) + ((( c_n r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) / ((( c_d r) . (n + 2)) + ((( c_d r) . (n + 1)) * (1 / (( rfs r) . (n + 3)))))) * ((( rfs r) . (n + 3)) / (( rfs r) . (n + 3)))) by A10

        .= ((((( c_n r) . (n + 2)) + ((( c_n r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) * (( rfs r) . (n + 3))) / (((( c_d r) . (n + 2)) + ((( c_d r) . (n + 1)) * (1 / (( rfs r) . (n + 3))))) * (( rfs r) . (n + 3)))) by XCMPLX_1: 76

        .= ((((( c_n r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_n r) . (n + 1)) * ((1 / (( rfs r) . (n + 3))) * (( rfs r) . (n + 3))))) / (((( c_d r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_d r) . (n + 1)) * ((1 / (( rfs r) . (n + 3))) * (( rfs r) . (n + 3))))))

        .= ((((( c_n r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_n r) . (n + 1)) * 1)) / (((( c_d r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_d r) . (n + 1)) * ((1 / (( rfs r) . (n + 3))) * (( rfs r) . (n + 3)))))) by XCMPLX_1: 106, A1, Th3

        .= ((((( c_n r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_n r) . (n + 1)) * 1)) / (((( c_d r) . (n + 2)) * (( rfs r) . (n + 3))) + ((( c_d r) . (n + 1)) * 1))) by XCMPLX_1: 106, A1, Th3

        .= ((((( c_n r) . ((n + 1) + 1)) * (( rfs r) . ((n + 1) + 2))) + (( c_n r) . (n + 1))) / (((( c_d r) . ((n + 1) + 1)) * (( rfs r) . ((n + 1) + 2))) + (( c_d r) . (n + 1))));

        hence thesis;

      end;

      for n be Nat holds P[n] from NAT_1:sch 2( A2, A7);

      hence thesis;

    end;

    theorem :: DIOPHAN1:14

    

     Th15: r is irrational implies (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - r) = ((( - 1) |^ n) / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))))

    proof

      assume

       A1: r is irrational;

      then

       A3: (( c_d r) . (n + 1)) <> 0 by Th8;

      

       A4: (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) <> 0 by A1, Th12;

      

       A5: (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - r) = (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))) by A1, Th14

      .= ((((( c_n r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) - ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) * (( c_d r) . (n + 1)))) / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))) by A3, A4, XCMPLX_1: 130;

      (((( c_n r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) - ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) * (( c_d r) . (n + 1)))) = ((((((( c_n r) . (n + 1)) * (( c_d r) . (n + 1))) * (( rfs r) . (n + 2))) + ((( c_n r) . (n + 1)) * (( c_d r) . n))) - (((( c_n r) . (n + 1)) * (( c_d r) . (n + 1))) * (( rfs r) . (n + 2)))) - ((( c_n r) . n) * (( c_d r) . (n + 1))))

      .= (( - 1) |^ n) by REAL_3: 64;

      hence thesis by A5;

    end;

    theorem :: DIOPHAN1:15

    

     Th16: r is irrational & n is even & n > 0 implies r > ((( c_n r) . n) / (( c_d r) . n))

    proof

      assume

       A1: r is irrational;

      assume

       A2: n is even;

      assume n > 0 ;

      then

      reconsider m = (n - 1) as odd natural number by A2;

      ((( c_d r) . (m + 1)) * (((( c_d r) . (m + 1)) * (( rfs r) . (m + 2))) + (( c_d r) . m))) > 0 by A1, Th13;

      then ((( - 1) |^ m) / ((( c_d r) . (m + 1)) * (((( c_d r) . (m + 1)) * (( rfs r) . (m + 2))) + (( c_d r) . m)))) < 0 ;

      then (((( c_n r) . (m + 1)) / (( c_d r) . (m + 1))) - r) < 0 by A1, Th15;

      then ((((( c_n r) . ((n - 1) + 1)) / (( c_d r) . ((n - 1) + 1))) - r) + r) < ( 0 + r) by XREAL_1: 8;

      hence thesis;

    end;

    theorem :: DIOPHAN1:16

    

     Th17: r is irrational & n is odd implies r < ((( c_n r) . n) / (( c_d r) . n))

    proof

      assume

       A1: r is irrational;

      assume n is odd;

      then

      reconsider m = (n - 1) as even natural number;

      ((( c_d r) . (m + 1)) * (((( c_d r) . (m + 1)) * (( rfs r) . (m + 2))) + (( c_d r) . m))) > 0 by A1, Th13;

      then ((( - 1) |^ m) / ((( c_d r) . (m + 1)) * (((( c_d r) . (m + 1)) * (( rfs r) . (m + 2))) + (( c_d r) . m)))) > 0 ;

      then (((( c_n r) . (m + 1)) / (( c_d r) . (m + 1))) - r) > 0 by A1, Th15;

      then ((((( c_n r) . (m + 1)) / (( c_d r) . (m + 1))) - r) + r) > ( 0 + r) by XREAL_1: 8;

      hence thesis;

    end;

    theorem :: DIOPHAN1:17

    r is irrational & n > 0 implies ( |.(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)))).|

    proof

      assume that

       A1: r is irrational and

       A2: n > 0 ;

      per cases ;

        suppose

         A3: n is even;

        r > ((( c_n r) . n) / (( c_d r) . n)) by A1, A2, A3, Th16;

        then

         A4: (r - ((( c_n r) . n) / (( c_d r) . n))) > (((( c_n r) . n) / (( c_d r) . n)) - ((( c_n r) . n) / (( c_d r) . n))) by XREAL_1: 14;

        (r - ((( c_n r) . n) / (( c_d r) . n))) <> 0 by A1, A2, A3, Th16;

        then |.(r - ((( c_n r) . n) / (( c_d r) . n))).| <> 0 by ABSVALUE: 2;

        then

         A5: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > 0 by COMPLEX1: 46;

        

         A8: (r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) < (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) by A1, A3, Th17, XREAL_1: 14;

        then |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| <> 0 by ABSVALUE: 2;

        then

         A9: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| > 0 by COMPLEX1: 46;

        

         A10: ( |.(r - ((( c_n r) . n) / (( c_d r) . n))).| + |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).|) = ((r - ((( c_n r) . n) / (( c_d r) . n))) + |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).|) by A4, ABSVALUE:def 1

        .= ((r - ((( c_n r) . n) / (( c_d r) . n))) + ( - (r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))))) by A8, ABSVALUE:def 1

        .= ( - (((( c_n r) . n) / (( c_d r) . n)) - ((( 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)))) < 0 by A5, A9, A10;

        hence thesis by A10, ABSVALUE:def 1;

      end;

        suppose

         A11: n is odd;

        then

         A13: (r - ((( c_n r) . n) / (( c_d r) . n))) < (((( c_n r) . n) / (( c_d r) . n)) - ((( c_n r) . n) / (( c_d r) . n))) by XREAL_1: 14, A1, Th17;

        (r - ((( c_n r) . n) / (( c_d r) . n))) <> 0 by A1, A11, Th17;

        then |.(r - ((( c_n r) . n) / (( c_d r) . n))).| <> 0 by ABSVALUE: 2;

        then

         A14: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > 0 by COMPLEX1: 46;

        r > ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) by A1, A11, Th16;

        then

         A18: (r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) > (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) by XREAL_1: 14;

         |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| <> 0 by A18, ABSVALUE: 2;

        then

         A19: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| > 0 by COMPLEX1: 46;

        ( |.(r - ((( c_n r) . n) / (( c_d r) . n))).| + |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).|) = (( - (r - ((( c_n r) . n) / (( c_d r) . n)))) + |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).|) by A13, ABSVALUE:def 1

        .= ((( - r) + ((( c_n r) . n) / (( c_d r) . n))) + (r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))))) by A18, ABSVALUE:def 1

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

        hence thesis by A14, A19, ABSVALUE:def 1;

      end;

    end;

    theorem :: DIOPHAN1:18

    

     Th19: r is irrational implies |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > 0

    proof

      assume

       A1: r is irrational;

      assume not |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > 0 ;

      then |.(r - ((( c_n r) . n) / (( c_d r) . n))).| = 0 by COMPLEX1: 46;

      then

       A3: (r - ((( c_n r) . n) / (( c_d r) . n))) = 0 by COMPLEX1: 45;

      (( c_d r) . n) in NAT by REAL_3: 50;

      hence contradiction by A1, A3;

    end;

    theorem :: DIOPHAN1:19

    r is irrational implies (( c_d r) . (n + 2)) >= (2 * (( c_d r) . n))

    proof

      assume

       A1: r is irrational;

      then (( scf r) . ((n + 1) + 1)) > 0 by Th5;

      then

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

      

       A5: 0 < (( c_d r) . n) by A1, Th8;

      (( c_d r) . n) <= (( c_d r) . (n + 1)) by A1, Th7;

      then ((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) >= (1 * (( c_d r) . n)) by A4, A5, XREAL_1: 66;

      then (((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) >= ((1 * (( c_d r) . n)) + (( c_d r) . n)) by XREAL_1: 6;

      hence thesis by REAL_3:def 6;

    end;

    theorem :: DIOPHAN1:20

    

     Th21: r is irrational implies |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| < (1 / ((( c_d r) . (n + 1)) * (( c_d r) . (n + 2))))

    proof

      assume

       A1: r is irrational;

      then

       A2: (( c_d r) . (n + 1)) >= 1 by Th8;

      

       A3: (( c_d r) . ((n + 1) + 1)) >= 1 by A1, Th8;

      ((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) < ((( rfs r) . (n + 2)) * (( c_d r) . (n + 1))) by A1, Th4, A2, XREAL_1: 68;

      then (((( scf r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) < (((( rfs r) . (n + 2)) * (( c_d r) . (n + 1))) + (( c_d r) . n)) by XREAL_1: 8;

      then

       A5: (( c_d r) . (n + 2)) < (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) by REAL_3:def 6;

      then

       A6: ((( c_d r) . (n + 1)) * (( c_d r) . (n + 2))) < ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) by A2, XREAL_1: 68;

       |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| = |.(( - 1) * (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) - r)).|

      .= |.(( - 1) * ((( - 1) |^ n) / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))))).| by A1, Th15

      .= |.((( - 1) * (( - 1) |^ n)) / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))).|

      .= |.((( - 1) |^ (n + 1)) / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))).| by NEWTON: 6

      .= ( |.(( - 1) |^ (n + 1)).| / |.((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))).|) by COMPLEX1: 67

      .= (1 / |.((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))).|) by SERIES_2: 1

      .= (1 / ((( c_d r) . (n + 1)) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))) by A2, A3, A5, COMPLEX1: 43;

      hence thesis by A6, A2, A3, XREAL_1: 88;

    end;

    theorem :: DIOPHAN1:21

    

     Th22: r is irrational implies |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).| < |.((r * (( c_d r) . n)) - (( c_n r) . n)).| & |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| < |.(r - ((( c_n r) . n) / (( c_d r) . n))).|

    proof

      assume

       A1: r is irrational;

      

      then

       A2: r = ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) by Th14

      .= ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) * (1 / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))));

      

       A3: (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)) <> 0 by A1, Th12;

      

       A4: (((r * (( c_d r) . (n + 1))) * (( rfs r) . (n + 2))) + (r * (( c_d r) . n))) = ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) * ((1 / (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n))) * (((( c_d r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_d r) . n)))) by A2

      .= ((((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n)) * 1) by A3, XCMPLX_1: 106

      .= (((( c_n r) . (n + 1)) * (( rfs r) . (n + 2))) + (( c_n r) . n));

      

       A6: ( - ((r * (( c_d r) . n)) - (( c_n r) . n))) = (((r * (( c_d r) . (n + 1))) * (( rfs r) . (n + 2))) - ((( c_n r) . (n + 1)) * (( rfs r) . (n + 2)))) by A4

      .= ((( rfs r) . (n + 2)) * ((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))));

      

       A7: 1 < (( rfs r) . ((n + 1) + 1)) by A1, Th4;

      

       A8: |.((r * (( c_d r) . n)) - (( c_n r) . n)).| = |.( - ((r * (( c_d r) . n)) - (( c_n r) . n))).| by COMPLEX1: 52

      .= |.((( rfs r) . (n + 2)) * ((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1)))).| by A6

      .= ( |.(( rfs r) . (n + 2)).| * |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).|) by COMPLEX1: 65

      .= ((( rfs r) . (n + 2)) * |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).|) by A7, COMPLEX1: 43;

      

       A9: (( c_d r) . (n + 1)) >= 1 & (( c_d r) . n) >= 1 by A1, Th8;

       |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| > 0 by A1, Th19;

      then

       A11: (r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) <> 0 by COMPLEX1: 47;

      

       A12: ((r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))) * (( c_d r) . (n + 1))) = ((r * (( c_d r) . (n + 1))) - (((( c_n r) . (n + 1)) / (( c_d r) . (n + 1))) * (( c_d r) . (n + 1))))

      .= ((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))) by A9, XCMPLX_1: 87;

      then

       A13: |.((r * (( c_d r) . n)) - (( c_n r) . n)).| > |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).| by A7, A8, A9, A11, COMPLEX1: 47, XREAL_1: 155;

      

       A14: |.(r - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| = |.(((r * (( c_d r) . (n + 1))) / (( c_d r) . (n + 1))) - ((( c_n r) . (n + 1)) / (( c_d r) . (n + 1)))).| by A9, XCMPLX_1: 89

      .= |.(((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))) / (( c_d r) . (n + 1))).|

      .= ( |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).| / |.(( c_d r) . (n + 1)).|) by COMPLEX1: 67

      .= ( |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).| / (( c_d r) . (n + 1))) by A9, COMPLEX1: 43;

      

       A15: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| = |.(((r * (( c_d r) . n)) / (( c_d r) . n)) - ((( c_n r) . n) / (( c_d r) . n))).| by A9, XCMPLX_1: 89

      .= |.(((r * (( c_d r) . n)) - (( c_n r) . n)) / (( c_d r) . n)).|

      .= ( |.((r * (( c_d r) . n)) - (( c_n r) . n)).| / |.(( c_d r) . n).|) by COMPLEX1: 67

      .= ( |.((r * (( c_d r) . n)) - (( c_n r) . n)).| / (( c_d r) . n)) by A9, COMPLEX1: 43;

      

       A16: ( |.((r * (( c_d r) . (n + 1))) - (( c_n r) . (n + 1))).| / (( c_d r) . (n + 1))) < ( |.((r * (( c_d r) . n)) - (( c_n r) . n)).| / (( c_d r) . (n + 1))) by A9, A13, XREAL_1: 74;

       |.((r * (( c_d r) . n)) - (( c_n r) . n)).| >= 0 by COMPLEX1: 46;

      then ( |.((r * (( c_d r) . n)) - (( c_n r) . n)).| / (( c_d r) . (n + 1))) <= ( |.((r * (( c_d r) . n)) - (( c_n r) . n)).| / (( c_d r) . n)) by A1, Th7, A9, XREAL_1: 118;

      hence thesis by A7, A8, A9, A11, A12, A14, A15, A16, COMPLEX1: 47, XREAL_1: 155, XXREAL_0: 2;

    end;

    theorem :: DIOPHAN1:22

    

     Th23: r is irrational & m > n implies |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > |.(r - ((( c_n r) . m) / (( c_d r) . m))).|

    proof

      assume that

       A1: r is irrational and

       A3: m > n;

      defpred P[ Nat] means |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > |.(r - ((( c_n r) . ((n + 1) + $1)) / (( c_d r) . ((n + 1) + $1)))).|;

      

       A4: P[ 0 ] by A1, Th22;

      

       A5: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume P[k];

        then |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > |.(r - ((( c_n r) . (((n + 1) + k) + 1)) / (( c_d r) . (((n + 1) + k) + 1)))).| by A1, Th22, XXREAL_0: 2;

        hence thesis;

      end;

      

       A8: for k be Nat holds P[k] from NAT_1:sch 2( A4, A5);

      (m - n) > (n - n) by A3, XREAL_1: 14;

      then (m - n) >= ( 0 + 1) by INT_1: 7;

      then

       A9: ((m - n) - 1) >= (1 - 1) by XREAL_1: 9;

      reconsider i = ((m - n) - 1) as Integer;

      i in NAT by A9, INT_1: 3;

      then

      reconsider i as Nat;

       |.(r - ((( c_n r) . n) / (( c_d r) . n))).| > |.(r - ((( c_n r) . ((n + 1) + i)) / (( c_d r) . ((n + 1) + i)))).| by A8;

      hence thesis;

    end;

    theorem :: DIOPHAN1:23

    

     Th24: r is irrational implies |.(r - ((( c_n r) . n) / (( c_d r) . n))).| < (1 / ((( c_d r) . n) |^ 2))

    proof

      assume

       A1: r is irrational;

       |.(r - ((( c_n r) . n) / (( c_d r) . n))).| < (1 / ((( c_d r) . n) |^ 2))

      proof

        per cases ;

          suppose

           A3: n = 0 ;

          

          then

           A6: |.(r - ((( c_n r) . n) / (( c_d r) . n))).| = |.(r - ((( c_n r) . 0 ) / 1)).| by REAL_3:def 6

          .= |.(r - (( scf r) . 0 )).| by REAL_3:def 5

          .= |.(r - [\(( rfs r) . 0 )/]).| by REAL_3:def 4

          .= |.(r - [\r/]).| by REAL_3:def 3

          .= |.( frac r).| by INT_1:def 8

          .= ( frac r) by ABSVALUE:def 1, INT_1: 43;

          (1 / ((( c_d r) . n) |^ 2)) = (1 / ((( c_d r) . 0 ) |^ 2)) by A3

          .= (1 / (1 |^ 2)) by REAL_3:def 6

          .= 1;

          hence thesis by A6, INT_1: 43;

        end;

          suppose

           A8: n > 0 ;

          set m = (n - 1);

          reconsider m as Nat by A8;

          

           A10: (( c_d r) . (m + 1)) >= 1 by A1, Th8;

          then ((( c_d r) . (m + 1)) * (( c_d r) . (m + 1))) >= 1 by XREAL_1: 159;

          then

           A12: ((( c_d r) . (m + 1)) |^ 2) >= 1 by WSIERP_1: 1;

          ((( c_d r) . ((m + 1) + 1)) * (( c_d r) . (m + 1))) >= ((( c_d r) . (m + 1)) * (( c_d r) . (m + 1))) by A1, A10, Th7, XREAL_1: 64;

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

          then (1 / ((( c_d r) . (m + 1)) * (( c_d r) . (m + 2)))) <= (1 / ((( c_d r) . (m + 1)) |^ 2)) by A12, XREAL_1: 85;

          hence thesis by A1, XXREAL_0: 2, Th21;

        end;

      end;

      hence thesis;

    end;

    theorem :: DIOPHAN1:24

    for S be Subset of RAT , r st r is irrational & S = { p where p be Element of RAT : |.(r - p).| < (1 / (( denominator p) |^ 2)) } holds S is infinite

    proof

      let S be Subset of RAT , r;

      assume that

       A1: r is irrational and

       A2: S = { p where p be Element of RAT : |.(r - p).| < (1 / (( denominator p) |^ 2)) };

      deffunc F( Nat) = ((( c_n r) . ($1 + 1)) / (( c_d r) . ($1 + 1)));

      consider f be Real_Sequence such that

       A3: for n be Nat holds (f . n) = F(n) from SEQ_1:sch 1;

      for o be Real st o in ( rng f) holds o in S

      proof

        let o be Real;

        assume o in ( rng f);

        then

        consider i be object such that

         A6: i in ( dom f) and

         A7: o = (f . i) by FUNCT_1:def 3;

        reconsider i as Nat by A6;

        

         A8: o = F(i) by A7, A3

        .= ((( c_n r) . (i + 1)) / (( c_d r) . (i + 1)));

        

         A9: (( c_d r) . (i + 1)) in NAT by REAL_3: 50;

        

         A11: o in RAT by A8, A9, RAT_1:def 1;

        reconsider o as Rational by A8, A9;

        set cn = (( c_n r) . (i + 1));

        set cd = (( c_d r) . (i + 1));

        reconsider cd as Integer by A9;

        o = (cn / cd) & cd <> 0 by A1, Th8, A8;

        then

        consider m0 such that cn = (( numerator o) * m0) and

         A14: cd = (( denominator o) * m0) by RAT_1: 28;

        

         A19: (cd |^ 2) = (cd * cd) by WSIERP_1: 1

        .= (cd * (( denominator o) * m0)) by A14

        .= (((( denominator o) * ( denominator o)) * m0) * m0) by A14

        .= (((( denominator o) |^ 2) * m0) * m0) by WSIERP_1: 1

        .= ((( denominator o) |^ 2) * (m0 * m0))

        .= ((( denominator o) |^ 2) * (m0 |^ 2)) by WSIERP_1: 1;

        

         A20: m0 <> 0 by A14, A1, Th8;

        (m0 * m0) = (m0 ^2 ) by SQUARE_1:def 1;

        then

         A22: (m0 ^2 ) >= ( 0 + 1) by A20, SQUARE_1: 12, INT_1: 7;

        

         A23: (m0 |^ 2) = (m0 * m0) by WSIERP_1: 1

        .= (m0 ^2 ) by SQUARE_1:def 1;

        (( denominator o) |^ 2) <= ((( denominator o) |^ 2) * (m0 ^2 )) by A22, XREAL_1: 151;

        then (1 / (( denominator o) |^ 2)) >= (1 / ((( denominator o) |^ 2) * (m0 ^2 ))) by XREAL_1: 85;

        then |.(r - o).| < (1 / (( denominator o) |^ 2)) by A1, A8, A19, Th24, A23, XXREAL_0: 2;

        hence thesis by A2, A11;

      end;

      then

       A28: ( rng f) c= S;

      reconsider f as Function of NAT , REAL ;

      

       A29: f is one-to-one

      proof

        for n1,n2 be object st n1 in ( dom f) & n2 in ( dom f) & (f . n1) = (f . n2) holds n1 = n2

        proof

          let n1,n2 be object such that

           A31: n1 in ( dom f) and

           A32: n2 in ( dom f) and

           A33: (f . n1) = (f . n2);

          consider m1 be Nat such that

           A34: n1 = m1 by A31;

          consider m2 be Nat such that

           A35: n2 = m2 by A32;

          

           A36: (f . m1) = (f . n1) by A34

          .= (f . m2) by A33, A35;

          

           A37: ((( c_n r) . (m1 + 1)) / (( c_d r) . (m1 + 1))) = (f . m1) by A3

          .= F(m2) by A36, A3

          .= ((( c_n r) . (m2 + 1)) / (( c_d r) . (m2 + 1)));

          assume n1 <> n2;

          per cases by A34, A35, XXREAL_0: 1;

            suppose m1 > m2;

            then (m1 + 1) > (m2 + 1) by XREAL_1: 8;

            then |.(r - ((( c_n r) . (m1 + 1)) / (( c_d r) . (m1 + 1)))).| < |.(r - ((( c_n r) . (m2 + 1)) / (( c_d r) . (m2 + 1)))).| by A1, Th23;

            hence contradiction by A37;

          end;

            suppose m1 < m2;

            then (m1 + 1) < (m2 + 1) by XREAL_1: 8;

            then |.(r - ((( c_n r) . (m1 + 1)) / (( c_d r) . (m1 + 1)))).| > |.(r - ((( c_n r) . (m2 + 1)) / (( c_d r) . (m2 + 1)))).| by A1, Th23;

            hence contradiction by A37;

          end;

        end;

        hence thesis;

      end;

      ( dom f) is infinite by FUNCT_2:def 1;

      hence thesis by A28, A29, CARD_1: 59;

    end;

    theorem :: DIOPHAN1:25

    r is irrational implies ( cocf r) is convergent & ( lim ( cocf r)) = r

    proof

      assume

       A1: r is irrational;

      

       A2: for p be Real st 0 < p holds ex n st for m st n <= m holds |.((( cocf r) . m) - r).| < p

      proof

        let p be Real;

        assume

         A3: p > 0 ;

        then

         A4: ( sqrt p) > 0 by SQUARE_1: 25;

        

         A7: [/(1 / ( sqrt p))\] >= (1 / ( sqrt p)) by INT_1:def 7;

         [/(1 / ( sqrt p))\] > 0 by A4, INT_1:def 7;

        then [/(1 / ( sqrt p))\] in NAT by INT_1: 3;

        then

        consider n such that

         A9: n = [/(1 / ( sqrt p))\];

        

         A10: n > 0 by A4, INT_1:def 7, A9;

        for k be Nat st k >= n holds |.((( cocf r) . k) - r).| < p

        proof

          let k be Nat;

          assume

           A12: k >= n;

          

           A13: (( cocf r) . k) = ((( c_n r) /" ( c_d r)) . k) by REAL_3:def 7

          .= ((( c_n r) . k) * ((( c_d r) " ) . k)) by SEQ_1: 8

          .= ((( c_n r) . k) / (( c_d r) . k)) by VALUED_1: 10;

          

           A14: |.((( cocf r) . k) - r).| = |.( - ((( cocf r) . k) - r)).| by COMPLEX1: 52

          .= |.(r - ((( c_n r) . k) / (( c_d r) . k))).| by A13;

          ((1 / ( sqrt p)) ^2 ) = ((( sqrt p) " ) * (( sqrt p) " )) by SQUARE_1:def 1

          .= ((( sqrt p) * ( sqrt p)) " ) by XCMPLX_1: 204

          .= ((( sqrt p) ^2 ) " ) by SQUARE_1:def 1

          .= (p " ) by A3, SQUARE_1:def 2;

          then (n ^2 ) >= (p " ) by A4, A7, SQUARE_1: 15, A9;

          then

           A16: ((n ^2 ) " ) <= ((p " ) " ) by A3, XREAL_1: 85;

          (k ^2 ) >= (n ^2 ) by A12, SQUARE_1: 15;

          then

           A18: ((k ^2 ) " ) <= ((n ^2 ) " ) by A10, SQUARE_1: 12, XREAL_1: 85;

          

           A19: ((( c_d r) . k) ^2 ) = ((( c_d r) . k) * (( c_d r) . k)) by SQUARE_1:def 1

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

          

           A20: ((( c_d r) . k) ^2 ) >= (k ^2 ) by A1, Th10, SQUARE_1: 15;

          (((( c_d r) . k) ^2 ) " ) = (((( c_d r) . k) |^ 2) " ) by A19

          .= (1 / ((( c_d r) . k) |^ 2));

          then (1 / ((( c_d r) . k) |^ 2)) <= ((k ^2 ) " ) by A12, A10, SQUARE_1: 12, XREAL_1: 85, A20;

          then (1 / ((( c_d r) . k) |^ 2)) <= ((n ^2 ) " ) by A18, XXREAL_0: 2;

          then (1 / ((( c_d r) . k) |^ 2)) <= p by A16, XXREAL_0: 2;

          hence thesis by XXREAL_0: 2, A1, Th24, A14;

        end;

        hence thesis;

      end;

      ( cocf r) is convergent by A2, SEQ_2:def 6;

      hence thesis by A2, SEQ_2:def 7;

    end;

    begin

    registration

      cluster 1 _greater for Nat;

      existence

      proof

        take 2;

        thus thesis;

      end;

    end

    reserve t for 1 _greater Nat;

    

     Lm1: t > 0 & t > 1 & (t " ) > 0 & (t * (t " )) = 1

    proof

      t is 1 _greater;

      hence thesis by XCMPLX_0:def 7;

    end;

    definition

      let t;

      :: DIOPHAN1:def1

      func Equal_Div_interval (t) -> SetSequence of REAL means

      : Def1: for n be Nat holds (it . n) = [.(n / t), ((n / t) + (t " )).[;

      existence

      proof

        deffunc F( Element of NAT ) = ( halfline_fin (($1 / t),(($1 / t) + (t " ))));

        consider g be SetSequence of REAL such that

         A1: for x be Element of NAT holds (g . x) = F(x) from FUNCT_2:sch 4;

        take g;

        let n be Nat;

        n in NAT by ORDINAL1:def 12;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let i1,i2 be SetSequence of REAL ;

        assume

         A2: for n be Nat holds (i1 . n) = [.(n / t), ((n / t) + (t " )).[;

        assume

         A3: for n be Nat holds (i2 . n) = [.(n / t), ((n / t) + (t " )).[;

        now

          let n be Element of NAT ;

          (i1 . n) = [.(n / t), ((n / t) + (t " )).[ by A2;

          hence (i1 . n) = (i2 . n) by A3;

        end;

        hence i1 = i2;

      end;

    end

    theorem :: DIOPHAN1:26

    

     Lm2: ( [. 0 , ((k + 1) / t).[ \/ [.((k + 1) / t), ((k + 2) / t).[) = [. 0 , ((k + 2) / t).[

    proof

       0 <= ((k + 1) / t) & ((k + 1) / t) <= ((k + 2) / t)

      proof

        (k + 1) <= ((k + 1) + 1) by XREAL_1: 31;

        hence thesis by XREAL_1: 64;

      end;

      hence thesis by XXREAL_1: 168;

    end;

    theorem :: DIOPHAN1:27

    

     Lm3: (( Partial_Union ( Equal_Div_interval t)) . i) = [. 0 , ((i + 1) / t).[

    proof

      defpred P[ Nat] means (( Partial_Union ( Equal_Div_interval t)) . $1) = [. 0 , (($1 + 1) / t).[;

      

       A1: for k be Nat st P[k] holds P[(k + 1)]

      proof

        let k be Nat;

        assume

         A2: (( Partial_Union ( Equal_Div_interval t)) . k) = [. 0 , ((k + 1) / t).[;

        (( Partial_Union ( Equal_Div_interval t)) . (k + 1)) = ((( Partial_Union ( Equal_Div_interval t)) . k) \/ (( Equal_Div_interval t) . (k + 1))) by PROB_3:def 2

        .= ( [. 0 , ((k + 1) / t).[ \/ [.((k + 1) / t), (((k + 1) / t) + (t " )).[) by Def1, A2

        .= [. 0 , ((k + 2) / t).[ by Lm2;

        hence thesis;

      end;

      (( Partial_Union ( Equal_Div_interval t)) . 0 ) = (( Equal_Div_interval t) . 0 ) by PROB_3:def 2

      .= [.( 0 / t), (( 0 / t) + (t " )).[ by Def1

      .= [. 0 , (t " ).[;

      then

       A3: P[ 0 ];

      for n be Nat holds P[n] from NAT_1:sch 2( A3, A1);

      hence thesis;

    end;

    theorem :: DIOPHAN1:28

    

     Lm4: for r be Real, i be Nat st [\(r * t)/] = i holds r in (( Equal_Div_interval t) . i)

    proof

      let r be Real;

      let i be Nat;

      assume [\(r * t)/] = i;

      then

       A3: i <= (r * t) & ((r * t) - 1) < i by INT_1:def 6;

      then (i / t) <= ((r * t) / t) by XREAL_1: 64;

      then (i * (t " )) <= (r * (t * (t " )));

      then

       A6: (i * (t " )) <= (r * 1) by Lm1;

      

       A7: (((r * t) - 1) + 1) < (i + 1) by A3, XREAL_1: 8;

       0 < (t " ) by Lm1;

      then ((r * t) * (t " )) < ((i + 1) * (t " )) by A7, XREAL_1: 68;

      then (r * (t * (t " ))) < ((i + 1) * (t " ));

      then (r * 1) < ((i + 1) / t) by Lm1;

      then r in [.(i / t), ((i / t) + (t " )).[ by A6, XXREAL_1: 3;

      hence thesis by Def1;

    end;

    theorem :: DIOPHAN1:29

    

     Lm5: r1 in (( Equal_Div_interval t) . i) & r2 in (( Equal_Div_interval t) . i) implies |.(r1 - r2).| < (t " )

    proof

      assume that

       A2: r1 in (( Equal_Div_interval t) . i) and

       A3: r2 in (( Equal_Div_interval t) . i);

      

       A5: r1 in [.(i / t), ((i / t) + (t " )).[ & r1 in [.(i / t), ((i / t) + (t " )).[ & r2 in [.(i / t), ((i / t) + (t " )).[ by A2, A3, Def1;

      then

       A6: (i / t) <= r1 & (i / t) <= r2 & r1 < ((i / t) + (t " )) & r2 < ((i / t) + (t " )) by XXREAL_1: 3;

      per cases by XXREAL_0: 1;

        suppose r1 = r2;

        then |.(r1 - r2).| = 0 by ABSVALUE: 2;

        hence thesis by Lm1;

      end;

        suppose r1 > r2;

        then

         A9: (r1 - r2) > 0 by XREAL_1: 50;

        (((i * (t " )) + (t " )) - (i * (t " ))) > (r1 - r2) by A6, XREAL_1: 14;

        hence thesis by A9, ABSVALUE:def 1;

      end;

        suppose

         A10: r2 > r1;

        r2 < ((i * (t " )) + (t " )) by A5, XXREAL_1: 3;

        then

         A12: (((i * (t " )) + (t " )) - r1) > (r2 - r1) by XREAL_1: 14;

        (i * (t " )) <= r1 by A5, XXREAL_1: 3;

        then

         A13: (((i * (t " )) + (t " )) - (i * (t " ))) >= (((i * (t " )) + (t " )) - r1) by XREAL_1: 13;

         |.(r1 - r2).| = ( - (r1 - r2)) by A10, XREAL_1: 49, ABSVALUE:def 1;

        hence thesis by A13, A12, XXREAL_0: 2;

      end;

    end;

    theorem :: DIOPHAN1:30

    

     Lm6: (( Partial_Union ( Equal_Div_interval t)) . (t - 1)) = [. 0 , 1.[

    proof

      

       A0: 0 <= (t - 1) by Lm1, XREAL_1: 50;

      (( Partial_Union ( Equal_Div_interval t)) . (t - 1)) = [. 0 , (((t - 1) + 1) / t).[ by A0, Lm3

      .= [. 0 , 1.[ by Lm1;

      hence thesis;

    end;

    theorem :: DIOPHAN1:31

    

     Lm7: for r be Real st r in [. 0 , 1.[ holds ex i be Nat st i <= (t - 1) & r in (( Equal_Div_interval t) . i)

    proof

      let r be Real;

      assume r in [. 0 , 1.[;

      then

       A2: r in (( Partial_Union ( Equal_Div_interval t)) . (t - 1)) by Lm6;

      

       A3: (t - 1) > 0 by Lm1, XREAL_1: 50;

      (t - 1) in NAT by A3, INT_1: 3;

      hence thesis by A2, PROB_3: 13;

    end;

    theorem :: DIOPHAN1:32

    

     Lm8: for r be Real, i be Nat st r in (( Equal_Div_interval t) . i) holds [\(r * t)/] = i

    proof

      let r be Real;

      let i be Nat;

      assume

       A1: r in (( Equal_Div_interval t) . i);

      r in [.(i / t), ((i / t) + (t " )).[ by A1, Def1;

      then

       A3: (i / t) <= r & r < ((i / t) + (t " )) by XXREAL_1: 3;

      then ((i * (t " )) * t) <= (r * t) by XREAL_1: 64;

      then (i * ((t " ) * t)) <= (r * t);

      then

       A4: (i * 1) <= (r * t) by Lm1;

      t > 0 by Lm1;

      then (r * t) < (((i + 1) * (t " )) * t) by A3, XREAL_1: 68;

      then (r * t) < ((i + 1) * ((t " ) * t));

      then

       A6: (r * t) < ((i + 1) * 1) by Lm1;

      i <= (r * t) & ((r * t) - 1) < ((i + 1) - 1) by A4, A6, XREAL_1: 9;

      hence thesis by INT_1:def 6;

    end;

    theorem :: DIOPHAN1:33

    

     Lm9: for r be Real st r in [. 0 , 1.[ holds ex i be Nat st i <= (t - 1) & [\(r * t)/] = i

    proof

      let r be Real;

      assume r in [. 0 , 1.[;

      then

      consider i be Nat such that

       A2: i <= (t - 1) and

       A3: r in (( Equal_Div_interval t) . i) by Lm7;

      thus thesis by A2, Lm8, A3;

    end;

    definition

      let t, a;

      :: DIOPHAN1:def2

      func F_dp1 (t,a) -> FinSequence of ( Segm t) means

      : Def4: ( len it ) = (t + 1) & for i st i in ( dom it ) holds (it . i) = [\(( frac ((i - 1) * a)) * t)/];

      existence

      proof

        deffunc F( Nat) = [\(( frac (($1 - 1) * a)) * t)/];

        consider z be FinSequence such that

         A1: ( len z) = (t + 1) & for k be Nat st k in ( dom z) holds (z . k) = F(k) from FINSEQ_1:sch 2;

        take z;

        z is FinSequence of ( Segm t)

        proof

          

           A2: for y be object st y in ( rng z) holds y in ( Segm t)

          proof

            let y be object;

            assume y in ( rng z);

            then

            consider i be object such that

             A4: i in ( dom z) and

             A5: y = (z . i) by FUNCT_1:def 3;

            ( dom z) = ( Seg ( len z)) by FINSEQ_1:def 3

            .= ( Seg (t + 1)) by A1;

            then

            consider i0 be Nat such that

             A7: i0 = i and 1 <= i0 and i0 <= (t + 1) by A4;

            reconsider i as Nat by A7;

            

             A8: (z . i) = F(i) by A1, A4

            .= [\(( frac ((i - 1) * a)) * t)/];

             0 <= ( frac ((i - 1) * a)) & ( frac ((i - 1) * a)) < 1 by INT_1: 43;

            then

            consider j be Nat such that

             A10: j <= (t - 1) and

             A11: [\(( frac ((i - 1) * a)) * t)/] = j by Lm9, XXREAL_1: 3;

            j < ((t - 1) + 1) by A10, XREAL_1: 39;

            hence thesis by A5, NAT_1: 44, A11, A8;

          end;

          ( rng z) c= ( Segm t) by A2;

          hence thesis by FINSEQ_1:def 4;

        end;

        hence thesis by A1;

      end;

      uniqueness

      proof

        let z1,z2 be FinSequence of ( Segm t) such that

         A13: ( len z1) = (t + 1) and

         A14: for i be Nat st i in ( dom z1) holds (z1 . i) = [\(( frac ((i - 1) * a)) * t)/] and

         A15: ( len z2) = (t + 1) and

         A16: for i be Nat st i in ( dom z2) holds (z2 . i) = [\(( frac ((i - 1) * a)) * t)/];

        

         A17: ( dom z1) = ( Seg ( len z1)) by FINSEQ_1:def 3

        .= ( dom z2) by A13, A15, FINSEQ_1:def 3;

        for x be Nat st x in ( dom z1) holds (z1 . x) = (z2 . x)

        proof

          let x be Nat;

          assume

           A18: x in ( dom z1);

          then

          reconsider x9 = x as Element of NAT ;

          

          thus (z1 . x) = [\(( frac ((x9 - 1) * a)) * t)/] by A14, A18

          .= (z2 . x) by A16, A17, A18;

        end;

        hence thesis by A17;

      end;

    end

    registration

      let t, a;

      cluster ( rng ( F_dp1 (t,a))) -> non empty;

      coherence

      proof

        

         A8: 1 < (t + 1) by Lm1, XREAL_1: 39;

        ( dom ( F_dp1 (t,a))) = ( Seg ( len ( F_dp1 (t,a)))) by FINSEQ_1:def 3

        .= ( Seg (t + 1)) by Def4;

        then 1 in ( dom ( F_dp1 (t,a))) by A8;

        hence thesis by FUNCT_1: 3;

      end;

    end

    theorem :: DIOPHAN1:34

    

     Lm10: ( card ( rng ( F_dp1 (t,a)))) in ( card ( dom ( F_dp1 (t,a))))

    proof

      

       A1: ( card ( dom ( F_dp1 (t,a)))) = ( card ( Seg ( len ( F_dp1 (t,a))))) by FINSEQ_1:def 3

      .= ( card ( Seg (t + 1))) by Def4

      .= (t + 1) by FINSEQ_1: 57;

      per cases ;

        suppose

         A3: ( rng ( F_dp1 (t,a))) = ( Segm t);

        ( card ( Segm t)) in ( nextcard ( card ( Segm t))) by CARD_1: 18;

        then ( card ( Segm t)) in ( card ( Segm (t + 1))) by NAT_1: 42;

        hence thesis by A1, A3;

      end;

        suppose

         A6: ( rng ( F_dp1 (t,a))) c< ( Segm t);

        ( Segm t) c= ( Segm (t + 1)) by NAT_1: 39, XREAL_1: 31;

        then ( rng ( F_dp1 (t,a))) c< ( Segm (t + 1)) by A6, XBOOLE_1: 58;

        then ( card ( rng ( F_dp1 (t,a)))) in ( Segm ( card ( Segm (t + 1)))) by CARD_2: 48;

        hence thesis by A1;

      end;

    end;

    

     Th27: ex x1, x2 st x1 in ( dom ( F_dp1 (t,a))) & x2 in ( dom ( F_dp1 (t,a))) & x1 <> x2 & (( F_dp1 (t,a)) . x1) = (( F_dp1 (t,a)) . x2)

    proof

      set A = ( dom ( F_dp1 (t,a)));

      set B = ( rng ( F_dp1 (t,a)));

      

       A1: ( card B) in ( card A) & B <> {} by Lm10;

      defpred P[ object, object] means ex m1 be object st $1 in A & $2 = m1 & (( F_dp1 (t,a)) . $1) = m1;

      

       A2: for x be object st x in A holds ex y be object st y in B & P[x, y] by FUNCT_1: 3;

      consider h be Function of A, B such that

       A3: for x be object st x in A holds P[x, (h . x)] from FUNCT_2:sch 1( A2);

      consider m1,m2 be object such that

       A4: m1 in A and

       A5: m2 in A and

       A6: m1 <> m2 and

       A7: (h . m1) = (h . m2) by A1, FINSEQ_4: 65;

      

       A9: P[m2, (h . m2)] by A3, A5;

       P[m1, (h . m1)] by A3, A4;

      

      then (( F_dp1 (t,a)) . m1) = (h . m2) by A7

      .= (( F_dp1 (t,a)) . m2) by A9;

      hence thesis by A4, A5, A6;

    end;

    registration

      let t, a;

      cluster ( F_dp1 (t,a)) -> non one-to-one;

      coherence

      proof

        assume

         a1: ( F_dp1 (t,a)) is one-to-one;

        consider x1, x2 such that

         A2: x1 in ( dom ( F_dp1 (t,a))) & x2 in ( dom ( F_dp1 (t,a))) & x1 <> x2 & (( F_dp1 (t,a)) . x1) = (( F_dp1 (t,a)) . x2) by Th27;

        thus thesis by a1, A2;

      end;

    end

    begin

    ::$Notion-Name

    theorem :: DIOPHAN1:35

    ex x,y be Integer st |.((x * a) - y).| < (1 / t) & 0 < x & x <= t

    proof

      consider x1,x2 be object such that

       A1: x1 in ( dom ( F_dp1 (t,a))) and

       A2: x2 in ( dom ( F_dp1 (t,a))) and

       A3: x1 <> x2 and

       A4: (( F_dp1 (t,a)) . x1) = (( F_dp1 (t,a)) . x2) by Th27;

      

       A5: ( dom ( F_dp1 (t,a))) = ( Seg ( len ( F_dp1 (t,a)))) by FINSEQ_1:def 3

      .= ( Seg (t + 1)) by Def4;

      consider n1 be Nat such that

       A6: x1 = n1 and

       A7: 1 <= n1 and

       A8: n1 <= (t + 1) by A1, A5;

      reconsider x1 as Nat by A6;

      consider n2 be Nat such that

       A9: x2 = n2 and

       A10: 1 <= n2 and

       A11: n2 <= (t + 1) by A2, A5;

      reconsider x2 as Nat by A9;

      (( F_dp1 (t,a)) . x1) in ( rng ( F_dp1 (t,a))) by A1, FUNCT_1: 3;

      then (( F_dp1 (t,a)) . x1) in ( Segm t);

      then (( F_dp1 (t,a)) . x1) in { i where i be Nat : i < t } by AXIOMS: 4;

      then

      consider i be Nat such that

       A13: (( F_dp1 (t,a)) . x1) = i and i < t;

      

       A14: [\(( frac ((x1 - 1) * a)) * t)/] = i by Def4, A1, A13;

      reconsider r1 = ( frac ((x1 - 1) * a)) as Real;

      (( F_dp1 (t,a)) . x2) in ( rng ( F_dp1 (t,a))) by A2, FUNCT_1: 3;

      then (( F_dp1 (t,a)) . x2) in ( Segm t);

      then (( F_dp1 (t,a)) . x2) in { i where i be Nat : i < t } by AXIOMS: 4;

      then

      consider i2 be Nat such that

       A16: (( F_dp1 (t,a)) . x2) = i2 and i2 < t;

      

       A17: [\(( frac ((x2 - 1) * a)) * t)/] = i2 by Def4, A2, A16;

      reconsider r2 = ( frac ((x2 - 1) * a)) as Real;

      i = (( F_dp1 (t,a)) . x1) by A13

      .= (( F_dp1 (t,a)) . x2) by A4

      .= i2 by A16;

      then

       A18: r1 in (( Equal_Div_interval t) . i) & r2 in (( Equal_Div_interval t) . i) by A14, Lm4, A17;

      

       A19: |.(r1 - r2).| < (t " ) by Lm5, A18;

      set m1 = (x1 - 1);

      set m2 = (x2 - 1);

      

       A20: (r1 - r2) = (((m1 * a) - [\(m1 * a)/]) - ( frac (m2 * a))) by INT_1:def 8

      .= (((m1 * a) - [\(m1 * a)/]) - ((m2 * a) - [\(m2 * a)/])) by INT_1:def 8

      .= (((m1 - m2) * a) - ( [\(m1 * a)/] - [\(m2 * a)/]));

      per cases by A3, XXREAL_0: 1;

        suppose

         A21: x1 > x2;

        set x = (m1 - m2);

        set y = ( [\(m1 * a)/] - [\(m2 * a)/]);

        

         A24: x = (x1 - x2);

        

         A25: ((t + 1) - x2) >= (x1 - x2) by A6, A8, XREAL_1: 13;

        ((t + 1) - 1) >= ((t + 1) - x2) by A9, A10, XREAL_1: 10;

        then

         A27: x <= t by A25, XXREAL_0: 2;

        

         A28: 0 < x by A21, XREAL_1: 50, A24;

         |.((x * a) - y).| < (t " ) by Lm5, A18, A20;

        hence thesis by A27, A28;

      end;

        suppose

         A29: x1 < x2;

        set x = (m2 - m1);

        set y = ( [\(m2 * a)/] - [\(m1 * a)/]);

        

         A32: x = (x2 - x1);

        

         A33: ((t + 1) - x1) >= (x2 - x1) by A9, A11, XREAL_1: 13;

        ((t + 1) - 1) >= ((t + 1) - x1) by A6, A7, XREAL_1: 10;

        then

         A35: x <= t by A33, XXREAL_0: 2;

        

         A36: 0 < x by A29, XREAL_1: 50, A32;

        ( - (r1 - r2)) = ((x * a) - y) by A20;

        then |.((x * a) - y).| < (t " ) by A19, COMPLEX1: 52;

        hence thesis by A35, A36;

      end;

    end;