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