let n be Nat; :: thesis: for p being Prime st not p divides n holds
n,p are_coprime
let p be Prime; :: thesis: ( not p divides n implies n,p are_coprime )
assume A1: not p divides n ; :: thesis: n,p are_coprime
assume not n,p are_coprime ; :: thesis: contradiction
then consider q being Prime such that
A2: q divides n and
A3: q divides p by PYTHTRIP:def 2;
( q = p or q = 1 ) by A3, INT_2:def 4;
hence contradiction by A1, A2, INT_2:def 4; :: thesis: verum