let m, k be Nat; ( k >= 2 implies for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k))) )
assume A1:
k >= 2
; for r being Tuple of m + 2,k -SD holds (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
let r be Tuple of m + 2,k -SD ; (SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
A2:
for i being Nat holds
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
proof
let i be
Nat;
( not i in Seg (m + 2) or ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
assume A3:
i in Seg (m + 2)
;
( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )
then A4:
DigA (
(Mmin r),
i)
= MminDigit (
r,
i)
by Def6;
A5:
i >= 1
by A3, FINSEQ_1:1;
now ( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )per cases
( i < m or i >= m )
;
suppose A6:
i < m
;
( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )A7:
DigA (
(M0 r),
i) =
M0Digit (
r,
i)
by A3, Def2
.=
0
by A3, A6, Def1
;
DigA (
(Mmin r),
i) =
(- (Radix k)) + 1
by A1, A3, A4, A6, Def5
.=
SDMinDigit (
m,
k,
i)
by A1, A5, A6, RADIX_5:def 1
.=
DigA (
(SDMin ((m + 2),m,k)),
i)
by A3, RADIX_5:def 2
;
hence
( (
DigA (
(M0 r),
i)
= DigA (
(Mmin r),
i) &
DigA (
(SDMin ((m + 2),m,k)),
i)
= 0 ) or (
DigA (
(SDMin ((m + 2),m,k)),
i)
= DigA (
(Mmin r),
i) &
DigA (
(M0 r),
i)
= 0 ) )
by A7;
verum end; suppose A8:
i >= m
;
( ( DigA ((M0 r),i) = DigA ((Mmin r),i) & DigA ((SDMin ((m + 2),m,k)),i) = 0 ) or ( DigA ((SDMin ((m + 2),m,k)),i) = DigA ((Mmin r),i) & DigA ((M0 r),i) = 0 ) )A9:
DigA (
(SDMin ((m + 2),m,k)),
i) =
SDMinDigit (
m,
k,
i)
by A3, RADIX_5:def 2
.=
0
by A1, A8, RADIX_5:def 1
;
DigA (
(Mmin r),
i) =
r . i
by A1, A3, A4, A8, Def5
.=
M0Digit (
r,
i)
by A3, A8, Def1
.=
DigA (
(M0 r),
i)
by A3, Def2
;
hence
( (
DigA (
(M0 r),
i)
= DigA (
(Mmin r),
i) &
DigA (
(SDMin ((m + 2),m,k)),
i)
= 0 ) or (
DigA (
(SDMin ((m + 2),m,k)),
i)
= DigA (
(Mmin r),
i) &
DigA (
(M0 r),
i)
= 0 ) )
by A9;
verum end; end; end;
hence
( (
DigA (
(M0 r),
i)
= DigA (
(Mmin r),
i) &
DigA (
(SDMin ((m + 2),m,k)),
i)
= 0 ) or (
DigA (
(SDMin ((m + 2),m,k)),
i)
= DigA (
(Mmin r),
i) &
DigA (
(M0 r),
i)
= 0 ) )
;
verum
end;
m + 2 >= 1
by NAT_1:12;
hence
(SDDec (Mmin r)) + (SDDec (DecSD (0,(m + 2),k))) = (SDDec (M0 r)) + (SDDec (SDMin ((m + 2),m,k)))
by A1, A2, RADIX_5:15; verum