reconsider d = <%0%> as XFinSequence of NAT ;
reconsider N = n, B = b as Element of NAT by ORDINAL1:def 12;
thus
( n <> 0 implies ex d being XFinSequence of NAT st
( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) ) )
( not n <> 0 implies ex b1 being XFinSequence of NAT st b1 = <%0%> )proof
deffunc H1(
Nat,
Element of
NAT )
-> Element of
NAT = $2
div B;
consider f being
sequence of
NAT such that A2:
(
f . 0 = N & ( for
i being
Nat holds
f . (i + 1) = H1(
i,
f . i) ) )
from NAT_1:sch 12();
defpred S1[
Nat]
means f . $1
= 0 ;
defpred S2[
Nat]
means ex
i being
Nat st
f . i = $1;
A3:
for
k being
Nat st
k <> 0 &
S2[
k] holds
ex
l being
Nat st
(
l < k &
S2[
l] )
proof
let k be
Nat;
( k <> 0 & S2[k] implies ex l being Nat st
( l < k & S2[l] ) )
assume that A4:
k <> 0
and A5:
S2[
k]
;
ex l being Nat st
( l < k & S2[l] )
take l =
k div b;
( l < k & S2[l] )
thus
l < k
by A1, A4, INT_1:56;
S2[l]
consider i being
Nat such that A6:
f . i = k
by A5;
take
i + 1
;
f . (i + 1) = l
thus
f . (i + 1) = l
by A2, A6;
verum
end;
A7:
ex
k being
Nat st
S2[
k]
by A2;
S2[
0 ]
from NAT_1:sch 7(A7, A3);
then A8:
ex
l being
Nat st
S1[
l]
;
consider l being
Nat such that A9:
(
S1[
l] & ( for
i being
Nat st
S1[
i] holds
l <= i ) )
from NAT_1:sch 5(A8);
assume
n <> 0
;
ex d being XFinSequence of NAT st
( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) )
then consider m being
Nat such that A10:
m + 1
= l
by A2, A9, NAT_1:6;
reconsider m =
m as
Element of
NAT by ORDINAL1:def 12;
dom f = NAT
by FUNCT_2:def 1;
then
m + 1
c= dom f
by ORDINAL1:def 2;
then
dom (f | (m + 1)) = m + 1
by RELAT_1:62;
then reconsider g =
f | (m + 1) as
XFinSequence of
NAT by ORDINAL1:def 7;
defpred S3[
Nat,
Nat]
means $2
= (g . $1) mod b;
A11:
for
i being
Nat st
i in Segm (m + 1) holds
ex
x being
Element of
NAT st
S3[
i,
x]
;
consider d being
XFinSequence of
NAT such that A12:
(
dom d = Segm (m + 1) & ( for
i being
Nat st
i in Segm (m + 1) holds
S3[
i,
d . i] ) )
from STIRL2_1:sch 5(A11);
A13:
now for i being Nat st l <= i & S1[i] holds
S1[i + 1]let i be
Nat;
( l <= i & S1[i] implies S1[i + 1] )assume
l <= i
;
( S1[i] implies S1[i + 1] )assume
S1[
i]
;
S1[i + 1]then
f . (i + 1) = 0 div b
by A2;
hence
S1[
i + 1]
by NAT_2:2;
verum end;
A14:
S1[
l]
by A9;
A15:
for
i being
Nat st
l <= i holds
S1[
i]
from NAT_1:sch 8(A14, A13);
deffunc H2(
Nat)
-> set =
(d . $1) * (b |^ $1);
consider d9 being
XFinSequence such that A17:
(
len d9 = len d & ( for
i being
Nat st
i in len d holds
d9 . i = H2(
i) ) )
from AFINSQ_1:sch 2();
rng d9 c= NAT
then reconsider d9 =
d9 as
XFinSequence of
NAT by RELAT_1:def 19;
consider s being
sequence of
NAT such that A20:
s . 0 = d9 . 0
and A21:
for
i being
Nat st
i + 1
< len d9 holds
s . (i + 1) = addnat . (
(s . i),
(d9 . (i + 1)))
and A22:
addnat "**" d9 = s . ((len d9) - 1)
by A12, A17, AFINSQ_2:def 8;
defpred S4[
Nat]
means ( $1
< len d9 implies
s . $1
= n - ((f . ($1 + 1)) * (b |^ ($1 + 1))) );
A23:
now for i being Nat st S4[i] holds
S4[i + 1]let i be
Nat;
( S4[i] implies S4[i + 1] )assume A24:
S4[
i]
;
S4[i + 1]now ( i + 1 < len d9 implies s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))) )assume A25:
i + 1
< len d9
;
s . (i + 1) = n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))then A26:
i + 1
in dom d9
by AFINSQ_1:86;
thus s . (i + 1) =
addnat . (
(s . i),
(d9 . (i + 1)))
by A21, A25
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (d9 . (i + 1))
by A24, A25, BINOP_2:def 23, NAT_1:13
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + ((d . (i + 1)) * (b |^ (i + 1)))
by A17, A26
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((g . (i + 1)) mod b) * (b |^ (i + 1)))
by A12, A17, A26
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) mod b) * (b |^ (i + 1)))
by A12, A17, A26, FUNCT_1:49
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * ((f . (i + 1)) div B))) * (b |^ (i + 1)))
by A1, NEWTON:63
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) - (b * (f . ((i + 1) + 1)))) * (b |^ (i + 1)))
by A2
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b * (b |^ (i + 1)))))
.=
(n - ((f . (i + 1)) * (b |^ (i + 1)))) + (((f . (i + 1)) * (b |^ (i + 1))) - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1))))
by NEWTON:6
.=
n - ((f . ((i + 1) + 1)) * (b |^ ((i + 1) + 1)))
;
verum end; hence
S4[
i + 1]
;
verum end;
reconsider ld =
(len d9) - 1 as
Element of
NAT by A12, A17;
A27:
0 in Segm (m + 1)
by NAT_1:44;
then d9 . 0 =
(d . 0) * (b |^ 0)
by A12, A17
.=
((g . 0) mod b) * (b |^ 0)
by A12, A27
.=
((f . 0) mod b) * (b |^ 0)
by A27, FUNCT_1:49
.=
(n mod b) * 1
by A2, NEWTON:4
.=
N - (B * (N div B))
by A1, NEWTON:63
.=
n - ((n div b) * (b |^ 1))
.=
n - ((f . (0 + 1)) * (b |^ (0 + 1)))
by A2
;
then A28:
S4[
0 ]
by A20;
for
i being
Nat holds
S4[
i]
from NAT_1:sch 2(A28, A23);
then s . ld =
n - ((f . (m + 1)) * (b |^ (m + 1)))
by A12, A17, XREAL_1:44
.=
n
by A9, A10
;
then A29:
n = Sum d9
by A22, AFINSQ_2:51;
m < l
by A10, NAT_1:13;
then A30:
f . m <> 0
by A9;
take
d
;
( value (d,b) = n & d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) )
thus
value (
d,
b)
= n
by A17, A29, Def1;
( d . ((len d) - 1) <> 0 & ( for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b ) ) )
m in Segm (m + 1)
by NAT_1:45;
then A31:
g . m = f . m
by FUNCT_1:49;
then
(
m < m + 1 &
f . (m + 1) = (g . m) div b )
by A2, NAT_1:13;
then A32:
(g . m) div b = 0
by A16;
d . ((len d) - 1) =
(g . m) mod b
by A12, NAT_1:45
.=
g . m
by A1, A32, NAT_2:12, NAT_D:24
;
hence
d . ((len d) - 1) <> 0
by A30, A31;
for i being Nat st i in dom d holds
( 0 <= d . i & d . i < b )
let i be
Nat;
( i in dom d implies ( 0 <= d . i & d . i < b ) )
assume
i in dom d
;
( 0 <= d . i & d . i < b )
then
d . i = (g . i) mod b
by A12;
hence
(
0 <= d . i &
d . i < b )
by A1, NAT_D:1;
verum
end;
assume
n = 0
; ex b1 being XFinSequence of NAT st b1 = <%0%>
take
d
; d = <%0%>
thus
d = <%0%>
; verum