let a be Nat; :: thesis: for p being prime Nat holds
( a gcd p = 1 or a gcd p = p )
let p be prime Nat; :: thesis: ( a gcd p = 1 or a gcd p = p )

per cases ( p divides a or a gcd p = 1 ) by NAT_6:6;

suppose p divides a ; :: thesis: ( a gcd p = 1 or a gcd p = p )

hence ( a gcd p = 1 or a gcd p = p ) by NEWTON:49; :: thesis: verum

end;

suppose a gcd p = 1 ; :: thesis: ( a gcd p = 1 or a gcd p = p )

hence ( a gcd p = 1 or a gcd p = p ) ; :: thesis: verum

end;

end;