theorem Th21: :: INT_4:21

for p, q, n being Nat st n > 0 & p is prime & p,q are_coprime holds
not p divides q mod (p |^ n)