let D be even Integer; :: thesis: { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } is infinite
consider d being Integer such that
A1: D = 2 * d by ABIAN:11;
set A = { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } ;
set G2 = EvenNAT \ {0};
deffunc H₁( Element of EvenNAT \ {0}) -> object = |.(((d / 2) * ($1 ^2)) + 1).|;
deffunc H₂( Element of EvenNAT \ {0}) -> Element of EvenNAT \ {0} = $1;
deffunc H₃( Element of EvenNAT \ {0}) -> object = |.(((d / 2) * ($1 ^2)) - 1).|;
deffunc H₄( Element of EvenNAT \ {0}) -> object = [H₁($1),H₂($1),H₃($1)];
consider f being ManySortedSet of EvenNAT \ {0} such that
A2: for d being Element of EvenNAT \ {0} holds f . d = H₄(d) from PBOOLE:sch 5();
A3: dom f = EvenNAT \ {0} by PARTFUN1:def 2;
A4: rng f c= { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) }

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } )
assume y in rng f ; :: thesis: y in { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) }
then consider k being object such that
A5: k in dom f and
A6: f . k = y by FUNCT_1:def 3;
reconsider k = k as Element of EvenNAT \ {0} by A5;
consider kk being Nat such that
A7: k = 2 * kk by ABIAN:def 2;
((d / 2) * (k ^2)) + 1 = ((d / 2) * ((2 * kk) ^2)) + 1 by A7
.= ((((d / 2) * 2) * 2) * (kk ^2)) + 1
.= ((d * 2) * (kk ^2)) + 1 ;
then reconsider Xk = H₁(k) as positive Nat by TARSKI:1;
((d / 2) * (k ^2)) - 1 = ((d / 2) * ((2 * kk) ^2)) - 1 by A7
.= ((((d / 2) * 2) * 2) * (kk ^2)) - 1
.= ((d * 2) * (kk ^2)) - 1 ;
then A8: H₃(k) is positive Nat by TARSKI:1;
H₃(k) ^2 = (((d / 2) * (k ^2)) - 1) ^2 by COMPLEX1:75;
then A9: H₃(k) ^2 = ((((d / 2) * (k ^2)) + 1) ^2) - ((2 * d) * (k ^2))
.= (H₁(k) ^2) - (D * (H₂(k) ^2)) by A1, COMPLEX1:75 ;
A10: f . k = H₄(k) by A2;
2 divides 2 * (d * (kk ^2)) ;
then A11: 2,((2 * d) * (kk ^2)) + 1 are_coprime by NUMBER07:5;
k divides k ^2 ;
then k divides ((2 * 2) * (kk ^2)) * d by A7, INT_2:2;
then 2 * kk divides 2 * ((2 * (kk ^2)) * d) by A7;
then kk divides (2 * (kk ^2)) * d by INT_4:7;
then kk,((2 * d) * (kk ^2)) + 1 are_coprime by NUMBER07:5;
then 2 * kk,((2 * d) * (kk ^2)) + 1 are_coprime by A11, Th16;
then Xk,k are_coprime by A7, INT_6:14;
hence y in { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } by A6, A8, A9, A10; :: thesis: verum

end;

f is one-to-one

proof

let x1, x2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x1 in proj1 f or not x2 in proj1 f or not f . x1 = f . x2 or x1 = x2 )
assume ( x1 in dom f & x2 in dom f ) ; :: thesis: ( not f . x1 = f . x2 or x1 = x2 )
then reconsider x1 = x1, x2 = x2 as Element of EvenNAT \ {0} ;
( f . x1 = H₄(x1) & f . x2 = H₄(x2) ) by A2;
hence ( not f . x1 = f . x2 or x1 = x2 ) by XTUPLE_0:3; :: thesis: verum

end;

hence { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } is infinite by A3, A4, CARD_1:59; :: thesis: verum