let f be PartFunc of REAL,REAL; for a, b, c being Real st a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & f is_right_ext_Riemann_integrable_on b,c holds
( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) )
let a, b, c be Real; ( a <= b & b < c & [.a,c.[ c= dom f & f | ['a,b'] is bounded & f is_integrable_on ['a,b'] & f is_right_ext_Riemann_integrable_on b,c implies ( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) ) )
assume that
A1:
( a <= b & b < c )
and
A2:
[.a,c.[ c= dom f
and
A3:
f | ['a,b'] is bounded
and
A4:
f is_integrable_on ['a,b']
and
A5:
f is_right_ext_Riemann_integrable_on b,c
; ( f is_right_ext_Riemann_integrable_on a,c & ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c)) )
A6:
a < c
by A1, XXREAL_0:2;
A7:
( ['a,b'] = [.a,b.] & ['b,c'] = [.b,c.] & ['a,c'] = [.a,c.] )
by A1, XXREAL_0:2, INTEGRA5:def 3;
then
( ['a,b'] c= [.a,c.[ & ['b,c'] c= ['a,c'] )
by A1, XXREAL_1:34, XXREAL_1:43;
then A8:
['a,b'] c= dom f
by A2;
A9:
for e being Real st a <= e & e < c holds
( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded )
proof
let e be
Real;
( a <= e & e < c implies ( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded ) )
assume A10:
(
a <= e &
e < c )
;
( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded )
per cases
( e <= b or b < e )
;
suppose A11:
e <= b
;
( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded )then
e in ['a,b']
by A7, A10, XXREAL_1:1;
hence
f is_integrable_on ['a,e']
by A8, A1, A3, A4, INTEGRA6:17;
f | ['a,e'] is bounded
['a,e'] = [.a,e.]
by A10, INTEGRA5:def 3;
hence
f | ['a,e'] is
bounded
by A3, A7, A11, XXREAL_1:34, RFUNCT_1:74;
verum end; suppose A12:
b < e
;
( f is_integrable_on ['a,e'] & f | ['a,e'] is bounded )then A13:
(
f is_integrable_on ['b,e'] &
f | ['b,e'] is
bounded )
by A5, A10, INTEGR10:def 1;
A14:
['a,e'] = [.a,e.]
by A1, A12, XXREAL_0:2, INTEGRA5:def 3;
then
['a,e'] c= [.a,c.[
by A10, XXREAL_1:43;
then
['a,e'] c= dom f
by A2;
hence
f is_integrable_on ['a,e']
by A1, A3, A4, A12, A13, Th1;
f | ['a,e'] is bounded
['b,e'] = [.b,e.]
by A12, INTEGRA5:def 3;
then
['a,e'] = ['a,b'] \/ ['b,e']
by A1, A7, A12, A14, XXREAL_1:165;
hence
f | ['a,e'] is
bounded
by A3, A13, RFUNCT_1:87;
verum end; end;
end;
consider I being PartFunc of REAL,REAL such that
A15:
dom I = [.b,c.[
and
A16:
for x being Real st x in dom I holds
I . x = integral (f,b,x)
and
A17:
I is_left_convergent_in c
by A5, INTEGR10:def 1;
reconsider AC = [.a,c.[ as non empty Subset of REAL by A1, XXREAL_1:3;
deffunc H1( Element of AC) -> Element of REAL = In ((integral (f,a,$1)),REAL);
consider Intf being Function of AC,REAL such that
A18:
for x being Element of AC holds Intf . x = H1(x)
from FUNCT_2:sch 4();
A19:
dom Intf = AC
by FUNCT_2:def 1;
then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5;
A20:
for x being Real st x in dom Intf holds
Intf . x = integral (f,a,x)
proof
let x be
Real;
( x in dom Intf implies Intf . x = integral (f,a,x) )
assume
x in dom Intf
;
Intf . x = integral (f,a,x)
then
Intf . x = In (
(integral (f,a,x)),
REAL)
by A18, A19;
hence
Intf . x = integral (
f,
a,
x)
;
verum
end;
A21:
for r being Real st r < c holds
ex g being Real st
( r < g & g < c & g in dom Intf )
consider G being Real such that
A24:
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom I holds
|.((I . r1) - G).| < g1 ) )
by A17, LIMFUNC2:7;
set G1 = G + (integral (f,a,b));
A25:
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 ) )
proof
let g1 be
Real;
( 0 < g1 implies ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 ) ) )
assume
0 < g1
;
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 ) )
then consider R being
Real such that A26:
R < c
and A27:
for
r1 being
Real st
R < r1 &
r1 < c &
r1 in dom I holds
|.((I . r1) - G).| < g1
by A24;
set R1 =
max (
R,
b);
take
max (
R,
b)
;
( max (R,b) < c & ( for r1 being Real st max (R,b) < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 ) )
thus
max (
R,
b)
< c
by A26, A1, XXREAL_0:29;
for r1 being Real st max (R,b) < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1
thus
for
r1 being
Real st
max (
R,
b)
< r1 &
r1 < c &
r1 in dom Intf holds
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1
verumproof
let r1 be
Real;
( max (R,b) < r1 & r1 < c & r1 in dom Intf implies |.((Intf . r1) - (G + (integral (f,a,b)))).| < g1 )
assume that A28:
(
max (
R,
b)
< r1 &
r1 < c )
and A29:
r1 in dom Intf
;
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1
(
R <= max (
R,
b) &
b <= max (
R,
b) )
by XXREAL_0:25;
then A30:
(
R < r1 &
b < r1 )
by A28, XXREAL_0:2;
then A31:
(
f is_integrable_on ['b,r1'] &
f | ['b,r1'] is
bounded )
by A5, A28, INTEGR10:def 1;
a <= r1
by A19, A29, XXREAL_1:3;
then
['a,r1'] = [.a,r1.]
by INTEGRA5:def 3;
then
['a,r1'] c= [.a,c.[
by A28, XXREAL_1:43;
then A32:
['a,r1'] c= dom f
by A2;
A33:
r1 in dom I
by A15, A28, A30, XXREAL_1:3;
Intf . r1 = integral (
f,
a,
r1)
by A20, A29;
then
(Intf . r1) - (G + (integral (f,a,b))) = ((integral (f,a,r1)) - (integral (f,a,b))) - G
;
then
(Intf . r1) - (G + (integral (f,a,b))) = (((integral (f,a,b)) + (integral (f,b,r1))) - (integral (f,a,b))) - G
by A32, A1, A3, A4, A30, A31, Th1;
then
(Intf . r1) - (G + (integral (f,a,b))) = (I . r1) - G
by A16, A28, A30, A15, XXREAL_1:3;
hence
|.((Intf . r1) - (G + (integral (f,a,b)))).| < g1
by A30, A27, A28, A33;
verum
end;
end;
hence A34:
f is_right_ext_Riemann_integrable_on a,c
by A9, A19, A20, A21, LIMFUNC2:7, INTEGR10:def 1; ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c))
A35:
Intf is_left_convergent_in c
by A25, A21, LIMFUNC2:7;
then A36:
ext_right_integral (f,a,c) = lim_left (Intf,c)
by A19, A20, A34, INTEGR10:def 3;
A37:
ext_right_integral (f,b,c) = lim_left (I,c)
by A5, A15, A16, A17, INTEGR10:def 3;
for g1 being Real st 0 < g1 holds
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 ) )
proof
let g1 be
Real;
( 0 < g1 implies ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 ) ) )
assume A38:
0 < g1
;
ex r being Real st
( r < c & ( for r1 being Real st r < r1 & r1 < c & r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 ) )
consider r being
Real such that A39:
(
r < c & ( for
r1 being
Real st
r < r1 &
r1 < c &
r1 in dom I holds
|.((I . r1) - (ext_right_integral (f,b,c))).| < g1 ) )
by A38, A37, A17, LIMFUNC2:41;
set R =
max (
b,
r);
for
r1 being
Real st
max (
b,
r)
< r1 &
r1 < c &
r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1
proof
let r1 be
Real;
( max (b,r) < r1 & r1 < c & r1 in dom Intf implies |.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 )
assume A40:
(
max (
b,
r)
< r1 &
r1 < c &
r1 in dom Intf )
;
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1
then
(
a <= r1 &
a < c )
by A1, A19, XXREAL_0:2, XXREAL_1:3;
then A41:
(
[.a,r1.] = ['a,r1'] &
[.a,c.] = ['a,c'] )
by INTEGRA5:def 3;
[.a,r1.] c= [.a,c.[
by A40, XXREAL_1:43;
then A42:
['a,r1'] c= dom f
by A41, A2;
(
b <= max (
b,
r) &
r <= max (
b,
r) )
by XXREAL_0:25;
then A43:
(
b < r1 &
r < r1 )
by A40, XXREAL_0:2;
then A44:
r1 in dom I
by A40, A15, XXREAL_1:3;
(
f is_integrable_on ['b,r1'] &
f | ['b,r1'] is
bounded )
by A40, A43, A5, INTEGR10:def 1;
then
integral (
f,
a,
r1)
= (integral (f,a,b)) + (integral (f,b,r1))
by A1, A42, A3, A4, A43, Th1;
then
Intf . r1 = (integral (f,a,b)) + (integral (f,b,r1))
by A40, A20;
then (Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c))) =
(integral (f,b,r1)) - (ext_right_integral (f,b,c))
.=
(I . r1) - (ext_right_integral (f,b,c))
by A43, A16, A40, A15, XXREAL_1:3
;
hence
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1
by A39, A40, A44, A43;
verum
end;
hence
ex
r being
Real st
(
r < c & ( for
r1 being
Real st
r < r1 &
r1 < c &
r1 in dom Intf holds
|.((Intf . r1) - ((integral (f,a,b)) + (ext_right_integral (f,b,c)))).| < g1 ) )
by A1, A39, XXREAL_0:29;
verum
end;
hence
ext_right_integral (f,a,c) = (integral (f,a,b)) + (ext_right_integral (f,b,c))
by A35, A36, LIMFUNC2:41; verum