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

per cases ( 0 < y or y <= 0 ) ;

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

then x mod y < y by INT_1:58;
then A4: |.(x mod y).| < y by ABSVALUE:def 1, A2, INT_1:57;
y <= |.y.| by ABSVALUE:4;
hence |.(x mod y).| < |.y.| by A4, XXREAL_0:2; :: thesis: verum

end;

suppose A5: y <= 0 ; :: thesis: |.(x mod y).| < |.y.|

A6: y <> 0 by A1, ABSVALUE:2;
then A7: - (x mod y) < - y by Th4, A5;
A8: x mod y <= 0 by A5, Th3;
|.(x mod y).| = - (x mod y)

proof

per cases ( x mod y = 0 or x mod y <> 0 ) ;

suppose x mod y = 0 ; :: thesis: |.(x mod y).| = - (x mod y)

hence |.(x mod y).| = - (x mod y) by ABSVALUE:2; :: thesis: verum

end;

suppose x mod y <> 0 ; :: thesis: |.(x mod y).| = - (x mod y)

hence |.(x mod y).| = - (x mod y) by A8, ABSVALUE:def 1; :: thesis: verum

end;

end;

end;

hence |.(x mod y).| < |.y.| by A7, A6, A5, ABSVALUE:def 1; :: thesis: verum

end;

end;