let n, m, k be Nat; :: thesis: ( m in Seg n & k >= 2 implies SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) )
assume that
A1: m in Seg n and
A2: k >= 2 ; :: thesis: SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k))
n >= m by A1, FINSEQ_1:3;
then A3: n + 1 > m by NAT_1:13;
A4: n + 1 in Seg (n + 1) by FINSEQ_1:5;
then A5: DigA (Fmin (n + 1),m,k),(n + 1) = FminDigit m,k,(n + 1) by Def6
.= 0 by A2, A3, Def5 ;
A6: m in Seg (n + 1) by A1, FINSEQ_2:9;
A7: m >= 1 by A1, FINSEQ_1:3;
A8: for i being Nat st i in Seg (n + 1) holds
DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

proof

let i be Nat; :: thesis: ( i in Seg (n + 1) implies DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i )
A9: m + 1 > m by NAT_1:13;
assume A10: i in Seg (n + 1) ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i
then A11: DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = Add (Fmin (n + 1),m,k),(Fmax (n + 1),m,k),i,k by RADIX_1:def 14
.= (SD_Add_Data ((DigA (Fmin (n + 1),m,k),i) + (DigA (Fmax (n + 1),m,k),i)),k) + (SD_Add_Carry ((DigA (Fmin (n + 1),m,k),(i -' 1)) + (DigA (Fmax (n + 1),m,k),(i -' 1)))) by A2, A10, RADIX_1:def 13 ;
A12: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,i by A10, Def6;
A13: DigA (Fmin (n + 1),m,k),i = FminDigit m,k,i by A10, Def6;
A14: DigA (Fmax (n + 1),m,k),i = FmaxDigit m,k,i by A10, Def8;
A15: i >= 1 by A10, FINSEQ_1:3;

now

per cases ( i >= m + 1 or i < m + 1 ) ;

suppose A16: i >= m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

now

per cases ( i = m + 1 or i <> m + 1 ) ;

suppose A17: i = m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A18: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,(m + 1) by A10, Def6
.= 1 by A2, Def5 ;
A19: DigA (Fmax (n + 1),m,k),(i -' 1) = DigA (Fmax (n + 1),m,k),m by A17, NAT_D:34
.= FmaxDigit m,k,m by A6, Def8
.= (Radix k) - 1 by A2, Def7 ;
A20: DigA (Fmax (n + 1),m,k),i = FmaxDigit m,k,(m + 1) by A10, A17, Def8
.= 0 by A2, A9, Def7 ;
A21: DigA (Fmin (n + 1),m,k),(i -' 1) = DigA (Fmin (n + 1),m,k),m by A17, NAT_D:34
.= FminDigit m,k,m by A6, Def6
.= 1 by A2, Def5 ;
DigA (Fmin (n + 1),m,k),i = FminDigit m,k,(m + 1) by A10, A17, Def6
.= 0 by A2, A9, Def5 ;
then DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = 0 + (SD_Add_Carry (1 + ((Radix k) - 1))) by A11, A20, A21, A19, RADIX_1:22
.= 1 by A2, Th10 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A18; :: thesis: verum

end;

suppose A22: i <> m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then i > m + 1 by A16, XXREAL_0:1;
then i - 1 > (m + 1) - 1 by XREAL_1:16;
then A23: i -' 1 > m by XREAL_0:def 2;
i > m by A16, NAT_1:13;
then i > 1 by A7, XXREAL_0:2;
then A24: i -' 1 in Seg (n + 1) by A10, Th2;
then A25: DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(i -' 1) by Def6
.= 0 by A2, A23, Def5 ;
A26: DigA (Fmin (n + 1),(m + 1),k),i = 0 by A2, A12, A22, Def5;
A27: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(i -' 1) by A24, Def8
.= 0 by A2, A23, Def7 ;
( DigA (Fmin (n + 1),m,k),i = 0 & DigA (Fmax (n + 1),m,k),i = 0 ) by A2, A9, A13, A14, A16, Def5, Def7;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A11, A25, A27, A26, RADIX_1:21, RADIX_1:22; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

suppose i < m + 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A28: i <= m by NAT_1:13;

now

per cases ( i > 1 or i = 1 ) by A15, XXREAL_0:1;

suppose A29: i > 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A30: m > 1 by A28, XXREAL_0:2;
then A31: m -' 1 < m by JORDAN5B:1;
A32: m -' 1 in Seg (n + 1) by A6, A30, Th2;

now

per cases ( i = m or i < m ) by A28, XXREAL_0:1;

suppose A33: i = m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A34: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(m -' 1) by A32, Def8
.= 0 by A2, A31, Def7 ;
A35: DigA (Fmax (n + 1),m,k),i = (Radix k) - 1 by A2, A14, A33, Def7;
A36: DigA (Fmin (n + 1),(m + 1),k),i = FminDigit (m + 1),k,m by A10, A33, Def6
.= 0 by A2, A9, Def5 ;
DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(m -' 1) by A32, A33, Def6
.= 0 by A2, A31, Def5 ;
then DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (1 + ((Radix k) - 1)),k) + 0 by A2, A11, A13, A33, A35, A34, Def5, RADIX_1:21
.= 0 by A2, Th11 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A36; :: thesis: verum

end;

suppose A37: i < m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

A38: i -' 1 >= 1 by A29, NAT_D:49;
A39: i -' 1 < i by A15, JORDAN5B:1;
then i -' 1 < m by A37, XXREAL_0:2;
then i -' 1 <= n + 1 by A3, XXREAL_0:2;
then A40: i -' 1 in Seg (n + 1) by A38, FINSEQ_1:3;
then A41: DigA (Fmax (n + 1),m,k),(i -' 1) = FmaxDigit m,k,(i -' 1) by Def8
.= 0 by A2, A37, A39, Def7 ;
A42: DigA (Fmax (n + 1),m,k),i = 0 by A2, A14, A37, Def7;
A43: i < m + 1 by A37, NAT_1:13;
DigA (Fmin (n + 1),m,k),(i -' 1) = FminDigit m,k,(i -' 1) by A40, Def6
.= 0 by A2, A37, A39, Def5 ;
then DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (0 + 0 ),k) + (SD_Add_Carry (0 + 0 )) by A2, A11, A13, A37, A42, A41, Def5
.= 0 + 0 by RADIX_1:21, RADIX_1:22 ;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A2, A12, A43, Def5; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

suppose A44: i = 1 ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then A45: DigA (Fmax (n + 1),m,k),(i -' 1) = 0 by NAT_2:10, RADIX_1:def 3;

now

per cases ( i < m or i = m ) by A28, XXREAL_0:1;

suppose A46: i < m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then ( DigA (Fmin (n + 1),m,k),i = 0 & DigA (Fmax (n + 1),m,k),i = 0 ) by A2, A13, A14, Def5, Def7;
then A47: DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (0 + 0 ),k) + (SD_Add_Carry (0 + 0 )) by A11, A44, A45, NAT_2:10, RADIX_1:def 3
.= 0 + 0 by RADIX_1:21, RADIX_1:22 ;
i < m + 1 by A46, NAT_1:13;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A2, A12, A47, Def5; :: thesis: verum

end;

suppose A48: i = m ; :: thesis: DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i

then ( DigA (Fmin (n + 1),m,k),i = 1 & DigA (Fmax (n + 1),m,k),i = (Radix k) - 1 ) by A2, A13, A14, Def5, Def7;
then A49: DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i = (SD_Add_Data (1 + ((Radix k) - 1)),k) + 0 by A11, A44, A45, NAT_2:10, RADIX_1:21, RADIX_1:def 3
.= 0 by A2, Th11 ;
i < m + 1 by A48, NAT_1:13;
hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i by A2, A12, A49, Def5; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

end;

end;

hence DigA (Fmin (n + 1),(m + 1),k),i = DigA ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k)),i ; :: thesis: verum

end;

A50: DigA (Fmax (n + 1),m,k),(n + 1) = FmaxDigit m,k,(n + 1) by A4, Def8
.= 0 by A2, A3, Def7 ;
(SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) = (SDDec ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k))) + ((SD_Add_Carry ((DigA (Fmin (n + 1),m,k),(n + 1)) + (DigA (Fmax (n + 1),m,k),(n + 1)))) * ((Radix k) |^ (n + 1))) by A2, NAT_1:11, RADIX_2:11
.= (SDDec ((Fmin (n + 1),m,k) '+' (Fmax (n + 1),m,k))) + (0 * ((Radix k) |^ (n + 1))) by A5, A50, RADIX_1:21 ;
hence SDDec (Fmin (n + 1),(m + 1),k) = (SDDec (Fmin (n + 1),m,k)) + (SDDec (Fmax (n + 1),m,k)) by A8, Th12, NAT_1:11; :: thesis: verum