let l be Nat; :: thesis: for t, z being Integer st l > 0 & t divides z holds
t divides z |^ l
let t, z be Integer; :: thesis: ( l > 0 & t divides z implies t divides z |^ l )
assume A0: ( l > 0 & t divides z ) ; :: thesis: t divides z |^ l
then consider n being Nat such that
A1: l = 1 + n by NAT_1:10, NAT_1:14;
z |^ (1 + n) = (z |^ 1) * (z |^ n) by NEWTON:8
.= z * (z |^ n) ;
hence t divides z |^ l by A0, A1, INT_2:2; :: thesis: verum