let A be non empty closed_interval Subset of REAL; for f being Function of A,REAL
for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
let f be Function of A,REAL; for T being DivSequence of A st f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 holds
( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
let T be DivSequence of A; ( f | A is bounded & delta T is 0 -convergent & delta T is non-zero & vol A <> 0 implies ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
assume A1:
f | A is bounded
; ( not delta T is 0 -convergent or not delta T is non-zero or not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
then A2:
for D, D1 being Division of A ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & 0 <= (upper_sum (f,D)) - (upper_sum (f,D2)) & 0 <= (upper_sum (f,D1)) - (upper_sum (f,D2)) )
by Th22;
A7:
for D, D1 being Division of A st delta D1 < min (rng (upper_volume ((chi (A,A)),D))) holds
ex D2 being Division of A st
( D <= D2 & D1 <= D2 & rng D2 = (rng D1) \/ (rng D) & (upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )
by A1, Th23;
assume A559:
( delta T is 0 -convergent & delta T is non-zero )
; ( not vol A <> 0 or ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f ) )
then A560:
delta T is convergent
by FDIFF_1:def 1;
A561:
lim (delta T) = 0
by A559, FDIFF_1:def 1;
assume A562:
vol A <> 0
; ( upper_sum (f,T) is convergent & lim (upper_sum (f,T)) = upper_integral f )
A563:
delta T is non-zero
by A559;
A564:
for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
proof
let e be
Real;
( e > 0 implies ex n being Nat st
for m being Nat st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e ) )
assume
e > 0
;
ex n being Nat st
for m being Nat st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
then consider n being
Nat such that A565:
for
m being
Nat st
n <= m holds
|.(((delta T) . m) - 0).| < e
by A560, A561, SEQ_2:def 7;
take
n
;
for m being Nat st n <= m holds
( 0 < (delta T) . m & (delta T) . m < e )
let m be
Nat;
( n <= m implies ( 0 < (delta T) . m & (delta T) . m < e ) )
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
assume
n <= m
;
( 0 < (delta T) . m & (delta T) . m < e )
then
|.(((delta T) . m) - 0).| < e
by A565;
then A566:
((delta T) . m) + |.(((delta T) . m) - 0).| < e + |.(((delta T) . m) - 0).|
by ABSVALUE:4, XREAL_1:8;
reconsider D =
T . mm as
Division of
A ;
A567:
(delta T) . m = delta (T . mm)
by Def2;
delta (T . mm) in rng (upper_volume ((chi (A,A)),(T . mm)))
by XXREAL_2:def 8;
then consider i being
Element of
NAT such that A568:
i in dom (upper_volume ((chi (A,A)),(T . mm)))
and A569:
delta (T . mm) = (upper_volume ((chi (A,A)),(T . mm))) . i
by PARTFUN1:3;
i in Seg (len (upper_volume ((chi (A,A)),(T . mm))))
by A568, FINSEQ_1:def 3;
then
i in Seg (len D)
by INTEGRA1:def 6;
then
i in dom D
by FINSEQ_1:def 3;
then A570:
delta (T . mm) = vol (divset ((T . mm),i))
by A569, INTEGRA1:20;
(delta T) . m <> 0
by A563, SEQ_1:5;
hence
(
0 < (delta T) . m &
(delta T) . m < e )
by A566, A567, A570, INTEGRA1:9, XREAL_1:6;
verum
end;
A571:
for e being Real st e > 0 holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e
proof
let e be
Real;
( e > 0 implies ex n being Nat st
for m being Nat st n <= m holds
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )
assume A572:
e > 0
;
ex n being Nat st
for m being Nat st n <= m holds
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e
then A573:
e / 2
> 0
by XREAL_1:139;
reconsider e =
e as
Real ;
A574:
rng (upper_sum_set f) is
bounded_below
by A1, INTEGRA2:35;
upper_integral f = lower_bound (rng (upper_sum_set f))
by INTEGRA1:def 14;
then consider y being
Real such that A575:
y in rng (upper_sum_set f)
and A576:
(upper_integral f) + (e / 2) > y
by A573, A574, SEQ_4:def 2;
ex
D being
Division of
A st
(
D in dom (upper_sum_set f) &
y = (upper_sum_set f) . D &
D . 1
> lower_bound A )
proof
consider D3 being
Element of
divs A such that A577:
D3 in dom (upper_sum_set f)
and A578:
y = (upper_sum_set f) . D3
by A575, PARTFUN1:3;
reconsider D3 =
D3 as
Division of
A by INTEGRA1:def 3;
A579:
len D3 in Seg (len D3)
by FINSEQ_1:3;
then
1
<= len D3
by FINSEQ_1:1;
then
1
in Seg (len D3)
by FINSEQ_1:1;
then A580:
1
in dom D3
by FINSEQ_1:def 3;
per cases
( D3 . 1 <> lower_bound A or D3 . 1 = lower_bound A )
;
suppose A582:
D3 . 1
= lower_bound A
;
ex D being Division of A st
( D in dom (upper_sum_set f) & y = (upper_sum_set f) . D & D . 1 > lower_bound A )
ex
D being
Division of
A st
(
D in dom (upper_sum_set f) &
y = (upper_sum_set f) . D &
D . 1
> lower_bound A )
proof
A583:
(upper_volume (f,D3)) . 1
= (upper_bound (rng (f | (divset (D3,1))))) * (vol (divset (D3,1)))
by A580, INTEGRA1:def 6;
vol A >= 0
by INTEGRA1:9;
then A584:
(upper_bound A) - (lower_bound A) > 0
by A562, INTEGRA1:def 5;
A585:
y =
upper_sum (
f,
D3)
by A578, INTEGRA1:def 10
.=
Sum (upper_volume (f,D3))
by INTEGRA1:def 8
.=
Sum (((upper_volume (f,D3)) | 1) ^ ((upper_volume (f,D3)) /^ 1))
by RFINSEQ:8
;
A586:
D3 . (len D3) = upper_bound A
by INTEGRA1:def 2;
len D3 in dom D3
by A579, FINSEQ_1:def 3;
then A587:
len D3 > 1
by A580, A582, A586, A584, SEQ_4:137, XREAL_1:47;
then reconsider D =
D3 /^ 1 as
increasing FinSequence of
REAL by INTEGRA1:34;
A588:
len D = (len D3) - 1
by A587, RFINSEQ:def 1;
upper_bound A > lower_bound A
by A584, XREAL_1:47;
then
len D <> 0
by A582, A588, INTEGRA1:def 2;
then reconsider D =
D as non
empty increasing FinSequence of
REAL ;
A589:
len D in dom D
by FINSEQ_5:6;
(len D) + 1
= len D3
by A588;
then A590:
D . (len D) = upper_bound A
by A586, A587, A589, RFINSEQ:def 1;
A591:
len D in Seg (len D)
by FINSEQ_1:3;
1
+ 1
<= len D3
by A587, NAT_1:13;
then
2
in dom D3
by FINSEQ_3:25;
then A592:
D3 . 1
< D3 . 2
by A580, SEQM_3:def 1;
A593:
rng D3 c= A
by INTEGRA1:def 2;
rng D c= rng D3
by FINSEQ_5:33;
then
rng D c= A
by A593;
then reconsider D =
D as
Division of
A by A590, INTEGRA1:def 2;
A594:
1
in Seg 1
by FINSEQ_1:1;
A595:
len D3 >= 1
+ 1
by A587, NAT_1:13;
then A596:
2
<= len (upper_volume (f,D3))
by INTEGRA1:def 6;
1
<= len (upper_volume (f,D3))
by A587, INTEGRA1:def 6;
then A597:
len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) =
((len (upper_volume (f,D3))) -' 2) + 1
by A596, FINSEQ_6:118
.=
((len D3) -' 2) + 1
by INTEGRA1:def 6
.=
((len D3) - 2) + 1
by A595, XREAL_1:233
.=
(len D3) - 1
;
A598:
for
i being
Nat st 1
<= i &
i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) holds
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i
proof
let i be
Nat;
( 1 <= i & i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) implies (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i )
assume that A599:
1
<= i
and A600:
i <= len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3)))))
;
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i
A601:
1
<= i + 1
by NAT_1:12;
i + 1
<= len D3
by A597, A600, XREAL_1:19;
then A602:
i + 1
in Seg (len D3)
by A601, FINSEQ_1:1;
then A603:
i + 1
in dom D3
by FINSEQ_1:def 3;
A604:
divset (
D3,
(i + 1))
= divset (
D,
i)
proof
A605:
i + 1
in dom D3
by A602, FINSEQ_1:def 3;
A606:
1
<> i + 1
by A599, NAT_1:13;
then A607:
upper_bound (divset (D3,(i + 1))) = D3 . (i + 1)
by A605, INTEGRA1:def 4;
A608:
i in dom D
by A588, A597, A599, A600, FINSEQ_3:25;
then A609:
D . i = D3 . (i + 1)
by A587, RFINSEQ:def 1;
A610:
lower_bound (divset (D3,(i + 1))) = D3 . ((i + 1) - 1)
by A606, A605, INTEGRA1:def 4;
per cases
( i = 1 or i <> 1 )
;
suppose A611:
i = 1
;
divset (D3,(i + 1)) = divset (D,i)then A612:
upper_bound (divset (D,i)) = D . i
by A608, INTEGRA1:def 4;
A613:
lower_bound (divset (D,i)) = lower_bound A
by A608, A611, INTEGRA1:def 4;
divset (
D3,
(i + 1))
= [.(lower_bound A),(D . i).]
by A582, A607, A610, A609, A611, INTEGRA1:4;
hence
divset (
D3,
(i + 1))
= divset (
D,
i)
by A613, A612, INTEGRA1:4;
verum end; suppose A614:
i <> 1
;
divset (D3,(i + 1)) = divset (D,i)then
i - 1
in dom D
by A608, INTEGRA1:7;
then A615:
D . (i - 1) =
D3 . ((i - 1) + 1)
by A587, RFINSEQ:def 1
.=
D3 . i
;
A616:
upper_bound (divset (D,i)) = D . i
by A608, A614, INTEGRA1:def 4;
lower_bound (divset (D,i)) = D . (i - 1)
by A608, A614, INTEGRA1:def 4;
then
divset (
D3,
(i + 1))
= [.(lower_bound (divset (D,i))),(upper_bound (divset (D,i))).]
by A607, A610, A609, A616, A615, INTEGRA1:4;
hence
divset (
D3,
(i + 1))
= divset (
D,
i)
by INTEGRA1:4;
verum end; end;
end;
i <= (len (upper_volume (f,D3))) - 1
by A597, A600, INTEGRA1:def 6;
then A617:
i <= ((len (upper_volume (f,D3))) - 2) + 1
;
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i =
(upper_volume (f,D3)) . ((i + 2) - 1)
by A596, A599, A617, FINSEQ_6:122
.=
(upper_volume (f,D3)) . (i + 1)
;
then A618:
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_bound (rng (f | (divset (D3,(i + 1)))))) * (vol (divset (D3,(i + 1))))
by A603, INTEGRA1:def 6;
i in Seg (len D)
by A588, A597, A599, A600, FINSEQ_1:1;
then
i in dom D
by FINSEQ_1:def 3;
hence
(mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) . i = (upper_volume (f,D)) . i
by A618, A604, INTEGRA1:def 6;
verum
end;
A619:
1
<= len (upper_volume (f,D3))
by A587, INTEGRA1:def 6;
A620:
len ((upper_volume (f,D3)) | 1) = 1
;
1
in dom (upper_volume (f,D3))
by A619, FINSEQ_3:25;
then
((upper_volume (f,D3)) | 1) . 1
= (upper_volume (f,D3)) . 1
by A594, RFINSEQ:6;
then A621:
(upper_volume (f,D3)) | 1
= <*((upper_volume (f,D3)) . 1)*>
by A620, FINSEQ_1:40;
A622: 2
-' 1 =
2
- 1
by XREAL_1:233
.=
1
;
1
<= len D
by A591, FINSEQ_1:1;
then
1
in dom D
by FINSEQ_3:25;
then A623:
D . 1 =
D3 . (1 + 1)
by A587, RFINSEQ:def 1
.=
D3 . 2
;
D in divs A
by INTEGRA1:def 3;
then A624:
D in dom (upper_sum_set f)
by FUNCT_2:def 1;
len (upper_volume (f,D3)) >= 2
by A595, INTEGRA1:def 6;
then A625:
mid (
(upper_volume (f,D3)),2,
(len (upper_volume (f,D3))))
= (upper_volume (f,D3)) /^ 1
by A622, FINSEQ_6:117;
len (mid ((upper_volume (f,D3)),2,(len (upper_volume (f,D3))))) = len (upper_volume (f,D))
by A588, A597, INTEGRA1:def 6;
then A626:
(upper_volume (f,D3)) /^ 1
= upper_volume (
f,
D)
by A625, A598, FINSEQ_1:14;
vol (divset (D3,1)) =
(upper_bound (divset (D3,1))) - (lower_bound (divset (D3,1)))
by INTEGRA1:def 5
.=
(upper_bound (divset (D3,1))) - (lower_bound A)
by A580, INTEGRA1:def 4
.=
(D3 . 1) - (lower_bound A)
by A580, INTEGRA1:def 4
.=
0
by A582
;
then y =
0 + (Sum (upper_volume (f,D)))
by A585, A621, A583, A626, RVSUM_1:76
.=
upper_sum (
f,
D)
by INTEGRA1:def 8
;
then
y = (upper_sum_set f) . D
by INTEGRA1:def 10;
hence
ex
D being
Division of
A st
(
D in dom (upper_sum_set f) &
y = (upper_sum_set f) . D &
D . 1
> lower_bound A )
by A582, A624, A623, A592;
verum
end; hence
ex
D being
Division of
A st
(
D in dom (upper_sum_set f) &
y = (upper_sum_set f) . D &
D . 1
> lower_bound A )
;
verum end; end;
end;
then consider D being
Division of
A such that
D in dom (upper_sum_set f)
and A627:
y = (upper_sum_set f) . D
and A628:
D . 1
> lower_bound A
;
deffunc H1(
Nat)
-> Element of
REAL =
In (
(vol (divset (D,$1))),
REAL);
set p =
len D;
set H =
upper_bound (rng f);
set h =
lower_bound (rng f);
consider v being
FinSequence of
REAL such that A629:
(
len v = len D & ( for
j being
Nat st
j in dom v holds
v . j = H1(
j) ) )
from FINSEQ_2:sch 1();
A630:
2
* (len D) > 0
by XREAL_1:129;
consider v1 being
non-decreasing FinSequence of
REAL such that A631:
v,
v1 are_fiberwise_equipotent
by INTEGRA2:3;
defpred S1[
Nat]
means ( $1
in dom v1 &
v1 . $1
> 0 );
A632:
dom v = Seg (len D)
by A629, FINSEQ_1:def 3;
A633:
ex
k being
Nat st
S1[
k]
proof
consider H being
Function such that
dom H = dom v
and
rng H = dom v1
and
H is
one-to-one
and A634:
v = v1 * H
by A631, CLASSES1:77;
consider k being
Element of
NAT such that A635:
k in dom D
and A636:
vol (divset (D,k)) > 0
by A562, Th2;
A637:
dom D = Seg (len D)
by FINSEQ_1:def 3;
then
H . k in dom v1
by A632, A634, A635, FUNCT_1:11;
then reconsider Hk =
H . k as
Element of
NAT ;
v . k = H1(
k)
by A629, A632, A635, A637;
then
v . k > 0
by A636;
then
S1[
Hk]
by A632, A634, A635, A637, FUNCT_1:11, FUNCT_1:12;
hence
ex
k being
Nat st
S1[
k]
;
verum
end;
consider k being
Nat such that A638:
(
S1[
k] & ( for
n being
Nat st
S1[
n] holds
k <= n ) )
from NAT_1:sch 5(A633);
A639:
(upper_bound (rng f)) - (lower_bound (rng f)) >= 0
by A1, Lm3, XREAL_1:48;
then A640:
(2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1) > 0
by A630, XREAL_1:129;
min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))))
> 0
then consider n being
Nat such that A641:
for
m being
Nat st
n <= m holds
(
0 < (delta T) . m &
(delta T) . m < min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)))) )
by A564;
take
n
;
for m being Nat st n <= m holds
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e
A642:
y = upper_sum (
f,
D)
by A627, INTEGRA1:def 10;
A643:
v1 . 1
> 0
proof
A644:
for
n1 being
Element of
NAT st
n1 in dom D holds
vol (divset (D,n1)) > 0
proof
let n1 be
Element of
NAT ;
( n1 in dom D implies vol (divset (D,n1)) > 0 )
assume A645:
n1 in dom D
;
vol (divset (D,n1)) > 0
then A646:
1
<= n1
by FINSEQ_3:25;
per cases
( n1 = 1 or n1 > 1 )
by A646, XXREAL_0:1;
suppose A647:
n1 = 1
;
vol (divset (D,n1)) > 0 then A648:
upper_bound (divset (D,n1)) = D . n1
by A645, INTEGRA1:def 4;
lower_bound (divset (D,n1)) = lower_bound A
by A645, A647, INTEGRA1:def 4;
then
vol (divset (D,n1)) = (D . n1) - (lower_bound A)
by A648, INTEGRA1:def 5;
hence
vol (divset (D,n1)) > 0
by A628, A647, XREAL_1:50;
verum end; suppose A649:
n1 > 1
;
vol (divset (D,n1)) > 0 then A650:
upper_bound (divset (D,n1)) = D . n1
by A645, INTEGRA1:def 4;
lower_bound (divset (D,n1)) = D . (n1 - 1)
by A645, A649, INTEGRA1:def 4;
then A651:
vol (divset (D,n1)) = (D . n1) - (D . (n1 - 1))
by A650, INTEGRA1:def 5;
n1 < n1 + 1
by XREAL_1:29;
then A652:
n1 - 1
< n1
by XREAL_1:19;
n1 - 1
in dom D
by A645, A649, INTEGRA1:7;
then
D . (n1 - 1) < D . n1
by A645, A652, SEQM_3:def 1;
hence
vol (divset (D,n1)) > 0
by A651, XREAL_1:50;
verum end; end;
end;
A653:
k <= len v1
by A638, FINSEQ_3:25;
1
<= k
by A638, FINSEQ_3:25;
then
1
<= len v1
by A653, XXREAL_0:2;
then
1
in dom v1
by FINSEQ_3:25;
then A654:
v1 . 1
in rng v1
by FUNCT_1:def 3;
rng v = rng v1
by A631, CLASSES1:75;
then consider n1 being
Element of
NAT such that A655:
n1 in dom v
and A656:
v1 . 1
= v . n1
by A654, PARTFUN1:3;
n1 in Seg (len D)
by A629, A655, FINSEQ_1:def 3;
then A657:
n1 in dom D
by FINSEQ_1:def 3;
v1 . 1 =
H1(
n1)
by A629, A655, A656
.=
vol (divset (D,n1))
;
hence
v1 . 1
> 0
by A644, A657;
verum
end;
A658:
v1 . k = min (rng (upper_volume ((chi (A,A)),D)))
proof
A659:
k = 1
A662:
rng v = rng v1
by A631, CLASSES1:75;
v1 . k in rng (upper_volume ((chi (A,A)),D))
proof
v1 . k in rng v
by A638, A662, FUNCT_1:def 3;
then consider k2 being
Element of
NAT such that A663:
k2 in dom v
and A664:
v1 . k = v . k2
by PARTFUN1:3;
A665:
k2 in Seg (len D)
by A629, A663, FINSEQ_1:def 3;
then A666:
k2 in dom D
by FINSEQ_1:def 3;
k2 in Seg (len (upper_volume ((chi (A,A)),D)))
by A665, INTEGRA1:def 6;
then A667:
k2 in dom (upper_volume ((chi (A,A)),D))
by FINSEQ_1:def 3;
v1 . k =
H1(
k2)
by A629, A663, A664
.=
vol (divset (D,k2))
;
then
v1 . k = (upper_volume ((chi (A,A)),D)) . k2
by A666, INTEGRA1:20;
hence
v1 . k in rng (upper_volume ((chi (A,A)),D))
by A667, FUNCT_1:def 3;
verum
end;
then A668:
v1 . k >= min (rng (upper_volume ((chi (A,A)),D)))
by XXREAL_2:def 7;
min (rng (upper_volume ((chi (A,A)),D))) in rng (upper_volume ((chi (A,A)),D))
by XXREAL_2:def 7;
then consider m being
Element of
NAT such that A669:
m in dom (upper_volume ((chi (A,A)),D))
and A670:
min (rng (upper_volume ((chi (A,A)),D))) = (upper_volume ((chi (A,A)),D)) . m
by PARTFUN1:3;
m in Seg (len (upper_volume ((chi (A,A)),D)))
by A669, FINSEQ_1:def 3;
then A671:
m in Seg (len D)
by INTEGRA1:def 6;
then
m in dom D
by FINSEQ_1:def 3;
then A672:
min (rng (upper_volume ((chi (A,A)),D))) = vol (divset (D,m))
by A670, INTEGRA1:20;
A673:
v . m =
H1(
m)
by A629, A632, A671
.=
min (rng (upper_volume ((chi (A,A)),D)))
by A672
;
m in dom v
by A629, A671, FINSEQ_1:def 3;
then
min (rng (upper_volume ((chi (A,A)),D))) in rng v
by A673, FUNCT_1:def 3;
then consider m1 being
Element of
NAT such that A674:
m1 in dom v1
and A675:
min (rng (upper_volume ((chi (A,A)),D))) = v1 . m1
by A662, PARTFUN1:3;
m1 >= 1
by A674, FINSEQ_3:25;
then
v1 . 1
<= min (rng (upper_volume ((chi (A,A)),D)))
by A638, A659, A674, A675, INTEGRA2:2;
hence
v1 . k = min (rng (upper_volume ((chi (A,A)),D)))
by A659, A668, XXREAL_0:1;
verum
end;
A676:
min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))))
<= v1 . k
by XXREAL_0:17;
set s =
upper_integral f;
set sD =
upper_sum (
f,
D);
let m be
Nat;
( n <= m implies |.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e )
reconsider mm =
m as
Element of
NAT by ORDINAL1:def 12;
reconsider D1 =
T . mm as
Division of
A ;
A677:
delta D1 = (delta T) . m
by Def2;
consider D2 being
Division of
A such that A678:
D <= D2
and
D1 <= D2
and A679:
rng D2 = (rng D1) \/ (rng D)
and
0 <= (upper_sum (f,D)) - (upper_sum (f,D2))
and
0 <= (upper_sum (f,D1)) - (upper_sum (f,D2))
by A2;
set sD1 =
upper_sum (
f,
(T . mm));
set sD2 =
upper_sum (
f,
D2);
upper_sum (
f,
D2)
<= upper_sum (
f,
D)
by A1, A678, INTEGRA1:45;
then A680:
(upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= (upper_sum (f,(T . mm))) - (upper_sum (f,D2))
by XREAL_1:10;
(((upper_sum (f,D)) + (upper_sum (f,(T . mm)))) - (upper_sum (f,(T . mm)))) - (upper_integral f) < e / 2
by A576, A642, XREAL_1:19;
then
(((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D))) - (upper_sum (f,(T . mm))) < e / 2
;
then
((upper_sum (f,(T . mm))) - (upper_integral f)) + (upper_sum (f,D)) < (upper_sum (f,(T . mm))) + (e / 2)
by XREAL_1:19;
then A681:
(upper_sum (f,(T . mm))) - (upper_integral f) < ((upper_sum (f,(T . mm))) + (e / 2)) - (upper_sum (f,D))
by XREAL_1:20;
T . mm in divs A
by INTEGRA1:def 3;
then A682:
T . m in dom (upper_sum_set f)
by FUNCT_2:def 1;
(upper_sum (f,T)) . m = upper_sum (
f,
(T . mm))
by INTEGRA2:def 2;
then
(upper_sum (f,T)) . m = (upper_sum_set f) . (T . m)
by INTEGRA1:def 10;
then
(upper_sum (f,T)) . m in rng (upper_sum_set f)
by A682, FUNCT_1:def 3;
then
lower_bound (rng (upper_sum_set f)) <= (upper_sum (f,T)) . m
by A574, SEQ_4:def 2;
then
upper_integral f <= (upper_sum (f,T)) . m
by INTEGRA1:def 14;
then A683:
((upper_sum (f,T)) . m) - (upper_integral f) >= 0
by XREAL_1:48;
(upper_bound (rng f)) - (lower_bound (rng f)) <= ((upper_bound (rng f)) - (lower_bound (rng f))) + 1
by XREAL_1:29;
then A684:
(len D) * ((upper_bound (rng f)) - (lower_bound (rng f))) <= (len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)
by XREAL_1:64;
A685:
min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))))
<= e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))
by XXREAL_0:17;
assume A686:
n <= m
;
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e
then
(delta T) . m < min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))))
by A641;
then
(delta T) . m < e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))
by A685, XXREAL_0:2;
then
((delta T) . m) * ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) < e
by A630, A639, XREAL_1:79, XREAL_1:129;
then
(((delta T) . m) * ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))) * 2
< e
;
then A687:
((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m) < e / 2
by XREAL_1:81;
(delta T) . m < min (
(v1 . k),
(e / ((2 * (len D)) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1))))
by A641, A686;
then
delta D1 < v1 . k
by A677, A676, XXREAL_0:2;
then
ex
D3 being
Division of
A st
(
D <= D3 &
D1 <= D3 &
rng D3 = (rng D1) \/ (rng D) &
(upper_sum (f,D1)) - (upper_sum (f,D3)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1) )
by A7, A658;
then A688:
(upper_sum (f,D1)) - (upper_sum (f,D2)) <= ((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * (delta D1)
by A679, Th6;
0 < (delta T) . m
by A641, A686;
then
((len D) * ((upper_bound (rng f)) - (lower_bound (rng f)))) * ((delta T) . m) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m)
by A684, XREAL_1:64;
then
(upper_sum (f,(T . mm))) - (upper_sum (f,D2)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m)
by A677, A688, XXREAL_0:2;
then
(upper_sum (f,(T . mm))) - (upper_sum (f,D)) <= ((len D) * (((upper_bound (rng f)) - (lower_bound (rng f))) + 1)) * ((delta T) . m)
by A680, XXREAL_0:2;
then
(upper_sum (f,(T . mm))) - (upper_sum (f,D)) < e / 2
by A687, XXREAL_0:2;
then
((upper_sum (f,(T . mm))) - (upper_sum (f,D))) + (e / 2) < (e / 2) + (e / 2)
by XREAL_1:6;
then
(upper_sum (f,(T . mm))) - (upper_integral f) < e
by A681, XXREAL_0:2;
then
((upper_sum (f,T)) . m) - (upper_integral f) < e
by INTEGRA2:def 2;
hence
|.(((upper_sum (f,T)) . m) - (upper_integral f)).| < e
by A683, ABSVALUE:def 1;
verum
end;
hence
upper_sum (f,T) is convergent
by SEQ_2:def 6; lim (upper_sum (f,T)) = upper_integral f
hence
lim (upper_sum (f,T)) = upper_integral f
by A571, SEQ_2:def 7; verum