let i, i1 be Integer; :: thesis: ( i divides i1 & i1 <> 0 implies abs i <= abs i1 )
assume A1: ( i divides i1 & i1 <> 0 ) ; :: thesis: abs i <= abs i1
then abs i1 <> 0 by ABSVALUE:7;
then A2: abs i1 > 0 ;
abs i divides abs i1 by A1, INT_2:21;
hence abs i <= abs i1 by A2, NAT_D:7; :: thesis: verum