let n be Nat; :: thesis: for t, z being Integer holds (t |^ n) gcd (z |^ n) = (t gcd z) |^ n
let t, z be Integer; :: thesis: (t |^ n) gcd (z |^ n) = (t gcd z) |^ n
A1: ( (t |^ n) gcd (z |^ n) = |.(t |^ n).| gcd |.(z |^ n).| & t gcd z = |.t.| gcd |.z.| ) by INT_2:34;
( |.(t |^ n).| = |.t.| |^ n & |.(z |^ n).| = |.z.| |^ n ) by TAYLOR_2:1;
hence (t |^ n) gcd (z |^ n) = (t gcd z) |^ n by A1, NEWTON02:7; :: thesis: verum