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 ;
consider m being Nat such that
A3: b = k * m by ;
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
.= ((k |^ n) * (l |^ n)) gcd ((k * m) |^ n) by NEWTON:7
.= (a |^ n) gcd (b |^ n) by ;
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 ; :: thesis: verum
end;
end;
end;
hence (a |^ n) gcd (b |^ n) = (a gcd b) |^ n ; :: thesis: verum