let D, m be positive Integer; :: thesis: ( D = (m ^2) + 1 implies { [x,y] where x, y is positive Integer : (x ^2) - (D * (y ^2)) = 1 } is infinite )
assume A1: D = (m ^2) + 1 ; :: thesis: { [x,y] where x, y is positive Integer : (x ^2) - (D * (y ^2)) = 1 } is infinite
set f = exampleSierpinski150 (m,D);
defpred S1[ Complex, Complex] means ($1 ^2) - (D * ($2 ^2)) = 1;
set A = { [x,y] where x, y is positive Integer : S1[x,y] } ;
A2: S1[(2 * (m ^2)) + 1,2 * m] by A1;
then [((2 * (m ^2)) + 1),(2 * m)] in { [x,y] where x, y is positive Integer : S1[x,y] } ;
then reconsider A = { [x,y] where x, y is positive Integer : S1[x,y] } as non empty set ;
deffunc H5( Real, Real) -> set = ($1 ^2) + (D * ($2 ^2));
deffunc H6( Real, Real) -> set = (2 * $1) * $2;
A3: dom (exampleSierpinski150 (m,D)) = NAT by PARTFUN1:def 2;
defpred S2[ Nat] means (exampleSierpinski150 (m,D)) . $1 in A;
(exampleSierpinski150 (m,D)) . 0 = [((2 * (m ^2)) + 1),(2 * m)] by Def19;
then A4: S2[ 0 ] by A2;
A5: for a being Nat st S2[a] holds
S2[a + 1]
proof
let a be Nat; :: thesis: ( S2[a] implies S2[a + 1] )
assume S2[a] ; :: thesis: S2[a + 1]
then consider x, y being positive Integer such that
A6: ( (exampleSierpinski150 (m,D)) . a = [x,y] & S1[x,y] ) ;
A7: (exampleSierpinski150 (m,D)) . (a + 1) = [H5(((exampleSierpinski150 (m,D)) . a) `1 ,((exampleSierpinski150 (m,D)) . a) `2 ),H6(((exampleSierpinski150 (m,D)) . a) `1 ,((exampleSierpinski150 (m,D)) . a) `2 )] by Def19;
(((x ^2) + (D * (y ^2))) ^2) - (D * (((2 * x) * y) ^2)) = ((x ^2) - (D * (y ^2))) ^2 ;
hence S2[a + 1] by A6, A7; :: thesis: verum
end;
A8: for a being Nat holds S2[a] from NAT_1:sch 2(A4, A5);
 rng (exampleSierpinski150 (m,D)) c= A
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (exampleSierpinski150 (m,D)) or y in A )
assume y in rng (exampleSierpinski150 (m,D)) ; :: thesis: y in A
then ex k being object st
( k in dom (exampleSierpinski150 (m,D)) & (exampleSierpinski150 (m,D)) . k = y ) by FUNCT_1:def 3;
hence y in A by A8; :: thesis: verum
end;
hence { [x,y] where x, y is positive Integer : (x ^2) - (D * (y ^2)) = 1 } is infinite by A3, CARD_1:59; :: thesis: verum