let i be Integer; :: thesis: ( |.i.| divides i & i divides |.i.| )

per cases ( |.i.| = i or |.i.| = - i ) by ABSVALUE:1;

suppose |.i.| = i ; :: thesis: ( |.i.| divides i & i divides |.i.| )

hence ( |.i.| divides i & i divides |.i.| ) ; :: thesis: verum

end;

suppose A1: |.i.| = - i ; :: thesis: ( |.i.| divides i & i divides |.i.| )

then A2: i * (- 1) = |.i.| ;
|.i.| * (- 1) = i by A1;
hence ( |.i.| divides i & i divides |.i.| ) by A2, INT_1:def 3; :: thesis: verum

end;

end;