let A be non empty closed_interval Subset of REAL; :: thesis: 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; :: thesis: ( vol A <> 0 & len D1 = 1 implies <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )

assume A1: vol A <> 0 ; :: thesis: ( 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 ; :: thesis: <*(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

<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL

let D1 be Division of A; :: thesis: ( vol A <> 0 & len D1 = 1 implies <*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL )

assume A1: vol A <> 0 ; :: thesis: ( 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 ; :: thesis: <*(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

hence
<*(lower_bound A)*> ^ D1 is non empty increasing FinSequence of REAL
by SEQM_3:def 1; :: thesis: verum
let n, m be Nat; :: thesis: ( 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 ; :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m

A8: not m in dom <*(lower_bound A)*>

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;

end;assume that

A5: n in dom (<*lb*> ^ D1) and

A6: m in dom (<*lb*> ^ D1) and

A7: n < m ; :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m

A8: not m in dom <*(lower_bound A)*>

proof

A10:
not (<*lb*> ^ D1) . m in rng <*(lower_bound A)*>
assume
m in dom <*(lower_bound A)*>
; :: thesis: contradiction

then m in Seg (len <*(lower_bound A)*>) by FINSEQ_1:def 3;

then m in {1} by FINSEQ_1:2, FINSEQ_1:39;

then A9: n < 1 by A7, TARSKI:def 1;

n in Seg (len (<*lb*> ^ D1)) by A5, FINSEQ_1:def 3;

hence contradiction by A9, FINSEQ_1:1; :: thesis: verum

end;then m in Seg (len <*(lower_bound A)*>) by FINSEQ_1:def 3;

then m in {1} by FINSEQ_1:2, FINSEQ_1:39;

then A9: n < 1 by A7, TARSKI:def 1;

n in Seg (len (<*lb*> ^ D1)) by A5, FINSEQ_1:def 3;

hence contradiction by A9, FINSEQ_1:1; :: thesis: verum

proof

(<*lb*> ^ D1) . m in rng (<*lb*> ^ D1)
by A6, FUNCT_1:def 3;
assume
(<*lb*> ^ D1) . m in rng <*(lower_bound A)*>
; :: thesis: 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; :: thesis: verum

end;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; :: thesis: verum

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 :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . mend;

hence
(<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m
; :: thesis: verumper 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;

end;

( i in dom D1 & n = (len <*(lower_bound A)*>) + i ) ) by A5, FINSEQ_1:25;

suppose A17:
n in dom <*(lower_bound A)*>
; :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m

then
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; :: thesis: verum

end;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; :: thesis: verum

suppose
ex i being Nat st

( i in dom D1 & n = (len <*(lower_bound A)*>) + i ) ; :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m

( i in dom D1 & n = (len <*(lower_bound A)*>) + i ) ; :: thesis: (<*lb*> ^ D1) . n < (<*lb*> ^ D1) . m

then 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; :: thesis: verum

end;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; :: thesis: verum