let m, k be Integer; :: thesis: ( abs m divides k iff m divides k )

A1: now :: thesis: ( m divides k implies abs m divides k )

assume m divides k ; :: thesis: abs m divides k
then consider l being Integer such that
A2: m * l = k by INT_1:def 3;

now :: thesis: abs m divides k

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

suppose m >= 0 ; :: thesis: abs m divides k

then (abs m) * l = k by A2, ABSVALUE:def 1;
hence abs m divides k by INT_1:def 3; :: thesis: verum

end;

suppose m < 0 ; :: thesis: abs m divides k

then (abs m) * (- l) = (- m) * (- l) by ABSVALUE:def 1
.= k by A2 ;
hence abs m divides k by INT_1:def 3; :: thesis: verum

end;

end;

end;

hence abs m divides k ; :: thesis: verum

end;

now :: thesis: ( abs m divides k implies m divides k )

assume abs m divides k ; :: thesis: m divides k
then consider l being Integer such that
A3: (abs m) * l = k by INT_1:def 3;

now :: thesis: m divides k

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

suppose m >= 0 ; :: thesis: m divides k

then m * l = k by A3, ABSVALUE:def 1;
hence m divides k by INT_1:def 3; :: thesis: verum

end;

suppose m < 0 ; :: thesis: m divides k

then k = (- m) * l by A3, ABSVALUE:def 1
.= m * (- l) ;
hence m divides k by INT_1:def 3; :: thesis: verum

end;

end;

end;

hence m divides k ; :: thesis: verum

end;

hence ( abs m divides k iff m divides k ) by A1; :: thesis: verum