let s be Nat; ( s >= 2 implies for f being s -element real-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
Sierp162FS f is increasing )
assume A1:
s >= 2
; for f being s -element real-valued increasing positive-yielding FinSequence st f is with_sum_of_reciprocals_equal_1 holds
Sierp162FS f is increasing
let f be s -element real-valued increasing positive-yielding FinSequence; ( f is with_sum_of_reciprocals_equal_1 implies Sierp162FS f is increasing )
assume A2:
f is with_sum_of_reciprocals_equal_1
; Sierp162FS f is increasing
set g = Sierp162FS f;
let x, y be Nat; SEQM_3:def 1 ( not x in proj1 (Sierp162FS f) or not y in proj1 (Sierp162FS f) or y <= x or not (Sierp162FS f) . y <= (Sierp162FS f) . x )
assume that
A3:
x in dom (Sierp162FS f)
and
A4:
y in dom (Sierp162FS f)
and
A5:
x < y
; not (Sierp162FS f) . y <= (Sierp162FS f) . x
set F = 2 (#) f;
A6:
len (Sierp162FS f) = (len <*2*>) + (len (2 (#) f))
by FINSEQ_1:22;
A7:
y <= len (Sierp162FS f)
by A4, FINSEQ_3:25;
x >= 1
by A3, FINSEQ_3:25;
per cases then
( x = 1 or x > 1 )
by XXREAL_0:1;
suppose A8:
x = 1
;
not (Sierp162FS f) . y <= (Sierp162FS f) . xreconsider y1 =
y - 1 as
Element of
NAT by A5, INT_1:3;
A9:
1
<= y1
by A5, A8, INT_1:52;
A10:
y1 <= (len (Sierp162FS f)) - 1
by A7, XREAL_1:6;
then A11:
(Sierp162FS f) . (1 + y1) =
(2 (#) f) . y1
by A6, A9, Lm21, FINSEQ_1:65
.=
2
* (f . y1)
by VALUED_1:6
;
len (2 (#) f) = len f
by COMPLSP2:3;
then
f . y1 > 1
by A1, A2, A6, A9, A10, Lm21, Th113, FINSEQ_3:25;
then
2
* (f . y1) > 2
* 1
by XREAL_1:68;
hence
(Sierp162FS f) . x < (Sierp162FS f) . y
by A8, A11;
verum end; suppose A12:
x > 1
;
not (Sierp162FS f) . y <= (Sierp162FS f) . xthen reconsider x1 =
x - 1 as
Element of
NAT by INT_1:3;
1
+ 1
<= x
by A12, NAT_1:13;
then A13:
(1 + 1) - 1
<= x1
by XREAL_1:6;
x <= len (Sierp162FS f)
by A3, FINSEQ_3:25;
then
x1 <= (len (Sierp162FS f)) - 1
by XREAL_1:6;
then A14:
x1 in dom (2 (#) f)
by A6, A13, Lm21, FINSEQ_3:25;
then A15:
(Sierp162FS f) . (x1 + 1) =
(2 (#) f) . x1
by FINSEQ_3:103
.=
2
* (f . x1)
by VALUED_1:6
;
reconsider y1 =
y - 1 as
Element of
NAT by A5, INT_1:3;
y > 1
by A5, A12, XXREAL_0:2;
then
1
+ 1
<= y
by NAT_1:13;
then A16:
(1 + 1) - 1
<= y1
by XREAL_1:6;
y1 <= (len (Sierp162FS f)) - 1
by A7, XREAL_1:6;
then A17:
y1 in dom (2 (#) f)
by A6, A16, Lm21, FINSEQ_3:25;
then A18:
(Sierp162FS f) . (y1 + 1) =
(2 (#) f) . y1
by FINSEQ_3:103
.=
2
* (f . y1)
by VALUED_1:6
;
A19:
dom (2 (#) f) = dom f
by VALUED_1:def 5;
x1 < y1
by A5, XREAL_1:6;
hence
(Sierp162FS f) . x < (Sierp162FS f) . y
by A14, A15, A17, A18, A19, SEQM_3:def 1, XREAL_1:68;
verum end;