let D be Nat; :: thesis: ( not D is square implies ex k, a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) ) )
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 ; :: thesis: ex k, a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) )
sqrt D >= 0 by SQUARE_1:def 2;
then reconsider M = [/((2 * (sqrt D)) + 1)\] as Element of NAT by INT_1:53;
defpred S1[ object , object ] means for x, y being Integer st [x,y] = $1 holds
$2 = (x ^2) - (D * (y ^2));
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 ^2) - (D * (y ^2)); :: thesis: S1[xy,u]
let x1, y1 be Integer; :: thesis: ( [x1,y1] = xy implies u = (x1 ^2) - (D * (y1 ^2)) )
assume A5: [x1,y1] = xy ; :: thesis: u = (x1 ^2) - (D * (y1 ^2))
( x1 = x & y1 = y ) by A4, A5, XTUPLE_0:1;
hence u = (x1 ^2) - (D * (y1 ^2)) ; :: 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);
 sqrt D >= 0 by SQUARE_1:def 2;
then reconsider M = [/((2 * (sqrt D)) + 1)\] as Element of NAT by INT_1:53;
defpred S2[ Integer] means $1 <> 0 ;
deffunc H1( set ) -> set = $1;
set SS = { H1(i) where i is Element of INT : ( - M <= i & i <= M & S2[i] ) } ;
{ H1(i) where i is Element of INT : ( - M <= i & i <= M & S2[i] ) } is finite from XXREAL_2:sch 1();
 then reconsider SS = { H1(i) where i is Element of INT : ( - M <= i & i <= M & S2[i] ) } as finite set ;
A7: rng f c= SS
proof
let r be object ; :: according to TARSKI:def 3 :: thesis: ( not r in rng f or r in SS )
assume r in rng f ; :: thesis: r in SS
then consider xy being object such that
A8: ( xy in dom f & f . xy = r ) by FUNCT_1:def 3;
consider x, y being Integer such that
A9: ( xy = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) by A8, A6;
A10: f . xy = (x ^2) - (D * (y ^2)) by A8, A9, A6;
then reconsider r = r as Element of INT by A8, INT_1:def 2;
A11: S2[r] by A8, A9, A1, A10;
(2 * (sqrt D)) + 1 <= M by INT_1:def 7;
then |.r.| < M by A8, A9, A10, XXREAL_0:2;
then ( - M <= r & r <= M ) by ABSVALUE:5;
hence r in SS by A11; :: thesis: verum
end;
then consider k1 being object such that
A12: ( k1 in rng f & f " {k1} is infinite ) by A1, Th12, A6, CARD_2:101;
k1 in SS by A12, A7;
then consider k being Element of INT such that
A13: ( k = k1 & - M <= k & k <= M & S2[k] ) ;
set Z = f " {k};
take k ; :: thesis: ex a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) )
A14: f " {k} c= { [x,y] where x, y is Integer : ( y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) } by RELAT_1:132, A6;
defpred S3[ object , object ] means for x, y being Integer st [x,y] = $1 holds
$2 = [(x mod k),(y mod k)];
A15: for xy being object st xy in f " {k} holds
ex u being object st S3[xy,u]
proof
let xy be object ; :: thesis: ( xy in f " {k} implies ex u being object st S3[xy,u] )
assume A16: xy in f " {k} ; :: thesis: ex u being object st S3[xy,u]
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 A16, A14;
then consider x, y being Integer such that
A17: ( xy = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) ;
take u = [(x mod k),(y mod k)]; :: thesis: S3[xy,u]
let x1, y1 be Integer; :: thesis: ( [x1,y1] = xy implies u = [(x1 mod k),(y1 mod k)] )
assume A18: [x1,y1] = xy ; :: thesis: u = [(x1 mod k),(y1 mod k)]
( x1 = x & y1 = y ) by A17, A18, XTUPLE_0:1;
hence u = [(x1 mod k),(y1 mod k)] ; :: thesis: verum
end;
consider g being Function such that
A19: ( dom g = f " {k} & ( for xy being object st xy in f " {k} holds
S3[xy,g . xy] ) ) from CLASSES1:sch 1(A15);
 defpred S4[ object ] means verum;
set K = { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } ;
A20: { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } is finite from XXREAL_2:sch 1();
 rng g c= [: { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } , { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } :]
proof
let b be object ; :: according to TARSKI:def 3 :: thesis: ( not b in rng g or b in [: { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } , { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } :] )
assume b in rng g ; :: thesis: b in [: { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } , { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } :]
then consider a being object such that
A21: ( a in dom g & g . a = b ) by FUNCT_1:def 3;
( a in dom f & f . a in {k} ) by A19, A21, FUNCT_1:def 7;
then consider x, y being Integer such that
A22: ( a = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) by A6;
A23: g . a = [(x mod k),(y mod k)] by A22, A21, A19;
A24: x mod k in INT by INT_1:def 2;
|.(x mod k).| < |.k.| by Th2, A13;
then ( - |.k.| <= x mod k & x mod k <= |.k.| ) by ABSVALUE:5;
then A25: x mod k in { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } by A24;
A26: y mod k in INT by INT_1:def 2;
|.(y mod k).| < |.k.| by Th2, A13;
then ( - |.k.| <= y mod k & y mod k <= |.k.| ) by ABSVALUE:5;
then y mod k in { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } by A26;
hence b in [: { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } , { H1(i) where i is Element of INT : ( - |.k.| <= i & i <= |.k.| & S4[i] ) } :] by A21, A23, A25, ZFMISC_1:87; :: thesis: verum
end;
then consider ab being object such that
A27: ( ab in rng g & g " {ab} is infinite ) by A19, A12, A13, A20, CARD_2:101;
consider X being object such that
A28: X in g " {ab} by A27, XBOOLE_0:def 1;
A29: ( X in dom g & g . X in {ab} ) by A28, FUNCT_1:def 7;
A30: ( X in dom f & f . X in {k} ) by A29, A19, FUNCT_1:def 7;
then consider x, y being Integer such that
A31: ( X = [x,y] & y <> 0 & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 & 0 < x - (y * (sqrt D)) ) by A6;
A32: g . X = [(x mod k),(y mod k)] by A31, A29, A19;
ex a, b, c, d being Integer st
( (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) )
proof
assume A33: for a, b, c, d being Integer st (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k holds
( |.a.| = |.c.| & |.b.| = |.d.| ) ; :: thesis: contradiction
g " {ab} c= {[x,y],[(- x),y],[x,(- y)],[(- x),(- y)]}
proof
let Y be object ; :: according to TARSKI:def 3 :: thesis: ( not Y in g " {ab} or Y in {[x,y],[(- x),y],[x,(- y)],[(- x),(- y)]} )
assume Y in g " {ab} ; :: thesis: Y in {[x,y],[(- x),y],[x,(- y)],[(- x),(- y)]}
then A34: ( Y in dom g & g . Y in {ab} ) by FUNCT_1:def 7;
then A35: ( Y in dom f & f . Y in {k} ) by A19, FUNCT_1:def 7;
then consider x1, y1 being Integer such that
A36: ( Y = [x1,y1] & y1 <> 0 & |.((x1 ^2) - (D * (y1 ^2))).| < (2 * (sqrt D)) + 1 & 0 < x1 - (y1 * (sqrt D)) ) by A6;
A37: ( g . X = ab & ab = g . Y ) by A29, A34, TARSKI:def 1;
g . Y = [(x1 mod k),(y1 mod k)] by A36, A34, A19;
then A38: ( x mod k = x1 mod k & y mod k = y1 mod k ) by A32, A37, XTUPLE_0:1;
A39: x,x1 are_congruent_mod k
proof
( x = ((x div k) * k) + (x mod k) & x1 = ((x1 div k) * k) + (x1 mod k) ) by INT_1:59, A13;
then x - x1 = k * ((x div k) - (x1 div k)) by A38;
hence x,x1 are_congruent_mod k by INT_1:def 5; :: thesis: verum
end;
A40: y,y1 are_congruent_mod k
proof
( y = ((y div k) * k) + (y mod k) & y1 = ((y1 div k) * k) + (y1 mod k) ) by INT_1:59, A13;
then y - y1 = k * ((y div k) - (y1 div k)) by A38;
hence y,y1 are_congruent_mod k by INT_1:def 5; :: thesis: verum
end;
( f . X = k & k = f . Y ) by A30, A35, TARSKI:def 1;
then ( (x1 ^2) - (D * (y1 ^2)) = k & k = (x ^2) - (D * (y ^2)) ) by A36, A35, A30, A31, A6;
then ( |.x.| = |.x1.| & |.y.| = |.y1.| ) by A33, A39, A40;
then ( ( x = x1 or x = - x1 ) & ( y = y1 or y = - y1 ) ) by ABSVALUE:28;
hence Y in {[x,y],[(- x),y],[x,(- y)],[(- x),(- y)]} by A36, ENUMSET1:def 2; :: thesis: verum
end;
hence contradiction by A27; :: thesis: verum
end;
hence ex a, b, c, d being Integer st
( 0 <> k & (a ^2) - (D * (b ^2)) = k & k = (c ^2) - (D * (d ^2)) & a,c are_congruent_mod k & b,d are_congruent_mod k & ( |.a.| <> |.c.| or |.b.| <> |.d.| ) ) by A13; :: thesis: verum