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

|.(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;

end;

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;a - [\a/] < (1 + [\a/]) - [\a/] by INT_1:29, XREAL_1:14;

hence |.(a - n).| < 1 by A2, A3, ABSVALUE:def 1; :: thesis: verum

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;[\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