let a, b, d, s be Nat; ( b > 0 & d > 1 & s > 0 implies ex m, i being Nat st (digits (((ArProg (a,b)) . m),d)) /^ i = digits (s,d) )
assume that
A1:
( b > 0 & d > 1 )
and
A2:
s > 0
; ex m, i being Nat st (digits (((ArProg (a,b)) . m),d)) /^ i = digits (s,d)
set r = a mod b;
set t = a div b;
A3:
a = (b * (a div b)) + (a mod b)
by A1, NAT_D:2;
A4:
a mod b < b
by A1, NAT_D:1;
d >= 1 + 1
by A1, NAT_1:13;
then consider n being positive Nat such that
A5:
((2 * b) * ((a div b) + 1)) + 1 <= d |^ n
by LIOUVIL2:1;
b + 0 < b + b
by A1, XREAL_1:8;
then A6:
b * ((a div b) + 1) < (2 * b) * ((a div b) + 1)
by XREAL_1:68;
1 + 0 <= s
by A2, NAT_1:13;
then A7:
1 * (d |^ n) <= s * (d |^ n)
by XREAL_1:64;
A8:
(2 * b) * ((a div b) + 1) < d |^ n
by A5, NAT_1:13;
then
b * ((a div b) + 1) < d |^ n
by A6, XXREAL_0:2;
then
b * ((a div b) + 1) < s * (d |^ n)
by A7, XXREAL_0:2;
then
(a div b) + 1 < (s * (d |^ n)) / b
by A1, XREAL_1:81;
then A9:
((s * (d |^ n)) / b) - (a div b) > 1
by XREAL_1:20;
set k = [/(((s * (d |^ n)) / b) - (a div b))\];
((s * (d |^ n)) / b) - (a div b) <= [/(((s * (d |^ n)) / b) - (a div b))\]
by INT_1:def 7;
then reconsider k = [/(((s * (d |^ n)) / b) - (a div b))\] as Element of NAT by A9, INT_1:3;
take
k
; ex i being Nat st (digits (((ArProg (a,b)) . k),d)) /^ i = digits (s,d)
take
n
; (digits (((ArProg (a,b)) . k),d)) /^ n = digits (s,d)
(s * (d |^ n)) / b <= k + (a div b)
by INT_1:def 7, XREAL_1:20;
then A10:
s * (d |^ n) <= b * (k + (a div b))
by A1, XREAL_1:81;
k < (((s * (d |^ n)) / b) - (a div b)) + 1
by INT_1:def 7;
then A11:
k + 1 <= ((((s * (d |^ n)) / b) - (a div b)) + 1) + 1
by XREAL_1:6;
0 + 1 <= (a div b) + 1
by XREAL_1:6;
then
(2 * b) * 1 <= (2 * b) * ((a div b) + 1)
by XREAL_1:64;
then
(2 * b) * 1 < d |^ n
by A8, XXREAL_0:2;
then
2 < (d |^ n) / b
by A1, XREAL_1:81;
then A12:
(((s * (d |^ n)) / b) - (a div b)) + 2 < (((s * (d |^ n)) / b) - (a div b)) + ((d |^ n) / b)
by XREAL_1:8;
(((s * (d |^ n)) / b) - (a div b)) + ((d |^ n) / b) =
(((s * (d |^ n)) / b) + ((d |^ n) / b)) - (a div b)
.=
(((s * (d |^ n)) + (d |^ n)) / b) - (a div b)
by XCMPLX_1:62
.=
(((s + 1) * (d |^ n)) / b) - (a div b)
;
then
k + 1 < (((s + 1) * (d |^ n)) / b) - (a div b)
by A11, A12, XXREAL_0:2;
then
(k + 1) + (a div b) < ((s + 1) * (d |^ n)) / b
by XREAL_1:20;
then A13:
((k + 1) + (a div b)) * b < (s + 1) * (d |^ n)
by A1, XREAL_1:79;
(b * (k + (a div b))) + 0 <= (b * (k + (a div b))) + (a mod b)
by XREAL_1:7;
then A14:
s * (d |^ n) <= (b * k) + a
by A3, A10, XXREAL_0:2;
(b * k) + a = ((b * k) + (b * (a div b))) + (a mod b)
by A3;
then
(b * k) + a < ((b * k) + (b * (a div b))) + b
by A4, XREAL_1:8;
then
(b * k) + a < (s + 1) * (d |^ n)
by A13, XXREAL_0:2;
then
digits (s,d) = (digits (((b * k) + a),d)) /^ n
by Th2, A1, A2, A14;
hence
(digits (((ArProg (a,b)) . k),d)) /^ n = digits (s,d)
by NUMBER06:7; verum