let i, j be Integer; :: thesis: ( i divides j iff i divides |.j.| )
thus ( i divides j implies i divides |.j.| ) :: thesis: ( i divides |.j.| implies i divides j )

proof

assume A1: i divides j ; :: thesis: i divides |.j.|
then consider a being Integer such that
A2: j = i * a ;

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

suppose j >= 0 ; :: thesis: i divides |.j.|

hence i divides |.j.| by A1, ABSVALUE:def 1; :: thesis: verum

end;

suppose j < 0 ; :: thesis: i divides |.j.|

then A3: - j = |.j.| by ABSVALUE:def 1;
take - a ; :: according to INT_1:def 3 :: thesis: |.j.| = i * (- a)
thus |.j.| = i * (- a) by A2, A3; :: thesis: verum

end;

end;

end;

assume A4: i divides |.j.| ; :: thesis: i divides j
then consider a being Integer such that
A5: |.j.| = i * a ;

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

suppose j >= 0 ; :: thesis: i divides j

hence i divides j by A4, ABSVALUE:def 1; :: thesis: verum

end;

suppose j < 0 ; :: thesis: i divides j

then A6: - j = |.j.| by ABSVALUE:def 1;
take - a ; :: according to INT_1:def 3 :: thesis: j = i * (- a)
thus j = i * (- a) by A5, A6; :: thesis: verum

end;

end;