let F be FinSequence of INT ; for m, n, ma being Nat st 1 <= m & m <= n & n <= len F holds
( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) )
let m, n, ma be Nat; ( 1 <= m & m <= n & n <= len F implies ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) ) )
assume that
A1:
1 <= m
and
A2:
m <= n
and
A3:
n <= len F
; ( ma = min_at (F,m,n) iff ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) ) )
set Cut = (m,n) -cut F;
A4:
(len ((m,n) -cut F)) + m = n + 1
by A1, A2, A3, Def1;
hereby ( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) implies ma = min_at (F,m,n) )
A5:
n - m < (n - m) + 1
by XREAL_1:29;
assume
ma = min_at (
F,
m,
n)
;
( m <= ma & ma <= n & ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) )then consider X being non
empty finite Subset of
INT such that A6:
X = rng ((m,n) -cut F)
and A7:
ma + 1
= ((min X) .. ((m,n) -cut F)) + m
by A1, A2, A3, Def11;
A8:
ma = (((min X) .. ((m,n) -cut F)) - 1) + m
by A7;
A9:
ma = (((min X) .. ((m,n) -cut F)) + m) - 1
by A7;
A10:
min X in X
by XXREAL_2:def 7;
then A11:
1
<= (min X) .. ((m,n) -cut F)
by A6, FINSEQ_4:21;
then
1
- 1
<= ((min X) .. ((m,n) -cut F)) - 1
by XREAL_1:9;
then reconsider i1 =
((min X) .. ((m,n) -cut F)) - 1 as
Element of
NAT by INT_1:3;
A12:
(min X) .. ((m,n) -cut F) <= len ((m,n) -cut F)
by A6, A10, FINSEQ_4:21;
then
i1 < len ((m,n) -cut F)
by XREAL_1:146, XXREAL_0:2;
then A13:
F . ma =
((m,n) -cut F) . (i1 + 1)
by A1, A2, A3, A8, Def1
.=
((m,n) -cut F) . ((ma + 1) - m)
by A7
;
((min X) .. ((m,n) -cut F)) + m <= (len ((m,n) -cut F)) + m
by A12, XREAL_1:6;
then A14:
ma <= ((len ((m,n) -cut F)) + m) - 1
by A9, XREAL_1:9;
m + 1
<= ((min X) .. ((m,n) -cut F)) + m
by A11, XREAL_1:6;
then
(m + 1) - 1
<= ma
by A9, XREAL_1:9;
hence
(
m <= ma &
ma <= n )
by A4, A14;
( ( for i being Nat st m <= i & i <= n holds
F . ma <= F . i ) & ( for i being Nat st m <= i & i < ma holds
F . ma < F . i ) )A15:
((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X
by A6, A10, FINSEQ_4:19;
thus A16:
for
i being
Nat st
m <= i &
i <= n holds
F . ma <= F . i
for i being Nat st m <= i & i < ma holds
F . ma < F . iproof
let i be
Nat;
( m <= i & i <= n implies F . ma <= F . i )
assume that A17:
m <= i
and A18:
i <= n
;
F . ma <= F . i
m - m <= i - m
by A17, XREAL_1:9;
then reconsider i1 =
i - m as
Element of
NAT by INT_1:3;
A19:
0 + 1
<= i1 + 1
by XREAL_1:6;
A20:
n - m < (n - m) + 1
by XREAL_1:29;
i1 <= n - m
by A18, XREAL_1:9;
then A21:
i1 < len ((m,n) -cut F)
by A4, A20, XXREAL_0:2;
then
i1 + 1
<= len ((m,n) -cut F)
by NAT_1:13;
then A22:
i1 + 1
in dom ((m,n) -cut F)
by A19, FINSEQ_3:25;
((m,n) -cut F) . (i1 + 1) = F . (m + i1)
by A1, A2, A3, A21, Def1;
then
F . i in rng ((m,n) -cut F)
by A22, FUNCT_1:def 3;
hence
F . ma <= F . i
by A6, A7, A13, A15, XXREAL_2:def 7;
verum
end; let i be
Nat;
( m <= i & i < ma implies F . ma < F . i )assume that A23:
m <= i
and A24:
i < ma
;
F . ma < F . iA25:
i <= n
by A4, A14, A24, XXREAL_0:2;
then A26:
F . ma <= F . i
by A16, A23;
m - m <= i - m
by A23, XREAL_1:9;
then reconsider i1 =
i - m as
Element of
NAT by INT_1:3;
reconsider k =
i1 + 1 as
Element of
NAT ;
i <= ((len ((m,n) -cut F)) - 1) + m
by A14, A24, XXREAL_0:2;
then
i - m <= (len ((m,n) -cut F)) - 1
by XREAL_1:20;
then A27:
k <= len ((m,n) -cut F)
by XREAL_1:19;
i1 <= n - m
by A25, XREAL_1:9;
then A28:
i1 < len ((m,n) -cut F)
by A4, A5, XXREAL_0:2;
0 + 1
<= k
by XREAL_1:6;
then A29:
k in dom ((m,n) -cut F)
by A27, FINSEQ_3:25;
i - m < ma - m
by A24, XREAL_1:9;
then A30:
k < (ma - m) + 1
by XREAL_1:6;
F . i =
F . (i1 + m)
.=
((m,n) -cut F) . k
by A1, A2, A3, A28, Def1
;
then
F . i <> F . ma
by A6, A7, A10, A13, A30, A29, FINSEQ_4:19, FINSEQ_4:24;
hence
F . ma < F . i
by A26, XXREAL_0:1;
verum
end;
set Cut = (m,n) -cut F;
A31:
(len ((m,n) -cut F)) + m = n + 1
by A1, A2, A3, Def1;
then A32:
len ((m,n) -cut F) = (n + 1) - m
;
set X = rng ((m,n) -cut F);
A33:
rng ((m,n) -cut F) is Subset of INT
;
m < n + 1
by A2, NAT_1:13;
then
m - m < (n + 1) - m
by XREAL_1:9;
then
not (m,n) -cut F is empty
by A31;
then reconsider X = rng ((m,n) -cut F) as non empty finite Subset of INT by A33;
reconsider rX = X as non empty finite Subset of REAL by MEMBERED:3;
assume that
A34:
m <= ma
and
A35:
ma <= n
and
A36:
for i being Nat st m <= i & i <= n holds
F . ma <= F . i
and
A37:
for i being Nat st m <= i & i < ma holds
F . ma < F . i
; ma = min_at (F,m,n)
m - m <= ma - m
by A34, XREAL_1:9;
then reconsider qm = ma - m as Element of NAT by INT_1:3;
A38:
qm + 1 = (ma + 1) - m
;
then reconsider q1 = (ma + 1) - m as Element of NAT ;
ma + 1 <= n + 1
by A35, XREAL_1:6;
then A39:
q1 <= len ((m,n) -cut F)
by A32, XREAL_1:9;
0 + 1 <= qm + 1
by XREAL_1:6;
then A40:
q1 in dom ((m,n) -cut F)
by A39, FINSEQ_3:25;
A41:
ma = qm + m
;
qm < len ((m,n) -cut F)
by A38, A39, NAT_1:13;
then A42:
F . ma = ((m,n) -cut F) . ((ma + 1) - m)
by A1, A2, A3, A38, A41, Def1;
now ( F . ma in X & ( for k being ExtReal st k in X holds
F . ma <= k ) )thus
F . ma in X
by A40, A42, FUNCT_1:def 3;
for k being ExtReal st k in X holds
F . ma <= klet k be
ExtReal;
( k in X implies F . ma <= k )assume
k in X
;
F . ma <= kthen consider dk being
object such that A43:
dk in dom ((m,n) -cut F)
and A44:
((m,n) -cut F) . dk = k
by FUNCT_1:def 3;
reconsider dk =
dk as
Element of
NAT by A43;
1
<= dk
by A43, FINSEQ_3:25;
then
1
- 1
<= dk - 1
by XREAL_1:9;
then reconsider dk1 =
dk - 1 as
Element of
NAT by INT_1:3;
A45:
dk <= len ((m,n) -cut F)
by A43, FINSEQ_3:25;
then
dk + m <= (len ((m,n) -cut F)) + m
by XREAL_1:6;
then A46:
(dk + m) - 1
<= n
by A4, XREAL_1:20;
dk1 < len ((m,n) -cut F)
by A45, XREAL_1:146, XXREAL_0:2;
then F . (dk1 + m) =
((m,n) -cut F) . (dk1 + 1)
by A1, A2, A3, Def1
.=
((m,n) -cut F) . dk
;
hence
F . ma <= k
by A36, A44, A46, NAT_1:12;
verum end;
then A47:
F . ma = min rX
by XXREAL_2:def 7;
set mX = min X;
set mXC = (min X) .. ((m,n) -cut F);
A48:
min X in X
by XXREAL_2:def 7;
then
1 <= (min X) .. ((m,n) -cut F)
by FINSEQ_4:21;
then
1 - 1 <= ((min X) .. ((m,n) -cut F)) - 1
by XREAL_1:9;
then reconsider mXC1 = ((min X) .. ((m,n) -cut F)) - 1 as Element of NAT by INT_1:3;
set mXCm = mXC1 + m;
(min X) .. ((m,n) -cut F) <= len ((m,n) -cut F)
by A48, FINSEQ_4:21;
then A49:
mXC1 < len ((m,n) -cut F)
by XREAL_1:146, XXREAL_0:2;
(min X) .. ((m,n) -cut F) = mXC1 + 1
;
then A50:
F . (mXC1 + m) = ((m,n) -cut F) . ((min X) .. ((m,n) -cut F))
by A1, A2, A3, A49, Def1;
A51:
m <= mXC1 + m
by NAT_1:12;
A52:
((m,n) -cut F) . ((min X) .. ((m,n) -cut F)) = min X
by A48, FINSEQ_4:19;
then
ma + 1 = ((min X) .. ((m,n) -cut F)) + m
;
hence
ma = min_at (F,m,n)
by A1, A2, A3, Def11; verum