let n be Nat; :: thesis: for t being Integer st n > 0 holds

t divides t |^ n

let t be Integer; :: thesis: ( n > 0 implies t divides t |^ n )

t in INT by INT_1:def 2;

then consider k being Nat such that

A1: ( t = k or t = - k ) by INT_1:def 1;

( t |^ n = k |^ n or t |^ n = - (k |^ n) ) by A1, POWER:1, POWER:2;

then A2: ( |.k.| = |.t.| & |.(k |^ n).| = |.(t |^ n).| ) by A1, COMPLEX1:52;

assume n > 0 ; :: thesis: t divides t |^ n

then k |^ 1 divides k |^ n by NEWTON:89, NAT_1:14;

hence t divides t |^ n by A2, INT_2:16; :: thesis: verum

t divides t |^ n

let t be Integer; :: thesis: ( n > 0 implies t divides t |^ n )

t in INT by INT_1:def 2;

then consider k being Nat such that

A1: ( t = k or t = - k ) by INT_1:def 1;

( t |^ n = k |^ n or t |^ n = - (k |^ n) ) by A1, POWER:1, POWER:2;

then A2: ( |.k.| = |.t.| & |.(k |^ n).| = |.(t |^ n).| ) by A1, COMPLEX1:52;

assume n > 0 ; :: thesis: t divides t |^ n

then k |^ 1 divides k |^ n by NEWTON:89, NAT_1:14;

hence t divides t |^ n by A2, INT_2:16; :: thesis: verum