theorem :: NEWTON03:94

for n being Nat
for p being prime Nat
for a being non trivial Nat holds (p |-count a) * (a |-count (p |^ n)) <= n