let n be Nat; :: thesis: ( n >= 1 implies for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,n,k)) '+' (SD2SDSub (DecSD y,n,k))) )
assume A1:
n >= 1
; :: thesis: for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,n,k)) '+' (SD2SDSub (DecSD y,n,k)))
defpred S1[ Nat] means for k, x, y being Nat st k >= 3 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,$1,k)) '+' (SD2SDSub (DecSD y,$1,k)));
A2:
S1[1]
proof
let k,
x,
y be
Nat;
:: thesis: ( k >= 3 & x is_represented_by 1,k & y is_represented_by 1,k implies x + y = SDSub2IntOut ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))) )
assume A3:
(
k >= 3 &
x is_represented_by 1,
k &
y is_represented_by 1,
k )
;
:: thesis: x + y = SDSub2IntOut ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))
reconsider k =
k,
x =
x,
y =
y as
Element of
NAT by ORDINAL1:def 13;
set X =
SD2SDSub (DecSD x,1,k);
set Y =
SD2SDSub (DecSD y,1,k);
reconsider CRY1 =
SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),
k as
Integer ;
A4:
1
in Seg (1 + 1)
by FINSEQ_1:3;
then A5:
DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1 =
SDSubAddDigit (SD2SDSub (DecSD x,1,k)),
(SD2SDSub (DecSD y,1,k)),1,
k
by Def2
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),(1 -' 1)) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),(1 -' 1))),k)
by A3, A4, Def1, XXREAL_0:2
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),0 ) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),(1 -' 1))),k)
by XREAL_1:234
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),0 ) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),0 )),k)
by XREAL_1:234
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + (SDSub_Add_Carry (0 + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),0 )),k)
by RADIX_3:def 5
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + (SDSub_Add_Carry (0 + 0 ),k)
by RADIX_3:def 5
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) + 0
by A3, RADIX_3:17, XXREAL_0:2
.=
((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)) - ((Radix k) * CRY1)
by RADIX_3:def 4
;
2
- 1
= 1
;
then A6:
2
-' 1
= 1
by XREAL_0:def 2;
A7:
2
in Seg (1 + 1)
by FINSEQ_1:3;
then A8:
DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2 =
SDSubAddDigit (SD2SDSub (DecSD x,1,k)),
(SD2SDSub (DecSD y,1,k)),2,
k
by Def2
.=
(SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),2) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),2)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),(2 -' 1)) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),(2 -' 1))),k)
by A3, A7, Def1, XXREAL_0:2
.=
(SDSub_Add_Data ((SDSub_Add_Carry x,k) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),2)),k) + CRY1
by A3, A6, Th4, XXREAL_0:2
.=
(SDSub_Add_Data ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k) + CRY1
by A3, Th4, XXREAL_0:2
.=
(((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)) - ((Radix k) * (SDSub_Add_Carry ((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)),k))) + CRY1
by RADIX_3:def 4
.=
(((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)) - ((Radix k) * 0 )) + CRY1
by A3, Th2
.=
(((SDSub_Add_Carry x,k) + (SDSub_Add_Carry y,k)) - 0 ) + CRY1
;
A9:
(SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) /. 1 =
SDSub2INTDigit ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1,
k
by A4, RADIX_3:def 11
.=
((Radix k) |^ (1 -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1)
by RADIX_3:def 10
.=
((Radix k) |^ 0 ) * (DigB_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1)
by XREAL_1:234
.=
1
* (DigB_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1)
by NEWTON:9
.=
DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1
by RADIX_3:def 9
;
reconsider DIG1 =
DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),1 as
Element of
INT by INT_1:def 2;
A10:
(SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) /. 2 =
SDSub2INTDigit ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2,
k
by A7, RADIX_3:def 11
.=
((Radix k) |^ (2 -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2)
by RADIX_3:def 10
.=
(Radix k) * (DigB_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2)
by A6, NEWTON:10
.=
(Radix k) * (DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2)
by RADIX_3:def 9
;
reconsider DIG2 =
(Radix k) * (DigA_SDSub ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))),2) as
Element of
INT by INT_1:def 2;
A11:
len (SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) = 1
+ 1
by FINSEQ_1:def 18;
then
1
in dom (SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))))
by A4, FINSEQ_1:def 3;
then A12:
(SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) . 1
= DIG1
by A9, PARTFUN1:def 8;
2
in dom (SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))))
by A7, A11, FINSEQ_1:def 3;
then
(SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) . 2
= DIG2
by A10, PARTFUN1:def 8;
then
SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k))) = <*DIG1,DIG2*>
by A11, A12, FINSEQ_1:61;
then A13:
Sum (SDSub2INT ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))) = DIG1 + DIG2
by RVSUM_1:107;
reconsider RSDCX =
(Radix k) * (SDSub_Add_Carry x,k),
RSDCY =
(Radix k) * (SDSub_Add_Carry y,k) as
Integer ;
reconsider RCRY1 =
(Radix k) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,1,k)),1) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)),k) as
Integer ;
DIG1 =
((x - RSDCX) + (DigA_SDSub (SD2SDSub (DecSD y,1,k)),1)) - RCRY1
by A3, A5, Th6, XXREAL_0:2
.=
((x - RSDCX) + (y - RSDCY)) - RCRY1
by A3, Th6, XXREAL_0:2
.=
(((x + y) - RSDCX) - RSDCY) - RCRY1
;
hence
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,1,k)) '+' (SD2SDSub (DecSD y,1,k)))
by A8, A13, RADIX_3:def 12;
:: thesis: verum
end;
A14:
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 A15:
(
n >= 1 &
S1[
n] )
;
:: thesis: S1[n + 1]
then
n <> 0
;
then A16:
n in Seg n
by FINSEQ_1:5;
A17:
n + 1
in Seg (n + 1)
by FINSEQ_1:5;
let k,
x,
y be
Nat;
:: thesis: ( k >= 3 & x is_represented_by n + 1,k & y is_represented_by n + 1,k implies x + y = SDSub2IntOut ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))) )
assume A18:
(
k >= 3 &
x is_represented_by n + 1,
k &
y is_represented_by n + 1,
k )
;
:: thesis: x + y = SDSub2IntOut ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))
then A19:
k >= 2
by XXREAL_0:2;
reconsider k =
k,
x =
x,
y =
y as
Element of
NAT by ORDINAL1:def 13;
set xn =
x mod ((Radix k) |^ n);
set yn =
y mod ((Radix k) |^ n);
set z =
(SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k));
set zn =
(SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k));
A20:
Radix k > 0
by POWER:39;
then A21:
x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))
by NAT_D:2, PREPOWER:13;
(
x mod ((Radix k) |^ n) < (Radix k) |^ n &
y mod ((Radix k) |^ n) < (Radix k) |^ n )
by A20, NAT_D:1, PREPOWER:13;
then
(
x mod ((Radix k) |^ n) is_represented_by n,
k &
y mod ((Radix k) |^ n) is_represented_by n,
k )
by RADIX_1:def 12;
then A22:
(x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)) =
SDSub2IntOut ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))
by A15, A18
.=
Sum (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))))
by RADIX_3:def 12
;
A23:
n + 1
in Seg ((n + 1) + 1)
by A17, FINSEQ_2:9;
A24:
(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)) '+' (SD2SDSub (DecSD y,(n + 1),k))),$1,
k;
consider zp being
FinSequence of
INT such that A25:
len zp = n + 1
and A26:
for
i being
Nat st
i in dom zp holds
zp . i = H1(
i)
from FINSEQ_2:sch 1();
A27:
dom zp = Seg (n + 1)
by A25, FINSEQ_1:def 3;
consider zpp being
FinSequence of
INT such that A28:
len zpp = n
and A29:
for
i being
Nat st
i in dom zpp holds
zpp . i = H1(
i)
from FINSEQ_2:sch 1();
A30:
dom zpp = Seg n
by A28, FINSEQ_1:def 3;
deffunc H2(
Nat)
-> Element of
INT =
SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),$1,
k;
consider znpp being
FinSequence of
INT such that A31:
len znpp = n
and A32:
for
i being
Nat st
i in dom znpp holds
znpp . i = H2(
i)
from FINSEQ_2:sch 1();
A33:
dom znpp = Seg n
by A31, FINSEQ_1:def 3;
A34:
SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))) = zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>
proof
A35:
len (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) = (n + 1) + 1
by A25, FINSEQ_2:19;
A36:
len (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(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)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) holds
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(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)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) implies (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j )
assume
( 1
<= j &
j <= len (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) )
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j
then A37:
j in Seg ((n + 1) + 1)
by A36, FINSEQ_1:3;
then A38:
j in dom (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))))
by A36, FINSEQ_1:def 3;
now per cases
( j in Seg (n + 1) or j = (n + 1) + 1 )
by A37, FINSEQ_2:8;
suppose A39:
j in Seg (n + 1)
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . jthen
j in dom zp
by A25, FINSEQ_1:def 3;
then (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j =
zp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
j,
k
by A26, A39, A27
.=
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) /. j
by A37, RADIX_3:def 11
.=
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j
by A38, PARTFUN1:def 8
;
hence
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j
;
:: thesis: verum end; suppose A40:
j = (n + 1) + 1
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . jA41:
j in dom (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))))
by A36, A37, FINSEQ_1:def 3;
(zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j =
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
((n + 1) + 1),
k
by A25, A40, FINSEQ_1:59
.=
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) /. ((n + 1) + 1)
by A37, A40, RADIX_3:def 11
.=
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j
by A40, A41, PARTFUN1:def 8
;
hence
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j
;
:: thesis: verum end;
hence
(SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) . j = (zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>) . j
;
:: thesis: verum
end;
hence
SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))) = zp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)*>
by A35, A36, FINSEQ_1:18;
:: thesis: verum
end;
A42:
zp = zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>
proof
A43:
len (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) = n + 1
by A28, FINSEQ_2:19;
for
j being
Nat st 1
<= j &
j <= len zp holds
zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j
proof
let j be
Nat;
:: thesis: ( 1 <= j & j <= len zp implies zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j )
assume
( 1
<= j &
j <= len zp )
;
:: thesis: zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j
then A44:
j in Seg (n + 1)
by A25, FINSEQ_1:3;
now per cases
( j in Seg n or j = n + 1 )
by A44, FINSEQ_2:8;
suppose A45:
j in Seg n
;
:: thesis: zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . jthen
j in dom zpp
by A28, FINSEQ_1:def 3;
then (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j =
zpp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
j,
k
by A29, A45, A30
.=
zp . j
by A26, A44, A27
;
hence
zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j
;
:: thesis: verum end; suppose A46:
j = n + 1
;
:: thesis: zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . jthen (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j =
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
(n + 1),
k
by A28, FINSEQ_1:59
.=
zp . j
by A26, A44, A46, A27
;
hence
zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j
;
:: thesis: verum end;
hence
zp . j = (zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>) . j
;
:: thesis: verum
end;
hence
zp = zpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)*>
by A25, A43, FINSEQ_1:18;
:: thesis: verum
end;
A47:
SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))) = znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>
proof
A48:
len (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) = n + 1
by A31, FINSEQ_2:19;
A49:
len (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y 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)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) holds
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y 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)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) implies (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j )
assume
( 1
<= j &
j <= len (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) )
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j
then A50:
j in Seg (n + 1)
by A49, FINSEQ_1:3;
then A51:
j in dom (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))))
by A49, FINSEQ_1:def 3;
now per cases
( j in Seg n or j = n + 1 )
by A50, FINSEQ_2:8;
suppose A52:
j in Seg n
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . jthen
j in dom znpp
by A31, FINSEQ_1:def 3;
then (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j =
znpp . j
by FINSEQ_1:def 7
.=
SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),
j,
k
by A32, A52, A33
.=
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) /. j
by A50, RADIX_3:def 11
.=
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j
by A51, PARTFUN1:def 8
;
hence
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j
;
:: thesis: verum end; suppose A53:
j = n + 1
;
:: thesis: (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . jA54:
j in dom (SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))))
by A49, A50, FINSEQ_1:def 3;
(znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j =
SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),
(n + 1),
k
by A31, A53, FINSEQ_1:59
.=
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) /. (n + 1)
by A50, A53, RADIX_3:def 11
.=
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j
by A53, A54, PARTFUN1:def 8
;
hence
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j
;
:: thesis: verum end;
hence
(SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)))) . j = (znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>) . j
;
:: thesis: verum
end;
hence
SDSub2INT ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))) = znpp ^ <*(SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)*>
by A48, A49, FINSEQ_1:18;
:: thesis: verum
end;
A55:
zpp = znpp
proof
for
j being
Nat st 1
<= j &
j <= len znpp holds
znpp . j = zpp . j
proof
let j be
Nat;
:: thesis: ( 1 <= j & j <= len znpp implies znpp . j = zpp . j )
assume A56:
( 1
<= j &
j <= len znpp )
;
:: thesis: znpp . j = zpp . j
then A57:
j in Seg n
by A31, FINSEQ_1:3;
A58:
j <= n + 1
by A31, A56, NAT_1:12;
then A59:
j in Seg (n + 1)
by A56, FINSEQ_1:3;
j <= (n + 1) + 1
by A58, NAT_1:12;
then A60:
j in Seg ((n + 1) + 1)
by A56, FINSEQ_1:3;
zpp . j =
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
j,
k
by A29, A57, A30
.=
((Radix k) |^ (j -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),j)
by RADIX_3:def 10
.=
((Radix k) |^ (j -' 1)) * (DigA_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),j)
by RADIX_3:def 9
.=
((Radix k) |^ (j -' 1)) * (SDSubAddDigit (SD2SDSub (DecSD x,(n + 1),k)),(SD2SDSub (DecSD y,(n + 1),k)),j,k)
by A60, Def2
.=
((Radix k) |^ (j -' 1)) * (SDSubAddDigit (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),j,k)
by A18, A57, Th8, XXREAL_0:2
.=
((Radix k) |^ (j -' 1)) * (DigA_SDSub ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),j)
by A59, Def2
.=
((Radix k) |^ (j -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),j)
by RADIX_3:def 9
.=
SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),
j,
k
by RADIX_3:def 10
.=
znpp . j
by A32, A57, A33
;
hence
znpp . j = zpp . j
;
:: thesis: verum
end;
hence
zpp = znpp
by A28, A31, FINSEQ_1:18;
:: thesis: verum
end;
A61:
Sum (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) =
(Sum zp) + (SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)
by A34, RVSUM_1:104
.=
((Sum znpp) + (SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1),k)) + (SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1),k)
by A42, A55, RVSUM_1:104
;
A62:
((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + 0 = (Sum znpp) + (SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)
by A22, A47, RVSUM_1:104;
set SDN11 =
(DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1));
set SDN1 =
(DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1));
set SDN =
(DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n);
set RN1 =
(Radix k) |^ (n + 1);
set RN =
(Radix k) |^ n;
A63:
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
((n + 1) + 1),
k =
((Radix k) |^ (((n + 1) + 1) -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1))
by RADIX_3:def 10
.=
((Radix k) |^ (((n + 1) + 1) -' 1)) * (DigA_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1))
by RADIX_3:def 9
.=
((Radix k) |^ (n + 1)) * (DigA_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),((n + 1) + 1))
by NAT_D:34
.=
((Radix k) |^ (n + 1)) * (SDSubAddDigit (SD2SDSub (DecSD x,(n + 1),k)),(SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1),k)
by A24, Def2
.=
((Radix k) |^ (n + 1)) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(((n + 1) + 1) -' 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(((n + 1) + 1) -' 1))),k))
by A18, A24, Def1, XXREAL_0:2
.=
((Radix k) |^ (n + 1)) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(((n + 1) + 1) -' 1))),k))
by NAT_D:34
.=
((Radix k) |^ (n + 1)) * (((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k)) + 0 )
by NAT_D:34
.=
(((Radix k) |^ (n + 1)) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k)) + (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k))
;
A64:
SDSub2INTDigit ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),
(n + 1),
k =
((Radix k) |^ ((n + 1) -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1))
by RADIX_3:def 10
.=
((Radix k) |^ ((n + 1) -' 1)) * (DigA_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1))
by RADIX_3:def 9
.=
((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k))),(n + 1))
by NAT_D:34
.=
((Radix k) |^ n) * (SDSubAddDigit (SD2SDSub (DecSD x,(n + 1),k)),(SD2SDSub (DecSD y,(n + 1),k)),(n + 1),k)
by A23, Def2
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) -' 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) -' 1))),k))
by A18, A23, Def1, XXREAL_0:2
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) -' 1))),k))
by NAT_D:34
.=
((Radix k) |^ n) * (((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k)) + 0 )
by NAT_D:34
.=
(((Radix k) |^ n) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k)) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
.=
(((Radix k) |^ n) * (((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))) - ((Radix k) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
by RADIX_3:def 4
.=
((((Radix k) |^ n) * ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1)))) - ((((Radix k) |^ n) * (Radix k)) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
.=
((((Radix k) |^ n) * ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1)))) - (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
by NEWTON:11
.=
((((Radix k) |^ n) * ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1)))) + (- (((Radix k) |^ (n + 1)) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))),k)))) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
;
A65:
SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),
(n + 1),
k =
((Radix k) |^ ((n + 1) -' 1)) * (DigB_SDSub ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1))
by RADIX_3:def 10
.=
((Radix k) |^ ((n + 1) -' 1)) * (DigA_SDSub ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1))
by RADIX_3:def 9
.=
((Radix k) |^ n) * (DigA_SDSub ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1))
by NAT_D:34
.=
((Radix k) |^ n) * (SDSubAddDigit (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),(n + 1),k)
by A17, Def2
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1)) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k))
by A17, A18, Def1, XXREAL_0:2
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),n) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),((n + 1) -' 1))),k))
by NAT_D:34
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),n) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),n)),k))
by NAT_D:34
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),(n + 1))),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),n) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),n)),k))
by A15, A18, Th5
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)),n) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),n)),k))
by A15, A18, Th5
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k)),n)),k))
by A16, A18, RADIX_3:21, XXREAL_0:2
.=
((Radix k) |^ n) * ((SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),k) + (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
by A16, A18, RADIX_3:21, XXREAL_0:2
.=
(((Radix k) |^ n) * (SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),k)) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k))
;
set SDACx =
SDSub_Add_Carry (DigA (DecSD x,n,k),n),
k;
set SDACy =
SDSub_Add_Carry (DigA (DecSD y,n,k),n),
k;
A66:
SDSub_Add_Data ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),
k =
((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)) - ((Radix k) * (SDSub_Add_Carry ((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)),k))
by RADIX_3:def 4
.=
((SDSub_Add_Carry (DigA (DecSD x,n,k),n),k) + (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k)) - ((Radix k) * 0 )
by A18, Th2
;
set RN1SD11 =
((Radix k) |^ (n + 1)) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k);
set RNSC =
((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k);
A67:
Sum (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) = ((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1))))) + ((- (SDSub2INTDigit ((SD2SDSub (DecSD (x mod ((Radix k) |^ n)),n,k)) '+' (SD2SDSub (DecSD (y mod ((Radix k) |^ n)),n,k))),(n + 1),k)) + (((Radix k) |^ n) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),n) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),n)),k)))) + (((Radix k) |^ (n + 1)) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k))
by A61, A62, A63, A64;
A68:
((Radix k) |^ (n + 1)) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k) = ((Radix k) |^ (n + 1)) * (((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))) - ((Radix k) * (SDSub_Add_Carry ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k)))
by RADIX_3:def 4;
A69:
DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),
((n + 1) + 1) =
SD2SDSubDigitS (DecSD x,(n + 1),k),
((n + 1) + 1),
k
by A24, RADIX_3:def 8
.=
SD2SDSubDigit (DecSD x,(n + 1),k),
((n + 1) + 1),
k
by A18, A24, RADIX_3:def 7, XXREAL_0:2
.=
SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(((n + 1) + 1) -' 1)),
k
by RADIX_3:def 6
.=
SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),
k
by NAT_D:34
;
A70:
DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),
((n + 1) + 1) =
SD2SDSubDigitS (DecSD y,(n + 1),k),
((n + 1) + 1),
k
by A24, RADIX_3:def 8
.=
SD2SDSubDigit (DecSD y,(n + 1),k),
((n + 1) + 1),
k
by A18, A24, RADIX_3:def 7, XXREAL_0:2
.=
SDSub_Add_Carry (DigA (DecSD y,(n + 1),k),(((n + 1) + 1) -' 1)),
k
by RADIX_3:def 6
.=
SDSub_Add_Carry (DigA (DecSD y,(n + 1),k),(n + 1)),
k
by NAT_D:34
;
then A71:
((Radix k) |^ (n + 1)) * (SDSub_Add_Data ((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))),k) =
((Radix k) |^ (n + 1)) * (((DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),((n + 1) + 1)) + (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),((n + 1) + 1))) - ((Radix k) * 0 ))
by A18, A68, A69, Th2
.=
((Radix k) |^ (n + 1)) * ((SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k) + (SDSub_Add_Carry (DigA (DecSD y,(n + 1),k),(n + 1)),k))
by A69, A70
;
reconsider RNDx11 =
((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD x,(n + 1),k)),(n + 1)),
RNDy11 =
((Radix k) |^ n) * (DigA_SDSub (SD2SDSub (DecSD y,(n + 1),k)),(n + 1)),
RN1Cx11 =
((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),(n + 1)),k),
RN1Cy11 =
((Radix k) |^ (n + 1)) * (SDSub_Add_Carry (DigA (DecSD y,(n + 1),k),(n + 1)),k),
RNCx1 =
((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,(n + 1),k),n),k),
RNCy1 =
((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD y,(n + 1),k),n),k),
RNCx =
((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD x,n,k),n),k),
RNCy =
((Radix k) |^ n) * (SDSub_Add_Carry (DigA (DecSD y,n,k),n),k) as
Integer ;
A72:
Sum (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) =
(((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + RNDx11) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11)
by A65, A66, A67, A71
.=
(((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1))) - RN1Cx11) + RNCx1)) + RNDy11) + (- (RNCx + RNCy))) + (RN1Cx11 + RN1Cy11)
by A15, A18, A19, Th7
.=
((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + RNCx1) + RNDy11) + RN1Cy11) - (RNCx + RNCy)
.=
((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + RNCx1) + (((((Radix k) |^ n) * (DigA (DecSD y,(n + 1),k),(n + 1))) - RN1Cy11) + RNCy1)) + RN1Cy11) - (RNCx + RNCy)
by A15, A18, A19, Th7
.=
((((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + RNCx1) + (((Radix k) |^ n) * (DigA (DecSD y,(n + 1),k),(n + 1)))) + (- RN1Cy11)) + RNCy1) + RN1Cy11) + (- (RNCx + RNCy))
.=
((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + RNCx1) + (((Radix k) |^ n) * (DigA (DecSD y,(n + 1),k),(n + 1)))) + RNCy1) + (- (RNCx1 + RNCy))
by A16, Lm2
.=
((((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + RNCx1) + (((Radix k) |^ n) * (DigA (DecSD y,(n + 1),k),(n + 1)))) + RNCy1) + (- (RNCx1 + RNCy1))
by A16, Lm2
.=
((((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))) + (((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)))) + 0 ) + (((Radix k) |^ n) * (DigA (DecSD y,(n + 1),k),(n + 1)))
;
((Radix k) |^ n) * (DigA (DecSD x,(n + 1),k),(n + 1)) = ((Radix k) |^ n) * (x div ((Radix k) |^ n))
by A18, RADIX_1:27;
then A73:
Sum (SDSub2INT ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))) = ((y mod ((Radix k) |^ n)) + x) + (((Radix k) |^ n) * (y div ((Radix k) |^ n)))
by A18, A21, A72, RADIX_1:27;
y = ((y div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (y mod ((Radix k) |^ n))
by A20, NAT_D:2, PREPOWER:13;
hence
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,(n + 1),k)) '+' (SD2SDSub (DecSD y,(n + 1),k)))
by A73, RADIX_3:def 12;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A2, A14);
hence
for k, x, y being Nat st k >= 3 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = SDSub2IntOut ((SD2SDSub (DecSD x,n,k)) '+' (SD2SDSub (DecSD y,n,k)))
by A1; :: thesis: verum