let p be natural prime number ; :: thesis: for a being integer number holds
( a gcd p <> 1 iff p divides a )
let a be integer number ; :: 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