let i, k, n be Nat; :: thesis: ( i <> 0 & k <> 0 implies (n mod (i |^ k)) div (i |^ (k -' 1)) < i )
assume A1: ( i <> 0 & k <> 0 ) ; :: thesis: (n mod (i |^ k)) div (i |^ (k -' 1)) < i
then A2: i > 0 ;
then A3: n mod (i |^ k) < i |^ k by NAT_D:1, PREPOWER:13;
reconsider n = n, i = i, k = k as Element of NAT by ORDINAL1:def 13;
set I1 = i |^ (k -' 1);
set T = n mod (i |^ k);
A4: i |^ (k -' 1) > 0 by A2, PREPOWER:13;
A5: i |^ (k -' 1) <> 0 by A2, PREPOWER:13;
i |^ k = i * (i |^ (k -' 1)) by A1, PEPIN:27;
then (n mod (i |^ k)) mod (i |^ (k -' 1)) = n mod (i |^ (k -' 1)) by A1, Th4
.= n - ((i |^ (k -' 1)) * (n div (i |^ (k -' 1)))) by A2, NEWTON:77, PREPOWER:13 ;
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 A2, NAT_D:2, PREPOWER:13;
then ((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, A3, PEPIN:27;
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:76;
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:125;
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:90;
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:90;
then A6: (((n mod (i |^ k)) div (i |^ (k -' 1))) + (n / (i |^ (k -' 1)))) - (n div (i |^ (k -' 1))) < i by A5, XCMPLX_1:90;
A7: n div (i |^ (k -' 1)) = [\(n / (i |^ (k -' 1)))/] by INT_1:def 7;
[\(n / (i |^ (k -' 1)))/] <= n / (i |^ (k -' 1)) by INT_1:def 4;
then ((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 XREAL_1:8;
then (((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 A7, XREAL_1:11;
hence (n mod (i |^ k)) div (i |^ (k -' 1)) < i by A6, XXREAL_0:2; :: thesis: verum