let D be Nat; :: thesis: ( not D is square implies { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } is infinite )
set S = { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } ;
assume A1: ( not D is square & { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } is finite ) ; :: thesis: contradiction
ex f being Function of { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } ,REAL st
for x, y being Integer st [x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
f . [x,y] = x - (y * (sqrt D))
proof
defpred S1[ object , object ] means for x, y being Integer st [x,y] = $1 holds
$2 = x - (y * (sqrt D));
A2: for xy being object st xy in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
ex u being object st S1[xy,u]
proof
let xy be object ; :: thesis: ( xy in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } implies ex u being object st S1[xy,u] )
assume A3: xy in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } ; :: thesis: ex u being object st S1[xy,u]
consider x, y being Integer such that
A4: ( xy = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) by A3;
take u = x - (y * (sqrt D)); :: thesis: S1[xy,u]
let x1, y1 be Integer; :: thesis: ( [x1,y1] = xy implies u = x1 - (y1 * (sqrt D)) )
assume A5: [x1,y1] = xy ; :: thesis: u = x1 - (y1 * (sqrt D))
( x1 = x & y1 = y ) by A4, A5, XTUPLE_0:1;
hence u = x1 - (y1 * (sqrt D)) ; :: thesis: verum
end;
consider f being Function such that
A6: ( dom f = { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } & ( for xy being object st xy in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
S1[xy,f . xy] ) ) from CLASSES1:sch 1(A2);
 rng f c= REAL
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in rng f or a in REAL )
assume a in rng f ; :: thesis: a in REAL
then consider xy being object such that
A7: ( xy in dom f & f . xy = a ) by FUNCT_1:def 3;
consider x, y being Integer such that
A8: ( xy = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) by A6, A7;
f . xy = x - (y * (sqrt D)) by A6, A7, A8;
hence a in REAL by A7, XREAL_0:def 1; :: thesis: verum
end;
then reconsider f = f as Function of { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } ,REAL by A6, FUNCT_2:2;
take f ; :: thesis: for x, y being Integer st [x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
f . [x,y] = x - (y * (sqrt D))
thus for x, y being Integer st [x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
f . [x,y] = x - (y * (sqrt D)) by A6; :: thesis: verum
end;
then consider f being Function of { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } ,REAL such that
A9: for x, y being Integer st [x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } holds
f . [x,y] = x - (y * (sqrt D)) ;
not { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } is empty
proof
consider x, y being Integer such that
A10: ( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 ) by A1, Th11;
[x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } by A10;
hence not { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } is empty ; :: thesis: verum
end;
then reconsider R = rng f as non empty finite Subset of REAL by A1;
inf R > 0
proof
min R in R by XXREAL_2:def 7;
then consider xy being object such that
A11: ( xy in dom f & f . xy = inf R ) by FUNCT_1:def 3;
xy in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } by A11;
then ex x, y being Integer st
( xy = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) ;
hence inf R > 0 by A9, A11; :: thesis: verum
end;
then consider n being Nat such that
A12: 1 / n < inf R and
A13: n > 1 by Lm3;
consider x, y being Integer such that
A14: ( y <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n ) by A1, A13, Th9;
A15: |.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2)) by A1, A13, A14, Th10;
(2 * (sqrt D)) + (1 / (n ^2)) < (2 * (sqrt D)) + 1
proof
n * n > 1 * 1 by A13, XREAL_1:96;
then 1 / (n * n) < 1 by XREAL_1:189;
hence (2 * (sqrt D)) + (1 / (n ^2)) < (2 * (sqrt D)) + 1 by XREAL_1:6; :: thesis: verum
end;
then |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 by A15, XXREAL_0:2;
then ( [x,y] in { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } & { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } = dom f ) by A14, FUNCT_2:def 1;
then ( f . [x,y] in R & f . [x,y] = x - (y * (sqrt D)) ) by A9, FUNCT_1:def 3;
then x - (y * (sqrt D)) >= inf R by XXREAL_2:def 7;
hence contradiction by A12, A14, XXREAL_0:2; :: thesis: verum