let n be Nat; :: thesis: for t, z being Integer st t divides z holds
t |^ n divides z |^ n
let t, z be Integer; :: thesis: ( t divides z implies t |^ n divides z |^ n )
assume A1: t divides z ; :: thesis: t |^ n divides z |^ n
( |.t.| in NAT & |.z.| in NAT ) by INT_1:3;
then consider a, b being Nat such that
A2: ( a = |.t.| & b = |.z.| ) ;
A3: ( |.t.| |^ n = |.(t |^ n).| & |.z.| |^ n = |.(z |^ n).| ) by TAYLOR_2:1;
(a gcd b) |^ n = (|.t.| |^ n) gcd (|.z.| |^ n) by A2, Th7
.= (t |^ n) gcd (z |^ n) by A3, INT_2:34 ;
then (t |^ n) gcd (z |^ n) = |.a.| |^ n by A1, A2, INT_2:16, Th3
.= |.(t |^ n).| by A2, TAYLOR_2:1 ;
hence t |^ n divides z |^ n by Th3; :: thesis: verum