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;