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;

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 )
;

end;

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;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

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;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