let n be Nat; ( n >= 1 implies for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) )
A1:
1 in Seg 1
by FINSEQ_1:1;
assume A2:
n >= 1
; for m, k being Nat st m in Seg n & k >= 2 holds
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
then A3:
1 in Seg n
by FINSEQ_1:1;
let m, k be Nat; ( m in Seg n & k >= 2 implies SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) )
assume that
A4:
m in Seg n
and
A5:
k >= 2
; SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
A6:
n >= m
by A4, FINSEQ_1:1;
A7:
m >= 1
by A4, FINSEQ_1:1;
now SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))per cases
( n = 1 or n > 1 )
by A2, XXREAL_0:1;
suppose A8:
n = 1
;
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))then A9:
m = 1
by A6, A7, XXREAL_0:1;
A10:
SDDec (Fmin (1,m,k)) =
DigA (
(Fmin (1,m,k)),1)
by Th4
.=
FminDigit (
m,
k,1)
by A1, Def6
.=
1
by A5, A9, Def5
;
A11:
DigA (
(SDMax (1,m,k)),1) =
SDMaxDigit (
m,
k,1)
by A1, Def4
.=
0
by A5, A6, A8, Def3
;
SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k))) =
DigA (
((SDMax (1,m,k)) '+' (DecSD (1,1,k))),1)
by Th4
.=
Add (
(SDMax (1,m,k)),
(DecSD (1,1,k)),1,
k)
by A1, RADIX_1:def 14
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),(1 -' 1))) + (DigA ((DecSD (1,1,k)),(1 -' 1)))))
by A5, A1, RADIX_1:def 13
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + (DigA ((DecSD (1,1,k)),(1 -' 1)))))
by XREAL_1:232
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + (DigA ((DecSD (1,1,k)),0))))
by XREAL_1:232
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry ((DigA ((SDMax (1,m,k)),0)) + 0))
by RADIX_1:def 3
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + (SD_Add_Carry (0 + 0))
by RADIX_1:def 3
.=
(SD_Add_Data (((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1))),k)) + 0
by RADIX_1:def 10
.=
SD_Add_Data (
((DigA ((SDMax (1,m,k)),1)) + 1),
k)
by A5, A1, Th7
;
then A12:
SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k))) =
1
- ((SD_Add_Carry 1) * (Radix k))
by A11, RADIX_1:def 11
.=
1
- (0 * (Radix k))
by RADIX_1:def 10
.=
1
;
(SDDec (SDMax (1,m,k))) + (SDDec (DecSD (1,1,k))) =
(SDDec ((SDMax (1,m,k)) '+' (DecSD (1,1,k)))) + ((SD_Add_Carry ((DigA ((SDMax (1,m,k)),1)) + (DigA ((DecSD (1,1,k)),1)))) * ((Radix k) |^ 1))
by A5, RADIX_2:11
.=
1
+ ((SD_Add_Carry (0 + 1)) * ((Radix k) |^ 1))
by A5, A1, A11, A12, Th7
.=
1
+ (0 * ((Radix k) |^ 1))
by RADIX_1:def 10
;
hence
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
by A8, A10;
verum end; suppose A13:
n > 1
;
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))A14:
n in Seg n
by A2, FINSEQ_1:1;
then A15:
DigA (
(SDMax (n,m,k)),
n) =
SDMaxDigit (
m,
k,
n)
by Def4
.=
0
by A5, A6, Def3
;
A16:
for
i being
Nat st
i in Seg n holds
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
proof
let i be
Nat;
( i in Seg n implies DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i) )
assume A17:
i in Seg n
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
then A18:
DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
Add (
(SDMax (n,m,k)),
(DecSD (1,n,k)),
i,
k)
by RADIX_1:def 14
.=
(SD_Add_Data (((DigA ((SDMax (n,m,k)),i)) + (DigA ((DecSD (1,n,k)),i))),k)) + (SD_Add_Carry ((DigA ((SDMax (n,m,k)),(i -' 1))) + (DigA ((DecSD (1,n,k)),(i -' 1)))))
by A5, A17, RADIX_1:def 13
;
A19:
DigA (
(SDMax (n,m,k)),
i)
= SDMaxDigit (
m,
k,
i)
by A17, Def4;
A20:
DigA (
(Fmin (n,m,k)),
i)
= FminDigit (
m,
k,
i)
by A17, Def6;
A21:
i >= 1
by A17, FINSEQ_1:1;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i >= m + 1 or i < m + 1 )
;
suppose A22:
i >= m + 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A23:
i > m
by NAT_1:13;
then A24:
DigA (
(SDMax (n,m,k)),
i)
= 0
by A5, A19, Def3;
A25:
i > 1
by A7, A23, XXREAL_0:2;
then A26:
(
i -' 1
in Seg n &
DigA (
(DecSD (1,n,k)),
i)
= 0 )
by A5, A17, Th2, Th8;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i = m + 1 or i > m + 1 )
by A22, XXREAL_0:1;
suppose
i = m + 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then DigA (
(SDMax (n,m,k)),
(i -' 1)) =
DigA (
(SDMax (n,m,k)),
m)
by NAT_D:34
.=
SDMaxDigit (
m,
k,
m)
by A4, Def4
.=
0
by A5, Def3
;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((0 + 0),k)) + 0
by A5, A18, A24, A26, Lm2
.=
0
by RADIX_1:19
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A23, Def5;
verum end; suppose
i > m + 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
i - 1
> (m + 1) - 1
by XREAL_1:14;
then A27:
i -' 1
> m
by XREAL_0:def 2;
i -' 1
in Seg n
by A17, A25, Th2;
then DigA (
(SDMax (n,m,k)),
(i -' 1)) =
SDMaxDigit (
m,
k,
(i -' 1))
by Def4
.=
0
by A5, A27, Def3
;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((0 + 0),k)) + 0
by A5, A18, A24, A26, Lm2
.=
0
by RADIX_1:19
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A23, Def5;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; suppose
i < m + 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A28:
i <= m
by NAT_1:13;
A29:
i >= 1
by A17, FINSEQ_1:1;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i > 1 or i = 1 )
by A29, XXREAL_0:1;
suppose A30:
i > 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A31:
m > 1
by A28, XXREAL_0:2;
then A32:
m -' 1
< m
by JORDAN5B:1;
A33:
m -' 1
in Seg n
by A4, A31, Th2;
then A34:
m -' 1
>= 1
by FINSEQ_1:1;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i = m or i < m )
by A28, XXREAL_0:1;
suppose A35:
i = m
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A36:
(
DigA (
(SDMax (n,m,k)),
i)
= 0 &
DigA (
(DecSD (1,n,k)),
i)
= 0 )
by A4, A5, A19, A30, Def3, Th8;
A37:
DigA (
(Fmin (n,m,k)),
i) =
FminDigit (
m,
k,
m)
by A4, A35, Def6
.=
1
by A5, Def5
;
A38:
DigA (
(SDMax (n,m,k)),
(i -' 1)) =
SDMaxDigit (
m,
k,
(m -' 1))
by A33, A35, Def4
.=
(Radix k) - 1
by A5, A34, A32, Def3
;
A39:
i >= 1
+ 1
by A30, INT_1:7;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i = 2 or i > 2 )
by A39, XXREAL_0:1;
suppose
i = 2
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
i -' 1
= 2
- 1
by XREAL_1:233;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 1))
by A5, A3, A18, A36, A38, Th7
.=
0 + (SD_Add_Carry (((Radix k) - 1) + 1))
by RADIX_1:19
.=
1
by A5, Th10
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A37;
verum end; suppose A40:
i > 2
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
i - 1
> 2
- 1
by XREAL_1:14;
then A41:
i -' 1
> 1
by XREAL_0:def 2;
i > 1
by A40, XXREAL_0:2;
then
i -' 1
in Seg n
by A17, Th2;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((0 + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0))
by A5, A18, A36, A38, A41, Th8
.=
0 + (SD_Add_Carry ((Radix k) - 1))
by RADIX_1:19
.=
1
by A5, Lm1
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A37;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; suppose A42:
i < m
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)
i -' 1
< i
by A30, JORDAN5B:1;
then A43:
i -' 1
< m
by A42, XXREAL_0:2;
A44:
DigA (
(DecSD (1,n,k)),
i)
= 0
by A5, A17, A30, Th8;
A45:
i -' 1
in Seg n
by A17, A30, Th2;
A46:
i >= 1
+ 1
by A30, INT_1:7;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i = 2 or i > 2 )
by A46, XXREAL_0:1;
suppose
i = 2
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A47:
i -' 1
= 2
- 1
by XREAL_1:233;
then A48:
DigA (
(DecSD (1,n,k)),
(i -' 1))
= 1
by A5, A3, Th7;
DigA (
(SDMax (n,m,k)),
(i -' 1)) =
SDMaxDigit (
m,
k,
(i -' 1))
by A45, Def4
.=
(Radix k) - 1
by A5, A43, A47, Def3
;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data (((Radix k) - 1),k)) + (SD_Add_Carry (((Radix k) + 1) - 1))
by A5, A18, A19, A21, A42, A44, A48, Def3
.=
(SD_Add_Data (((Radix k) - 1),k)) + 1
by A5, Th10
.=
(((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1
by RADIX_1:def 11
.=
(((Radix k) - 1) - (1 * (Radix k))) + 1
by A5, Lm1
.=
0
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A42, Def5;
verum end; suppose A49:
i > 2
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
i - 1
> 2
- 1
by XREAL_1:14;
then A50:
i -' 1
> 1
by XREAL_0:def 2;
i > 1
by A49, XXREAL_0:2;
then
i -' 1
in Seg n
by A17, Th2;
then A51:
DigA (
(DecSD (1,n,k)),
(i -' 1))
= 0
by A5, A50, Th8;
DigA (
(SDMax (n,m,k)),
(i -' 1)) =
SDMaxDigit (
m,
k,
(i -' 1))
by A45, Def4
.=
(Radix k) - 1
by A5, A43, A50, Def3
;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((((Radix k) - 1) + 0),k)) + (SD_Add_Carry (((Radix k) - 1) + 0))
by A5, A18, A19, A21, A42, A44, A51, Def3
.=
(SD_Add_Data (((Radix k) - 1),k)) + 1
by A5, Lm1
.=
(((Radix k) - 1) - ((SD_Add_Carry ((Radix k) - 1)) * (Radix k))) + 1
by RADIX_1:def 11
.=
(((Radix k) - 1) - (1 * (Radix k))) + 1
by A5, Lm1
.=
0
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A42, Def5;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; suppose A52:
i = 1
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then A53:
(
DigA (
(SDMax (n,m,k)),
(i -' 1))
= 0 &
DigA (
(DecSD (1,n,k)),
(i -' 1))
= 0 )
by NAT_2:8, RADIX_1:def 3;
now DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)per cases
( i < m or i = m )
by A28, XXREAL_0:1;
suppose A54:
i < m
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
DigA (
(SDMax (n,m,k)),
i)
= (Radix k) - 1
by A5, A19, A52, Def3;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((((Radix k) - 1) + 1),k)) + (SD_Add_Carry (0 + 0))
by A5, A3, A18, A52, A53, Th7
.=
(Radix k) - ((SD_Add_Carry (Radix k)) * (Radix k))
by RADIX_1:18, RADIX_1:def 11
.=
(Radix k) - (1 * (Radix k))
by A5, Th10
.=
0
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A54, Def5;
verum end; suppose A55:
i = m
;
DigA ((Fmin (n,m,k)),i) = DigA (((SDMax (n,m,k)) '+' (DecSD (1,n,k))),i)then
DigA (
(SDMax (n,m,k)),
i)
= 0
by A5, A19, Def3;
then DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i) =
(SD_Add_Data ((1 + 0),k)) + (SD_Add_Carry (0 + 0))
by A5, A3, A18, A52, A53, Th7
.=
1
- ((SD_Add_Carry 1) * (Radix k))
by RADIX_1:18, RADIX_1:def 11
.=
1
- (0 * (Radix k))
by RADIX_1:def 10
.=
1
;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
by A5, A20, A55, Def5;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; end; end; hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum end; end; end;
hence
DigA (
(Fmin (n,m,k)),
i)
= DigA (
((SDMax (n,m,k)) '+' (DecSD (1,n,k))),
i)
;
verum
end; (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k))) =
(SDDec ((SDMax (n,m,k)) '+' (DecSD (1,n,k)))) + ((SD_Add_Carry ((DigA ((SDMax (n,m,k)),n)) + (DigA ((DecSD (1,n,k)),n)))) * ((Radix k) |^ n))
by A2, A5, RADIX_2:11
.=
(SDDec ((SDMax (n,m,k)) '+' (DecSD (1,n,k)))) + (0 * ((Radix k) |^ n))
by A5, A13, A14, A15, Th8, RADIX_1:18
;
hence
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
by A2, A16, Th12;
verum end; end; end;
hence
SDDec (Fmin (n,m,k)) = (SDDec (SDMax (n,m,k))) + (SDDec (DecSD (1,n,k)))
; verum