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:1;
then A3: n + 1 > m by NAT_1:13;
A4: n + 1 in Seg (n + 1) by FINSEQ_1:3;
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:8;
A7: m >= 1 by A1, FINSEQ_1:1;
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:1;
now :: thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
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 :: thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
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:19
.= 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:14;
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:18, RADIX_1:19; :: 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 :: thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
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 :: thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
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:18
.= 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:1;
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:18, RADIX_1:19 ;
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:8, RADIX_1:def 3;
now :: thesis: DigA ((Fmin ((n + 1),(m + 1),k)),i) = DigA (((Fmin ((n + 1),m,k)) '+' (Fmax ((n + 1),m,k))),i)
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:8, RADIX_1:def 3
.= 0 + 0 by RADIX_1:18, RADIX_1:19 ;
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:8, RADIX_1:18, 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:18 ;
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