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