let n, m, k be Nat; ( k >= 2 implies for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
assume A1:
k >= 2
; for i being Nat st i in Seg n holds
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
let i be Nat; ( i in Seg n implies (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 )
reconsider a = SDMinDigit (m,k,i) as Element of INT ;
reconsider b = SDMaxDigit (m,k,i) as Element of INT ;
assume A2:
i in Seg n
; (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
then A3:
i >= 1
by FINSEQ_1:1;
A4:
DigA ((SDMin (n,m,k)),i) = SDMinDigit (m,k,i)
by A2, Def2;
now (DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 per cases
( i < m or i >= m )
;
suppose A5:
i < m
;
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 then a + b =
((- (Radix k)) + 1) + b
by A1, A3, Def1
.=
((- (Radix k)) + 1) + ((Radix k) - 1)
by A1, A3, A5, Def3
.=
0
;
hence
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
by A2, A4, Def4;
verum end; suppose A6:
i >= m
;
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0 then a + b =
0 + b
by A1, Def1
.=
0 + 0
by A1, A6, Def3
;
hence
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
by A2, A4, Def4;
verum end;
hence
(DigA ((SDMax (n,m,k)),i)) + (DigA ((SDMin (n,m,k)),i)) = 0
; verum