let a be non trivial Nat; :: thesis: for b being non zero Integer
for n being non zero Nat holds
( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) )
let b be non zero Integer; :: thesis: for n being non zero Nat holds
( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) )
let n be non zero Nat; :: thesis: ( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) )
reconsider k = a |-count b as Nat ;
A0: ( (a |^ k) |^ n = a |^ (k * n) & (a |^ (k + 1)) |^ n = a |^ ((k + 1) * n) ) by NEWTON:9;
a <> 1 by NAT_2:def 1;
then A1: ( a |^ k divides b & not a |^ (k + 1) divides b ) by Def6;
( (a |^ k) gcd b = |.(a |^ k).| & (a |^ (k + 1)) gcd b <> |.(a |^ (k + 1)).| ) by A1, NEWTON02:3;
then ( ((a |^ k) gcd b) |^ n = (a |^ k) |^ n & ((a |^ (k + 1)) gcd b) |^ n <> (a |^ (k + 1)) |^ n ) by WSIERP_1:3;
then ( ((a |^ k) |^ n) gcd (b |^ n) = |.((a |^ k) |^ n).| & ((a |^ (k + 1)) |^ n) gcd (b |^ n) <> |.((a |^ (k + 1)) |^ n).| ) by NEWTON027;
hence ( n * (a |-count b) <= a |-count (b |^ n) & a |-count (b |^ n) < n * ((a |-count b) + 1) ) by Count1, A0, NEWTON02:3; :: thesis: verum