let a, b, n be Nat; :: thesis: (a |^ n) gcd (b |^ n) = (a gcd b) |^ n
for k being Nat st a gcd b = k holds
(a |^ n) gcd (b |^ n) = k |^ n

proof

let k be Nat; :: thesis: ( a gcd b = k implies (a |^ n) gcd (b |^ n) = k |^ n )
assume A0: a gcd b = k ; :: thesis: (a |^ n) gcd (b |^ n) = k |^ n
then consider l being Nat such that
A2: a = k * l by INT_2:21, NAT_D:def 3;
consider m being Nat such that
A3: b = k * m by A0, INT_2:21, NAT_D:def 3;

per cases ( a > 0 or a = 0 ) ;

suppose A4: a > 0 ; :: thesis: (a |^ n) gcd (b |^ n) = k |^ n

then l gcd m = 1 by A0, A2, A3, Lm6;
then A6: (l |^ n) gcd (m |^ n) = 1 by WSIERP_1:12;
a10: l > 0 by A2, A4;
k |^ n = (k |^ n) * ((l |^ n) gcd (m |^ n)) by A6
.= ((k |^ n) * (l |^ n)) gcd ((k |^ n) * (m |^ n)) by a10, EULER_1:15
.= ((k |^ n) * (l |^ n)) gcd ((k * m) |^ n) by NEWTON:7
.= (a |^ n) gcd (b |^ n) by A2, A3, NEWTON:7 ;
hence (a |^ n) gcd (b |^ n) = k |^ n ; :: thesis: verum

end;

suppose A14: a = 0 ; :: thesis: (a |^ n) gcd (b |^ n) = k |^ n

then A16: ( a |^ n = 0 or n < 1 ) by NEWTON:11;
( n = 0 implies ( a |^ n = 1 & b |^ n = 1 & k |^ n = 1 ) ) by NEWTON:4;
hence (a |^ n) gcd (b |^ n) = k |^ n by A0, A14, A16, NAT_1:14, NAT_D:32; :: thesis: verum

end;

end;

end;

hence (a |^ n) gcd (b |^ n) = (a gcd b) |^ n ; :: thesis: verum