let i, j, k be Integer; :: thesis: ( i <> 0 & i divides k & i * j,k are_coprime & not i = 1 implies i = - 1 )
assume that
A1: i <> 0 and
A2: i divides k ; :: thesis: ( not i * j,k are_coprime or i = 1 or i = - 1 )
A3: |.(i * j).| = |.i.| * |.j.| by COMPLEX1:65;
assume i * j,k are_coprime ; :: thesis: ( i = 1 or i = - 1 )
then |.(i * j).|,|.k.| are_coprime by INT_2:34;
then A4: |.i.| = 1 by A1, A2, A3, INT_2:16, GROUP_22:2;
( |.i.| = i or |.i.| = - i ) by COMPLEX1:71;
hence ( i = 1 or i = - 1 ) by A4; :: thesis: verum