theorem :: NAT_4:10

for n, q, b being Nat st q gcd b = 1 & q <> 0 & b <> 0 holds
(q |^ n) gcd b = 1