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)) mod (b |^ k))
let b be non zero Nat; :: thesis: (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) mod (b |^ k))
A1: a div (b |^ n) = ((b |^ k) * ((a div (b |^ n)) div (b |^ k))) + ((a div (b |^ n)) mod (b |^ k)) by NAT_D:2;
(a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * (a div (b |^ (n + k))))) by DMK
.= (b |^ n) * ((a div (b |^ n)) - ((b |^ k) * ((a div (b |^ n)) div (b |^ k)))) by DNK
.= (b |^ n) * ((a div (b |^ n)) mod (b |^ k)) by A1 ;
hence (a mod (b |^ (n + k))) - (a mod (b |^ n)) = (b |^ n) * ((a div (b |^ n)) mod (b |^ k)) ; :: thesis: verum