let a, n be Nat; :: thesis: for b being non zero Nat holds (a mod (b |^ (n + 1))) div (b |^ n) < b
let b be non zero Nat; :: thesis: (a mod (b |^ (n + 1))) div (b |^ n) < b
A1: (a mod (b |^ (n + 1))) div (b |^ (n + 1)) = (a mod (b |^ (n + 1))) div ((b |^ n) * b) by NEWTON:6
.= ((a mod (b |^ (n + 1))) div (b |^ n)) div b by PRE_FF:5 ;
assume not (a mod (b |^ (n + 1))) div (b |^ n) < b ; :: thesis: contradiction
then ((a mod (b |^ (n + 1))) div (b |^ n)) div b >= b div b by NAT_2:24;
hence contradiction by A1; :: thesis: verum