let f be PartFunc of REAL,REAL; for b being Real st dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) holds
for b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
let b be Real; ( dom f = REAL & f is_-infty_improper_integrable_on b & f is_+infty_improper_integrable_on b & ( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty ) & ( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty ) implies for b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) )
assume that
A1:
dom f = REAL
and
A2:
f is_-infty_improper_integrable_on b
and
A3:
f is_+infty_improper_integrable_on b
and
A4:
( not improper_integral_-infty (f,b) = -infty or not improper_integral_+infty (f,b) = +infty )
and
A5:
( not improper_integral_-infty (f,b) = +infty or not improper_integral_+infty (f,b) = -infty )
; for b1 being Real st b1 <= b holds
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
A6:
( left_closed_halfline b c= dom f & right_closed_halfline b c= dom f )
by A1;
let b1 be Real; ( b1 <= b implies (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) )
assume A7:
b1 <= b
; (improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
then A8:
( f is_integrable_on ['b1,b'] & f | ['b1,b'] is bounded )
by A2;
A9:
( right_closed_halfline b1 c= dom f & [.b1,b.] c= dom f )
by A1;
per cases
( f is_-infty_ext_Riemann_integrable_on b or improper_integral_-infty (f,b) = +infty or improper_integral_-infty (f,b) = -infty )
by A2, Th22;
suppose
f is_-infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then A10:
improper_integral_-infty (
f,
b)
= infty_ext_left_integral (
f,
b)
by A2, Th22;
then A11:
(
f is_-infty_improper_integrable_on b1 &
improper_integral_-infty (
f,
b1)
= infty_ext_left_integral (
f,
b1) )
by A1, A7, A2, Lm3;
A12:
improper_integral_-infty (
f,
b) =
(improper_integral_-infty (f,b1)) + (integral (f,b1,b))
by A7, A6, A8, A11, Lm7
.=
(infty_ext_left_integral (f,b1)) + (integral (f,b1,b))
by A11, XXREAL_3:def 2
;
per cases
( f is_+infty_ext_Riemann_integrable_on b or improper_integral_+infty (f,b) = +infty or improper_integral_+infty (f,b) = -infty )
by A3, Th27;
suppose A13:
f is_+infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then A14:
improper_integral_+infty (
f,
b)
= infty_ext_right_integral (
f,
b)
by A3, Th27;
then improper_integral_+infty (
f,
b1) =
(improper_integral_+infty (f,b)) + (integral (f,b1,b))
by A7, A9, A8, A3, Th31
.=
(infty_ext_right_integral (f,b)) + (integral (f,b1,b))
by A14, XXREAL_3:def 2
;
then (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) =
(infty_ext_left_integral (f,b1)) + ((infty_ext_right_integral (f,b)) + (integral (f,b1,b)))
by A11, XXREAL_3:def 2
.=
((infty_ext_left_integral (f,b1)) + (integral (f,b1,b))) + (infty_ext_right_integral (f,b))
.=
(improper_integral_-infty (f,b)) + (infty_ext_right_integral (f,b))
by A12, XXREAL_3:def 2
;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A13, A3, Th27;
verum end; suppose A15:
improper_integral_+infty (
f,
b)
= +infty
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
improper_integral_+infty (
f,
b1)
= +infty
by A7, A9, A8, A3, A15, Th31;
then
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = +infty
by A11, XXREAL_3:def 2;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A15, A10, XXREAL_3:def 2;
verum end; suppose A16:
improper_integral_+infty (
f,
b)
= -infty
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
improper_integral_+infty (
f,
b1)
= -infty
by A7, A9, A8, A3, A16, Th31;
then
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = -infty
by A11, XXREAL_3:def 2;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A16, A10, XXREAL_3:def 2;
verum end; end; end; suppose A17:
improper_integral_-infty (
f,
b)
= +infty
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))A18:
improper_integral_-infty (
f,
b1)
= +infty
by A1, A2, A17, A7, Lm4;
per cases
( f is_+infty_ext_Riemann_integrable_on b or not f is_+infty_ext_Riemann_integrable_on b )
;
suppose
f is_+infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then A19:
improper_integral_+infty (
f,
b)
= infty_ext_right_integral (
f,
b)
by A3, Th27;
then improper_integral_+infty (
f,
b1) =
(improper_integral_+infty (f,b)) + (integral (f,b1,b))
by A7, A9, A8, A3, Th31
.=
(infty_ext_right_integral (f,b)) + (integral (f,b1,b))
by A19, XXREAL_3:def 2
;
then
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = +infty
by A18, XXREAL_3:def 2;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A17, A19, XXREAL_3:def 2;
verum end; suppose
not
f is_+infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then
improper_integral_+infty (
f,
b)
= +infty
by A17, A5, A3, Th27;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A17, A18, A7, A9, A8, A3, Th31;
verum end; end; end; suppose A20:
improper_integral_-infty (
f,
b)
= -infty
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))A21:
improper_integral_-infty (
f,
b1)
= -infty
by A1, A2, A20, A7, Lm5;
per cases
( f is_+infty_ext_Riemann_integrable_on b or not f is_+infty_ext_Riemann_integrable_on b )
;
suppose
f is_+infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then A22:
improper_integral_+infty (
f,
b)
= infty_ext_right_integral (
f,
b)
by A3, Th27;
then improper_integral_+infty (
f,
b1) =
(improper_integral_+infty (f,b)) + (integral (f,b1,b))
by A7, A9, A8, A3, Th31
.=
(infty_ext_right_integral (f,b)) + (integral (f,b1,b))
by A22, XXREAL_3:def 2
;
then
(improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1)) = -infty
by A21, XXREAL_3:def 2;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A20, A22, XXREAL_3:def 2;
verum end; suppose
not
f is_+infty_ext_Riemann_integrable_on b
;
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))then
improper_integral_+infty (
f,
b)
= -infty
by A20, A4, A3, Th27;
hence
(improper_integral_-infty (f,b)) + (improper_integral_+infty (f,b)) = (improper_integral_-infty (f,b1)) + (improper_integral_+infty (f,b1))
by A20, A21, A7, A9, A8, A3, Th31;
verum end; end; end; end;