let D be Nat; :: thesis: ( not D is square implies ex x, y being Integer st
( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 ) )
assume A1: not D is square ; :: thesis: ex x, y being Integer st
( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 )
then consider x, y being Integer such that
A2: y <> 0 and
A3: |.y.| <= 2 and
A4: ( 0 < x - (y * (sqrt D)) & x - (y * (sqrt D)) < 1 / 2 ) by Th9;
A5: |.((x ^2) - (D * (y ^2))).| <= (2 * (sqrt D)) + (1 / (2 ^2)) by A1, A3, A4, Th10;
take x ; :: thesis: ex y being Integer st
( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 )
take y ; :: thesis: ( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 )
(2 * (sqrt D)) + (1 / (2 ^2)) < (2 * (sqrt D)) + 1 by XREAL_1:6;
hence ( y <> 0 & 0 < x - (y * (sqrt D)) & |.((x ^2) - (D * (y ^2))).| < (2 * (sqrt D)) + 1 ) by A2, A4, A5, XXREAL_0:2; :: thesis: verum