let I be non empty closed_interval Subset of REAL; for D being Division of I
for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
let D be Division of I; for fc being Function of I,REAL st fc = chi (I,I) holds
( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
let fc be Function of I,REAL; ( fc = chi (I,I) implies ( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) ) )
assume A1:
fc = chi (I,I)
; ( 0 <= min (rng (upper_volume (fc,D))) & ( 0 = min (rng (upper_volume (fc,D))) implies divset (D,1) = [.(D . 1),(D . 1).] ) & ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) ) )
consider i0 being Nat such that
A2:
i0 in dom D
and
A3:
min (rng (upper_volume (fc,D))) = (upper_volume (fc,D)) . i0
by Th43;
min (rng (upper_volume (fc,D))) = vol (divset (D,i0))
by A1, A2, A3, INTEGRA1:20;
hence
0 <= min (rng (upper_volume (fc,D)))
by INTEGRA1:9; ( 0 = min (rng (upper_volume (fc,D))) iff divset (D,1) = [.(D . 1),(D . 1).] )
thus
( 0 = min (rng (upper_volume (fc,D))) iff divset (D,1) = [.(D . 1),(D . 1).] )
verumproof
hereby ( divset (D,1) = [.(D . 1),(D . 1).] implies 0 = min (rng (upper_volume (fc,D))) )
assume
0 = min (rng (upper_volume (fc,D)))
;
divset (D,1) = [.(D . 1),(D . 1).]then A4:
vol (divset (D,i0)) = 0
by A3, A1, A2, INTEGRA1:20;
rng D <> {}
;
then
1
in dom D
by FINSEQ_3:32;
then
D . 1
in I
by INTEGRA1:6;
then
D . 1
in [.(lower_bound I),(upper_bound I).]
by INTEGRA1:4;
then A5:
lower_bound I <= D . 1
by XXREAL_1:1;
now divset (D,1) = [.(D . 1),(D . 1).]
( 1
<= i0 &
i0 <= len D )
by A2, FINSEQ_3:25;
per cases then
( i0 = 1 or 1 < i0 )
by XXREAL_0:1;
suppose A6:
1
< i0
;
divset (D,1) = [.(D . 1),(D . 1).]then A8:
D . (i0 - 1) < D . i0
by VALUED_0:def 13;
divset (
D,
i0)
= [.(D . (i0 - 1)),(D . i0).]
by A6, A2, COUSIN:50;
then
(
lower_bound (divset (D,i0)) = D . (i0 - 1) &
upper_bound (divset (D,i0)) = D . i0 )
by A8, JORDAN5A:19;
then
vol (divset (D,i0)) = (D . i0) - (D . (i0 - 1))
by INTEGRA1:def 5;
hence
divset (
D,1)
= [.(D . 1),(D . 1).]
by A4, A7, VALUED_0:def 13;
verum end; end; end; hence
divset (
D,1)
= [.(D . 1),(D . 1).]
;
verum
end;
assume A9:
divset (
D,1)
= [.(D . 1),(D . 1).]
;
0 = min (rng (upper_volume (fc,D)))
A10:
vol (divset (D,1)) =
(upper_bound (divset (D,1))) - (lower_bound (divset (D,1)))
by INTEGRA1:def 5
.=
(D . 1) - (lower_bound (divset (D,1)))
by A9, JORDAN5A:19
.=
(D . 1) - (D . 1)
by A9, JORDAN5A:19
.=
0
;
rng D <> {}
;
then A11:
1
in dom D
by FINSEQ_3:32;
then A12:
(upper_volume (fc,D)) . 1
= 0
by A1, A10, INTEGRA1:20;
1
in Seg (len D)
by A11, FINSEQ_1:def 3;
then
1
in Seg (len (upper_volume (fc,D)))
by INTEGRA1:def 6;
then A13:
1
in dom (upper_volume (fc,D))
by FINSEQ_1:def 3;
hence
0 = min (rng (upper_volume (fc,D)))
by A13, A12, Th45;
verum
end;