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

proof

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;
A5: ( b < 0 implies a divides b )

proof

assume 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;

( b >= 0 implies a divides b )

proof

assume 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;

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

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;
A7: ( b < 0 implies a divides b )

proof

assume 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;

( b >= 0 implies a divides b )

proof

assume 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;

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

end;

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

end;

( a divides b implies abs a divides abs 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;

hence ( a divides b iff abs a divides abs b ) by A1; :: thesis: verum