defpred S1[ Nat] means for k, x, y being Nat st k >= 2 & x is_represented_by $1,k & y is_represented_by $1,k holds
x + y = (SDDec ((DecSD (x,$1,k)) '+' (DecSD (y,$1,k)))) + (((Radix k) |^ $1) * (SD_Add_Carry ((DigA ((DecSD (x,$1,k)),$1)) + (DigA ((DecSD (y,$1,k)),$1)))));
let n be Nat; ( n >= 1 implies for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n))))) )
assume A1:
n >= 1
; for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n)))))
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,
y be
Nat;
( k >= 2 & x is_represented_by n + 1,k & y is_represented_by n + 1,k implies x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))))) )
A6:
n + 1
in Seg (n + 1)
by FINSEQ_1:3;
set z =
(DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k));
set yn =
y mod ((Radix k) |^ n);
set xn =
x mod ((Radix k) |^ n);
assume that A7:
k >= 2
and A8:
x is_represented_by n + 1,
k
and A9:
y is_represented_by n + 1,
k
;
x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1))))))
set zn =
(DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k));
A10:
len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) = n
by CARD_1:def 7;
A11:
len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) = n + 1
by CARD_1:def 7;
A12:
for
i being
Nat st 1
<= i &
i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) holds
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
proof
let i be
Nat;
( 1 <= i & i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) implies (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i )
assume that A13:
1
<= i
and A14:
i <= len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))))
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
A15:
i -' 1
= i - 1
by A13, XREAL_1:233;
A16:
i <= n + 1
by A14, CARD_1:def 7;
then A17:
i in Seg (n + 1)
by A13, FINSEQ_1:1;
then A18:
i in dom (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))))
by A11, FINSEQ_1:def 3;
per cases
( i in Seg n or i = n + 1 )
by A17, FINSEQ_2:7;
suppose A19:
i in Seg n
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . ithen A20:
i in dom (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))
by A10, FINSEQ_1:def 3;
then A21:
((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i =
(DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) . i
by FINSEQ_1:def 7
.=
(DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) /. i
by A20, PARTFUN1:def 6
.=
SubDigit (
((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))),
i,
k)
by A19, Def6
.=
((Radix k) |^ (i -' 1)) * (Add ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(DecSD ((y mod ((Radix k) |^ n)),n,k)),i,k))
by A19, Def14
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),(i -' 1))))))
by A7, A19, Def13
;
A22:
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i =
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) /. i
by A18, PARTFUN1:def 6
.=
SubDigit (
((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),
i,
k)
by A17, Def6
.=
((Radix k) |^ (i -' 1)) * (Add ((DecSD (x,(n + 1),k)),(DecSD (y,(n + 1),k)),i,k))
by A17, Def14
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1))))))
by A7, A17, Def13
;
now (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . iper cases
( i = 1 or i > 1 )
by A13, XXREAL_0:1;
suppose A23:
i = 1
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . ithen A24:
((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i =
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),0)))))
by A21, XREAL_1:232
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),0)))))
by A23, XREAL_1:232
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),0)) + 0)))
by Def3
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + 0)
by Def3, Th17
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i =
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),0)))))
by A22, A23, XREAL_1:232
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),0)) + (DigA ((DecSD (y,(n + 1),k)),0)))))
by A23, XREAL_1:232
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),0)) + 0)))
by Def3
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + 0)
by Def3, Th17
.=
((Radix k) |^ (i -' 1)) * (SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k))
by A19, Lm3
.=
((Radix k) |^ (i -' 1)) * (SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k))
by A19, Lm3
;
hence
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
by A24;
verum end; suppose A25:
i > 1
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . iA26:
i - 1
<= n
by A16, XREAL_1:20;
i -' 1
>= 1
by A25, NAT_D:49;
then A27:
i -' 1
in Seg n
by A15, A26, FINSEQ_1:1;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i =
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD (y,(n + 1),k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1))))))
by A19, A22, Lm3
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1))))))
by A19, Lm3
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD (y,(n + 1),k)),(i -' 1))))))
by A27, Lm3
.=
((Radix k) |^ (i -' 1)) * ((SD_Add_Data (((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),i)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),i))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),(i -' 1))) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),(i -' 1))))))
by A27, Lm3
;
hence
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
by A21;
verum end; hence
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
;
verum end; suppose A28:
i = n + 1
;
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . ithen ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i =
((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . ((len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) + 1)
by CARD_1:def 7
.=
SubDigit (
((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),
(n + 1),
k)
by FINSEQ_1:42
.=
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) /. (n + 1)
by A6, Def6
.=
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . (n + 1)
by A18, A28, PARTFUN1:def 6
;
hence
(DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) . i = ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) . i
by A28;
verum end;
end;
A29:
SubDigit (
((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),
(n + 1),
k)
= ((Radix k) |^ n) * (DigB (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1)))
by NAT_D:34;
A30:
Radix k > 0
by POWER:34;
then A31:
x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))
by NAT_D:2, PREPOWER:6;
set y1 =
y div ((Radix k) |^ n);
set x1 =
x div ((Radix k) |^ n);
A32:
len <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*> = 1
by FINSEQ_1:39;
A33:
DigA (
(DecSD (y,(n + 1),k)),
(n + 1))
= y div ((Radix k) |^ n)
by A9, Th23;
y mod ((Radix k) |^ n) < (Radix k) |^ n
by A30, NAT_D:1, PREPOWER:6;
then A34:
y mod ((Radix k) |^ n) is_represented_by n,
k
;
x mod ((Radix k) |^ n) < (Radix k) |^ n
by A30, NAT_D:1, PREPOWER:6;
then A35:
x mod ((Radix k) |^ n) is_represented_by n,
k
;
len ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>) =
(len (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k))))) + (len <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>)
by FINSEQ_1:22
.=
n + 1
by A32, CARD_1:def 7
;
then
len (DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) = len ((DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>)
by CARD_1:def 7;
then
DigitSD ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))) = (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))) ^ <*(SubDigit (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1),k))*>
by A12, FINSEQ_1:14;
then SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))) =
(((Radix k) |^ n) * (DigB (((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k))),(n + 1)))) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A29, RVSUM_1:74
.=
((Add ((DecSD (x,(n + 1),k)),(DecSD (y,(n + 1),k)),(n + 1),k)) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A6, Def14
.=
(((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))) + (DigA ((DecSD (y,(n + 1),k)),((n + 1) -' 1)))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A6, A7, Def13
.=
(((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),((n + 1) -' 1))) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by NAT_D:34
.=
(((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),n)) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by NAT_D:34
.=
(((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD (y,(n + 1),k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A5, Lm3
.=
(((SD_Add_Data (((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1)))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A5, Lm3
.=
(((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) + (SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n))))) * ((Radix k) |^ n)) + (Sum (DigitSD ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
by A8, A33, Th23
.=
((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + (((SD_Add_Carry ((DigA ((DecSD ((x mod ((Radix k) |^ n)),n,k)),n)) + (DigA ((DecSD ((y mod ((Radix k) |^ n)),n,k)),n)))) * ((Radix k) |^ n)) + (SDDec ((DecSD ((x mod ((Radix k) |^ n)),n,k)) '+' (DecSD ((y mod ((Radix k) |^ n)),n,k)))))
.=
((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((x mod ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)))
by A4, A7, A35, A34
.=
(((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n))
;
then (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1))) =
((((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * ((Radix k) |^ (n + 1)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n))
.=
((((SD_Add_Data (((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n))),k)) * ((Radix k) |^ n)) + ((SD_Add_Carry ((x div ((Radix k) |^ n)) + (y div ((Radix k) |^ n)))) * (((Radix k) |^ n) * (Radix k)))) + (x mod ((Radix k) |^ n))) + (y mod ((Radix k) |^ n))
by NEWTON:6
.=
(((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n))) + (((y div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (y mod ((Radix k) |^ n)))
.=
x + y
by A30, A31, NAT_D:2, PREPOWER:6
;
hence
x + y = (SDDec ((DecSD (x,(n + 1),k)) '+' (DecSD (y,(n + 1),k)))) + (((Radix k) |^ (n + 1)) * (SD_Add_Carry ((DigA ((DecSD (x,(n + 1),k)),(n + 1))) + (DigA ((DecSD (y,(n + 1),k)),(n + 1))))))
by A8, A33, Th23;
verum
end;
A36:
S1[1]
proof
let k,
x,
y be
Nat;
( k >= 2 & x is_represented_by 1,k & y is_represented_by 1,k implies x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1))))) )
assume
(
k >= 2 &
x is_represented_by 1,
k &
y is_represented_by 1,
k )
;
x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1)))))
then A37:
(
SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k))) = SD_Add_Data (
(x + y),
k) &
SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1))) = SD_Add_Carry (x + y) )
by Th22, Th24;
thus
x + y = (SDDec ((DecSD (x,1,k)) '+' (DecSD (y,1,k)))) + (((Radix k) |^ 1) * (SD_Add_Carry ((DigA ((DecSD (x,1,k)),1)) + (DigA ((DecSD (y,1,k)),1)))))
by A37;
verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A36, A2);
hence
for k, x, y being Nat st k >= 2 & x is_represented_by n,k & y is_represented_by n,k holds
x + y = (SDDec ((DecSD (x,n,k)) '+' (DecSD (y,n,k)))) + (((Radix k) |^ n) * (SD_Add_Carry ((DigA ((DecSD (x,n,k)),n)) + (DigA ((DecSD (y,n,k)),n)))))
by A1; verum