let A be non empty closed_interval Subset of REAL; for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds
x = y
let D, D1 be Division of A; ( delta D1 < min (rng (upper_volume ((chi (A,A)),D))) implies for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds
x = y )
assume A1:
delta D1 < min (rng (upper_volume ((chi (A,A)),D)))
; for x, y being Real
for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds
x = y
let x, y be Real; for i being Element of NAT st i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) holds
x = y
let i be Element of NAT ; ( i in dom D1 & x in (rng D) /\ (divset (D1,i)) & y in (rng D) /\ (divset (D1,i)) implies x = y )
assume A2:
i in dom D1
; ( not x in (rng D) /\ (divset (D1,i)) or not y in (rng D) /\ (divset (D1,i)) or x = y )
assume A3:
x in (rng D) /\ (divset (D1,i))
; ( not y in (rng D) /\ (divset (D1,i)) or x = y )
then
x in rng D
by XBOOLE_0:def 4;
then consider n being Element of NAT such that
A4:
n in dom D
and
A5:
x = D . n
by PARTFUN1:3;
assume A6:
y in (rng D) /\ (divset (D1,i))
; x = y
then
y in rng D
by XBOOLE_0:def 4;
then consider m being Element of NAT such that
A7:
m in dom D
and
A8:
y = D . m
by PARTFUN1:3;
assume A9:
x <> y
; contradiction
A10:
|.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
proof
per cases
( n < m or n > m )
by A9, A5, A8, XXREAL_0:1;
suppose
n < m
;
|.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))then A11:
n + 1
<= m
by NAT_1:13;
A12:
1
<= n + 1
by NAT_1:12;
m in Seg (len D)
by A7, FINSEQ_1:def 3;
then
m <= len D
by FINSEQ_1:1;
then
n + 1
<= len D
by A11, XXREAL_0:2;
then A13:
n + 1
in Seg (len D)
by A12, FINSEQ_1:1;
then A14:
n + 1
in dom D
by FINSEQ_1:def 3;
then
D . m >= D . (n + 1)
by A7, A11, SEQ_4:137;
then
(D . n) - (D . m) <= (D . n) - (D . (n + 1))
by XREAL_1:10;
then A15:
- ((D . n) - (D . m)) >= - ((D . n) - (D . (n + 1)))
by XREAL_1:24;
n + 1
in Seg (len (upper_volume ((chi (A,A)),D)))
by A13, INTEGRA1:def 6;
then
n + 1
in dom (upper_volume ((chi (A,A)),D))
by FINSEQ_1:def 3;
then A16:
(upper_volume ((chi (A,A)),D)) . (n + 1) in rng (upper_volume ((chi (A,A)),D))
by FUNCT_1:def 3;
n in Seg (len D)
by A4, FINSEQ_1:def 3;
then
1
<= n
by FINSEQ_1:1;
then A17:
n + 1
<> 1
by NAT_1:13;
then A18:
upper_bound (divset (D,(n + 1))) = D . (n + 1)
by A14, INTEGRA1:def 4;
- |.((D . n) - (D . m)).| <= (D . n) - (D . m)
by ABSVALUE:4;
then A19:
|.((D . n) - (D . m)).| >= - ((D . n) - (D . m))
by XREAL_1:26;
lower_bound (divset (D,(n + 1))) = D . ((n + 1) - 1)
by A14, A17, INTEGRA1:def 4;
then
vol (divset (D,(n + 1))) = (D . (n + 1)) - (D . n)
by A18, INTEGRA1:def 5;
then
(D . (n + 1)) - (D . n) = (upper_volume ((chi (A,A)),D)) . (n + 1)
by A14, INTEGRA1:20;
then
(D . (n + 1)) - (D . n) >= min (rng (upper_volume ((chi (A,A)),D)))
by A16, XXREAL_2:def 7;
then
- ((D . n) - (D . m)) >= min (rng (upper_volume ((chi (A,A)),D)))
by A15, XXREAL_0:2;
hence
|.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
by A19, XXREAL_0:2;
verum end; suppose
n > m
;
|.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))then A20:
m + 1
<= n
by NAT_1:13;
n in Seg (len D)
by A4, FINSEQ_1:def 3;
then
n <= len D
by FINSEQ_1:1;
then A21:
m + 1
<= len D
by A20, XXREAL_0:2;
A22:
1
<= m + 1
by NAT_1:12;
then A23:
m + 1
in dom D
by A21, FINSEQ_3:25;
then
D . (m + 1) <= D . n
by A4, A20, SEQ_4:137;
then A24:
(D . n) - (D . m) >= (D . (m + 1)) - (D . m)
by XREAL_1:9;
m + 1
in Seg (len D)
by A22, A21, FINSEQ_1:1;
then
m + 1
in Seg (len (upper_volume ((chi (A,A)),D)))
by INTEGRA1:def 6;
then
m + 1
in dom (upper_volume ((chi (A,A)),D))
by FINSEQ_1:def 3;
then A25:
(upper_volume ((chi (A,A)),D)) . (m + 1) in rng (upper_volume ((chi (A,A)),D))
by FUNCT_1:def 3;
m in Seg (len D)
by A7, FINSEQ_1:def 3;
then
1
<= m
by FINSEQ_1:1;
then A26:
1
< m + 1
by NAT_1:13;
then A27:
upper_bound (divset (D,(m + 1))) = D . (m + 1)
by A23, INTEGRA1:def 4;
lower_bound (divset (D,(m + 1))) = D . ((m + 1) - 1)
by A23, A26, INTEGRA1:def 4;
then
vol (divset (D,(m + 1))) = (D . (m + 1)) - (D . m)
by A27, INTEGRA1:def 5;
then
(D . (m + 1)) - (D . m) = (upper_volume ((chi (A,A)),D)) . (m + 1)
by A23, INTEGRA1:20;
then
(D . (m + 1)) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D)))
by A25, XXREAL_2:def 7;
then A28:
(D . n) - (D . m) >= min (rng (upper_volume ((chi (A,A)),D)))
by A24, XXREAL_0:2;
|.((D . n) - (D . m)).| >= (D . n) - (D . m)
by ABSVALUE:4;
hence
|.((D . n) - (D . m)).| >= min (rng (upper_volume ((chi (A,A)),D)))
by A28, XXREAL_0:2;
verum end; end;
end;
|.((D . n) - (D . m)).| <= delta D1
proof
per cases
( n < m or n > m )
by A9, A5, A8, XXREAL_0:1;
suppose A29:
n < m
;
|.((D . n) - (D . m)).| <= delta D1
i in Seg (len D1)
by A2, FINSEQ_1:def 3;
then
i in Seg (len (upper_volume ((chi (A,A)),D1)))
by INTEGRA1:def 6;
then
i in dom (upper_volume ((chi (A,A)),D1))
by FINSEQ_1:def 3;
then
(upper_volume ((chi (A,A)),D1)) . i in rng (upper_volume ((chi (A,A)),D1))
by FUNCT_1:def 3;
then
(upper_volume ((chi (A,A)),D1)) . i <= max (rng (upper_volume ((chi (A,A)),D1)))
by XXREAL_2:def 8;
then A30:
(upper_volume ((chi (A,A)),D1)) . i <= delta D1
;
D . m in divset (
D1,
i)
by A6, A8, XBOOLE_0:def 4;
then
D . m <= upper_bound (divset (D1,i))
by INTEGRA2:1;
then A31:
(D . m) - (lower_bound (divset (D1,i))) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i)))
by XREAL_1:9;
D . n in divset (
D1,
i)
by A3, A5, XBOOLE_0:def 4;
then
D . n >= lower_bound (divset (D1,i))
by INTEGRA2:1;
then
(D . m) - (D . n) <= (D . m) - (lower_bound (divset (D1,i)))
by XREAL_1:10;
then
(D . m) - (D . n) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i)))
by A31, XXREAL_0:2;
then
(D . m) - (D . n) <= vol (divset (D1,i))
by INTEGRA1:def 5;
then A32:
(D . m) - (D . n) <= (upper_volume ((chi (A,A)),D1)) . i
by A2, INTEGRA1:20;
D . n < D . m
by A4, A7, A29, SEQM_3:def 1;
then
(D . n) - (D . m) < 0
by XREAL_1:49;
then |.((D . n) - (D . m)).| =
- ((D . n) - (D . m))
by ABSVALUE:def 1
.=
(D . m) - (D . n)
;
hence
|.((D . n) - (D . m)).| <= delta D1
by A32, A30, XXREAL_0:2;
verum end; suppose A33:
n > m
;
|.((D . n) - (D . m)).| <= delta D1
i in Seg (len D1)
by A2, FINSEQ_1:def 3;
then
i in Seg (len (upper_volume ((chi (A,A)),D1)))
by INTEGRA1:def 6;
then
i in dom (upper_volume ((chi (A,A)),D1))
by FINSEQ_1:def 3;
then
(upper_volume ((chi (A,A)),D1)) . i in rng (upper_volume ((chi (A,A)),D1))
by FUNCT_1:def 3;
then
(upper_volume ((chi (A,A)),D1)) . i <= max (rng (upper_volume ((chi (A,A)),D1)))
by XXREAL_2:def 8;
then A34:
(upper_volume ((chi (A,A)),D1)) . i <= delta D1
;
D . n in divset (
D1,
i)
by A3, A5, XBOOLE_0:def 4;
then
D . n <= upper_bound (divset (D1,i))
by INTEGRA2:1;
then A35:
(D . n) - (lower_bound (divset (D1,i))) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i)))
by XREAL_1:9;
D . m in divset (
D1,
i)
by A6, A8, XBOOLE_0:def 4;
then
D . m >= lower_bound (divset (D1,i))
by INTEGRA2:1;
then
(D . n) - (D . m) <= (D . n) - (lower_bound (divset (D1,i)))
by XREAL_1:10;
then
(D . n) - (D . m) <= (upper_bound (divset (D1,i))) - (lower_bound (divset (D1,i)))
by A35, XXREAL_0:2;
then
(D . n) - (D . m) <= vol (divset (D1,i))
by INTEGRA1:def 5;
then A36:
(D . n) - (D . m) <= (upper_volume ((chi (A,A)),D1)) . i
by A2, INTEGRA1:20;
D . n > D . m
by A4, A7, A33, SEQM_3:def 1;
then
(D . n) - (D . m) > 0
by XREAL_1:50;
then
|.((D . n) - (D . m)).| = (D . n) - (D . m)
by ABSVALUE:def 1;
hence
|.((D . n) - (D . m)).| <= delta D1
by A36, A34, XXREAL_0:2;
verum end; end;
end;
hence
contradiction
by A1, A10, XXREAL_0:2; verum