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