let p be Prime; :: thesis: for a, b being non zero Nat holds p |-count (a * b) = (p |-count a) + (p |-count b)
let a, b be non zero Nat; :: thesis: p |-count (a * b) = (p |-count a) + (p |-count b)
set x = p |-count a;
set y = p |-count b;
A1: p <> 1 by INT_2:def 4;
then A2: p |^ (p |-count b) divides b by Def7;
A3: p |^ (p |-count a) divides a by A1, Def7;

A4: now :: thesis: not p |^ (((p |-count a) + (p |-count b)) + 1) divides a * b

assume p |^ (((p |-count a) + (p |-count b)) + 1) divides a * b ; :: thesis: contradiction
then consider v being Nat such that
A5: a * b = (p |^ (((p |-count a) + (p |-count b)) + 1)) * v ;
p |^ (((p |-count a) + (p |-count b)) + 1) = (p |^ ((p |-count a) + (p |-count b))) * p by NEWTON:6;
then A6: a * b = (p |^ ((p |-count a) + (p |-count b))) * (p * v) by A5;
consider t being Nat such that
A7: a = (p |^ (p |-count a)) * t by A3;
A8: not p |^ ((p |-count a) + 1) divides a by A1, Def7;
A9: not p |^ ((p |-count b) + 1) divides b by A1, Def7;
consider u being Nat such that
A10: b = (p |^ (p |-count b)) * u by A2;
a * b = (((p |^ (p |-count a)) * (p |^ (p |-count b))) * t) * u by A7, A10
.= ((p |^ ((p |-count a) + (p |-count b))) * t) * u by NEWTON:8
.= (p |^ ((p |-count a) + (p |-count b))) * (t * u) ;
then p * v = t * u by A6, XCMPLX_1:5;
then A11: p divides t * u ;

per cases ( p divides t or p divides u ) by A11, NEWTON:80;

suppose p divides t ; :: thesis: contradiction

then consider t1 being Nat such that
A12: t = p * t1 ;
a = ((p |^ (p |-count a)) * p) * t1 by A7, A12
.= (p |^ ((p |-count a) + 1)) * t1 by NEWTON:6 ;
hence contradiction by A8; :: thesis: verum

end;

suppose p divides u ; :: thesis: contradiction

then consider t1 being Nat such that
A13: u = p * t1 ;
b = ((p |^ (p |-count b)) * p) * t1 by A10, A13
.= (p |^ ((p |-count b) + 1)) * t1 by NEWTON:6 ;
hence contradiction by A9; :: thesis: verum

end;

end;

end;

p |^ ((p |-count a) + (p |-count b)) = (p |^ (p |-count a)) * (p |^ (p |-count b)) by NEWTON:8;
then p |^ ((p |-count a) + (p |-count b)) divides a * b by A3, A2, Th1;
hence p |-count (a * b) = (p |-count a) + (p |-count b) by A1, A4, Def7; :: thesis: verum