let a be Integer; :: thesis: for p being Prime st a gcd p = 1 holds

not p divides a

let p be Prime; :: thesis: ( a gcd p = 1 implies not p divides a )

assume A1: a gcd p = 1 ; :: thesis: not p divides a

assume p divides a ; :: thesis: contradiction

then p divides p gcd a by INT_2:def 2;

then p = 1 by A1, WSIERP_1:15;

hence contradiction by INT_2:def 4; :: thesis: verum

not p divides a

let p be Prime; :: thesis: ( a gcd p = 1 implies not p divides a )

assume A1: a gcd p = 1 ; :: thesis: not p divides a

assume p divides a ; :: thesis: contradiction

then p divides p gcd a by INT_2:def 2;

then p = 1 by A1, WSIERP_1:15;

hence contradiction by INT_2:def 4; :: thesis: verum