let p, n be Nat; :: thesis: ( p is prime & p,n are_coprime implies not p divides n )

assume that

A1: p is prime and

A2: p,n are_coprime ; :: thesis: not p divides n

assume p divides n ; :: thesis: contradiction

then n gcd p = p by NEWTON:49;

then n gcd p > 1 by A1, INT_2:def 4;

hence contradiction by A2, INT_2:def 3; :: thesis: verum

assume that

A1: p is prime and

A2: p,n are_coprime ; :: thesis: not p divides n

assume p divides n ; :: thesis: contradiction

then n gcd p = p by NEWTON:49;

then n gcd p > 1 by A1, INT_2:def 4;

hence contradiction by A2, INT_2:def 3; :: thesis: verum