let i, j be Integer; :: thesis: ( not i,j are_coprime or i <> j or ( i = j & j = 1 ) or ( i = j & j = - 1 ) )
A1: i gcd i = |.i.| by INT_5:12;
( |.i.| = i or |.i.| = - i ) by ABSVALUE:1;
hence ( not i,j are_coprime or i <> j or ( i = j & j = 1 ) or ( i = j & j = - 1 ) ) by A1; :: thesis: verum