let i be Integer; :: thesis: for p being Prime holds
( i,p are_coprime or p divides i )

let p be Prime; :: thesis: ( i,p are_coprime or p divides i )
per cases ( i >= 0 or i < 0 ) ;
suppose i >= 0 ; :: thesis: ( i,p are_coprime or p divides i )
then reconsider i = i as Element of NAT by INT_1:3;
( i,p are_coprime or i gcd p = p ) by PEPIN:2;
hence ( i,p are_coprime or p divides i ) by NAT_D:def 5; :: thesis: verum
end;
suppose A1: i < 0 ; :: thesis: ( i,p are_coprime or p divides i )
then reconsider m = - i as Element of NAT by INT_1:3;
A2: ( m,p are_coprime or m gcd p = p ) by PEPIN:2;
per cases by ;
suppose A3: m,p are_coprime ; :: thesis: ( i,p are_coprime or p divides i )
m = |.i.| by ;
then i gcd p = m gcd |.p.| by INT_2:34
.= m gcd p by ABSVALUE:def 1
.= 1 by ;
hence ( i,p are_coprime or p divides i ) by INT_2:def 3; :: thesis: verum
end;
suppose p divides m ; :: thesis: ( i,p are_coprime or p divides i )
then consider t being Nat such that
A4: m = p * t by NAT_D:def 3;
i = p * (- t) by A4;
hence ( i,p are_coprime or p divides i ) ; :: thesis: verum
end;
end;
end;
end;