let p be Nat; :: thesis: for n0, m0 being non zero Nat st p is prime holds
p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0))
let n0, m0 be non zero Nat; :: thesis: ( p is prime implies p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0)) )
reconsider h9 = n0 gcd m0 as non zero Nat by INT_2:5;
assume A1: p is prime ; :: thesis: p |-count (n0 gcd m0) = min ((p |-count n0),(p |-count m0))
then reconsider p9 = p as Prime ;
h9 divides n0 by INT_2:def 2;
then A2: p9 |-count h9 <= p9 |-count n0 by NAT_3:30;
h9 divides m0 by INT_2:def 2;
then A3: p9 |-count h9 <= p9 |-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 = p9 |^ (p9 |-count n0);
A5: p9 |^ (p |-count n0) divides m0 by A4, MOEBIUS1:9;
A6: p > 1 by A1, INT_2:def 4;
then p9 |^ (p9 |-count n0) divides n0 by NAT_3:def 7;
then p9 |^ (p9 |-count n0) divides h9 by A5, INT_2:def 2;
then p9 |-count (p9 |^ (p9 |-count n0)) <= p9 |-count h9 by NAT_3:30;
then p9 |-count n0 <= p9 |-count h9 by A6, 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 = p9 |^ (p9 |-count m0);
A8: p9 |^ (p |-count m0) divides n0 by A7, MOEBIUS1:9;
A9: p > 1 by A1, INT_2:def 4;
then p9 |^ (p9 |-count m0) divides m0 by NAT_3:def 7;
then p9 |^ (p9 |-count m0) divides h9 by A8, INT_2:def 2;
then p9 |-count (p9 |^ (p9 |-count m0)) <= p9 |-count h9 by NAT_3:30;
then p9 |-count m0 <= p9 |-count h9 by A9, 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;