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

per cases ( i >= 0 or i < 0 ) ;

suppose i >= 0 ; :: thesis: ( i,p are_relative_prime or p divides i )

then reconsider i = i as Element of NAT by INT_1:3;
( i,p are_relative_prime or i gcd p = p ) by PEPIN:2;
hence ( i,p are_relative_prime or p divides i ) by NAT_D:def 5; :: thesis: verum

end;

suppose A1: i < 0 ; :: thesis: ( i,p are_relative_prime or p divides i )

then reconsider m = - i as Element of NAT by INT_1:3;
A2: ( m,p are_relative_prime or m gcd p = p ) by PEPIN:2;

per cases ( m,p are_relative_prime or p divides m ) by A2, NAT_D:def 5;

suppose A3: m,p are_relative_prime ; :: thesis: ( i,p are_relative_prime or p divides i )

m = abs i by A1, ABSVALUE:def 1;
then i gcd p = m gcd (abs p) by INT_2:34
.= m gcd p by ABSVALUE:def 1
.= 1 by A3, INT_2:def 3 ;
hence ( i,p are_relative_prime or p divides i ) by INT_2:def 3; :: thesis: verum

end;

suppose p divides m ; :: thesis: ( i,p are_relative_prime 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_relative_prime or p divides i ) by INT_1:def 3; :: thesis: verum

end;

end;

end;

end;