let a be Real; :: thesis: for n being Integer st a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) holds
|.(a - n).| < 1
let n be Integer; :: thesis: ( a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) implies |.(a - n).| < 1 )
assume A1: ( a is not Integer & ( n = [\a/] or n = [\a/] + 1 ) ) ; :: thesis: |.(a - n).| < 1
per cases ( n = [\a/] or n = [\a/] + 1 ) by A1;
suppose A2: n = [\a/] ; :: thesis: |.(a - n).| < 1
then A3: a - n > 0 by A1, INT_1:26, XREAL_1:50;
a - [\a/] < (1 + [\a/]) - [\a/] by INT_1:29, XREAL_1:14;
hence |.(a - n).| < 1 by A2, A3, ABSVALUE:def 1; :: thesis: verum
end;
suppose A5: n = [\a/] + 1 ; :: thesis: |.(a - n).| < 1
then A6: a - n < 0 by INT_1:29, XREAL_1:49;
[\a/] < [/a\] by A1, INT_1:35;
then n = [/a\] by A5, INT_1:41;
then n < a + 1 by INT_1:def 7;
then A8: n - a < 1 by XREAL_1:19;
|.(a - n).| = - (a - n) by A6, ABSVALUE:def 1;
hence |.(a - n).| < 1 by A8; :: thesis: verum
end;
end;