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 12;
A8: (n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:3;
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 CARD_1:def 7;
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:1;
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 :: 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
per cases ( j in Seg n or j = n + 1 ) by A16, FINSEQ_2:7;
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 6 ;
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:42
.= (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 6 ;
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:16;
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:14;
A22: Radix k > 0 by POWER:34;
then y mod ((Radix k) |^ n) < (Radix k) |^ n by NAT_D:1, PREPOWER:6;
then A23: y mod ((Radix k) |^ n) is_represented_by n,k ;
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:1;
j <= (n + 1) + 1 by A31, NAT_1:12;
then A33: j in Seg ((n + 1) + 1) by A29, FINSEQ_1:1;
A34: j in Seg n by A11, A29, A30, FINSEQ_1:1;
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:14;
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:24;
x mod ((Radix k) |^ n) < (Radix k) |^ n by A22, NAT_D:1, PREPOWER:6;
then x mod ((Radix k) |^ n) is_represented_by n,k ;
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:74;
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:3;
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:1;
now :: thesis: zp . j = (zpp ^ <*(SDSub2INTDigit (((SD2SDSub (DecSD (x,(n + 1),k))) '+' (SD2SDSub (DecSD (y,(n + 1),k)))),(n + 1),k))*>) . j
per cases ( j in Seg n or j = n + 1 ) by A44, FINSEQ_2:7;
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:42
.= 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 CARD_1:def 7;
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:1;
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 :: 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
per cases ( j in Seg (n + 1) or j = (n + 1) + 1 ) by A49, FINSEQ_2:7;
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 6 ;
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:42
.= (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 6 ;
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:16;
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:14;
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:16;
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:14;
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:74
.= ((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:74 ;
A56: n + 1 in Seg (n + 1) by FINSEQ_1:3;
then A57: n + 1 in Seg ((n + 1) + 1) by FINSEQ_2:8;
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:6
.= ((((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:20, 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:20, 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:6;
x = ((x div ((Radix k) |^ n)) * ((Radix k) |^ n)) + (x mod ((Radix k) |^ n)) by A22, NAT_D:2, PREPOWER:6;
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:24;
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 12;
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:1;
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:232
.= 1 * (DigB_SDSub (((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))),1)) by NEWTON:4
.= 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 CARD_1:def 7;
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 6;
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:232
.= (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:232
.= (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:16
.= ((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:1;
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
.= (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 6;
then SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k)))) = <*DIG1,DIG2*> by A67, A68, FINSEQ_1:44;
then A73: Sum (SDSub2INT ((SD2SDSub (DecSD (x,1,k))) '+' (SD2SDSub (DecSD (y,1,k))))) = DIG1 + DIG2 by RVSUM_1:77;
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