let a, b, n be Nat; :: thesis: ( n > 0 implies (a gcd b) gcd (b |^ n) = a gcd b )
assume n > 0 ; :: thesis: (a gcd b) gcd (b |^ n) = a gcd b
then A2: n >= 1 by NAT_1:14;
(a gcd b) gcd (b |^ n) = a gcd (b gcd (b |^ n)) by NEWTON:48
.= a gcd (b |^ 1) by A2, NEWTON:49, NEWTON:89
.= a gcd b ;
hence (a gcd b) gcd (b |^ n) = a gcd b ; :: thesis: verum