let a be Integer; :: thesis: for b being non zero Integer
for n being non zero Nat st a = b |^ n holds
for p being prime Nat holds n divides p |-count a
let b be non zero Integer; :: thesis: for n being non zero Nat st a = b |^ n holds
for p being prime Nat holds n divides p |-count a
let n be non zero Nat; :: thesis: ( a = b |^ n implies for p being prime Nat holds n divides p |-count a )
assume A1: a = b |^ n ; :: thesis: for p being prime Nat holds n divides p |-count a
for p being prime Nat holds n divides p |-count a

proof

let p be prime Nat; :: thesis: n divides p |-count a
p |-count (b |^ n) = n * (p |-count b) by NAT332;
hence n divides p |-count a by A1; :: thesis: verum

end;

hence for p being prime Nat holds n divides p |-count a ; :: thesis: verum