theorem :: NAT_5:21

for p being Nat
for n0, m0 being non zero Nat st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) by Lm1;