let n be Nat; :: thesis: ( 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
; :: thesis: 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))))
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))));
A2:
S1[1]
proof
let k,
x,
y be
Nat;
:: thesis: ( 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 A3:
(
k >= 2 &
x is_represented_by 1,
k &
y is_represented_by 1,
k )
;
:: thesis: 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 A4:
SDDec ((DecSD x,1,k) '+' (DecSD y,1,k)) = SD_Add_Data (x + y),
k
by Th28;
A5:
SD_Add_Carry ((DigA (DecSD x,1,k),1) + (DigA (DecSD y,1,k),1)) = SD_Add_Carry (x + y)
by A3, Th26;
(SD_Add_Data (x + y),k) + ((SD_Add_Carry (x + y)) * (Radix k)) = (x + y) - 0
;
hence
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 A4, A5, NEWTON:10;
:: thesis: verum
end;
A6:
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 A7:
(
n >= 1 &
S1[
n] )
;
:: thesis: S1[n + 1]
then A8:
n in Seg n
by FINSEQ_1:5;
A9:
n + 1
in Seg (n + 1)
by FINSEQ_1:5;
let k,
x,
y be
Nat;
:: thesis: ( 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))))) )
assume A10:
(
k >= 2 &
x is_represented_by n + 1,
k &
y is_represented_by n + 1,
k )
;
:: thesis: 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 x1 =
x div ((Radix k) |^ n);
set xn =
x mod ((Radix k) |^ n);
set y1 =
y div ((Radix k) |^ n);
set yn =
y mod ((Radix k) |^ n);
set z =
(DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k);
set zn =
(DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k);
A11:
DigA (DecSD y,(n + 1),k),
(n + 1) = y div ((Radix k) |^ n)
by A10, Th27;
A12:
Radix k > 0
by POWER:39;
then A13:
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 A12, NAT_D:1, PREPOWER:13;
then A14:
(
x mod ((Radix k) |^ n) is_represented_by n,
k &
y mod ((Radix k) |^ n) is_represented_by n,
k )
by Def12;
A15:
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)*>
proof
A16:
len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) = n + 1
by FINSEQ_1:def 18;
A17:
len (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k))) = n
by FINSEQ_1:def 18;
A18:
len <*(SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),(n + 1),k)*> = 1
by FINSEQ_1:56;
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:35
.=
n + 1
by A18, FINSEQ_1:def 18
;
then A19:
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 FINSEQ_1:def 18;
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;
:: thesis: ( 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 A20:
( 1
<= i &
i <= len (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) )
;
:: thesis: (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
then A21:
i <= n + 1
by FINSEQ_1:def 18;
then A22:
i in Seg (n + 1)
by A20, FINSEQ_1:3;
then A23:
i in dom (DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)))
by A16, FINSEQ_1:def 3;
A24:
i -' 1
= i - 1
by A20, XREAL_1:235;
per cases
( i in Seg n or i = n + 1 )
by A22, FINSEQ_2:8;
suppose A25:
i in Seg n
;
:: thesis: (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 A26:
i in dom (DigitSD ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)))
by A17, FINSEQ_1:def 3;
then A27:
((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 A26, PARTFUN1:def 8
.=
SubDigit ((DecSD (x mod ((Radix k) |^ n)),n,k) '+' (DecSD (y mod ((Radix k) |^ n)),n,k)),
i,
k
by A25, 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 A25, 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 A10, A25, Def13
;
A28:
(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 A23, PARTFUN1:def 8
.=
SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),
i,
k
by A22, Def6
.=
((Radix k) |^ (i -' 1)) * (Add (DecSD x,(n + 1),k),(DecSD y,(n + 1),k),i,k)
by A22, 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 A10, A22, Def13
;
now per cases
( i = 1 or i > 1 )
by A20, XXREAL_0:1;
suppose A29:
i = 1
;
:: thesis: (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 A30:
((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 A27, XREAL_1:234
.=
((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 A29, XREAL_1:234
.=
((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, Th21
;
(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 A28, A29, XREAL_1:234
.=
((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 A29, XREAL_1:234
.=
((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, Th21
.=
((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 A25, 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 A25, 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 A30;
:: thesis: verum end; suppose
i > 1
;
:: thesis: (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 A31:
i -' 1
>= 1
by NAT_D:49;
i - 1
<= n
by A21, XREAL_1:22;
then A32:
i -' 1
in Seg n
by A24, A31, FINSEQ_1:3;
(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 A25, A28, 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 A25, 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 A32, 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 A32, 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 A27;
:: thesis: 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
;
:: thesis: verum end; suppose A33:
i = n + 1
;
:: thesis: (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 FINSEQ_1:def 18
.=
SubDigit ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k)),
(n + 1),
k
by FINSEQ_1:59
.=
(DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) /. (n + 1)
by A9, Def6
.=
(DigitSD ((DecSD x,(n + 1),k) '+' (DecSD y,(n + 1),k))) . (n + 1)
by A23, A33, PARTFUN1:def 8
;
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 A33;
:: thesis: verum end;
end;
hence
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 A19, FINSEQ_1:18;
:: thesis: verum
end;
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;
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 A15, RVSUM_1:104
.=
((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 A9, 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 A9, A10, 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 A8, 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 A8, 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 A10, A11, Th27
.=
((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 A7, A10, A14
.=
(((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:11
.=
(((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 A12, A13, NAT_D:2, PREPOWER:13
;
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 A10, A11, Th27;
:: thesis: verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A2, A6);
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; :: thesis: verum