defpred S1[ Nat] means for k, x being Nat st k >= 2 & x is_represented_by $1,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,$1,k)));
let n be Nat; ( n >= 1 implies for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k))) )
assume A1:
n >= 1
; for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))
A2:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that A3:
n >= 1
and A4:
S1[
n]
;
S1[n + 1]
A5:
n in Seg n
by A3, FINSEQ_1:3;
let k,
x be
Nat;
( k >= 2 & x is_represented_by n + 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k))) )
assume that A6:
k >= 2
and A7:
x is_represented_by n + 1,
k
;
x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k)))
reconsider k =
k as
Element of
NAT by ORDINAL1:def 12;
set xn =
x mod ((Radix k) |^ n);
set RN1 =
(Radix k) |^ (n + 1);
set RN =
(Radix k) |^ n;
A8:
(n + 1) + 1
in Seg ((n + 1) + 1)
by FINSEQ_1:3;
A9:
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
((n + 1) + 1),
k) =
((Radix k) |^ (n + 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1)))
by NAT_D:34
.=
((Radix k) |^ (n + 1)) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),((n + 1) + 1),k))
by A8, Def8
.=
((Radix k) |^ (n + 1)) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),((n + 1) + 1),k))
by A6, A8, Def7
.=
((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(((n + 1) + 1) -' 1))),k))
by Def6
.=
((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k))
by NAT_D:34
;
set XN =
SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k));
set X =
SD2SDSub (DecSD (x,(n + 1),k));
deffunc H1(
Nat)
-> Element of
INT =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),$1,
k);
consider xp being
FinSequence of
INT such that A10:
len xp = n + 1
and A11:
for
i being
Nat st
i in dom xp holds
xp . i = H1(
i)
from FINSEQ_2:sch 1();
A12:
dom xp = Seg (n + 1)
by A10, FINSEQ_1:def 3;
A13:
len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = (n + 1) + 1
by CARD_1:def 7;
A14:
for
j being
Nat st 1
<= j &
j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) holds
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
proof
let j be
Nat;
( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) implies (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j )
assume that A15:
1
<= j
and A16:
j <= len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))))
;
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
j <= (n + 1) + 1
by A16, CARD_1:def 7;
then A17:
j in Seg ((n + 1) + 1)
by A15, FINSEQ_1:1;
A18:
j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))))
by A15, A16, FINSEQ_3:25;
now (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . jper cases
( j in Seg (n + 1) or j = (n + 1) + 1 )
by A17, FINSEQ_2:7;
suppose A19:
j in Seg (n + 1)
;
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . jthen
j in dom xp
by A10, FINSEQ_1:def 3;
then (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j =
xp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
j,
k)
by A11, A12, A19
.=
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. j
by A17, Def11
.=
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j
by A18, PARTFUN1:def 6
;
hence
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
;
verum end; suppose A20:
j = (n + 1) + 1
;
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . jA21:
j in dom (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))))
by A13, A17, FINSEQ_1:def 3;
(xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
((n + 1) + 1),
k)
by A10, A20, FINSEQ_1:42
.=
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) /. ((n + 1) + 1)
by A17, A20, Def11
.=
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j
by A20, A21, PARTFUN1:def 6
;
hence
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
;
verum end; end; end;
hence
(SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) . j = (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) . j
;
verum
end;
Radix k > 0
by RADIX_2:6;
then
x mod ((Radix k) |^ n) < (Radix k) |^ n
by NAT_D:1, PREPOWER:6;
then
x mod ((Radix k) |^ n) is_represented_by n,
k
;
then A22:
x mod ((Radix k) |^ n) =
SDSub2IntOut (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))
by A4, A6
.=
Sum (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))))
;
A23:
n + 1
in Seg (n + 1)
by FINSEQ_1:3;
then A24:
n + 1
in Seg ((n + 1) + 1)
by FINSEQ_2:8;
consider xpp being
FinSequence of
INT such that A25:
len xpp = n
and A26:
for
i being
Nat st
i in dom xpp holds
xpp . i = H1(
i)
from FINSEQ_2:sch 1();
A27:
dom xpp = Seg n
by A25, FINSEQ_1:def 3;
A28:
for
j being
Nat st 1
<= j &
j <= len xp holds
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
proof
let j be
Nat;
( 1 <= j & j <= len xp implies xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j )
assume
( 1
<= j &
j <= len xp )
;
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
then A29:
j in Seg (n + 1)
by A10, FINSEQ_1:1;
now xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . jper cases
( j in Seg n or j = n + 1 )
by A29, FINSEQ_2:7;
suppose A30:
j in Seg n
;
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . jthen
j in dom xpp
by A25, FINSEQ_1:def 3;
then (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j =
xpp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
j,
k)
by A26, A27, A30
.=
xp . j
by A11, A12, A29
;
hence
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
;
verum end; suppose A31:
j = n + 1
;
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . jthen (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
(n + 1),
k)
by A25, FINSEQ_1:42
.=
xp . j
by A11, A12, A29, A31
;
hence
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
;
verum end; end; end;
hence
xp . j = (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>) . j
;
verum
end;
deffunc H2(
Nat)
-> Element of
INT =
SDSub2INTDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),$1,
k);
consider xnpp being
FinSequence of
INT such that A32:
len xnpp = n
and A33:
for
i being
Nat st
i in dom xnpp holds
xnpp . i = H2(
i)
from FINSEQ_2:sch 1();
A34:
dom xnpp = Seg n
by A32, FINSEQ_1:def 3;
for
j being
Nat st 1
<= j &
j <= len xnpp holds
xnpp . j = xpp . j
proof
let j be
Nat;
( 1 <= j & j <= len xnpp implies xnpp . j = xpp . j )
assume
( 1
<= j &
j <= len xnpp )
;
xnpp . j = xpp . j
then A35:
j in Seg n
by A32, FINSEQ_1:1;
then xpp . j =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
j,
k)
by A26, A27
.=
SDSub2INTDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
j,
k)
by A6, A35, Th20
.=
xnpp . j
by A33, A34, A35
;
hence
xnpp . j = xpp . j
;
verum
end;
then A36:
xpp = xnpp
by A25, A32, FINSEQ_1:14;
A37:
len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) = n + 1
by CARD_1:def 7;
A38:
for
j being
Nat st 1
<= j &
j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) holds
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
proof
let j be
Nat;
( 1 <= j & j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) implies (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j )
assume A39:
( 1
<= j &
j <= len (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) )
;
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
then A40:
j in Seg (n + 1)
by A37, FINSEQ_1:1;
A41:
j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))))
by A39, FINSEQ_3:25;
now (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . jper cases
( j in Seg n or j = n + 1 )
by A40, FINSEQ_2:7;
suppose A42:
j in Seg n
;
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . jthen
j in dom xnpp
by A32, FINSEQ_1:def 3;
then (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j =
xnpp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
j,
k)
by A33, A34, A42
.=
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. j
by A40, Def11
.=
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j
by A41, PARTFUN1:def 6
;
hence
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
;
verum end; suppose A43:
j = n + 1
;
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . jA44:
j in dom (SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))))
by A37, A40, FINSEQ_1:def 3;
(xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j =
SDSub2INTDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(n + 1),
k)
by A32, A43, FINSEQ_1:42
.=
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) /. (n + 1)
by A40, A43, Def11
.=
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j
by A43, A44, PARTFUN1:def 6
;
hence
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
;
verum end; end; end;
hence
(SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k)))) . j = (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) . j
;
verum
end;
len xp = len (xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>)
by A10, A25, FINSEQ_2:16;
then A45:
xp = xpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))*>
by A28, FINSEQ_1:14;
len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>) = (n + 1) + 1
by A10, FINSEQ_2:16;
then
len (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) = len (xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>)
by CARD_1:def 7;
then
SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k))) = xp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))*>
by A14, FINSEQ_1:14;
then A46:
Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) =
(Sum xp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))
by RVSUM_1:74
.=
((Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1),k))) + (SDSub2INTDigit ((SD2SDSub (DecSD (x,(n + 1),k))),((n + 1) + 1),k))
by A45, A36, RVSUM_1:74
;
set RNDIG =
((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)));
set RNSDC =
((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k));
A47:
Radix k > 0
by RADIX_2:6;
len (xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>) = n + 1
by A32, FINSEQ_2:16;
then
SDSub2INT (SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))) = xnpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))*>
by A37, A38, FINSEQ_1:14;
then A48:
(x mod ((Radix k) |^ n)) + 0 = (Sum xnpp) + (SDSub2INTDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1),k))
by A22, RVSUM_1:74;
A49:
SDSub2INTDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
(n + 1),
k) =
((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(n + 1)))
by NAT_D:34
.=
((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD (x,(n + 1),k)),(n + 1),k))
by A24, Def8
.=
((Radix k) |^ n) * (SD2SDSubDigit ((DecSD (x,(n + 1),k)),(n + 1),k))
by A6, A24, Def7
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))),k)))
by A23, Def6
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
by NAT_D:34
.=
((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
.=
((((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
by NEWTON:6
;
SDSub2INTDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(n + 1),
k) =
((Radix k) |^ n) * (DigB_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(n + 1)))
by NAT_D:34
.=
((Radix k) |^ n) * (SD2SDSubDigitS ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k))
by A23, Def8
.=
((Radix k) |^ n) * (SD2SDSubDigit ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(n + 1),k))
by A23, A6, Def7
.=
((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k))
by Def6
.=
((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)),k))
by NAT_D:34
.=
((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k))
by A5, Lm5
;
then Sum (SDSub2INT (SD2SDSub (DecSD (x,(n + 1),k)))) =
(((x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (DigA ((DecSD (x,(n + 1),k)),(n + 1))))) - (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)),k)))
by A46, A48, A49, A9
.=
(x mod ((Radix k) |^ n)) + (((Radix k) |^ n) * (x div ((Radix k) |^ n)))
by A7, RADIX_1:24
;
hence
x = SDSub2IntOut (SD2SDSub (DecSD (x,(n + 1),k)))
by A47, NAT_D:2, PREPOWER:6;
verum
end;
A50:
S1[1]
proof
A51:
1
in Seg 1
by FINSEQ_1:1;
2
- 1
= 1
;
then A52:
2
-' 1
= 1
by XREAL_0:def 2;
let k,
x be
Nat;
( k >= 2 & x is_represented_by 1,k implies x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k))) )
assume that A53:
k >= 2
and A54:
x is_represented_by 1,
k
;
x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k)))
set X =
DecSD (
x,1,
k);
reconsider CRY =
(Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)) as
Integer ;
reconsider DIG2 =
CRY as
Element of
INT by INT_1:def 2;
reconsider DIG1 =
(DigA ((DecSD (x,1,k)),1)) - CRY as
Element of
INT by INT_1:def 2;
A55:
1
in Seg (1 + 1)
by FINSEQ_1:1;
A56:
len (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) = 1
+ 1
by CARD_1:def 7;
then A57:
1
in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k))))
by A55, FINSEQ_1:def 3;
A58:
2
in Seg (1 + 1)
by FINSEQ_1:1;
then A59:
2
in dom (SDSub2INT (SD2SDSub (DecSD (x,1,k))))
by A56, FINSEQ_1:def 3;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 2 =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,1,k))),2,
k)
by A58, Def11
.=
(Radix k) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),2))
by A52
.=
(Radix k) * (SD2SDSubDigitS ((DecSD (x,1,k)),2,k))
by A58, Def8
.=
(Radix k) * (SD2SDSubDigit ((DecSD (x,1,k)),2,k))
by A53, A58, Def7
.=
(Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k))
by A52, A58, Def6
;
then A60:
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 2
= CRY
by A59, PARTFUN1:def 6;
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) /. 1 =
SDSub2INTDigit (
(SD2SDSub (DecSD (x,1,k))),1,
k)
by A55, Def11
.=
((Radix k) |^ 0) * (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1))
by XREAL_1:232
.=
1
* (DigB_SDSub ((SD2SDSub (DecSD (x,1,k))),1))
by NEWTON:4
.=
SD2SDSubDigitS (
(DecSD (x,1,k)),1,
k)
by A55, Def8
.=
SD2SDSubDigit (
(DecSD (x,1,k)),1,
k)
by A53, A55, Def7
.=
(SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),(1 -' 1))),k))
by A51, Def6
.=
(SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),0)),k))
by XREAL_1:232
.=
(SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + (SDSub_Add_Carry (0,k))
by RADIX_1:def 3
.=
(SDSub_Add_Data ((DigA ((DecSD (x,1,k)),1)),k)) + 0
by Th16
.=
(DigA ((DecSD (x,1,k)),1)) - ((Radix k) * (SDSub_Add_Carry ((DigA ((DecSD (x,1,k)),1)),k)))
;
then
(SDSub2INT (SD2SDSub (DecSD (x,1,k)))) . 1
= (DigA ((DecSD (x,1,k)),1)) - CRY
by A57, PARTFUN1:def 6;
then
SDSub2INT (SD2SDSub (DecSD (x,1,k))) = <*DIG1,DIG2*>
by A56, A60, FINSEQ_1:44;
then Sum (SDSub2INT (SD2SDSub (DecSD (x,1,k)))) =
DIG1 + DIG2
by RVSUM_1:77
.=
x
by A54, RADIX_1:21
;
hence
x = SDSub2IntOut (SD2SDSub (DecSD (x,1,k)))
;
verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A50, A2);
hence
for k, x being Nat st k >= 2 & x is_represented_by n,k holds
x = SDSub2IntOut (SD2SDSub (DecSD (x,n,k)))
by A1; verum