let i, j, k be Integer; :: thesis: ( i divides j & i,j are_coprime & not i = 1 implies i = - 1 )
assume i divides j ; :: thesis: ( not i,j are_coprime or i = 1 or i = - 1 )
then A1: |.i.| divides |.j.| by INT_2:16;
assume i,j are_coprime ; :: thesis: ( i = 1 or i = - 1 )
then |.i.|,|.j.| are_coprime by INT_2:34;
then A2: |.i.| = 1 by A1, PYTHTRIP:def 1;
( |.i.| = i or |.i.| = - i ) by COMPLEX1:71;
hence ( i = 1 or i = - 1 ) by A2; :: thesis: verum