set G2 = GreaterOrEqualsNumbers 2;
let D be odd 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
set A = { [x,y,z] where x, y, z is positive Nat : ( (x ^2) - (D * (y ^2)) = z ^2 & x,y are_coprime ) } ;
deffunc H₁( Element of GreaterOrEqualsNumbers 2) -> Element of omega = |.(D + (2 |^ ($1 - 2))).|;
deffunc H₂( Element of GreaterOrEqualsNumbers 2) -> Element of omega = 2 |^ $1;
deffunc H₃( Element of GreaterOrEqualsNumbers 2) -> Element of omega = |.(D - (2 |^ ($1 - 2))).|;
defpred S₁[ Element of GreaterOrEqualsNumbers 2, object ] means ex fx being Element of GreaterOrEqualsNumbers 2 st
( fx = 2 * $1 & $2 = [H₁(fx),H₂($1),H₃(fx)] );
A1: for i being Element of GreaterOrEqualsNumbers 2 ex j being object st S₁[i,j]

proof

let i be Element of GreaterOrEqualsNumbers 2; :: thesis: ex j being object st S₁[i,j]
reconsider i2 = 2 * i as Element of GreaterOrEqualsNumbers 2 by EC_PF_2:def 1, NUMBER09:56;
take [H₁(i2),H₂(i),H₃(i2)] ; :: thesis: S₁[i,[H₁(i2),H₂(i),H₃(i2)]]
thus S₁[i,[H₁(i2),H₂(i),H₃(i2)]] ; :: thesis: verum

end;

consider f being ManySortedSet of GreaterOrEqualsNumbers 2 such that
A2: for d being Element of GreaterOrEqualsNumbers 2 holds S₁[d,f . d] from PBOOLE:sch 6(A1);
A3: dom f = GreaterOrEqualsNumbers 2 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 GreaterOrEqualsNumbers 2 by A5;
consider fx being Element of GreaterOrEqualsNumbers 2 such that
A7: fx = 2 * k and
A8: f . k = [H₁(fx),H₂(k),H₃(fx)] by A2;
A9: 2 <= k by NUMBER09:56;
1 * k < 2 * k by XREAL_1:68;
then 2 < fx by A7, A9, XXREAL_0:2;
then A10: fx - 2 > fx - fx by XREAL_1:10;
then A11: H₁(fx) is positive Element of NAT by INT_1:3;
A12: H₃(fx) is positive Element of NAT by A10, INT_1:3;
A13: H₁(fx) ^2 = (D + (2 |^ (fx - 2))) ^2 by COMPLEX1:75;
A14: H₃(fx) ^2 = (D - (2 |^ (fx - 2))) ^2 by COMPLEX1:75;
A15: (2 |^ (fx - 2)) |^ 2 = (2 |^ (fx - 2)) ^2 by PEPIN:24;
A16: (2 * D) * (2 |^ (fx - 2)) = D * (2 * (2 |^ (fx - 2)))
.= D * (2 |^ ((fx - 2) + 1)) by NEWTON:6 ;
A17: D * (H₂(k) ^2) = D * ((2 |^ k) |^ 2) by PEPIN:24
.= D * (2 |^ (k * 2)) by NEWTON:9 ;
A18: 2 |^ ((fx - 1) + 1) = 2 * (2 |^ (fx - 1)) by NEWTON:6;
A19: (D * (2 |^ (fx - 1))) - (D * (2 |^ (k * 2))) = - (D * (2 |^ (fx - 1))) by A7, A18
.= - ((2 * D) * (2 |^ (fx - 2))) by A16 ;
A20: (H₁(fx) ^2) - (D * (H₂(k) ^2)) = (((D ^2) + ((2 * D) * (2 |^ (fx - 2)))) + ((2 |^ (fx - 2)) |^ 2)) - (D * (H₂(k) ^2)) by A13, A15
.= (((D ^2) + (D * (2 |^ (fx - 1)))) + ((2 |^ (fx - 2)) |^ 2)) - (D * (H₂(k) ^2)) by A16
.= H₃(fx) ^2 by A14, A15, A17, A19 ;
H₁(fx),H₂(k) are_coprime by A10, PEPIN:18, NAT_5:3;
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, A11, A12, A20; :: 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
A21: ( x1 in dom f & x2 in dom f ) and
A22: f . x1 = f . x2 ; :: thesis: x1 = x2
reconsider x1 = x1, x2 = x2 as Element of GreaterOrEqualsNumbers 2 by A21;
( ex fx1 being Element of GreaterOrEqualsNumbers 2 st
( fx1 = 2 * x1 & f . x1 = [H₁(fx1),H₂(x1),H₃(fx1)] ) & ex fx2 being Element of GreaterOrEqualsNumbers 2 st
( fx2 = 2 * x2 & f . x2 = [H₁(fx2),H₂(x2),H₃(fx2)] ) ) by A2;
then H₂(x1) = H₂(x2) by A22, XTUPLE_0:3;
hence x1 = x2 by PEPIN:30; :: 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