let n be Nat; :: thesis: for a, b being Integer holds (a |^ n) lcm (b |^ n) = (a lcm b) |^ n
let a, b be Integer; :: thesis: (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 ;

per cases ( a gcd b = 0 or a gcd b <> 0 ) ;

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

then ( a = 0 & b = 0 ) ;
hence (a |^ n) lcm (b |^ n) = (a lcm b) |^ n ; :: thesis: verum

end;

suppose a gcd b <> 0 ; :: thesis: (a |^ n) lcm (b |^ n) = (a lcm b) |^ n

hence (a |^ n) lcm (b |^ n) = (a lcm b) |^ n by A2, A4, XCMPLX_1:5; :: thesis: verum

end;

end;