let D be non zero 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
( D is odd or D is even ) ;
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 Lm11, Lm12; :: thesis: verum