let x be Real; for A being non empty closed_interval Subset of REAL
for D being Division of A st x in A holds
ex j being Element of NAT st
( j in dom D & x in divset (D,j) )
let A be non empty closed_interval Subset of REAL; for D being Division of A st x in A holds
ex j being Element of NAT st
( j in dom D & x in divset (D,j) )
let D be Division of A; ( x in A implies ex j being Element of NAT st
( j in dom D & x in divset (D,j) ) )
assume A1:
x in A
; ex j being Element of NAT st
( j in dom D & x in divset (D,j) )
then A2:
lower_bound A <= x
by INTEGRA2:1;
A3:
x <= upper_bound A
by A1, INTEGRA2:1;
A4:
rng D <> {}
;
then A5:
1 in dom D
by FINSEQ_3:32;
per cases
( x in rng D or not x in rng D )
;
suppose A12:
not
x in rng D
;
ex j being Element of NAT st
( j in dom D & x in divset (D,j) )defpred S1[
Nat]
means (
x < upper_bound (divset (D,$1)) & $1
in dom D );
A13:
len D in dom D
by FINSEQ_5:6;
upper_bound (divset (D,(len D))) = D . (len D)
then A14:
upper_bound (divset (D,(len D))) = upper_bound A
by INTEGRA1:def 2;
x <> upper_bound A
then
x < upper_bound (divset (D,(len D)))
by A3, A14, XXREAL_0:1;
then A15:
ex
k being
Nat st
S1[
k]
by A13;
consider k being
Nat such that A16:
(
S1[
k] & ( for
n being
Nat st
S1[
n] holds
k <= n ) )
from NAT_1:sch 5(A15);
defpred S2[
Nat]
means (
x >= lower_bound (divset (D,$1)) & $1
in dom D );
lower_bound (divset (D,1)) = lower_bound A
by A5, INTEGRA1:def 4;
then A17:
ex
k being
Nat st
S2[
k]
by A2, A4, FINSEQ_3:32;
A18:
for
k being
Nat st
S2[
k] holds
k <= len D
by FINSEQ_3:25;
consider j being
Nat such that A19:
(
S2[
j] & ( for
n being
Nat st
S2[
n] holds
n <= j ) )
from NAT_1:sch 6(A18, A17);
k = j
proof
assume A20:
k <> j
;
contradiction
per cases
( k < j or k > j )
by A20, XXREAL_0:1;
suppose A21:
k < j
;
contradictionA22:
upper_bound (divset (D,k)) = D . k
A23:
1
<= k
by A16, FINSEQ_3:25;
then
D . (j - 1) <= x
by A19, A21, INTEGRA1:def 4;
then A24:
D . (j - 1) < D . k
by A16, A22, XXREAL_0:2;
j - 1
in dom D
by A19, A21, A23, INTEGRA1:7;
then
j - 1
< k
by A16, A24, SEQ_4:137;
then
j < k + 1
by XREAL_1:19;
hence
contradiction
by A21, NAT_1:13;
verum end; suppose A25:
k > j
;
contradiction
x < upper_bound (divset (D,j))
proof
A26:
upper_bound (divset (D,j)) = D . j
assume A27:
x >= upper_bound (divset (D,j))
;
contradiction
A28:
j + 1
<= k
by A25, NAT_1:13;
A29:
1
<= j
by A19, FINSEQ_3:25;
then A30:
1
<= j + 1
by NAT_1:13;
k <= len D
by A16, FINSEQ_3:25;
then
j + 1
<= len D
by A28, XXREAL_0:2;
then A31:
j + 1
in dom D
by A30, FINSEQ_3:25;
j + 1
> 1
by A29, NAT_1:13;
then lower_bound (divset (D,(j + 1))) =
D . ((j + 1) - 1)
by A31, INTEGRA1:def 4
.=
D . j
;
then
j + 1
<= j
by A19, A27, A26, A31;
hence
contradiction
by NAT_1:13;
verum
end; hence
contradiction
by A16, A19, A25;
verum end; end;
end; then
x in divset (
D,
k)
by A16, A19, INTEGRA2:1;
hence
ex
j being
Element of
NAT st
(
j in dom D &
x in divset (
D,
j) )
by A16;
verum end; end;