defpred S1[ Nat] means for k being Nat
for tx, ty being Tuple of $1,k -SD st ( for i being Nat st i in Seg $1 holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec ty;
A1:
for n being Nat st n >= 1 & S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( n >= 1 & S1[n] implies S1[n + 1] )
assume that
n >= 1
and A2:
S1[
n]
;
S1[n + 1]
let k be
Nat;
for tx, ty being Tuple of n + 1,k -SD st ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec tylet tx,
ty be
Tuple of
n + 1,
k -SD ;
( ( for i being Nat st i in Seg (n + 1) holds
DigA (tx,i) >= DigA (ty,i) ) implies SDDec tx >= SDDec ty )
assume A3:
for
i being
Nat st
i in Seg (n + 1) holds
DigA (
tx,
i)
>= DigA (
ty,
i)
;
SDDec tx >= SDDec ty
reconsider n =
n as
Element of
NAT by ORDINAL1:def 12;
deffunc H1(
Nat)
-> Element of
INT =
DigB (
tx,$1);
consider txn being
FinSequence of
INT such that A4:
len txn = n
and A5:
for
i being
Nat st
i in dom txn holds
txn . i = H1(
i)
from FINSEQ_2:sch 1();
deffunc H2(
Nat)
-> Element of
INT =
DigB (
ty,$1);
consider tyn being
FinSequence of
INT such that A6:
len tyn = n
and A7:
for
i being
Nat st
i in dom tyn holds
tyn . i = H2(
i)
from FINSEQ_2:sch 1();
A8:
dom tyn = Seg n
by A6, FINSEQ_1:def 3;
rng tyn c= k -SD
then reconsider tyn =
tyn as
FinSequence of
k -SD by FINSEQ_1:def 4;
A12:
for
i being
Nat st
i in Seg n holds
tyn . i = ty . i
tyn is
Element of
n -tuples_on (k -SD)
by A6, FINSEQ_2:92;
then reconsider tyn =
tyn as
Tuple of
n,
k -SD ;
A15:
dom txn = Seg n
by A4, FINSEQ_1:def 3;
rng txn c= k -SD
then reconsider txn =
txn as
FinSequence of
k -SD by FINSEQ_1:def 4;
A19:
for
i being
Nat st
i in Seg n holds
txn . i = tx . i
txn is
Element of
n -tuples_on (k -SD)
by A4, FINSEQ_2:92;
then reconsider txn =
txn as
Tuple of
n,
k -SD ;
for
i being
Nat st
i in Seg n holds
DigA (
txn,
i)
>= DigA (
tyn,
i)
proof
let i be
Nat;
( i in Seg n implies DigA (txn,i) >= DigA (tyn,i) )
assume A22:
i in Seg n
;
DigA (txn,i) >= DigA (tyn,i)
then A23:
DigA (
tyn,
i) =
tyn . i
by RADIX_1:def 3
.=
DigB (
ty,
i)
by A7, A8, A22
.=
DigA (
ty,
i)
by RADIX_1:def 4
;
DigA (
txn,
i) =
txn . i
by A22, RADIX_1:def 3
.=
DigB (
tx,
i)
by A5, A15, A22
.=
DigA (
tx,
i)
by RADIX_1:def 4
;
hence
DigA (
txn,
i)
>= DigA (
tyn,
i)
by A3, A22, A23, FINSEQ_2:8;
verum
end;
then A24:
SDDec txn >= SDDec tyn
by A2;
n + 1
in Seg (n + 1)
by FINSEQ_1:4;
then A25:
((Radix k) |^ n) * (DigA (tx,(n + 1))) >= ((Radix k) |^ n) * (DigA (ty,(n + 1)))
by A3, XREAL_1:64;
A26:
(SDDec tyn) + (((Radix k) |^ n) * (DigA (ty,(n + 1)))) = SDDec ty
by A12, RADIX_2:10;
(SDDec txn) + (((Radix k) |^ n) * (DigA (tx,(n + 1)))) = SDDec tx
by A19, RADIX_2:10;
hence
SDDec tx >= SDDec ty
by A26, A24, A25, XREAL_1:7;
verum
end;
A27:
S1[1]
proof
let k be
Nat;
for tx, ty being Tuple of 1,k -SD st ( for i being Nat st i in Seg 1 holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec tylet tx,
ty be
Tuple of 1,
k -SD ;
( ( for i being Nat st i in Seg 1 holds
DigA (tx,i) >= DigA (ty,i) ) implies SDDec tx >= SDDec ty )
assume A28:
for
i being
Nat st
i in Seg 1 holds
DigA (
tx,
i)
>= DigA (
ty,
i)
;
SDDec tx >= SDDec ty
A29:
SDDec ty = DigA (
ty,1)
by Th4;
( 1
in Seg 1 &
SDDec tx = DigA (
tx,1) )
by Th4, FINSEQ_1:1;
hence
SDDec tx >= SDDec ty
by A28, A29;
verum
end;
for n being Nat st n >= 1 holds
S1[n]
from NAT_1:sch 8(A27, A1);
hence
for n being Nat st n >= 1 holds
for k being Nat
for tx, ty being Tuple of n,k -SD st ( for i being Nat st i in Seg n holds
DigA (tx,i) >= DigA (ty,i) ) holds
SDDec tx >= SDDec ty
; verum