let n be Nat; :: thesis: for b being non trivial Nat holds n div b = value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)
let b be non trivial Nat; :: thesis: n div b = value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b)
((n div b) * b) + (n mod b) = n by NAT_D:2
.= (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + ((digits (n,b)) . 0) by NEWTON03:def 1, NUMERAL2:19
.= (b * (value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b))) + (n mod b) by NMB ;
hence n div b = value ((mid ((digits (n,b)),2,(len (digits (n,b))))),b) by XCMPLX_1:5; :: thesis: verum