let n, q, b be Nat; :: thesis: ( q gcd b = 1 & q <> 0 & b <> 0 implies (q |^ n) gcd b = 1 )
assume A1: ( q gcd b = 1 & q <> 0 & b <> 0 ) ; :: thesis: (q |^ n) gcd b = 1
then q,b are_relative_prime by INT_2:def 4;
then q |^ n,b are_relative_prime by A1, EULER_2:32;
hence (q |^ n) gcd b = 1 by INT_2:def 4; :: thesis: verum