let n, q, b be Nat; :: thesis: ( q gcd b = 1 & q <> 0 & b <> 0 implies (q |^ n) gcd b = 1 )
assume that
A1: q gcd b = 1 and
A2: ( q <> 0 & b <> 0 ) ; :: thesis: (q |^ n) gcd b = 1
q,b are_coprime by A1, INT_2:def 3;
then q |^ n,b are_coprime by A2, EULER_2:17;
hence (q |^ n) gcd b = 1 by INT_2:def 3; :: thesis: verum