let a be non trivial Nat; :: thesis: for n, b being non zero Nat holds a |-count b >= n * ((a |^ n) |-count b)
let n, b be non zero Nat; :: thesis: a |-count b >= n * ((a |^ n) |-count b)
A1: ( a <> 1 & b <> 0 ) by Def0;
reconsider k = a |^ n as non trivial Nat ;
( k <> 1 & b <> 0 ) by Def0;
then ( k |^ (k |-count b) divides b & not k |^ ((k |-count b) + 1) divides b ) by NAT_3:def 7;
then a |^ (n * ((a |^ n) |-count b)) divides b by NEWTON:9;
hence a |-count b >= n * ((a |^ n) |-count b) by A1, NAT330; :: thesis: verum