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

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

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

hence ( k divides m iff k divides |.m.| ) by ABSVALUE:def 1; :: thesis: verum

end;

suppose m < 0 ; :: thesis: ( k divides m iff k divides |.m.| )

then |.m.| = - m by ABSVALUE:def 1;
hence ( k divides m iff k divides |.m.| ) by INT_2:10; :: thesis: verum

end;

end;