let a, n, k be Nat; :: thesis: for b being non zero Nat holds (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k)))))
let b be non zero Nat; :: thesis: (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k)))))
( a mod (b |^ n) = a - ((b |^ n) * (a div (b |^ n))) & a mod (b |^ (n + k)) = a - ((b |^ (n + k)) * (a div (b |^ (n + k)))) ) by MD;
then (a mod (b |^ (n + k))) - (a mod (b |^ n)) = ((b |^ n) * (a div (b |^ n))) - ((b |^ (n + k)) * (a div (b |^ (n + k))))
.= ((b |^ n) * (a div (b |^ n))) - (((b |^ n) * (b |^ k)) * (a div (b |^ (n + k)))) by NEWTON:8
.= (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k))))) ;
hence (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k))))) ; :: thesis: verum