let p be Prime; :: thesis: for n, m being Nat st n divides p |^ m holds
ex r being Nat st
( n = p |^ r & r <= m )
let n, m be Nat; :: thesis: ( n divides p |^ m implies ex r being Nat st
( n = p |^ r & r <= m ) )
assume A1: n divides p |^ m ; :: thesis: ex r being Nat st
( n = p |^ r & r <= m )
n > 0

proof

assume n <= 0 ; :: thesis: contradiction
then n = 0 ;
hence contradiction by A1, INT_2:3; :: thesis: verum

end;

then n in NatDivisors (p |^ m) by A1, MOEBIUS1:39;
then n in { (p |^ k) where k is Element of NAT : k <= m } by NAT_5:19;
then consider r being Element of NAT such that
A2: ( n = p |^ r & r <= m ) ;
take r ; :: thesis: ( n = p |^ r & r <= m )
thus ( n = p |^ r & r <= m ) by A2; :: thesis: verum