let p be prime Nat; 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; ( n divides p |^ m implies ex r being Nat st
( n = p |^ r & r <= m ) )
assume A1:
n divides p |^ m
; ex r being Nat st
( n = p |^ r & r <= m )
n > 0
proof
assume
n <= 0
;
contradiction
then
n = 0
;
hence
contradiction
by A1, INT_2:3;
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
; ( n = p |^ r & r <= m )
thus
( n = p |^ r & r <= m )
by A2; verum