theorem Th10: :: PELLS_EQ:10

for n, D being Nat
for x, y being Integer st not D is square & n <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n holds
|.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2))