let a, b be Integer; :: thesis:
thus ( a divides b implies |.a.| divides |.b.| ) :: thesis:

proof

assume a divides b ; :: thesis:
then consider c being Integer such that
A1: b = a * c ;
|.b.| = |.a.| * |.c.| by A1, COMPLEX1:65;
hence |.a.| divides |.b.| ; :: thesis:

end;

assume |.a.| divides |.b.| ; :: thesis:
then consider m being Integer such that
A2: |.b.| = |.a.| * m ;
A3: ( a >= 0 implies a divides b )

proof

assume a >= 0 ; :: thesis:
then A4: |.b.| = a * m by A2, ABSVALUE:def 1;

per cases ;

suppose b < 0 ; :: thesis:

then - b = a * m by A4, ABSVALUE:def 1;
then b = a * (- m) ;
hence a divides b ; :: thesis:

end;

suppose b >= 0 ; :: thesis:

then b = a * m by A4, ABSVALUE:def 1;
hence a divides b ; :: thesis:

end;

end;

end;

( a < 0 implies a divides b )

proof

assume a < 0 ; :: thesis:
then A5: |.b.| = (- a) * m by A2, ABSVALUE:def 1;

per cases ;

suppose b < 0 ; :: thesis:

then - b = - (a * m) by A5, ABSVALUE:def 1;
hence a divides b ; :: thesis:

end;

suppose b >= 0 ; :: thesis:

then b = a * (- m) by A5, ABSVALUE:def 1;
hence a divides b ; :: thesis:

end;

end;

end;

hence a divides b by A3; :: thesis: