theorem Ciek: :: MOEBIUS2:40

for n, i being Nat
for p being Prime st n <> 0 & p |^ i divides n holds
i <= p |-count n