let D be Integer; :: thesis: ( D > 0 implies { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite )
assume A1: D > 0 ; :: thesis: { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite
set A = { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } ;
deffunc H₁( Nat) -> set = (D * $1) + 1;
deffunc H₂( Nat, Real) -> set = ($2 ^2) + (D * ($1 ^2));
deffunc H₃( Nat, Real) -> set = (2 * $2) * $1;
deffunc H₄( Nat, Real) -> set = ($2 ^2) - (D * ($1 ^2));
deffunc H₅( Element of NATPLUS ) -> object = [H₂($1,H₁($1)),H₃($1,H₁($1)),H₄($1,H₁($1))];
consider f being ManySortedSet of NATPLUS such that
A2: for d being Element of NATPLUS holds f . d = H₅(d) from PBOOLE:sch 5();
A3: dom f = NATPLUS 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 }

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 } )
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 }
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 NATPLUS by A5, PARTFUN1:def 2;
A7: H₂(k,H₁(k)) is positive Element of NAT by A1, INT_1:3;
A8: H₃(k,H₁(k)) is positive Element of NAT by A1, INT_1:3;
D >= 0 + 1 by A1, INT_1:7;
then D * (D * (k ^2)) >= 1 * (D * (k ^2)) by XREAL_1:64;
then ((k * (D * k)) * D) + ((k * D) + ((D * k) + 1)) > (D * (k ^2)) + 0 by A1, XREAL_1:8;
then (H₁(k) ^2) - (D * (k ^2)) > (D * (k ^2)) - (D * (k ^2)) by XREAL_1:9;
then A9: H₄(k,H₁(k)) is positive Element of NAT by INT_1:3;
(H₂(k,H₁(k)) ^2) - (D * (H₃(k,H₁(k)) ^2)) = H₄(k,H₁(k)) ^2 ;
then H₅(k) in { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } by A7, A8, A9;
hence y in { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } by A2, A6; :: 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 that
A10: ( x1 in dom f & x2 in dom f ) and
A11: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of NATPLUS by A10, PARTFUN1:def 2;
A12: ( (D * x1) / D = x1 & (D * x2) / D = x2 ) by A1, XCMPLX_1:203;
( f . x1 = H₅(x1) & f . x2 = H₅(x2) ) by A2;
then ( H₂(x1,H₁(x1)) = H₂(x2,H₁(x2)) & H₄(x1,H₁(x1)) = H₄(x2,H₁(x2)) ) by A11, XTUPLE_0:3;
then ( H₁(x1) = H₁(x2) or H₁(x1) = - H₁(x2) ) by SQUARE_1:40;
hence x1 = x2 by A1, A12; :: thesis: verum

end;

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