let A be closed-interval Subset of REAL; for D1 being Division of A st vol A <> 0 & len D1 = 1 holds
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
let D1 be Division of A; ( vol A <> 0 & len D1 = 1 implies <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )
assume A1:
vol A <> 0
; ( not len D1 = 1 or <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )
set MD1 = <*(lower_bound A)*> ^ D1;
A2:
vol A >= 0
by INTEGRA1:11;
assume
len D1 = 1
; <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
then
D1 . 1 = upper_bound A
by INTEGRA1:def 2;
then A3:
(D1 . 1) - (lower_bound A) > 0
by A1, A2, INTEGRA1:def 6;
then A4:
lower_bound A < D1 . 1
by XREAL_1:49;
for n, m being Element of NAT st n in dom (<*(lower_bound A)*> ^ D1) & m in dom (<*(lower_bound A)*> ^ D1) & n < m holds
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m
proof
let n,
m be
Element of
NAT ;
( n in dom (<*(lower_bound A)*> ^ D1) & m in dom (<*(lower_bound A)*> ^ D1) & n < m implies (<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m )
assume that A5:
n in dom (<*(lower_bound A)*> ^ D1)
and A6:
m in dom (<*(lower_bound A)*> ^ D1)
and A7:
n < m
;
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m
A8:
not
m in dom <*(lower_bound A)*>
A10:
not
(<*(lower_bound A)*> ^ D1) . m in rng <*(lower_bound A)*>
proof
assume
(<*(lower_bound A)*> ^ D1) . m in rng <*(lower_bound A)*>
;
contradiction
then
(<*(lower_bound A)*> ^ D1) . m in {(lower_bound A)}
by FINSEQ_1:55;
then A11:
(<*(lower_bound A)*> ^ D1) . m = lower_bound A
by TARSKI:def 1;
rng D1 <> {}
;
then A12:
1
in dom D1
by FINSEQ_3:34;
consider n being
Nat such that A13:
n in dom D1
and A14:
m = (len <*(lower_bound A)*>) + n
by A6, A8, FINSEQ_1:38;
n in Seg (len D1)
by A13, FINSEQ_1:def 3;
then A15:
1
<= n
by FINSEQ_1:3;
D1 . n = (<*(lower_bound A)*> ^ D1) . m
by A13, A14, FINSEQ_1:def 7;
hence
contradiction
by A3, A11, A13, A15, A12, SEQ_4:154, XREAL_1:49;
verum
end;
(<*(lower_bound A)*> ^ D1) . m in rng (<*(lower_bound A)*> ^ D1)
by A6, FUNCT_1:def 5;
then
(<*(lower_bound A)*> ^ D1) . m in (rng <*(lower_bound A)*>) \/ (rng D1)
by FINSEQ_1:44;
then A16:
(<*(lower_bound A)*> ^ D1) . m in rng D1
by A10, XBOOLE_0:def 3;
now per cases
( n in dom <*(lower_bound A)*> or ex i being Nat st
( i in dom D1 & n = (len <*(lower_bound A)*>) + i ) )
by A5, FINSEQ_1:38;
suppose A17:
n in dom <*(lower_bound A)*>
;
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . mthen
n in Seg (len <*(lower_bound A)*>)
by FINSEQ_1:def 3;
then
n in {1}
by FINSEQ_1:4, FINSEQ_1:56;
then A18:
n = 1
by TARSKI:def 1;
A19:
(<*(lower_bound A)*> ^ D1) . n =
<*(lower_bound A)*> . n
by A17, FINSEQ_1:def 7
.=
lower_bound A
by A18, FINSEQ_1:def 8
;
rng D1 <> {}
;
then A20:
1
in dom D1
by FINSEQ_3:34;
consider k being
Element of
NAT such that A21:
k in dom D1
and A22:
(<*(lower_bound A)*> ^ D1) . m = D1 . k
by A16, PARTFUN1:26;
1
<= k
by A21, FINSEQ_3:27;
then
D1 . 1
<= (<*(lower_bound A)*> ^ D1) . m
by A21, A22, A20, SEQ_4:154;
hence
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m
by A4, A19, XXREAL_0:2;
verum end; suppose
ex
i being
Nat st
(
i in dom D1 &
n = (len <*(lower_bound A)*>) + i )
;
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . mthen consider i being
Element of
NAT such that A23:
i in dom D1
and A24:
n = (len <*(lower_bound A)*>) + i
;
A25:
D1 . i = (<*(lower_bound A)*> ^ D1) . n
by A23, A24, FINSEQ_1:def 7;
consider j being
Nat such that A26:
j in dom D1
and A27:
m = (len <*(lower_bound A)*>) + j
by A6, A8, FINSEQ_1:38;
A28:
D1 . j = (<*(lower_bound A)*> ^ D1) . m
by A26, A27, FINSEQ_1:def 7;
i < j
by A7, A24, A27, XREAL_1:8;
hence
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m
by A23, A26, A25, A28, SEQM_3:def 1;
verum end;
hence
(<*(lower_bound A)*> ^ D1) . n < (<*(lower_bound A)*> ^ D1) . m
;
verum
end;
hence
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
by SEQM_3:def 1; verum