let i be Integer; :: thesis: ( abs i divides i & i divides abs i )

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

suppose abs i = i ; :: thesis: ( abs i divides i & i divides abs i )

hence ( abs i divides i & i divides abs i ) ; :: thesis: verum

end;

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

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

end;

end;