let a, b, i be Nat; ( 1 <= i & 0 < b implies (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b )
assume that
A1:
1 <= i
and
A2:
0 < b
; (a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b
set j = i -' 1;
set B0 = b |^ (i -' 1);
A3:
b |^ (i -' 1) > 0
by A2, PREPOWER:6;
set B1 = b |^ ((i -' 1) + 1);
A4:
a mod (b |^ ((i -' 1) + 1)) = a - ((b |^ ((i -' 1) + 1)) * (a div (b |^ ((i -' 1) + 1))))
by A2, NEWTON:63, PREPOWER:6;
reconsider Z = b * (- (a div (b |^ ((i -' 1) + 1)))) as Integer ;
(i -' 1) + 1 =
(i - 1) + 1
by A1, XREAL_1:233
.=
i
;
then (a mod (b |^ i)) div (b |^ (i -' 1)) =
(a + ((b |^ ((i -' 1) + 1)) * (- (a div (b |^ ((i -' 1) + 1)))))) div (b |^ (i -' 1))
by A4
.=
(a + (((b |^ (i -' 1)) * b) * (- (a div (b |^ ((i -' 1) + 1)))))) div (b |^ (i -' 1))
by NEWTON:6
.=
[\((a + ((b |^ (i -' 1)) * Z)) / (b |^ (i -' 1)))/]
by INT_1:def 9
.=
[\((a / (b |^ (i -' 1))) + Z)/]
by A3, XCMPLX_1:113
.=
[\(a / (b |^ (i -' 1)))/] + Z
by INT_1:28
.=
(a div (b |^ (i -' 1))) + (- (b * (a div (b |^ ((i -' 1) + 1)))))
by INT_1:def 9
.=
(a div (b |^ (i -' 1))) - (b * (a div (b |^ ((i -' 1) + 1))))
.=
(a div (b |^ (i -' 1))) - (b * (a div ((b |^ (i -' 1)) * b)))
by NEWTON:6
.=
(a div (b |^ (i -' 1))) - (b * ((a div (b |^ (i -' 1))) div b))
by NAT_2:27
;
hence
(a mod (b |^ i)) div (b |^ (i -' 1)) = (a div (b |^ (i -' 1))) mod b
by A2, NEWTON:63; verum