let n be Nat; :: thesis: for p being prime Nat
for a being non trivial Nat holds (p |-count a) * (a |-count (p |^ n)) <= n
let p be prime Nat; :: thesis: for a being non trivial Nat holds (p |-count a) * (a |-count (p |^ n)) <= n
let a be non trivial Nat; :: thesis: (p |-count a) * (a |-count (p |^ n)) <= n
A1: p > 1 by NAT_4:14;
p |^ ((p |-count a) * (a |-count (p |^ n))) <= p |^ n by Count7;
hence (p |-count a) * (a |-count (p |^ n)) <= n by A1, PEPIN:66; :: thesis: verum