let n, r be Nat; :: thesis: for p being prime Nat st n divides p |^ r & n > 1 holds
p divides n
let p be prime Nat; :: 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;