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

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