let x, j be Integer; :: thesis: ( j <> 0 implies |.(x mod j).| < |.j.| )
assume j <> 0 ; :: thesis: |.(x mod j).| < |.j.|

per cases then ( j > 0 or j < 0 ) ;

suppose j > 0 ; :: thesis: |.(x mod j).| < |.j.|

then ( 0 <= x mod j & x mod j < j & |.j.| = j ) by INT_1:57, INT_1:58, ABSVALUE:def 1;
hence |.(x mod j).| < |.j.| by ABSVALUE:def 1; :: thesis: verum

end;

suppose j < 0 ; :: thesis: |.(x mod j).| < |.j.|

then A2: ( j < x mod j & x mod j <= 0 & |.j.| = - j ) by Th1, ABSVALUE:def 1;
then |.(x mod j).| = - (x mod j) by ABSVALUE:30;
hence |.(x mod j).| < |.j.| by A2, XREAL_1:24; :: thesis: verum

end;

end;