let a, b be non zero Integer; :: thesis: for c being non trivial Nat holds c |-count (a gcd b) = min ((c |-count a),(c |-count b))
let c be non trivial Nat; :: thesis: c |-count (a gcd b) = min ((c |-count a),(c |-count b))
A1: |.c.| > 1 by NEWTON03:def 1;
then A3: ( c |^ (c |-count a) divides a & not c |^ ((c |-count a) + 1) divides a ) by NEWTON03:def 7;
A4: ( c |^ (c |-count b) divides b & not c |^ ((c |-count b) + 1) divides b ) by A1, NEWTON03:def 7;
A5: ( |.(c |^ ((c |-count b) + 1)).| in NAT & |.a.| in NAT & |.b.| in NAT ) by INT_1:3;

per cases ( c |-count a >= c |-count b or c |-count b > c |-count a ) ;

suppose B1: c |-count a >= c |-count b ; :: thesis: c |-count (a gcd b) = min ((c |-count a),(c |-count b))

then B2: min ((c |-count a),(c |-count b)) = c |-count b by XXREAL_0:def 9;
c |^ (c |-count b) divides c |^ (c |-count a) by B1, NEWTON:89;
then c |^ (c |-count b) divides a by A3, INT_2:9;
then B3: c |^ (c |-count b) divides a gcd b by A4, INT_2:def 2;
not |.(c |^ ((c |-count b) + 1)).| divides |.b.| by A4, INT_2:16;
then not |.(c |^ ((c |-count b) + 1)).| divides |.a.| gcd |.b.| by A5, NEWTON:50;
then not c |^ ((c |-count b) + 1) divides a gcd b by INT_2:34;
hence c |-count (a gcd b) = min ((c |-count a),(c |-count b)) by A1, B2, B3, NEWTON03:def 7; :: thesis: verum

end;

suppose B1: c |-count b > c |-count a ; :: thesis: c |-count (a gcd b) = min ((c |-count a),(c |-count b))

then B2: min ((c |-count b),(c |-count a)) = c |-count a by XXREAL_0:def 9;
c |^ (c |-count a) divides c |^ (c |-count b) by B1, NEWTON:89;
then c |^ (c |-count a) divides b by A4, INT_2:9;
then B3: c |^ (c |-count a) divides a gcd b by A3, INT_2:def 2;
not |.(c |^ ((c |-count a) + 1)).| divides |.a.| by A3, INT_2:16;
then not |.(c |^ ((c |-count a) + 1)).| divides |.a.| gcd |.b.| by A5, NEWTON:50;
then not c |^ ((c |-count a) + 1) divides a gcd b by INT_2:34;
hence c |-count (a gcd b) = min ((c |-count a),(c |-count b)) by A1, B2, B3, NEWTON03:def 7; :: thesis: verum

end;

end;