let p be natural number ; :: thesis: for n0, m0 being non zero natural number st p is prime holds
p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0)
let n0, m0 be non zero natural number ; :: thesis: ( p is prime implies p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0) )
assume A1: p is prime ; :: thesis: p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0)
then reconsider p' = p as Prime ;
reconsider h' = n0 gcd m0 as non empty natural number by INT_2:5;
h' divides n0 by INT_2:def 3;
then A2: p' |-count h' <= p' |-count n0 by NAT_3:30;
h' divides m0 by INT_2:def 3;
then A3: p' |-count h' <= p' |-count m0 by NAT_3:30;

per cases ( p |-count n0 <= p |-count m0 or not p |-count n0 <= p |-count m0 ) ;

suppose A4: p |-count n0 <= p |-count m0 ; :: thesis: p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0)

set k = p' |^ (p' |-count n0);
A5: p > 1 by A1, INT_2:def 5;
then A6: p' |^ (p' |-count n0) divides n0 by NAT_3:def 7;
p' |^ (p |-count n0) divides m0 by A4, MOEBIUS1:9;
then p' |^ (p' |-count n0) divides h' by A6, INT_2:def 3;
then p' |-count (p' |^ (p' |-count n0)) <= p' |-count h' by NAT_3:30;
then p' |-count n0 <= p' |-count h' by A5, NAT_3:25;
then p |-count (n0 gcd m0) = p |-count n0 by A2, XXREAL_0:1;
hence p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0) by A4, XXREAL_0:def 9; :: thesis: verum

end;

suppose A7: not p |-count n0 <= p |-count m0 ; :: thesis: p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0)

set k = p' |^ (p' |-count m0);
A8: p > 1 by A1, INT_2:def 5;
then A9: p' |^ (p' |-count m0) divides m0 by NAT_3:def 7;
p' |^ (p |-count m0) divides n0 by A7, MOEBIUS1:9;
then p' |^ (p' |-count m0) divides h' by A9, INT_2:def 3;
then p' |-count (p' |^ (p' |-count m0)) <= p' |-count h' by NAT_3:30;
then p' |-count m0 <= p' |-count h' by A8, NAT_3:25;
then p |-count (n0 gcd m0) = p |-count m0 by A3, XXREAL_0:1;
hence p |-count (n0 gcd m0) = min (p |-count n0),(p |-count m0) by A7, XXREAL_0:def 9; :: thesis: verum

end;

end;