let i, k, n be Nat; ( i <> 0 & k <> 0 implies (n mod (i |^ k)) div (i |^ (k -' 1)) < i )
assume that
A1:
i <> 0
and
A2:
k <> 0
; (n mod (i |^ k)) div (i |^ (k -' 1)) < i
A3:
n mod (i |^ k) < i |^ k
by A1, NAT_D:1, PREPOWER:6;
reconsider n = n, i = i, k = k as Element of NAT by ORDINAL1:def 12;
set I1 = i |^ (k -' 1);
set T = n mod (i |^ k);
i |^ k = i * (i |^ (k -' 1))
by A1, A2, PEPIN:26;
then (n mod (i |^ k)) mod (i |^ (k -' 1)) =
n mod (i |^ (k -' 1))
by A1, Th3
.=
n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))
by A1, NEWTON:63, PREPOWER:6
;
then
n mod (i |^ k) = ((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + (n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))))
by A1, NAT_D:2, PREPOWER:6;
then A4:
((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + (n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))) < i * (i |^ (k -' 1))
by A1, A2, A3, PEPIN:26;
A5:
i |^ (k -' 1) <> 0
by A1, PREPOWER:6;
[\(n / (i |^ (k -' 1)))/] <= n / (i |^ (k -' 1))
by INT_1:def 6;
then
( n div (i |^ (k -' 1)) = [\(n / (i |^ (k -' 1)))/] & ((n mod (i |^ k)) div (i |^ (k -' 1))) + [\(n / (i |^ (k -' 1)))/] <= ((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1))) )
by INT_1:def 9, XREAL_1:6;
then A6:
(((n mod (i |^ k)) div (i |^ (k -' 1))) + [\(n / (i |^ (k -' 1)))/]) - [\(n / (i |^ (k -' 1)))/] <= (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1)))
by XREAL_1:9;
i |^ (k -' 1) > 0
by A1, PREPOWER:6;
then
((((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) + n) - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1))))) / (i |^ (k -' 1)) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1))
by A4, XREAL_1:74;
then
((((i |^ (k -' 1)) * ((n mod (i |^ k)) div (i |^ (k -' 1)))) / (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) / (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1))
by XCMPLX_1:124;
then
(((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) / (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1))
by A5, XCMPLX_1:89;
then
(((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) < (i * (i |^ (k -' 1))) / (i |^ (k -' 1))
by A5, XCMPLX_1:89;
then
(((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) < i
by A5, XCMPLX_1:89;
hence
(n mod (i |^ k)) div (i |^ (k -' 1)) < i
by A6, XXREAL_0:2; verum