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

A1: now :: thesis: ( m divides k implies |.m.| divides k )

assume m divides k ; :: thesis: |.m.| divides k
then consider l being Integer such that
A2: m * l = k ;

now :: thesis: |.m.| divides k

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

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

then |.m.| * l = k by A2, ABSVALUE:def 1;
hence |.m.| divides k ; :: thesis: verum

end;

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

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

end;

end;

end;

hence |.m.| divides k ; :: thesis: verum

end;

now :: thesis: ( |.m.| divides k implies m divides k )

assume |.m.| divides k ; :: thesis: m divides k
then consider l being Integer such that
A3: |.m.| * l = k ;

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 ; :: 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 ; :: thesis: verum

end;

end;

end;

hence m divides k ; :: thesis: verum

end;

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