theorem NAT328: :: NEWTON03:57

for p being prime Nat
for a, b being non zero Integer holds p |-count (a * b) = (p |-count a) + (p |-count b)