let D be Integer; :: thesis: { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite
( D < 0 or D = 0 or D > 0 ) ;
hence { [x,y,z] where x, y, z is positive Nat : (x ^2) - (D * (y ^2)) = z ^2 } is infinite by Lm52, Lm53, Lm54; :: thesis: verum