theorem GCDP: :: NEWTON03:46

for a being Nat
for p being prime Nat holds
( a gcd p = 1 or a gcd p = p )