let n be Nat; :: thesis: for a being non trivial Nat
for b being non zero Integer holds
( a |^ n divides b iff n <= a |-count b )
let a be non trivial Nat; :: thesis: for b being non zero Integer holds
( a |^ n divides b iff n <= a |-count b )
let b be non zero Integer; :: thesis: ( a |^ n divides b iff n <= a |-count b )
L0: a <> 1 by Def0;
L1: ( a |^ n divides b implies n <= a |-count b )

proof

assume A1: a |^ n divides b ; :: thesis: n <= a |-count b
( a |^ n divides b & not a |^ ((a |-count b) + 1) divides b implies not a |^ ((a |-count b) + 1) divides a |^ n ) by INT_2:9;
then (a |-count b) + 1 > n by L0, A1, Def6, NEWTON:89;
hence n <= a |-count b by NAT_1:13; :: thesis: verum

end;

( not a |^ n divides b implies a |-count b < n )

proof

assume A1: not a |^ n divides b ; :: thesis: a |-count b < n
( not a |^ n divides b & a |^ (a |-count b) divides b implies not a |^ n divides a |^ (a |-count b) ) by INT_2:9;
hence a |-count b < n by L0, A1, Def6, NEWTON:89; :: thesis: verum

end;

hence ( a |^ n divides b iff n <= a |-count b ) by L1; :: thesis: verum