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