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;