let n, r be Nat; :: thesis: for p being Prime st n divides p |^ r & n > 1 holds
p divides n
let p be Prime; :: thesis: ( n divides p |^ r & n > 1 implies p divides n )
assume A1: n divides p |^ r ; :: thesis: ( not n > 1 or p divides n )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
assume A2: n > 1 ; :: thesis: p divides n

per cases ( n9 = 1 or ex k being Element of NAT st n9 = p * k ) by A1, PEPIN:32;

suppose n9 = 1 ; :: thesis: p divides n

hence p divides n by A2; :: thesis: verum

end;

suppose ex k being Element of NAT st n9 = p * k ; :: thesis: p divides n

hence p divides n by NAT_D:def 3; :: thesis: verum

end;

end;