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

for k being Nat st a gcd b = k holds

(a |^ n) gcd (b |^ n) = k |^ n

proof

hence
(a |^ n) gcd (b |^ n) = (a gcd b) |^ n
; :: thesis: verum
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;

end;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 )
;

end;

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;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