let n be Nat; for a, b being Integer holds (a |^ n) lcm (b |^ n) = (a lcm b) |^ n
let a, b be Integer; (a |^ n) lcm (b |^ n) = (a lcm b) |^ n
A2:
(a |^ n) gcd (b |^ n) = (a gcd b) |^ n
by NEWTON027;
A3:
( |.((a |^ n) * (b |^ n)).| = ((a |^ n) gcd (b |^ n)) * ((a |^ n) lcm (b |^ n)) & |.(a * b).| = (a gcd b) * (a lcm b) )
by NATD29;
then A4: ((a |^ n) gcd (b |^ n)) * ((a |^ n) lcm (b |^ n)) =
|.((a * b) |^ n).|
by NEWTON:7
.=
((a gcd b) * (a lcm b)) |^ n
by A3, TAYLOR_2:1
.=
((a gcd b) |^ n) * ((a lcm b) |^ n)
by NEWTON:7
.=
((a |^ n) gcd (b |^ n)) * ((a lcm b) |^ n)
by NEWTON027
;