let n be Nat; :: thesis: for a being non trivial Nat
for b being non zero Integer holds a |-count ((a |^ n) * b) = n + (a |-count b)
let a be non trivial Nat; :: thesis: for b being non zero Integer holds a |-count ((a |^ n) * b) = n + (a |-count b)
let b be non zero Integer; :: thesis: a |-count ((a |^ n) * b) = n + (a |-count b)
A0: ( (a |^ n) * (a |^ (a |-count b)) = a |^ ((a |-count b) + n) & (a |^ n) * (a |^ ((a |-count b) + 1)) = a |^ (((a |-count b) + 1) + n) ) by NEWTON:8;
A1: a <> 1 by Def0;
then ( a |^ (a |-count b) divides b & not a |^ ((a |-count b) + 1) divides b ) by Def6;
then ( a |^ ((a |-count b) + n) divides (a |^ n) * b & not a |^ (((a |-count b) + n) + 1) divides (a |^ n) * b ) by INT_4:7, A0;
hence a |-count ((a |^ n) * b) = n + (a |-count b) by A1, Def6; :: thesis: verum