let n, k, x, y, i be Nat; ( i in Seg n & 2 <= k implies SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
set X = x mod ((Radix k) |^ n);
set Y = y mod ((Radix k) |^ n);
assume A1:
i in Seg n
; ( not 2 <= k or SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k) )
then
i <= n
by FINSEQ_1:1;
then A2:
i <= n + 1
by NAT_1:12;
A3:
1 <= i
by A1, FINSEQ_1:1;
then A4:
i in Seg (n + 1)
by A2, FINSEQ_1:1;
i <= (n + 1) + 1
by A2, NAT_1:12;
then A5:
i in Seg ((n + 1) + 1)
by A3, FINSEQ_1:1;
reconsider i = i as Element of NAT by ORDINAL1:def 12;
assume A6:
2 <= k
; SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
then A7:
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = (SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k))
by A5, Def1;
now SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)per cases
( i = 1 or i <> 1 )
;
suppose A8:
i = 1
;
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)then A9:
DigA_SDSub (
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
(i -' 1)) =
DigA_SDSub (
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
0)
by XREAL_1:232
.=
0
by RADIX_3:def 5
;
A10:
DigA_SDSub (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(i -' 1)) =
DigA_SDSub (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
0)
by A8, XREAL_1:232
.=
0
by RADIX_3:def 5
;
A11:
DigA_SDSub (
(SD2SDSub (DecSD (y,(n + 1),k))),
(i -' 1)) =
DigA_SDSub (
(SD2SDSub (DecSD (y,(n + 1),k))),
0)
by A8, XREAL_1:232
.=
0
by RADIX_3:def 5
;
A12:
DigA_SDSub (
(SD2SDSub (DecSD (x,(n + 1),k))),
(i -' 1)) =
DigA_SDSub (
(SD2SDSub (DecSD (x,(n + 1),k))),
0)
by A8, XREAL_1:232
.=
0
by RADIX_3:def 5
;
(
DigA_SDSub (
(SD2SDSub (DecSD (x,(n + 1),k))),
i)
= DigA_SDSub (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
i) &
DigA_SDSub (
(SD2SDSub (DecSD (y,(n + 1),k))),
i)
= DigA_SDSub (
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
i) )
by A1, A6, RADIX_3:20;
hence
SDSubAddDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
(SD2SDSub (DecSD (y,(n + 1),k))),
i,
k)
= SDSubAddDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
i,
k)
by A4, A6, A7, A12, A11, A10, A9, Def1;
verum end; suppose A13:
i <> 1
;
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
i >= 1
by A1, FINSEQ_1:1;
then
1
< i
by A13, XXREAL_0:1;
then A14:
0 + 1
<= i -' 1
by INT_1:7, JORDAN12:1;
i <= n
by A1, FINSEQ_1:1;
then
i -' 1
<= n
by NAT_D:44;
then A15:
i -' 1
in Seg n
by A14, FINSEQ_1:1;
SDSubAddDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
(SD2SDSub (DecSD (y,(n + 1),k))),
i,
k) =
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k))
by A1, A6, A7, RADIX_3:20
.=
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD (x,(n + 1),k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k))
by A1, A6, RADIX_3:20
.=
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD (y,(n + 1),k))),(i -' 1)))),k))
by A6, A15, RADIX_3:20
.=
(SDSub_Add_Data (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),i)) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i))),k)) + (SDSub_Add_Carry (((DigA_SDSub ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(i -' 1))) + (DigA_SDSub ((SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),(i -' 1)))),k))
by A6, A15, RADIX_3:20
.=
SDSubAddDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
i,
k)
by A4, A6, Def1
;
hence
SDSubAddDigit (
(SD2SDSub (DecSD (x,(n + 1),k))),
(SD2SDSub (DecSD (y,(n + 1),k))),
i,
k)
= SDSubAddDigit (
(SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),
(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),
i,
k)
;
verum end;
hence
SDSubAddDigit ((SD2SDSub (DecSD (x,(n + 1),k))),(SD2SDSub (DecSD (y,(n + 1),k))),i,k) = SDSubAddDigit ((SD2SDSub (DecSD ((x mod ((Radix k) |^ n)),n,k))),(SD2SDSub (DecSD ((y mod ((Radix k) |^ n)),n,k))),i,k)
; verum