let k, n be Nat; ( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k)) )
defpred S1[ Nat] means for m being Nat st m is_represented_by $1,k holds
m = SDDec (DecSD (m,$1,k));
A1:
for u being Nat st u >= 1 & S1[u] holds
S1[u + 1]
proof
let u be
Nat;
( u >= 1 & S1[u] implies S1[u + 1] )
assume that
u >= 1
and A2:
S1[
u]
;
S1[u + 1]
for
p being
Nat st
p is_represented_by u + 1,
k holds
p = SDDec (DecSD (p,(u + 1),k))
proof
let p be
Nat;
( p is_represented_by u + 1,k implies p = SDDec (DecSD (p,(u + 1),k)) )
set I =
u + 1;
set R =
(Radix k) |^ u;
set M =
p mod ((Radix k) |^ u);
set N =
((Radix k) |^ u) * (p div ((Radix k) |^ u));
A3:
(u + 1) -' 1
= u
by NAT_D:34;
A4:
u + 1
<= len (DigitSD (DecSD (p,(u + 1),k)))
by CARD_1:def 7;
A5:
1
<= u + 1
by NAT_1:12;
then A6:
u + 1
in Seg (u + 1)
by FINSEQ_1:1;
assume
p is_represented_by u + 1,
k
;
p = SDDec (DecSD (p,(u + 1),k))
then
p < (Radix k) |^ (u + 1)
;
then
p div ((Radix k) |^ u) = DigitDC (
p,
(u + 1),
k)
by A3, NAT_D:24;
then A7:
((Radix k) |^ u) * (p div ((Radix k) |^ u)) =
SubDigit (
(DecSD (p,(u + 1),k)),
(u + 1),
k)
by A3, A6, Def9
.=
(DigitSD (DecSD (p,(u + 1),k))) /. (u + 1)
by A6, Def6
.=
(DigitSD (DecSD (p,(u + 1),k))) . (u + 1)
by A4, FINSEQ_4:15, NAT_1:12
;
A8:
(DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD (p,(u + 1),k))
proof
((Radix k) |^ u) * (p div ((Radix k) |^ u)) is
Element of
INT
by INT_1:def 2;
then reconsider z1 =
<*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> as
FinSequence of
INT by FINSEQ_1:74;
reconsider DD =
DigitSD (DecSD (p,(u + 1),k)) as
FinSequence of
INT ;
set z0 =
DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k));
reconsider z =
(DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1 as
FinSequence of
INT ;
A9:
len z =
(len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))) + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>)
by FINSEQ_1:22
.=
u + (len <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*>)
by CARD_1:def 7
.=
u + 1
by FINSEQ_1:39
;
A10:
for
i being
Nat st 1
<= i &
i <= len z holds
z /. i = DD /. i
proof
let i be
Nat;
( 1 <= i & i <= len z implies z /. i = DD /. i )
assume
( 1
<= i &
i <= len z )
;
z /. i = DD /. i
then A11:
i in Seg (u + 1)
by A9, FINSEQ_1:1;
per cases
( i in Seg u or i = u + 1 )
by A11, FINSEQ_2:7;
suppose A12:
i in Seg u
;
z /. i = DD /. iA13:
(p mod ((Radix k) |^ u)) mod ((Radix k) |^ i) = p mod ((Radix k) |^ i)
A15:
i in dom ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1)
by A9, A11, FINSEQ_1:def 3;
len DD = u + 1
by CARD_1:def 7;
then A16:
i in dom DD
by A11, FINSEQ_1:def 3;
then A17:
DD . i = DD /. i
by PARTFUN1:def 6;
A18:
DD . i =
(DigitSD (DecSD (p,(u + 1),k))) /. i
by A16, PARTFUN1:def 6
.=
SubDigit (
(DecSD (p,(u + 1),k)),
i,
k)
by A11, Def6
.=
((Radix k) |^ (i -' 1)) * (DigitDC (p,i,k))
by A11, Def9
.=
((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)))
;
len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) = u
by CARD_1:def 7;
then A19:
i in dom (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))
by A12, FINSEQ_1:def 3;
then ((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) . i =
(DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) . i
by FINSEQ_1:def 7
.=
(DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) /. i
by A19, PARTFUN1:def 6
.=
SubDigit (
(DecSD ((p mod ((Radix k) |^ u)),u,k)),
i,
k)
by A12, Def6
.=
((Radix k) |^ (i -' 1)) * (DigitDC ((p mod ((Radix k) |^ u)),i,k))
by A12, Def9
.=
((Radix k) |^ (i -' 1)) * ((p mod ((Radix k) |^ i)) div ((Radix k) |^ (i -' 1)))
by A13
;
hence
z /. i = DD /. i
by A18, A17, A15, PARTFUN1:def 6;
verum end; suppose A20:
i = u + 1
;
z /. i = DD /. ihence z /. i =
z . (u + 1)
by A5, A9, FINSEQ_4:15
.=
((DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ z1) . ((len (DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k)))) + 1)
by CARD_1:def 7
.=
(DigitSD (DecSD (p,(u + 1),k))) . (u + 1)
by A7, FINSEQ_1:42
.=
DD /. i
by A4, A20, FINSEQ_4:15, NAT_1:12
;
verum end;
end;
len DD = u + 1
by CARD_1:def 7;
hence
(DigitSD (DecSD ((p mod ((Radix k) |^ u)),u,k))) ^ <*(((Radix k) |^ u) * (p div ((Radix k) |^ u)))*> = DigitSD (DecSD (p,(u + 1),k))
by A9, A10, FINSEQ_5:13;
verum
end;
Radix k <> 0
by POWER:34;
then A21:
(Radix k) |^ u <> 0
by PREPOWER:5;
then
p mod ((Radix k) |^ u) < (Radix k) |^ u
by NAT_D:1;
then A22:
p mod ((Radix k) |^ u) is_represented_by u,
k
;
p = (((Radix k) |^ u) * (p div ((Radix k) |^ u))) + (p mod ((Radix k) |^ u))
by A21, NAT_D:2;
then
p = (SDDec (DecSD ((p mod ((Radix k) |^ u)),u,k))) + (((Radix k) |^ u) * (p div ((Radix k) |^ u)))
by A2, A22;
hence
p = SDDec (DecSD (p,(u + 1),k))
by A8, RVSUM_1:74;
verum
end;
hence
S1[
u + 1]
;
verum
end;
A23:
S1[1]
proof
let m be
Nat;
( m is_represented_by 1,k implies m = SDDec (DecSD (m,1,k)) )
assume A24:
m is_represented_by 1,
k
;
m = SDDec (DecSD (m,1,k))
reconsider i =
m as
Element of
REAL by XREAL_0:def 1;
reconsider M =
<*i*> as
FinSequence of
REAL ;
A25:
1
in Seg 1
by FINSEQ_1:1;
SubDigit (
(DecSD (m,1,k)),1,
k) =
((Radix k) |^ 0) * (DigB ((DecSD (m,1,k)),1))
by XREAL_1:232
.=
1
* (DigB ((DecSD (m,1,k)),1))
by NEWTON:4
.=
m
by A24, Th20
;
then
(DigitSD (DecSD (m,1,k))) /. 1
= m
by A25, Def6;
hence SDDec (DecSD (m,1,k)) =
Sum M
by Th16
.=
m
by FINSOP_1:11
;
verum
end;
for u being Nat st u >= 1 holds
S1[u]
from NAT_1:sch 8(A23, A1);
hence
( n >= 1 implies for m being Nat st m is_represented_by n,k holds
m = SDDec (DecSD (m,n,k)) )
; verum