let a, b be Integer; :: thesis: ( a divides b iff abs a divides abs b )
A1: ( 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
A2: b = a * c by INT_1:def 9;
abs b = (abs a) * (abs c) by A2, COMPLEX1:151;
hence abs a divides abs b by INT_1:def 9; :: thesis: verum

end;

( 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
A3: abs b = (abs a) * m by INT_1:def 9;
A4: ( a >= 0 implies a divides b )

proof

assume a >= 0 ; :: thesis: a divides b
then A5: abs b = a * m by A3, ABSVALUE:def 1;
A6: ( b >= 0 implies a divides b )

proof

assume b >= 0 ; :: thesis: a divides b
then b = a * m by A5, 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 A5, ABSVALUE:def 1;
then b = a * (- m) ;
hence a divides b by INT_1:def 9; :: thesis: verum

end;

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

end;

( a < 0 implies a divides b )

proof

assume a < 0 ; :: thesis: a divides b
then A7: abs b = (- a) * m by A3, ABSVALUE:def 1;
A8: ( b >= 0 implies a divides b )

proof

assume b >= 0 ; :: thesis: a divides b
then b = a * (- m) by A7, 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 A7, ABSVALUE:def 1;
hence a divides b by INT_1:def 9; :: thesis: verum

end;

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

end;

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

end;

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