let a be non trivial Nat; :: thesis: for b, c being non zero Integer holds
( a |-count b = a |-count c iff for n being Nat holds
( a |^ n divides b iff a |^ n divides c ) )
let b, c be non zero Integer; :: thesis: ( a |-count b = a |-count c iff for n being Nat holds
( a |^ n divides b iff a |^ n divides c ) )
A1: a > 1 by Def0;
( a |-count b <> a |-count c implies ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) ) )

proof

reconsider n = a |-count b, m = a |-count c as Nat ;
assume a |-count b <> a |-count c ; :: thesis: ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) )

per cases then ( n > m or n < m ) by XXREAL_0:1;

suppose n > m ; :: thesis: ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) )

then ( a |^ n divides b & not a |^ n divides c ) by DL, A1, Def6;
hence ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) ) ; :: thesis: verum

end;

suppose n < m ; :: thesis: ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) )

then m >= n + 1 by NAT_1:13;
then ( a |^ (n + 1) divides a |^ m & a |^ m divides c ) by NEWTON:89, Def6, A1;
then ( a |^ (n + 1) divides c & not a |^ (n + 1) divides b ) by INT_2:9, A1, Def6;
hence ex n being Nat st
( ( a |^ n divides b & not a |^ n divides c ) or ( a |^ n divides c & not a |^ n divides b ) ) ; :: thesis: verum

end;

end;

end;

hence ( a |-count b = a |-count c iff for n being Nat holds
( a |^ n divides b iff a |^ n divides c ) ) by DN; :: thesis: verum