let n be Nat; :: thesis: for i being Integer
for p being Prime st p divides i |^ n holds
p divides i
let i be Integer; :: thesis: for p being Prime st p divides i |^ n holds
p divides i
let p be Prime; :: thesis: ( p divides i |^ n implies p divides i )
assume p divides i |^ n ; :: thesis: p divides i
then p divides |.(i |^ n).| by Th4;
then p divides |.i.| |^ n by TAYLOR_2:1;
then p divides |.i.| by NAT_3:5;
hence p divides i by Th4; :: thesis: verum