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