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

proof

assume a divides b ; :: thesis: abs a divides abs b
then consider c being Integer such that
A8: b = a * c by INT_1:def 9;
abs b = (abs a) * (abs c) by A8, COMPLEX1:151;
hence abs a divides abs b by INT_1:def 9; :: thesis: verum

end;

assume abs a divides abs b ; :: thesis: a divides b
then consider m being Integer such that
A2: abs b = (abs a) * m by INT_1:def 9;
A3: ( a >= 0 implies a divides b )

proof

assume a >= 0 ; :: thesis: a divides b
then A4: abs 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 by INT_1:def 9; :: thesis: verum

end;

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

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

end;

end;

end;

( a < 0 implies a divides b )

proof

assume a < 0 ; :: thesis: a divides b
then A6: abs 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 A6, ABSVALUE:def 1;
hence a divides b by INT_1:def 9; :: thesis: verum

end;

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

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

end;

end;

end;

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