let n, r be natural number ; :: thesis: for p being natural prime number st n divides p |^ r & n > 1 holds
p divides n
let p be natural prime number ; :: 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 )
assume A2: n > 1 ; :: thesis: p divides n
reconsider n' = n as Element of NAT by ORDINAL1:def 13;

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

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

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

end;

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

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

end;

end;