let n, D be 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))
let x, y be Integer; ( not D is square & n <> 0 & |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n implies |.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2)) )
assume that
A1:
( not D is square & n <> 0 )
and
A2:
( |.y.| <= n & 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / n )
; |.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2))
A3:
sqrt D > 0
by A1, SQUARE_1:25;
then A4:
|.(sqrt D).| = sqrt D
by ABSVALUE:def 1;
A5:
( - n <= y & y <= n )
by A2, ABSVALUE:5;
A6:
( y * (sqrt D) < x & x < (1 / n) + (y * (sqrt D)) )
by A2, XREAL_1:19, XREAL_1:47;
A7:
( (- n) * (sqrt D) <= y * (sqrt D) & y * (sqrt D) <= n * (sqrt D) )
by XREAL_1:64, A5, A3;
then A8:
(y * (sqrt D)) + (1 / n) <= (n * (sqrt D)) + (1 / n)
by XREAL_1:6;
((- n) * (sqrt D)) - (1 / n) <= (- n) * (sqrt D)
by XREAL_1:51;
then
((- n) * (sqrt D)) - (1 / n) <= y * (sqrt D)
by A7, XXREAL_0:2;
then
( - ((n * (sqrt D)) + (1 / n)) < x & x < (n * (sqrt D)) + (1 / n) )
by A6, A8, XXREAL_0:2;
then A9:
|.x.| <= (n * (sqrt D)) + (1 / n)
by ABSVALUE:5;
A10:
|.y.| * |.(sqrt D).| <= n * |.(sqrt D).|
by A2, XREAL_1:64, A3;
|.(x + (y * (sqrt D))).| <= |.x.| + |.(y * (sqrt D)).|
by COMPLEX1:56;
then A11:
|.(x + (y * (sqrt D))).| <= |.x.| + (|.y.| * (sqrt D))
by A4, COMPLEX1:65;
|.x.| + (|.y.| * (sqrt D)) <= ((n * (sqrt D)) + (1 / n)) + (n * (sqrt D))
by A4, A9, A10, XREAL_1:7;
then A12:
( 0 <= |.(x + (y * (sqrt D))).| & |.(x + (y * (sqrt D))).| <= ((2 * n) * (sqrt D)) + (1 / n) )
by COMPLEX1:46, A11, XXREAL_0:2;
( - (1 / n) <= 0 & 0 <= x - (y * (sqrt D)) & x - (y * (sqrt D)) <= 1 / n )
by A2;
then A13:
( 0 <= |.(x - (y * (sqrt D))).| & |.(x - (y * (sqrt D))).| <= 1 / n )
by ABSVALUE:5;
A14:
(2 * n) / n = 2
by A1, XCMPLX_1:89;
|.(x + (y * (sqrt D))).| * |.(x - (y * (sqrt D))).| <= (((2 * n) * (sqrt D)) + (1 / n)) * (1 / n)
by XREAL_1:66, A12, A13;
then
|.(x + (y * (sqrt D))).| * |.(x - (y * (sqrt D))).| <= (((2 * n) * (1 / n)) * (sqrt D)) + ((1 / n) * (1 / n))
;
then
|.(x + (y * (sqrt D))).| * |.(x - (y * (sqrt D))).| <= (((2 * n) / n) * (sqrt D)) + ((1 / n) * (1 / n))
by XCMPLX_1:99;
then
|.(x + (y * (sqrt D))).| * |.(x - (y * (sqrt D))).| <= ((2 * 1) * (sqrt D)) + ((1 * 1) / (n * n))
by XCMPLX_1:76, A14;
then
|.((x + (y * (sqrt D))) * (x - (y * (sqrt D)))).| <= (2 * (sqrt D)) + (1 / (n * n))
by COMPLEX1:65;
then
|.((x ^2) - ((y ^2) * ((sqrt D) ^2))).| <= (2 * (sqrt D)) + (1 / (n * n))
;
then
|.((x ^2) - ((y ^2) * (sqrt (D ^2)))).| <= (2 * (sqrt D)) + (1 / (n * n))
by SQUARE_1:29;
hence
|.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (n ^2))
by SQUARE_1:22; verum