let p be Prime; :: thesis: for a being Integer holds
( a gcd p <> 1 iff p divides a )
let a be Integer; :: thesis: ( a gcd p <> 1 iff p divides a )

hereby :: thesis: ( p divides a implies a gcd p <> 1 )

assume a gcd p <> 1 ; :: thesis: p divides a
then a gcd p = p by INT_2:21, INT_2:def 4;
hence p divides a by INT_2:21; :: thesis: verum

end;

assume A1: p divides a ; :: thesis: a gcd p <> 1
p divides a gcd p by A1, INT_2:22;
hence a gcd p <> 1 by INT_2:27, INT_2:def 4; :: thesis: verum