let n, D be Nat; ( 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 )
; 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
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 )
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
;
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;
verum
end;
set X = (x . n2) - (x . n1);
set Y = n2 - n1;
take
(x . n2) - (x . n1)
; 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
; ( 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; verum