let f, g be PartFunc of REAL,REAL; :: thesis: ( dom f = REAL & dom g = REAL & f is_improper_integrable_on_REAL & g is_improper_integrable_on_REAL & ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = -infty ) & ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = +infty ) implies ( f + g is_improper_integrable_on_REAL & improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) ) )
assume that
A1: dom f = REAL and
A2: dom g = REAL and
A3: f is_improper_integrable_on_REAL and
A4: g is_improper_integrable_on_REAL and
A5: ( not improper_integral_on_REAL f = +infty or not improper_integral_on_REAL g = -infty ) and
A6: ( not improper_integral_on_REAL f = -infty or not improper_integral_on_REAL g = +infty ) ; :: thesis: ( f + g is_improper_integrable_on_REAL & improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) )
consider c being Real such that
A7: f is_-infty_improper_integrable_on c and
A8: f is_+infty_improper_integrable_on c and
A9: ( not improper_integral_-infty (f,c) = -infty or not improper_integral_+infty (f,c) = +infty ) and
A10: ( not improper_integral_-infty (f,c) = +infty or not improper_integral_+infty (f,c) = -infty ) by A3;
consider c1 being Real such that
A11: g is_-infty_improper_integrable_on c1 and
A12: g is_+infty_improper_integrable_on c1 and
A13: ( not improper_integral_-infty (g,c1) = -infty or not improper_integral_+infty (g,c1) = +infty ) and
A14: ( not improper_integral_-infty (g,c1) = +infty or not improper_integral_+infty (g,c1) = -infty ) by A4;
A15: left_closed_halfline c c= dom g by A2;
A16: right_closed_halfline c c= dom g by A2;
A17: left_closed_halfline c1 c= dom g by A2;
A18: right_closed_halfline c1 c= dom g by A2;
A19: g is_-infty_improper_integrable_on c

proof

per cases ( c < c1 or c1 <= c ) ;

suppose c < c1 ; :: thesis: g is_-infty_improper_integrable_on c

hence g is_-infty_improper_integrable_on c by A2, A11, Th25; :: thesis: verum

end;

suppose A20: c1 <= c ; :: thesis: g is_-infty_improper_integrable_on c

then ( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A12;
hence g is_-infty_improper_integrable_on c by A20, A15, A11, Th26; :: thesis: verum

end;

end;

end;

A21: g is_+infty_improper_integrable_on c

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A22: c < c1 ; :: thesis: g is_+infty_improper_integrable_on c

( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A22, A11;
hence g is_+infty_improper_integrable_on c by A22, A16, A12, Th31; :: thesis: verum

end;

suppose c1 <= c ; :: thesis: g is_+infty_improper_integrable_on c

hence g is_+infty_improper_integrable_on c by A2, A12, Th30; :: thesis: verum

end;

end;

end;

A23: ( not improper_integral_-infty (g,c) = -infty or not improper_integral_+infty (g,c) = +infty )

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A24: c < c1 ; :: thesis: ( not improper_integral_-infty (g,c) = -infty or not improper_integral_+infty (g,c) = +infty )

then A25: ( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A11;
A26: g is_-infty_improper_integrable_on c by A24, A2, A11, Th25;
g is_+infty_improper_integrable_on c by A24, A16, A25, A12, Th31;
hence ( not improper_integral_-infty (g,c) = -infty or not improper_integral_+infty (g,c) = +infty ) by A13, A2, A17, A24, A25, A26, Th26, Th30; :: thesis: verum

end;

suppose A27: c1 <= c ; :: thesis: ( not improper_integral_-infty (g,c) = -infty or not improper_integral_+infty (g,c) = +infty )

then A28: ( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A12;
then A29: g is_-infty_improper_integrable_on c by A27, A15, A11, Th26;
g is_+infty_improper_integrable_on c by A27, A2, A12, Th30;
hence ( not improper_integral_-infty (g,c) = -infty or not improper_integral_+infty (g,c) = +infty ) by A13, A2, A18, A28, A27, A29, Th25, Th31; :: thesis: verum

end;

end;

end;

A30: ( not improper_integral_-infty (g,c) = +infty or not improper_integral_+infty (g,c) = -infty )

proof

per cases ( c < c1 or c1 <= c ) ;

suppose A31: c < c1 ; :: thesis: ( not improper_integral_-infty (g,c) = +infty or not improper_integral_+infty (g,c) = -infty )

A32: ( g | ['c,c1'] is bounded & g is_integrable_on ['c,c1'] ) by A31, A11;
A33: g is_-infty_improper_integrable_on c by A31, A2, A11, Th25;
g is_+infty_improper_integrable_on c by A31, A16, A32, A12, Th31;
hence ( not improper_integral_-infty (g,c) = +infty or not improper_integral_+infty (g,c) = -infty ) by A14, A2, A17, A31, A32, A33, Th26, Th30; :: thesis: verum

end;

suppose A34: c1 <= c ; :: thesis: ( not improper_integral_-infty (g,c) = +infty or not improper_integral_+infty (g,c) = -infty )

A35: ( g | ['c1,c'] is bounded & g is_integrable_on ['c1,c'] ) by A34, A12;
A36: g is_-infty_improper_integrable_on c by A34, A35, A15, A11, Th26;
g is_+infty_improper_integrable_on c by A34, A2, A12, Th30;
hence ( not improper_integral_-infty (g,c) = +infty or not improper_integral_+infty (g,c) = -infty ) by A14, A2, A18, A35, A34, A36, Th25, Th31; :: thesis: verum

end;

end;

end;

A37: improper_integral_on_REAL f = (improper_integral_-infty (f,c)) + (improper_integral_+infty (f,c)) by A1, A3, Th36;
A38: improper_integral_on_REAL g = (improper_integral_-infty (g,c)) + (improper_integral_+infty (g,c)) by A2, A4, Th36;
A39: ( not improper_integral_-infty (f,c) = +infty or not improper_integral_-infty (g,c) = -infty ) by A5, A37, A38, A10, A23, XXREAL_3:def 2;
A40: ( not improper_integral_-infty (f,c) = -infty or not improper_integral_-infty (g,c) = +infty ) by A6, A37, A38, A9, A30, XXREAL_3:def 2;
A41: ( not improper_integral_+infty (f,c) = +infty or not improper_integral_+infty (g,c) = -infty ) by A5, A37, A38, A9, A30, XXREAL_3:def 2;
A42: ( not improper_integral_+infty (f,c) = -infty or not improper_integral_+infty (g,c) = +infty ) by A6, A37, A38, A10, A23, XXREAL_3:def 2;
A43: f + g is_-infty_improper_integrable_on c by A7, A19, A1, A2, A39, A40, Th45;
A44: improper_integral_-infty ((f + g),c) = (improper_integral_-infty (f,c)) + (improper_integral_-infty (g,c)) by A1, A2, A7, A19, A39, A40, Th45;
A45: f + g is_+infty_improper_integrable_on c by A1, A2, A8, A21, A41, A42, Th46;
A46: improper_integral_+infty ((f + g),c) = (improper_integral_+infty (f,c)) + (improper_integral_+infty (g,c)) by A1, A2, A8, A21, A41, A42, Th46;

A47: now :: thesis: ( improper_integral_-infty ((f + g),c) = -infty implies not improper_integral_+infty ((f + g),c) = +infty )

assume A48: ( improper_integral_-infty ((f + g),c) = -infty & improper_integral_+infty ((f + g),c) = +infty ) ; :: thesis: contradiction

per cases ( ( improper_integral_-infty (f,c) = -infty & improper_integral_+infty (g,c) = +infty ) or ( improper_integral_-infty (g,c) = -infty & improper_integral_+infty (f,c) = +infty ) ) by A9, A23, A44, A46, A48, XXREAL_3:16, XXREAL_3:17;

suppose ( improper_integral_-infty (f,c) = -infty & improper_integral_+infty (g,c) = +infty ) ; :: thesis: contradiction

hence contradiction by A6, A9, A37, A38, A23, XXREAL_3:def 2; :: thesis: verum

end;

suppose ( improper_integral_-infty (g,c) = -infty & improper_integral_+infty (f,c) = +infty ) ; :: thesis: contradiction

hence contradiction by A5, A9, A37, A38, A23, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

A49: now :: thesis: ( improper_integral_-infty ((f + g),c) = +infty implies not improper_integral_+infty ((f + g),c) = -infty )

assume A50: ( improper_integral_-infty ((f + g),c) = +infty & improper_integral_+infty ((f + g),c) = -infty ) ; :: thesis: contradiction

per cases ( ( improper_integral_-infty (f,c) = +infty & improper_integral_+infty (g,c) = -infty ) or ( improper_integral_-infty (g,c) = +infty & improper_integral_+infty (f,c) = -infty ) ) by A10, A30, A46, A50, A44, XXREAL_3:16, XXREAL_3:17;

suppose ( improper_integral_-infty (f,c) = +infty & improper_integral_+infty (g,c) = -infty ) ; :: thesis: contradiction

hence contradiction by A5, A10, A37, A38, A30, XXREAL_3:def 2; :: thesis: verum

end;

suppose ( improper_integral_-infty (g,c) = +infty & improper_integral_+infty (f,c) = -infty ) ; :: thesis: contradiction

hence contradiction by A6, A10, A37, A38, A30, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

hence A51: f + g is_improper_integrable_on_REAL by A43, A45, A47; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)
dom (f + g) = (dom f) /\ (dom g) by VALUED_1:def 1;
then A52: improper_integral_on_REAL (f + g) = (improper_integral_-infty ((f + g),c)) + (improper_integral_+infty ((f + g),c)) by A1, A2, A51, Th36;

per cases ( improper_integral_-infty ((f + g),c) = +infty or improper_integral_-infty ((f + g),c) = -infty or improper_integral_-infty ((f + g),c) in REAL ) by XXREAL_0:14;

suppose A53: improper_integral_-infty ((f + g),c) = +infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then A54: improper_integral_on_REAL (f + g) = +infty by A49, A52, XXREAL_3:def 2;

per cases ( improper_integral_-infty (f,c) = +infty or improper_integral_-infty (g,c) = +infty ) by A53, A44, XXREAL_3:16;

suppose improper_integral_-infty (f,c) = +infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then improper_integral_on_REAL f = +infty by A10, A37, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A5, A54, XXREAL_3:def 2; :: thesis: verum

end;

suppose improper_integral_-infty (g,c) = +infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then improper_integral_on_REAL g = +infty by A38, A30, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A6, A54, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A55: improper_integral_-infty ((f + g),c) = -infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then A56: improper_integral_on_REAL (f + g) = -infty by A47, A52, XXREAL_3:def 2;

per cases ( improper_integral_-infty (f,c) = -infty or improper_integral_-infty (g,c) = -infty ) by A55, A44, XXREAL_3:17;

suppose improper_integral_-infty (f,c) = -infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then improper_integral_on_REAL f = -infty by A9, A37, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A6, A56, XXREAL_3:def 2; :: thesis: verum

end;

suppose improper_integral_-infty (g,c) = -infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then improper_integral_on_REAL g = -infty by A23, A38, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A5, A56, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

suppose A57: improper_integral_-infty ((f + g),c) in REAL ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then A58: ( improper_integral_-infty (f,c) in REAL & improper_integral_-infty (g,c) in REAL ) by A39, A40, A44, XXREAL_3:20;
then reconsider lf = improper_integral_-infty (f,c), lg = improper_integral_-infty (g,c) as Real ;

per cases ( improper_integral_+infty ((f + g),c) = +infty or improper_integral_+infty ((f + g),c) = -infty or improper_integral_+infty ((f + g),c) in REAL ) by XXREAL_0:14;

suppose A59: improper_integral_+infty ((f + g),c) = +infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then ( improper_integral_+infty (f,c) = +infty or improper_integral_+infty (g,c) = +infty ) by A46, XXREAL_3:16;
then ( improper_integral_on_REAL f = +infty or improper_integral_on_REAL g = +infty ) by A58, A37, A38, XXREAL_3:def 2;
then (improper_integral_on_REAL f) + (improper_integral_on_REAL g) = +infty by A5, A6, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A57, A59, A52, XXREAL_3:def 2; :: thesis: verum

end;

suppose A60: improper_integral_+infty ((f + g),c) = -infty ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then ( improper_integral_+infty (f,c) = -infty or improper_integral_+infty (g,c) = -infty ) by A46, XXREAL_3:17;
then ( improper_integral_on_REAL f = -infty or improper_integral_on_REAL g = -infty ) by A58, A37, A38, XXREAL_3:def 2;
then (improper_integral_on_REAL f) + (improper_integral_on_REAL g) = -infty by A5, A6, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A57, A60, A52, XXREAL_3:def 2; :: thesis: verum

end;

suppose improper_integral_+infty ((f + g),c) in REAL ; :: thesis: improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g)

then ( improper_integral_+infty (f,c) in REAL & improper_integral_+infty (g,c) in REAL ) by A41, A42, A46, XXREAL_3:20;
then reconsider rf = improper_integral_+infty (f,c), rg = improper_integral_+infty (g,c) as Real ;
( improper_integral_on_REAL f = lf + rf & improper_integral_on_REAL g = lg + rg ) by A37, A38, XXREAL_3:def 2;
then A61: (improper_integral_on_REAL f) + (improper_integral_on_REAL g) = (lf + rf) + (lg + rg) by XXREAL_3:def 2;
( improper_integral_-infty ((f + g),c) = lf + lg & improper_integral_+infty ((f + g),c) = rf + rg ) by A44, A46, XXREAL_3:def 2;
then improper_integral_on_REAL (f + g) = (lf + lg) + (rf + rg) by A52, XXREAL_3:def 2;
hence improper_integral_on_REAL (f + g) = (improper_integral_on_REAL f) + (improper_integral_on_REAL g) by A61; :: thesis: verum

end;

end;

end;

end;