let A be non empty 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 )
reconsider lb = lower_bound A as Element of REAL by XREAL_0:def 1;
set MD1 = <*lb*> ^ D1;
A2:
vol A >= 0
by INTEGRA1:9;
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 5;
then A4:
lower_bound A < D1 . 1
by XREAL_1:47;
for n, m being Nat st n in dom (<*lb*> ^ D1) & m in dom (<*lb*> ^ D1) & n < m holds
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m
proof
let n,
m be
Nat;
( n in dom (<*lb*> ^ D1) & m in dom (<*lb*> ^ D1) & n < m implies (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m )
assume that A5:
n in dom (<*lb*> ^ D1)
and A6:
m in dom (<*lb*> ^ D1)
and A7:
n < m
;
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m
A8:
not
m in dom <*(lower_bound A)*>
A10:
not
(<*lb*> ^ D1) . m in rng <*(lower_bound A)*>
proof
assume
(<*lb*> ^ D1) . m in rng <*(lower_bound A)*>
;
contradiction
then
(<*lb*> ^ D1) . m in {(lower_bound A)}
by FINSEQ_1:38;
then A11:
(<*lb*> ^ D1) . m = lower_bound A
by TARSKI:def 1;
rng D1 <> {}
;
then A12:
1
in dom D1
by FINSEQ_3:32;
consider n being
Nat such that A13:
n in dom D1
and A14:
m = (len <*(lower_bound A)*>) + n
by A6, A8, FINSEQ_1:25;
n in Seg (len D1)
by A13, FINSEQ_1:def 3;
then A15:
1
<= n
by FINSEQ_1:1;
D1 . n = (<*lb*> ^ D1) . m
by A13, A14, FINSEQ_1:def 7;
hence
contradiction
by A3, A11, A13, A15, A12, SEQ_4:137, XREAL_1:47;
verum
end;
(<*lb*> ^ D1) . m in rng (<*lb*> ^ D1)
by A6, FUNCT_1:def 3;
then
(<*lb*> ^ D1) . m in (rng <*(lower_bound A)*>) \/ (rng D1)
by FINSEQ_1:31;
then A16:
(<*lb*> ^ D1) . m in rng D1
by A10, XBOOLE_0:def 3;
now (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . mper 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:25;
suppose A17:
n in dom <*(lower_bound A)*>
;
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . mthen
n in Seg (len <*(lower_bound A)*>)
by FINSEQ_1:def 3;
then
n in {1}
by FINSEQ_1:2, FINSEQ_1:39;
then A18:
n = 1
by TARSKI:def 1;
A19:
(<*lb*> ^ 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:32;
consider k being
Element of
NAT such that A21:
k in dom D1
and A22:
(<*lb*> ^ D1) . m = D1 . k
by A16, PARTFUN1:3;
1
<= k
by A21, FINSEQ_3:25;
then
D1 . 1
<= (<*lb*> ^ D1) . m
by A21, A22, A20, SEQ_4:137;
hence
(<*lb*> ^ D1) . n < (<*lb*> ^ 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 )
;
(<*lb*> ^ D1) . n < (<*lb*> ^ 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 = (<*lb*> ^ 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:25;
A28:
D1 . j = (<*lb*> ^ D1) . m
by A26, A27, FINSEQ_1:def 7;
i < j
by A7, A24, A27, XREAL_1:6;
hence
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m
by A23, A26, A25, A28, SEQM_3:def 1;
verum end;
hence
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m
;
verum
end;
hence
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
by SEQM_3:def 1; verum