let f be PartFunc of REAL,REAL; for a, b, c being Real st ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) holds
for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
let a, b, c be Real; ( ].a,c.[ c= dom f & a < b & b < c & f is_left_improper_integrable_on a,b & f is_right_improper_integrable_on b,c & ( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty ) & ( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty ) implies for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) )
assume that
A1:
].a,c.[ c= dom f
and
A2:
( a < b & b < c )
and
A3:
f is_left_improper_integrable_on a,b
and
A4:
f is_right_improper_integrable_on b,c
and
A5:
( not left_improper_integral (f,a,b) = -infty or not right_improper_integral (f,b,c) = +infty )
and
A6:
( not left_improper_integral (f,a,b) = +infty or not right_improper_integral (f,b,c) = -infty )
; for b1 being Real st a < b1 & b1 <= b holds
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
let b1 be Real; ( a < b1 & b1 <= b implies (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) )
assume A7:
( a < b1 & b1 <= b )
; (left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
( ].a,b.] c= ].a,c.[ & [.b,c.[ c= ].a,c.[ )
by A2, XXREAL_1:48, XXREAL_1:49;
then A8:
( ].a,b.] c= dom f & [.b,c.[ c= dom f )
by A1;
( [.b1,c.[ c= ].a,c.[ & [.b1,b.] c= ].a,c.[ )
by A7, A2, XXREAL_1:47, XXREAL_1:48;
then A9:
( [.b1,c.[ c= dom f & [.b1,b.] c= dom f )
by A1;
A10:
( f is_integrable_on ['b1,b'] & f | ['b1,b'] is bounded )
by A7, A3;
per cases
( f is_left_ext_Riemann_integrable_on a,b or left_improper_integral (f,a,b) = +infty or left_improper_integral (f,a,b) = -infty )
by A3, Th34;
suppose
f is_left_ext_Riemann_integrable_on a,
b
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then A11:
left_improper_integral (
f,
a,
b)
= ext_left_integral (
f,
a,
b)
by A3, Th34;
then A12:
(
f is_left_improper_integrable_on a,
b1 &
left_improper_integral (
f,
a,
b1)
= ext_left_integral (
f,
a,
b1) )
by A7, A8, A3, Lm8;
A13:
left_improper_integral (
f,
a,
b) =
(left_improper_integral (f,a,b1)) + (integral (f,b1,b))
by A7, A8, A10, A12, Lm12
.=
(ext_left_integral (f,a,b1)) + (integral (f,b1,b))
by A12, XXREAL_3:def 2
;
per cases
( f is_right_ext_Riemann_integrable_on b,c or right_improper_integral (f,b,c) = +infty or right_improper_integral (f,b,c) = -infty )
by A4, Th39;
suppose A14:
f is_right_ext_Riemann_integrable_on b,
c
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then A15:
right_improper_integral (
f,
b,
c)
= ext_right_integral (
f,
b,
c)
by A4, Th39;
then right_improper_integral (
f,
b1,
c) =
(right_improper_integral (f,b,c)) + (integral (f,b1,b))
by A7, A2, A9, A10, A4, Lm20
.=
(ext_right_integral (f,b,c)) + (integral (f,b1,b))
by A15, XXREAL_3:def 2
;
then (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) =
(ext_left_integral (f,a,b1)) + ((ext_right_integral (f,b,c)) + (integral (f,b1,b)))
by A12, XXREAL_3:def 2
.=
((ext_left_integral (f,a,b1)) + (integral (f,b1,b))) + (ext_right_integral (f,b,c))
.=
(left_improper_integral (f,a,b)) + (ext_right_integral (f,b,c))
by A13, XXREAL_3:def 2
;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A14, A4, Th39;
verum end; suppose A16:
right_improper_integral (
f,
b,
c)
= +infty
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
right_improper_integral (
f,
b1,
c)
= +infty
by A7, A2, A9, A10, A4, A16, Lm21;
then
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = +infty
by A12, XXREAL_3:def 2;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A16, A11, XXREAL_3:def 2;
verum end; suppose A17:
right_improper_integral (
f,
b,
c)
= -infty
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
right_improper_integral (
f,
b1,
c)
= -infty
by A7, A2, A9, A10, A4, A17, Lm22;
then
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = -infty
by A12, XXREAL_3:def 2;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A17, A11, XXREAL_3:def 2;
verum end; end; end; suppose A18:
left_improper_integral (
f,
a,
b)
= +infty
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))A19:
left_improper_integral (
f,
a,
b1)
= +infty
by A8, A3, A18, A7, Lm9;
per cases
( f is_right_ext_Riemann_integrable_on b,c or not f is_right_ext_Riemann_integrable_on b,c )
;
suppose
f is_right_ext_Riemann_integrable_on b,
c
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then A20:
right_improper_integral (
f,
b,
c)
= ext_right_integral (
f,
b,
c)
by A4, Th39;
then right_improper_integral (
f,
b1,
c) =
(right_improper_integral (f,b,c)) + (integral (f,b1,b))
by A7, A2, A9, A10, A4, Lm20
.=
(ext_right_integral (f,b,c)) + (integral (f,b1,b))
by A20, XXREAL_3:def 2
;
then
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = +infty
by A19, XXREAL_3:def 2;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A18, A20, XXREAL_3:def 2;
verum end; suppose
not
f is_right_ext_Riemann_integrable_on b,
c
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then
right_improper_integral (
f,
b,
c)
= +infty
by A18, A6, A4, Th39;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A18, A19, A7, A2, A9, A10, A4, Lm21;
verum end; end; end; suppose A21:
left_improper_integral (
f,
a,
b)
= -infty
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))A22:
left_improper_integral (
f,
a,
b1)
= -infty
by A8, A3, A21, A7, Lm10;
per cases
( f is_right_ext_Riemann_integrable_on b,c or not f is_right_ext_Riemann_integrable_on b,c )
;
suppose
f is_right_ext_Riemann_integrable_on b,
c
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then A23:
right_improper_integral (
f,
b,
c)
= ext_right_integral (
f,
b,
c)
by A4, Th39;
then right_improper_integral (
f,
b1,
c) =
(right_improper_integral (f,b,c)) + (integral (f,b1,b))
by A7, A2, A9, A10, A4, Lm20
.=
(ext_right_integral (f,b,c)) + (integral (f,b1,b))
by A23, XXREAL_3:def 2
;
then
(left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c)) = -infty
by A22, XXREAL_3:def 2;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A21, A23, XXREAL_3:def 2;
verum end; suppose
not
f is_right_ext_Riemann_integrable_on b,
c
;
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))then
right_improper_integral (
f,
b,
c)
= -infty
by A21, A5, A4, Th39;
hence
(left_improper_integral (f,a,b)) + (right_improper_integral (f,b,c)) = (left_improper_integral (f,a,b1)) + (right_improper_integral (f,b1,c))
by A21, A22, A7, A2, A9, A10, A4, Lm22;
verum end; end; end; end;