let x, j be Integer; :: thesis: ( j < 0 implies ( j < x mod j & x mod j <= 0 ) )
assume A1: j < 0 ; :: thesis: ( j < x mod j & x mod j <= 0 )
then A2: (x / j) * j = x by XCMPLX_1:87;
(x / j) - 1 < [\(x / j)/] by INT_1:def 6;
then (x / j) - 1 < x div j by INT_1:def 9;
then ((x / j) - 1) * j > (x div j) * j by A1, XREAL_1:69;
then x - j > ((x div j) * j) - 0 by A2;
then x - ((x div j) * j) > j - 0 by XREAL_1:16;
hence x mod j > j by INT_1:def 10, A1; :: thesis: x mod j <= 0
[\(x / j)/] <= x / j by INT_1:def 6;
then x div j <= x / j by INT_1:def 9;
then (x div j) * j >= (x / j) * j by A1, XREAL_1:65;
then 0 >= x - ((x div j) * j) by A2, XREAL_1:47;
hence x mod j <= 0 by INT_1:def 10; :: thesis: verum