let i, j be Element of NAT ; for A, B being non empty closed_interval Subset of REAL
for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds
mid (D,i,j) is Division of B
let A, B be non empty closed_interval Subset of REAL; for D being Division of A st i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B holds
mid (D,i,j) is Division of B
let D be Division of A; ( i in dom D & j in dom D & i <= j & D . i >= lower_bound B & D . j = upper_bound B implies mid (D,i,j) is Division of B )
assume that
A1:
i in dom D
and
A2:
j in dom D
and
A3:
i <= j
and
A4:
D . i >= lower_bound B
and
A5:
D . j = upper_bound B
; mid (D,i,j) is Division of B
A6:
(((j - i) + 1) + i) - 1 = j
;
i in Seg (len D)
by A1, FINSEQ_1:def 3;
then A7:
1 <= i
by FINSEQ_1:1;
0 <= j - i
by A3, XREAL_1:48;
then A8:
0 + 1 <= (j - i) + 1
by XREAL_1:6;
j in Seg (len D)
by A2, FINSEQ_1:def 3;
then A9:
j <= len D
by FINSEQ_1:1;
consider A1 being non empty closed_interval Subset of REAL such that
A10:
lower_bound A1 = (mid (D,i,j)) . 1
and
A11:
upper_bound A1 = (mid (D,i,j)) . (len (mid (D,i,j)))
and
A12:
mid (D,i,j) is Division of A1
by A1, A2, A3, Th34;
A13:
len (mid (D,i,j)) = (j - i) + 1
by A1, A2, A3, Lm1;
A14:
(1 + i) - 1 = i
;
for x being Element of REAL st x in A1 holds
x in B
proof
let x be
Element of
REAL ;
( x in A1 implies x in B )
assume
x in A1
;
x in B
then
x in [.(lower_bound A1),(upper_bound A1).]
by Th2;
then
x in { a where a is Real : ( lower_bound A1 <= a & a <= upper_bound A1 ) }
by RCOMP_1:def 1;
then A15:
ex
a being
Real st
(
x = a &
lower_bound A1 <= a &
a <= upper_bound A1 )
;
then
D . i <= x
by A3, A10, A7, A9, A8, A14, FINSEQ_6:122;
then A16:
lower_bound B <= x
by A4, XXREAL_0:2;
x <= upper_bound B
by A3, A5, A11, A13, A7, A9, A8, A6, A15, FINSEQ_6:122;
then
x in { a where a is Real : ( lower_bound B <= a & a <= upper_bound B ) }
by A16;
then
x in [.(lower_bound B),(upper_bound B).]
by RCOMP_1:def 1;
hence
x in B
by Th2;
verum
end;
then A17:
A1 c= B
;
rng (mid (D,i,j)) c= A1
by A12, Def1;
then A18:
rng (mid (D,i,j)) c= B
by A17;
(mid (D,i,j)) . (len (mid (D,i,j))) = D . j
by A3, A13, A7, A9, A8, A6, FINSEQ_6:122;
hence
mid (D,i,j) is Division of B
by A5, A12, A18, Def1; verum