let p, n be Nat; :: thesis: ( p is prime & p,n are_relative_prime implies not p divides n )
assume A1: ( p is prime & p,n are_relative_prime ) ; :: thesis: not p divides n
assume p divides n ; :: thesis: contradiction
then n gcd p = p by NEWTON:62;
then n gcd p > 1 by A1, INT_2:def 5;
hence contradiction by A1, INT_2:def 4; :: thesis: verum