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