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

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