let a, n, k be Nat; :: thesis: for b being non zero Nat holds (b |^ n) * ((a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k))) = (a mod (b |^ (n + k))) - (a mod (b |^ n))
let b be non zero Nat; :: thesis: (b |^ n) * ((a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k))) = (a mod (b |^ (n + k))) - (a mod (b |^ n))
( a = ((b |^ (n + k)) * (a div (b |^ (n + k)))) + (a mod (b |^ (n + k))) & a = ((b |^ n) * (a div (b |^ n))) + (a mod (b |^ n)) ) by NAT_D:2;
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 (b |^ n) * ((a div (b |^ n)) - ((a div (b |^ (n + k))) * (b |^ k))) = (a mod (b |^ (n + k))) - (a mod (b |^ n)) ; :: thesis: verum