let n, D be Nat; :: thesis: ( not D is square & n > 1 implies ex x, y being Integer st
( y <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n ) )
assume A1: ( not D is square & n > 1 ) ; :: thesis: ex x, y being Integer st
( y <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n )
consider x being FinSequence of NAT such that
A2: len x = n + 1 and
A3: for k being Nat st k in dom x holds
x . k = [\((k - 1) * (sqrt D))/] + 1 and
( not D is square implies x is one-to-one ) by Th7;
deffunc H1( Nat) -> set = (x . $1) - (($1 - 1) * (sqrt D));
consider u being FinSequence such that
A4: len u = n + 1 and
A5: for k being Nat st k in dom u holds
u . k = H1(k) from FINSEQ_1:sch 2();
 rng u c= REAL
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng u or y in REAL )
assume y in rng u ; :: thesis: y in REAL
then consider x being object such that
A6: ( x in dom u & u . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A6;
u . x = H1(x) by A5, A6;
hence y in REAL by A6, XREAL_0:def 1; :: thesis: verum
end;
then reconsider u = u as FinSequence of REAL by FINSEQ_1:def 4;
A7: dom x = dom u by A2, A4, FINSEQ_3:29;
for k being Nat st k in dom u holds
( 0 < u . k & u . k <= 1 )
proof
let k be Nat; :: thesis: ( k in dom u implies ( 0 < u . k & u . k <= 1 ) )
assume A8: k in dom u ; :: thesis: ( 0 < u . k & u . k <= 1 )
A9: u . k = (x . k) - ((k - 1) * (sqrt D)) by A8, A5;
x . k = [\((k - 1) * (sqrt D))/] + 1 by A8, A7, A3;
then u . k = ([\((k - 1) * (sqrt D))/] - ((k - 1) * (sqrt D))) + 1 by A9;
hence ( 0 < u . k & u . k <= 1 ) by Lm1; :: thesis: verum
end;
then consider n1, n2 being Nat such that
A10: ( n1 in dom u & n2 in dom u & n1 <> n2 & u . n1 <= u . n2 & (u . n2) - (u . n1) < (1 - 0) / n ) by A1, A4, Th8;
A11: ( u . n1 = (x . n1) - ((n1 - 1) * (sqrt D)) & u . n2 = (x . n2) - ((n2 - 1) * (sqrt D)) ) by A5, A10;
A12: u . n1 <> u . n2
proof
assume u . n1 = u . n2 ; :: thesis: contradiction
then (x . n1) + ((1 - n1) * (sqrt D)) = (x . n2) + ((1 - n2) * (sqrt D)) by A11;
then 1 - n1 = 1 - n2 by A1, Th3;
hence contradiction by A10; :: thesis: verum
end;
set X = (x . n2) - (x . n1);
set Y = n2 - n1;
take (x . n2) - (x . n1) ; :: thesis: ex y being Integer st
( y <> 0 & |.y.| <= n & 0 < ((x . n2) - (x . n1)) - (y * (sqrt D)) & ((x . n2) - (x . n1)) - (y * (sqrt D)) < 1 / n )
take n2 - n1 ; :: thesis: ( n2 - n1 <> 0 & |.(n2 - n1).| <= n & 0 < ((x . n2) - (x . n1)) - ((n2 - n1) * (sqrt D)) & ((x . n2) - (x . n1)) - ((n2 - n1) * (sqrt D)) < 1 / n )
( 1 <= n1 & n1 <= n + 1 & 1 <= n2 & n2 <= n + 1 ) by A4, A10, FINSEQ_3:25;
then ( 1 - (n + 1) <= n2 - n1 & n2 - n1 <= (n + 1) - 1 ) by XREAL_1:13;
then A13: ( - n <= n2 - n1 & n2 - n1 <= n ) ;
u . n2 > u . n1 by A12, A10, XXREAL_0:1;
hence ( n2 - n1 <> 0 & |.(n2 - n1).| <= n & 0 < ((x . n2) - (x . n1)) - ((n2 - n1) * (sqrt D)) & ((x . n2) - (x . n1)) - ((n2 - n1) * (sqrt D)) < 1 / n ) by A13, ABSVALUE:5, A10, A11, XREAL_1:50; :: thesis: verum