let b be Real; :: thesis: for n being Integer st n <= b & b <= n + 1 holds
|.(n - b).| * |.((n + 1) - b).| <= 1 / 4
let n be Integer; :: thesis: ( n <= b & b <= n + 1 implies |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 )
assume that
A1: n <= b and
A2: b <= n + 1 ; :: thesis: |.(n - b).| * |.((n + 1) - b).| <= 1 / 4
set x = b - n;
set y = (n + 1) - b;
b - n >= 0 by A1, XREAL_1:48;
then A4: |.(n - b).| = - (- (b - n)) by ABSVALUE:30
.= b - n ;
A5: (b - n) + ((n + 1) - b) = 1 ;
|.(n - b).| * |.((n + 1) - b).| = (b - n) * ((n + 1) - b) by A4, A2, XREAL_1:48, ABSVALUE:def 1;
hence |.(n - b).| * |.((n + 1) - b).| <= 1 / 4 by A5, SERIES_3:18; :: thesis: verum