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

proof

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

end;

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

proof

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

per cases ( b < 0 or b >= 0 ) ;

suppose b < 0 ; :: thesis: a divides b

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

end;

suppose b >= 0 ; :: thesis: a divides b

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

end;

end;

end;

( a < 0 implies a divides b )

proof

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

per cases ( b < 0 or b >= 0 ) ;

suppose b < 0 ; :: thesis: a divides b

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

end;

suppose b >= 0 ; :: thesis: a divides b

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

end;

end;

end;

hence a divides b by A3; :: thesis: verum