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 ( i >= 0 or i < 0 ) ;

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

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

end;

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

then A3: - i = |.i.| 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 ( i >= 0 or i < 0 ) ;

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

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

end;

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

then A6: - i = |.i.| 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;