:: INTEGR10 semantic presentation begin theorem Th1: :: INTEGR10:1 for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds ex r being Element of REAL st ( a < r & r < b & (b - r) * M < g1 ) proof let a, b, g1, M be real number ; ::_thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Element of REAL st ( a < r & r < b & (b - r) * M < g1 ) ) assume that A1: a < b and A2: 0 < g1 and A3: 0 < M ; ::_thesis: ex r being Element of REAL st ( a < r & r < b & (b - r) * M < g1 ) set r3 = max (a,(b - (g1 / M))); b - (g1 / M) < b by A2, A3, XREAL_1:44, XREAL_1:139; then max (a,(b - (g1 / M))) < b by A1, XXREAL_0:16; then consider q being real number such that A4: max (a,(b - (g1 / M))) < q and A5: q < b by XREAL_1:5; reconsider r = q as Real by XREAL_0:def_1; take r ; ::_thesis: ( a < r & r < b & (b - r) * M < g1 ) b - (g1 / M) <= max (a,(b - (g1 / M))) by XXREAL_0:25; then b - (g1 / M) < r by A4, XXREAL_0:2; then (b - (g1 / M)) - (r - (g1 / M)) < r - (r - (g1 / M)) by XREAL_1:14; then (b - r) * 1 < g1 / M ; then ( a <= max (a,(b - (g1 / M))) & (b - r) * M < g1 / 1 ) by A3, XREAL_1:111, XXREAL_0:25; hence ( a < r & r < b & (b - r) * M < g1 ) by A4, A5, XXREAL_0:2; ::_thesis: verum end; theorem Th2: :: INTEGR10:2 for a, b, g1, M being real number st a < b & 0 < g1 & 0 < M holds ex r being Element of REAL st ( a < r & r < b & (r - a) * M < g1 ) proof let a, b, g1, M be real number ; ::_thesis: ( a < b & 0 < g1 & 0 < M implies ex r being Element of REAL st ( a < r & r < b & (r - a) * M < g1 ) ) assume that A1: a < b and A2: ( 0 < g1 & 0 < M ) ; ::_thesis: ex r being Element of REAL st ( a < r & r < b & (r - a) * M < g1 ) - b < - a by A1, XREAL_1:24; then consider r1 being Real such that A3: ( - b < r1 & r1 < - a ) and A4: ((- a) - r1) * M < g1 by A2, Th1; reconsider r = - r1 as Real ; take r ; ::_thesis: ( a < r & r < b & (r - a) * M < g1 ) ( - (- b) > - r1 & - r1 > - (- a) ) by A3, XREAL_1:24; hence ( a < r & r < b & (r - a) * M < g1 ) by A4; ::_thesis: verum end; theorem :: INTEGR10:3 for b, a being Element of REAL holds (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) proof let b, a be Element of REAL ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) A1: min (a,b) <= a by XXREAL_0:17; A2: [.(min (a,b)),(max (a,b)).] c= REAL ; ( exp_R | REAL is continuous & a <= max (a,b) ) by XXREAL_0:25; then A3: exp_R . (max (a,b)) = (integral (exp_R,(min (a,b)),(max (a,b)))) + (exp_R . (min (a,b))) by A1, A2, INTEGRA7:20, INTEGRA7:27, SIN_COS:47, XXREAL_0:2; A4: ( min (a,b) = a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume A5: min (a,b) = a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then max (a,b) = b by XXREAL_0:36; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A3, A5; ::_thesis: verum end; ( min (a,b) = b implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume A6: min (a,b) = b ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then A7: max (a,b) = a by XXREAL_0:36; ( b < a implies (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ) proof assume b < a ; ::_thesis: (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) then integral (exp_R,a,b) = - (integral (exp_R,['b,a'])) by INTEGRA5:def_4; then exp_R . a = (- (integral (exp_R,a,b))) + (exp_R . b) by A1, A3, A6, A7, INTEGRA5:def_4; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) ; ::_thesis: verum end; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A1, A4, A6, XXREAL_0:1; ::_thesis: verum end; hence (exp_R . b) - (exp_R . a) = integral (exp_R,a,b) by A4, XXREAL_0:15; ::_thesis: verum end; begin definition let f be PartFunc of REAL,REAL; let a, b be Real; predf is_right_ext_Riemann_integrable_on a,b means :Def1: :: INTEGR10:def 1 ( ( for d being Real st a <= d & d < b holds ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) ); end; :: deftheorem Def1 defines is_right_ext_Riemann_integrable_on INTEGR10:def_1_:_ for f being PartFunc of REAL,REAL for a, b being Real holds ( f is_right_ext_Riemann_integrable_on a,b iff ( ( for d being Real st a <= d & d < b holds ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; predf is_left_ext_Riemann_integrable_on a,b means :Def2: :: INTEGR10:def 2 ( ( for d being Real st a < d & d <= b holds ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) ); end; :: deftheorem Def2 defines is_left_ext_Riemann_integrable_on INTEGR10:def_2_:_ for f being PartFunc of REAL,REAL for a, b being Real holds ( f is_left_ext_Riemann_integrable_on a,b iff ( ( for d being Real st a < d & d <= b holds ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; assume A1: f is_right_ext_Riemann_integrable_on a,b ; func ext_right_integral (f,a,b) -> Real means :Def3: :: INTEGR10:def 3 ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & it = lim_left (Intf,b) ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b1 = lim_left (Intf,b) ) proof consider Intf being PartFunc of REAL,REAL such that A2: ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b ) by A1, Def1; take lim_left (Intf,b) ; ::_thesis: ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) ) thus ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & lim_left (Intf,b) = lim_left (Intf,b) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b1 = lim_left (Intf,b) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b2 = lim_left (Intf,b) ) holds b1 = b2 proof let y1, y2 be Real; ::_thesis: ( ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & y1 = lim_left (Intf,b) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & y2 = lim_left (Intf,b) ) implies y1 = y2 ) assume ex Intf1 being PartFunc of REAL,REAL st ( dom Intf1 = [.a,b.[ & ( for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,a,x) ) & Intf1 is_left_convergent_in b & y1 = lim_left (Intf1,b) ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds ( not dom Intf = [.a,b.[ or ex x being Real st ( x in dom Intf & not Intf . x = integral (f,a,x) ) or not Intf is_left_convergent_in b or not y2 = lim_left (Intf,b) ) or y1 = y2 ) then consider Intf1 being PartFunc of REAL,REAL such that A3: dom Intf1 = [.a,b.[ and A4: for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,a,x) and Intf1 is_left_convergent_in b and A5: y1 = lim_left (Intf1,b) ; assume ex Intf2 being PartFunc of REAL,REAL st ( dom Intf2 = [.a,b.[ & ( for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,a,x) ) & Intf2 is_left_convergent_in b & y2 = lim_left (Intf2,b) ) ; ::_thesis: y1 = y2 then consider Intf2 being PartFunc of REAL,REAL such that A6: dom Intf2 = [.a,b.[ and A7: for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,a,x) and Intf2 is_left_convergent_in b and A8: y2 = lim_left (Intf2,b) ; now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_ Intf1_._x_=_Intf2_._x let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x ) assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x hence Intf1 . x = integral (f,a,x) by A4 .= Intf2 . x by A3, A6, A7, A9 ; ::_thesis: verum end; hence y1 = y2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def3 defines ext_right_integral INTEGR10:def_3_:_ for f being PartFunc of REAL,REAL for a, b being Real st f is_right_ext_Riemann_integrable_on a,b holds for b4 being Real holds ( b4 = ext_right_integral (f,a,b) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = [.a,b.[ & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is_left_convergent_in b & b4 = lim_left (Intf,b) ) ); definition let f be PartFunc of REAL,REAL; let a, b be Real; assume A1: f is_left_ext_Riemann_integrable_on a,b ; func ext_left_integral (f,a,b) -> Real means :Def4: :: INTEGR10:def 4 ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & it = lim_right (Intf,a) ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b1 = lim_right (Intf,a) ) proof consider Intf being PartFunc of REAL,REAL such that A2: ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a ) by A1, Def2; take lim_right (Intf,a) ; ::_thesis: ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) ) thus ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & lim_right (Intf,a) = lim_right (Intf,a) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b1 = lim_right (Intf,a) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b2 = lim_right (Intf,a) ) holds b1 = b2 proof let y1, y2 be Real; ::_thesis: ( ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & y1 = lim_right (Intf,a) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & y2 = lim_right (Intf,a) ) implies y1 = y2 ) assume ex Intf1 being PartFunc of REAL,REAL st ( dom Intf1 = ].a,b.] & ( for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,x,b) ) & Intf1 is_right_convergent_in a & y1 = lim_right (Intf1,a) ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds ( not dom Intf = ].a,b.] or ex x being Real st ( x in dom Intf & not Intf . x = integral (f,x,b) ) or not Intf is_right_convergent_in a or not y2 = lim_right (Intf,a) ) or y1 = y2 ) then consider Intf1 being PartFunc of REAL,REAL such that A3: dom Intf1 = ].a,b.] and A4: for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,x,b) and Intf1 is_right_convergent_in a and A5: y1 = lim_right (Intf1,a) ; assume ex Intf2 being PartFunc of REAL,REAL st ( dom Intf2 = ].a,b.] & ( for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,x,b) ) & Intf2 is_right_convergent_in a & y2 = lim_right (Intf2,a) ) ; ::_thesis: y1 = y2 then consider Intf2 being PartFunc of REAL,REAL such that A6: dom Intf2 = ].a,b.] and A7: for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,x,b) and Intf2 is_right_convergent_in a and A8: y2 = lim_right (Intf2,a) ; now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_ Intf1_._x_=_Intf2_._x let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x ) assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x hence Intf1 . x = integral (f,x,b) by A4 .= Intf2 . x by A3, A6, A7, A9 ; ::_thesis: verum end; hence y1 = y2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def4 defines ext_left_integral INTEGR10:def_4_:_ for f being PartFunc of REAL,REAL for a, b being Real st f is_left_ext_Riemann_integrable_on a,b holds for b4 being Real holds ( b4 = ext_left_integral (f,a,b) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = ].a,b.] & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is_right_convergent_in a & b4 = lim_right (Intf,a) ) ); definition let f be PartFunc of REAL,REAL; let a be real number ; predf is_+infty_ext_Riemann_integrable_on a means :Def5: :: INTEGR10:def 5 ( ( for b being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty ) ); end; :: deftheorem Def5 defines is_+infty_ext_Riemann_integrable_on INTEGR10:def_5_:_ for f being PartFunc of REAL,REAL for a being real number holds ( f is_+infty_ext_Riemann_integrable_on a iff ( ( for b being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty ) ) ); definition let f be PartFunc of REAL,REAL; let b be real number ; predf is_-infty_ext_Riemann_integrable_on b means :Def6: :: INTEGR10:def 6 ( ( for a being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty ) ); end; :: deftheorem Def6 defines is_-infty_ext_Riemann_integrable_on INTEGR10:def_6_:_ for f being PartFunc of REAL,REAL for b being real number holds ( f is_-infty_ext_Riemann_integrable_on b iff ( ( for a being Real st a <= b holds ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty ) ) ); definition let f be PartFunc of REAL,REAL; let a be real number ; assume A1: f is_+infty_ext_Riemann_integrable_on a ; func infty_ext_right_integral (f,a) -> Real means :Def7: :: INTEGR10:def 7 ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & it = lim_in+infty Intf ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b1 = lim_in+infty Intf ) proof consider Intf being PartFunc of REAL,REAL such that A2: ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty ) by A1, Def5; take lim_in+infty Intf ; ::_thesis: ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & lim_in+infty Intf = lim_in+infty Intf ) thus ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & lim_in+infty Intf = lim_in+infty Intf ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b1 = lim_in+infty Intf ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b2 = lim_in+infty Intf ) holds b1 = b2 proof let L1, L2 be Real; ::_thesis: ( ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & L1 = lim_in+infty Intf ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & L2 = lim_in+infty Intf ) implies L1 = L2 ) assume ex Intf1 being PartFunc of REAL,REAL st ( dom Intf1 = right_closed_halfline a & ( for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,a,x) ) & Intf1 is convergent_in+infty & L1 = lim_in+infty Intf1 ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds ( not dom Intf = right_closed_halfline a or ex x being Real st ( x in dom Intf & not Intf . x = integral (f,a,x) ) or not Intf is convergent_in+infty or not L2 = lim_in+infty Intf ) or L1 = L2 ) then consider Intf1 being PartFunc of REAL,REAL such that A3: dom Intf1 = right_closed_halfline a and A4: for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,a,x) and Intf1 is convergent_in+infty and A5: L1 = lim_in+infty Intf1 ; assume ex Intf2 being PartFunc of REAL,REAL st ( dom Intf2 = right_closed_halfline a & ( for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,a,x) ) & Intf2 is convergent_in+infty & L2 = lim_in+infty Intf2 ) ; ::_thesis: L1 = L2 then consider Intf2 being PartFunc of REAL,REAL such that A6: dom Intf2 = right_closed_halfline a and A7: for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,a,x) and Intf2 is convergent_in+infty and A8: L2 = lim_in+infty Intf2 ; now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_ Intf1_._x_=_Intf2_._x let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x ) assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x hence Intf1 . x = integral (f,a,x) by A4 .= Intf2 . x by A3, A6, A7, A9 ; ::_thesis: verum end; hence L1 = L2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def7 defines infty_ext_right_integral INTEGR10:def_7_:_ for f being PartFunc of REAL,REAL for a being real number st f is_+infty_ext_Riemann_integrable_on a holds for b3 being Real holds ( b3 = infty_ext_right_integral (f,a) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = right_closed_halfline a & ( for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) ) & Intf is convergent_in+infty & b3 = lim_in+infty Intf ) ); definition let f be PartFunc of REAL,REAL; let b be real number ; assume A1: f is_-infty_ext_Riemann_integrable_on b ; func infty_ext_left_integral (f,b) -> Real means :Def8: :: INTEGR10:def 8 ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & it = lim_in-infty Intf ); existence ex b1 being Real ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & b1 = lim_in-infty Intf ) proof consider Intf being PartFunc of REAL,REAL such that A2: ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty ) by A1, Def6; take lim_in-infty Intf ; ::_thesis: ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & lim_in-infty Intf = lim_in-infty Intf ) thus ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & lim_in-infty Intf = lim_in-infty Intf ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being Real st ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & b1 = lim_in-infty Intf ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & b2 = lim_in-infty Intf ) holds b1 = b2 proof let L1, L2 be Real; ::_thesis: ( ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & L1 = lim_in-infty Intf ) & ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & L2 = lim_in-infty Intf ) implies L1 = L2 ) assume ex Intf1 being PartFunc of REAL,REAL st ( dom Intf1 = left_closed_halfline b & ( for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,x,b) ) & Intf1 is convergent_in-infty & L1 = lim_in-infty Intf1 ) ; ::_thesis: ( for Intf being PartFunc of REAL,REAL holds ( not dom Intf = left_closed_halfline b or ex x being Real st ( x in dom Intf & not Intf . x = integral (f,x,b) ) or not Intf is convergent_in-infty or not L2 = lim_in-infty Intf ) or L1 = L2 ) then consider Intf1 being PartFunc of REAL,REAL such that A3: dom Intf1 = left_closed_halfline b and A4: for x being Real st x in dom Intf1 holds Intf1 . x = integral (f,x,b) and Intf1 is convergent_in-infty and A5: L1 = lim_in-infty Intf1 ; assume ex Intf2 being PartFunc of REAL,REAL st ( dom Intf2 = left_closed_halfline b & ( for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,x,b) ) & Intf2 is convergent_in-infty & L2 = lim_in-infty Intf2 ) ; ::_thesis: L1 = L2 then consider Intf2 being PartFunc of REAL,REAL such that A6: dom Intf2 = left_closed_halfline b and A7: for x being Real st x in dom Intf2 holds Intf2 . x = integral (f,x,b) and Intf2 is convergent_in-infty and A8: L2 = lim_in-infty Intf2 ; now__::_thesis:_for_x_being_Real_st_x_in_dom_Intf1_holds_ Intf1_._x_=_Intf2_._x let x be Real; ::_thesis: ( x in dom Intf1 implies Intf1 . x = Intf2 . x ) assume A9: x in dom Intf1 ; ::_thesis: Intf1 . x = Intf2 . x hence Intf1 . x = integral (f,x,b) by A4 .= Intf2 . x by A3, A6, A7, A9 ; ::_thesis: verum end; hence L1 = L2 by A3, A5, A6, A8, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def8 defines infty_ext_left_integral INTEGR10:def_8_:_ for f being PartFunc of REAL,REAL for b being real number st f is_-infty_ext_Riemann_integrable_on b holds for b3 being Real holds ( b3 = infty_ext_left_integral (f,b) iff ex Intf being PartFunc of REAL,REAL st ( dom Intf = left_closed_halfline b & ( for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) ) & Intf is convergent_in-infty & b3 = lim_in-infty Intf ) ); definition let f be PartFunc of REAL,REAL; attrf is infty_ext_Riemann_integrable means :: INTEGR10:def 9 ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ); end; :: deftheorem defines infty_ext_Riemann_integrable INTEGR10:def_9_:_ for f being PartFunc of REAL,REAL holds ( f is infty_ext_Riemann_integrable iff ( f is_+infty_ext_Riemann_integrable_on 0 & f is_-infty_ext_Riemann_integrable_on 0 ) ); definition let f be PartFunc of REAL,REAL; func infty_ext_integral f -> Real equals :: INTEGR10:def 10 (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)); coherence (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)) is Real ; end; :: deftheorem defines infty_ext_integral INTEGR10:def_10_:_ for f being PartFunc of REAL,REAL holds infty_ext_integral f = (infty_ext_right_integral (f,0)) + (infty_ext_left_integral (f,0)); begin theorem :: INTEGR10:4 for f, g being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b holds ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b holds ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_right_ext_Riemann_integrable_on a,b & g is_right_ext_Riemann_integrable_on a,b implies ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) ) assume that A1: a < b and A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and A3: f is_right_ext_Riemann_integrable_on a,b and A4: g is_right_ext_Riemann_integrable_on a,b ; ::_thesis: ( f + g is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) ) consider Intg being PartFunc of REAL,REAL such that A5: dom Intg = [.a,b.[ and A6: for x being Real st x in dom Intg holds Intg . x = integral (g,a,x) and A7: Intg is_left_convergent_in b and A8: ext_right_integral (g,a,b) = lim_left (Intg,b) by A4, Def3; consider Intf being PartFunc of REAL,REAL such that A9: dom Intf = [.a,b.[ and A10: for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) and A11: Intf is_left_convergent_in b and A12: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3; set Intfg = Intf + Intg; A13: ( dom (Intf + Intg) = [.a,b.[ & ( for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),a,x) ) ) proof A14: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1 .= [.a,b.[ by A9, A5 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),a,x) let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) ) assume A16: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),a,x) then A17: x < b by A15, XXREAL_1:3; then A18: [.a,x.] c= [.a,b.] by XXREAL_1:34; A19: a <= x by A15, A16, XXREAL_1:3; then A20: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A17, Def1; ['a,x'] = [.a,x.] by A19, INTEGRA5:def_3; then A21: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A2, A14, A18, XBOOLE_1:1; A22: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A4, A19, A17, Def1; thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A16, VALUED_1:def_1 .= (integral (f,a,x)) + (Intg . x) by A9, A10, A15, A16 .= (integral (f,a,x)) + (integral (g,a,x)) by A5, A6, A15, A16 .= integral ((f + g),a,x) by A19, A21, A20, A22, INTEGRA6:12 ; ::_thesis: verum end; A23: for r being Element of REAL st r < b holds ex g being Element of REAL st ( r < g & g < b & g in dom (Intf + Intg) ) proof let r be Real; ::_thesis: ( r < b implies ex g being Element of REAL st ( r < g & g < b & g in dom (Intf + Intg) ) ) assume A24: r < b ; ::_thesis: ex g being Element of REAL st ( r < g & g < b & g in dom (Intf + Intg) ) percases ( r < a or not r < a ) ; supposeA25: r < a ; ::_thesis: ex g being Element of REAL st ( r < g & g < b & g in dom (Intf + Intg) ) reconsider g = a as Real ; take g ; ::_thesis: ( r < g & g < b & g in dom (Intf + Intg) ) thus ( r < g & g < b & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:3; ::_thesis: verum end; suppose not r < a ; ::_thesis: ex g being Element of REAL st ( r < g & g < b & g in dom (Intf + Intg) ) then A26: a - a <= r - a by XREAL_1:9; reconsider g = r + ((b - r) / 2) as Real ; take g ; ::_thesis: ( r < g & g < b & g in dom (Intf + Intg) ) A27: 0 < b - r by A24, XREAL_1:50; then (b - r) / 2 < b - r by XREAL_1:216; then A28: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8; r < g by A27, XREAL_1:29, XREAL_1:215; then A29: r - (r - a) < g - 0 by A26, XREAL_1:14; 0 < (b - r) / 2 by A27, XREAL_1:215; hence ( r < g & g < b & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:8, XXREAL_1:3; ::_thesis: verum end; end; end; then A30: Intf + Intg is_left_convergent_in b by A11, A7, LIMFUNC2:45; for d being Real st a <= d & d < b holds ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) proof let d be Real; ::_thesis: ( a <= d & d < b implies ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) ) assume A31: ( a <= d & d < b ) ; ::_thesis: ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) then A32: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A33: ( ['a,d'] c= dom f & ['a,d'] c= dom g ) by A2, A32, XBOOLE_1:1; A34: ( f is_integrable_on ['a,d'] & g is_integrable_on ['a,d'] ) by A3, A4, A31, Def1; A35: ( f | ['a,d'] is bounded & g | ['a,d'] is bounded ) by A3, A4, A31, Def1; then (f + g) | (['a,d'] /\ ['a,d']) is bounded by RFUNCT_1:83; hence ( f + g is_integrable_on ['a,d'] & (f + g) | ['a,d'] is bounded ) by A33, A34, A35, INTEGRA6:11; ::_thesis: verum end; hence A36: f + g is_right_ext_Riemann_integrable_on a,b by A13, A30, Def1; ::_thesis: ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) lim_left ((Intf + Intg),b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:45; hence ext_right_integral ((f + g),a,b) = (ext_right_integral (f,a,b)) + (ext_right_integral (g,a,b)) by A13, A30, A36, Def3; ::_thesis: verum end; theorem :: INTEGR10:5 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_right_ext_Riemann_integrable_on a,b implies for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) ) assume that A1: a < b and A2: ['a,b'] c= dom f and A3: f is_right_ext_Riemann_integrable_on a,b ; ::_thesis: for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) proof let r be Real; ::_thesis: ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) consider Intf being PartFunc of REAL,REAL such that A4: dom Intf = [.a,b.[ and A5: for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) and A6: Intf is_left_convergent_in b and A7: ext_right_integral (f,a,b) = lim_left (Intf,b) by A3, Def3; set Intfg = r (#) Intf; A8: r (#) Intf is_left_convergent_in b by A6, LIMFUNC2:43; A9: ( dom (r (#) Intf) = [.a,b.[ & ( for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),a,x) ) ) proof A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; thus A11: dom (r (#) Intf) = [.a,b.[ by A4, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),a,x) let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) ) assume A12: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),a,x) then A13: a <= x by A11, XXREAL_1:3; then A14: ['a,x'] = [.a,x.] by INTEGRA5:def_3; A15: x < b by A11, A12, XXREAL_1:3; then A16: [.a,x.] c= [.a,b.] by XXREAL_1:34; A17: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A3, A13, A15, Def1; thus (r (#) Intf) . x = r * (Intf . x) by A12, VALUED_1:def_5 .= r * (integral (f,a,x)) by A4, A5, A11, A12 .= integral ((r (#) f),a,x) by A2, A13, A14, A10, A16, A17, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum end; for d being Real st a <= d & d < b holds ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) proof let d be Real; ::_thesis: ( a <= d & d < b implies ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) ) assume A18: ( a <= d & d < b ) ; ::_thesis: ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) then A19: ( ['a,d'] = [.a,d.] & [.a,d.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34; A20: ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A3, A18, Def1; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then ['a,d'] c= dom f by A2, A19, XBOOLE_1:1; hence ( r (#) f is_integrable_on ['a,d'] & (r (#) f) | ['a,d'] is bounded ) by A20, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum end; hence A21: r (#) f is_right_ext_Riemann_integrable_on a,b by A9, A8, Def1; ::_thesis: ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) lim_left ((r (#) Intf),b) = r * (ext_right_integral (f,a,b)) by A6, A7, LIMFUNC2:43; hence ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) by A9, A8, A21, Def3; ::_thesis: verum end; hence for r being Real holds ( r (#) f is_right_ext_Riemann_integrable_on a,b & ext_right_integral ((r (#) f),a,b) = r * (ext_right_integral (f,a,b)) ) ; ::_thesis: verum end; theorem :: INTEGR10:6 for f, g being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b holds ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b holds ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & ['a,b'] c= dom g & f is_left_ext_Riemann_integrable_on a,b & g is_left_ext_Riemann_integrable_on a,b implies ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) ) assume that A1: a < b and A2: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) and A3: f is_left_ext_Riemann_integrable_on a,b and A4: g is_left_ext_Riemann_integrable_on a,b ; ::_thesis: ( f + g is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) ) consider Intg being PartFunc of REAL,REAL such that A5: dom Intg = ].a,b.] and A6: for x being Real st x in dom Intg holds Intg . x = integral (g,x,b) and A7: Intg is_right_convergent_in a and A8: ext_left_integral (g,a,b) = lim_right (Intg,a) by A4, Def4; consider Intf being PartFunc of REAL,REAL such that A9: dom Intf = ].a,b.] and A10: for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) and A11: Intf is_right_convergent_in a and A12: ext_left_integral (f,a,b) = lim_right (Intf,a) by A3, Def4; set Intfg = Intf + Intg; A13: ( dom (Intf + Intg) = ].a,b.] & ( for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),x,b) ) ) proof A14: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; thus A15: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1 .= ].a,b.] by A9, A5 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),x,b) let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) ) assume A16: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),x,b) then A17: a < x by A15, XXREAL_1:2; then A18: [.x,b.] c= [.a,b.] by XXREAL_1:34; A19: x <= b by A15, A16, XXREAL_1:2; then A20: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A17, Def2; ['x,b'] = [.x,b.] by A19, INTEGRA5:def_3; then A21: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by A2, A14, A18, XBOOLE_1:1; A22: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by A4, A17, A19, Def2; thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A16, VALUED_1:def_1 .= (integral (f,x,b)) + (Intg . x) by A9, A10, A15, A16 .= (integral (f,x,b)) + (integral (g,x,b)) by A5, A6, A15, A16 .= integral ((f + g),x,b) by A19, A21, A20, A22, INTEGRA6:12 ; ::_thesis: verum end; A23: for r being Element of REAL st a < r holds ex g being Element of REAL st ( g < r & a < g & g in dom (Intf + Intg) ) proof let r be Real; ::_thesis: ( a < r implies ex g being Element of REAL st ( g < r & a < g & g in dom (Intf + Intg) ) ) assume A24: a < r ; ::_thesis: ex g being Element of REAL st ( g < r & a < g & g in dom (Intf + Intg) ) percases ( b < r or not b < r ) ; supposeA25: b < r ; ::_thesis: ex g being Element of REAL st ( g < r & a < g & g in dom (Intf + Intg) ) reconsider g = b as Real ; take g ; ::_thesis: ( g < r & a < g & g in dom (Intf + Intg) ) thus ( g < r & a < g & g in dom (Intf + Intg) ) by A1, A13, A25, XXREAL_1:2; ::_thesis: verum end; supposeA26: not b < r ; ::_thesis: ex g being Element of REAL st ( g < r & a < g & g in dom (Intf + Intg) ) reconsider g = r - ((r - a) / 2) as Real ; take g ; ::_thesis: ( g < r & a < g & g in dom (Intf + Intg) ) A27: 0 < r - a by A24, XREAL_1:50; then (r - a) / 2 < r - a by XREAL_1:216; then A28: ((r - a) / 2) + (a - ((r - a) / 2)) < (r - a) + (a - ((r - a) / 2)) by XREAL_1:8; A29: 0 < (r - a) / 2 by A27, XREAL_1:215; then r - ((r - a) / 2) < b - 0 by A26, XREAL_1:15; hence ( g < r & a < g & g in dom (Intf + Intg) ) by A13, A29, A28, XREAL_1:44, XXREAL_1:2; ::_thesis: verum end; end; end; then A30: Intf + Intg is_right_convergent_in a by A11, A7, LIMFUNC2:54; for d being Real st a < d & d <= b holds ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) proof let d be Real; ::_thesis: ( a < d & d <= b implies ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) ) assume A31: ( a < d & d <= b ) ; ::_thesis: ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) then A32: ( ['d,b'] = [.d,b.] & [.d,b.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then A33: ( ['d,b'] c= dom f & ['d,b'] c= dom g ) by A2, A32, XBOOLE_1:1; A34: ( f is_integrable_on ['d,b'] & g is_integrable_on ['d,b'] ) by A3, A4, A31, Def2; A35: ( f | ['d,b'] is bounded & g | ['d,b'] is bounded ) by A3, A4, A31, Def2; then (f + g) | (['d,b'] /\ ['d,b']) is bounded by RFUNCT_1:83; hence ( f + g is_integrable_on ['d,b'] & (f + g) | ['d,b'] is bounded ) by A33, A34, A35, INTEGRA6:11; ::_thesis: verum end; hence A36: f + g is_left_ext_Riemann_integrable_on a,b by A13, A30, Def2; ::_thesis: ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) lim_right ((Intf + Intg),a) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A11, A12, A7, A8, A23, LIMFUNC2:54; hence ext_left_integral ((f + g),a,b) = (ext_left_integral (f,a,b)) + (ext_left_integral (g,a,b)) by A13, A30, A36, Def4; ::_thesis: verum end; theorem :: INTEGR10:7 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_left_ext_Riemann_integrable_on a,b holds for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_left_ext_Riemann_integrable_on a,b implies for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) ) assume that A1: a < b and A2: ['a,b'] c= dom f and A3: f is_left_ext_Riemann_integrable_on a,b ; ::_thesis: for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) proof let r be Real; ::_thesis: ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) consider Intf being PartFunc of REAL,REAL such that A4: dom Intf = ].a,b.] and A5: for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) and A6: Intf is_right_convergent_in a and A7: ext_left_integral (f,a,b) = lim_right (Intf,a) by A3, Def4; set Intfg = r (#) Intf; A8: r (#) Intf is_right_convergent_in a by A6, LIMFUNC2:52; A9: ( dom (r (#) Intf) = ].a,b.] & ( for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),x,b) ) ) proof A10: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; thus A11: dom (r (#) Intf) = ].a,b.] by A4, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),x,b) let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) ) assume A12: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),x,b) then A13: a < x by A11, XXREAL_1:2; then A14: [.x,b.] c= [.a,b.] by XXREAL_1:34; A15: x <= b by A11, A12, XXREAL_1:2; then A16: ['x,b'] = [.x,b.] by INTEGRA5:def_3; A17: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A3, A13, A15, Def2; thus (r (#) Intf) . x = r * (Intf . x) by A12, VALUED_1:def_5 .= r * (integral (f,x,b)) by A4, A5, A11, A12 .= integral ((r (#) f),x,b) by A2, A15, A16, A10, A14, A17, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum end; for d being Real st a < d & d <= b holds ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) proof let d be Real; ::_thesis: ( a < d & d <= b implies ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) ) assume A18: ( a < d & d <= b ) ; ::_thesis: ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) then A19: ( ['d,b'] = [.d,b.] & [.d,b.] c= [.a,b.] ) by INTEGRA5:def_3, XXREAL_1:34; A20: ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A3, A18, Def2; ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; then ['d,b'] c= dom f by A2, A19, XBOOLE_1:1; hence ( r (#) f is_integrable_on ['d,b'] & (r (#) f) | ['d,b'] is bounded ) by A20, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum end; hence A21: r (#) f is_left_ext_Riemann_integrable_on a,b by A9, A8, Def2; ::_thesis: ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) lim_right ((r (#) Intf),a) = r * (ext_left_integral (f,a,b)) by A6, A7, LIMFUNC2:52; hence ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) by A9, A8, A21, Def4; ::_thesis: verum end; hence for r being Real holds ( r (#) f is_left_ext_Riemann_integrable_on a,b & ext_left_integral ((r (#) f),a,b) = r * (ext_left_integral (f,a,b)) ) ; ::_thesis: verum end; theorem Th8: :: INTEGR10:8 for f, g being PartFunc of REAL,REAL for a being real number st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a holds ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for a being real number st right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a holds ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) let a be real number ; ::_thesis: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g & f is_+infty_ext_Riemann_integrable_on a & g is_+infty_ext_Riemann_integrable_on a implies ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) ) assume that A1: ( right_closed_halfline a c= dom f & right_closed_halfline a c= dom g ) and A2: f is_+infty_ext_Riemann_integrable_on a and A3: g is_+infty_ext_Riemann_integrable_on a ; ::_thesis: ( f + g is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) ) consider Intg being PartFunc of REAL,REAL such that A4: dom Intg = right_closed_halfline a and A5: for x being Real st x in dom Intg holds Intg . x = integral (g,a,x) and A6: Intg is convergent_in+infty and A7: infty_ext_right_integral (g,a) = lim_in+infty Intg by A3, Def7; consider Intf being PartFunc of REAL,REAL such that A8: dom Intf = right_closed_halfline a and A9: for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) and A10: Intf is convergent_in+infty and A11: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7; set Intfg = Intf + Intg; A12: ( dom (Intf + Intg) = right_closed_halfline a & ( for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),a,x) ) ) proof thus A13: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1 .= right_closed_halfline a by A8, A4 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),a,x) let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),a,x) ) assume A14: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),a,x) then A15: a <= x by A13, XXREAL_1:236; then A16: ( f is_integrable_on ['a,x'] & f | ['a,x'] is bounded ) by A2, Def5; A17: [.a,x.] c= right_closed_halfline a by XXREAL_1:251; ['a,x'] = [.a,x.] by A15, INTEGRA5:def_3; then A18: ( ['a,x'] c= dom f & ['a,x'] c= dom g ) by A1, A17, XBOOLE_1:1; A19: ( g is_integrable_on ['a,x'] & g | ['a,x'] is bounded ) by A3, A15, Def5; thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def_1 .= (integral (f,a,x)) + (Intg . x) by A8, A9, A13, A14 .= (integral (f,a,x)) + (integral (g,a,x)) by A4, A5, A13, A14 .= integral ((f + g),a,x) by A15, A18, A16, A19, INTEGRA6:12 ; ::_thesis: verum end; A20: for r being Element of REAL ex g being Element of REAL st ( r < g & g in dom (Intf + Intg) ) proof let r be Real; ::_thesis: ex g being Element of REAL st ( r < g & g in dom (Intf + Intg) ) percases ( r < a or not r < a ) ; supposeA21: r < a ; ::_thesis: ex g being Element of REAL st ( r < g & g in dom (Intf + Intg) ) reconsider g = a as Real by XREAL_0:def_1; take g ; ::_thesis: ( r < g & g in dom (Intf + Intg) ) thus ( r < g & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:236; ::_thesis: verum end; supposeA22: not r < a ; ::_thesis: ex g being Element of REAL st ( r < g & g in dom (Intf + Intg) ) reconsider g = r + 1 as Real ; take g ; ::_thesis: ( r < g & g in dom (Intf + Intg) ) A23: r + 0 < r + 1 by XREAL_1:8; then a <= g by A22, XXREAL_0:2; hence ( r < g & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:236; ::_thesis: verum end; end; end; then A24: Intf + Intg is convergent_in+infty by A10, A6, LIMFUNC1:82; for b being Real st a <= b holds ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) proof let b be Real; ::_thesis: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) ) A25: [.a,b.] c= right_closed_halfline a by XXREAL_1:251; assume A26: a <= b ; ::_thesis: ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) then A27: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] ) by A2, A3, Def5; ['a,b'] = [.a,b.] by A26, INTEGRA5:def_3; then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25, XBOOLE_1:1; A29: ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A2, A3, A26, Def5; then (f + g) | (['a,b'] /\ ['a,b']) is bounded by RFUNCT_1:83; hence ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by A28, A27, A29, INTEGRA6:11; ::_thesis: verum end; hence A30: f + g is_+infty_ext_Riemann_integrable_on a by A12, A24, Def5; ::_thesis: infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) lim_in+infty (Intf + Intg) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A10, A11, A6, A7, A20, LIMFUNC1:82; hence infty_ext_right_integral ((f + g),a) = (infty_ext_right_integral (f,a)) + (infty_ext_right_integral (g,a)) by A12, A24, A30, Def7; ::_thesis: verum end; theorem Th9: :: INTEGR10:9 for f being PartFunc of REAL,REAL for a being real number st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for a being real number st right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a holds for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) let a be real number ; ::_thesis: ( right_closed_halfline a c= dom f & f is_+infty_ext_Riemann_integrable_on a implies for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) ) assume that A1: right_closed_halfline a c= dom f and A2: f is_+infty_ext_Riemann_integrable_on a ; ::_thesis: for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) proof let r be Real; ::_thesis: ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) consider Intf being PartFunc of REAL,REAL such that A3: dom Intf = right_closed_halfline a and A4: for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) and A5: Intf is convergent_in+infty and A6: infty_ext_right_integral (f,a) = lim_in+infty Intf by A2, Def7; set Intfg = r (#) Intf; A7: r (#) Intf is convergent_in+infty by A5, LIMFUNC1:80; A8: ( dom (r (#) Intf) = right_closed_halfline a & ( for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),a,x) ) ) proof thus A9: dom (r (#) Intf) = right_closed_halfline a by A3, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),a,x) let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),a,x) ) assume A10: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),a,x) then A11: a <= x by A9, XXREAL_1:236; then A12: ( ['a,x'] = [.a,x.] & f is_integrable_on ['a,x'] ) by A2, Def5, INTEGRA5:def_3; A13: ( [.a,x.] c= right_closed_halfline a & f | ['a,x'] is bounded ) by A2, A11, Def5, XXREAL_1:251; thus (r (#) Intf) . x = r * (Intf . x) by A10, VALUED_1:def_5 .= r * (integral (f,a,x)) by A3, A4, A9, A10 .= integral ((r (#) f),a,x) by A1, A11, A12, A13, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum end; for b being Real st a <= b holds ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) proof let b be Real; ::_thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) ) A14: [.a,b.] c= right_closed_halfline a by XXREAL_1:251; assume A15: a <= b ; ::_thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) then A16: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2, Def5; ['a,b'] = [.a,b.] by A15, INTEGRA5:def_3; then ['a,b'] c= dom f by A1, A14, XBOOLE_1:1; hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by A16, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum end; hence A17: r (#) f is_+infty_ext_Riemann_integrable_on a by A8, A7, Def5; ::_thesis: infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) lim_in+infty (r (#) Intf) = r * (infty_ext_right_integral (f,a)) by A5, A6, LIMFUNC1:80; hence infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) by A8, A7, A17, Def7; ::_thesis: verum end; hence for r being Real holds ( r (#) f is_+infty_ext_Riemann_integrable_on a & infty_ext_right_integral ((r (#) f),a) = r * (infty_ext_right_integral (f,a)) ) ; ::_thesis: verum end; theorem :: INTEGR10:10 for f, g being PartFunc of REAL,REAL for b being real number st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b holds ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for b being real number st left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b holds ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) let b be real number ; ::_thesis: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g & f is_-infty_ext_Riemann_integrable_on b & g is_-infty_ext_Riemann_integrable_on b implies ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) ) assume that A1: ( left_closed_halfline b c= dom f & left_closed_halfline b c= dom g ) and A2: f is_-infty_ext_Riemann_integrable_on b and A3: g is_-infty_ext_Riemann_integrable_on b ; ::_thesis: ( f + g is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) ) consider Intg being PartFunc of REAL,REAL such that A4: dom Intg = left_closed_halfline b and A5: for x being Real st x in dom Intg holds Intg . x = integral (g,x,b) and A6: Intg is convergent_in-infty and A7: infty_ext_left_integral (g,b) = lim_in-infty Intg by A3, Def8; consider Intf being PartFunc of REAL,REAL such that A8: dom Intf = left_closed_halfline b and A9: for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) and A10: Intf is convergent_in-infty and A11: infty_ext_left_integral (f,b) = lim_in-infty Intf by A2, Def8; set Intfg = Intf + Intg; A12: ( dom (Intf + Intg) = left_closed_halfline b & ( for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),x,b) ) ) proof thus A13: dom (Intf + Intg) = (dom Intf) /\ (dom Intg) by VALUED_1:def_1 .= left_closed_halfline b by A8, A4 ; ::_thesis: for x being Real st x in dom (Intf + Intg) holds (Intf + Intg) . x = integral ((f + g),x,b) let x be Real; ::_thesis: ( x in dom (Intf + Intg) implies (Intf + Intg) . x = integral ((f + g),x,b) ) assume A14: x in dom (Intf + Intg) ; ::_thesis: (Intf + Intg) . x = integral ((f + g),x,b) then A15: x <= b by A13, XXREAL_1:234; then A16: ( f is_integrable_on ['x,b'] & f | ['x,b'] is bounded ) by A2, Def6; A17: [.x,b.] c= left_closed_halfline b by XXREAL_1:265; ['x,b'] = [.x,b.] by A15, INTEGRA5:def_3; then A18: ( ['x,b'] c= dom f & ['x,b'] c= dom g ) by A1, A17, XBOOLE_1:1; A19: ( g is_integrable_on ['x,b'] & g | ['x,b'] is bounded ) by A3, A15, Def6; thus (Intf + Intg) . x = (Intf . x) + (Intg . x) by A14, VALUED_1:def_1 .= (integral (f,x,b)) + (Intg . x) by A8, A9, A13, A14 .= (integral (f,x,b)) + (integral (g,x,b)) by A4, A5, A13, A14 .= integral ((f + g),x,b) by A15, A18, A16, A19, INTEGRA6:12 ; ::_thesis: verum end; A20: for r being Element of REAL ex g being Element of REAL st ( g < r & g in dom (Intf + Intg) ) proof let r be Real; ::_thesis: ex g being Element of REAL st ( g < r & g in dom (Intf + Intg) ) percases ( b < r or not b < r ) ; supposeA21: b < r ; ::_thesis: ex g being Element of REAL st ( g < r & g in dom (Intf + Intg) ) reconsider g = b as Real by XREAL_0:def_1; take g ; ::_thesis: ( g < r & g in dom (Intf + Intg) ) thus ( g < r & g in dom (Intf + Intg) ) by A12, A21, XXREAL_1:234; ::_thesis: verum end; supposeA22: not b < r ; ::_thesis: ex g being Element of REAL st ( g < r & g in dom (Intf + Intg) ) reconsider g = r - 1 as Real ; take g ; ::_thesis: ( g < r & g in dom (Intf + Intg) ) A23: r - 1 < r - 0 by XREAL_1:15; then g <= b by A22, XXREAL_0:2; hence ( g < r & g in dom (Intf + Intg) ) by A12, A23, XXREAL_1:234; ::_thesis: verum end; end; end; then A24: Intf + Intg is convergent_in-infty by A10, A6, LIMFUNC1:91; for a being Real st a <= b holds ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) proof let a be Real; ::_thesis: ( a <= b implies ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) ) A25: [.a,b.] c= left_closed_halfline b by XXREAL_1:265; assume A26: a <= b ; ::_thesis: ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) then A27: ( f is_integrable_on ['a,b'] & g is_integrable_on ['a,b'] ) by A2, A3, Def6; ['a,b'] = [.a,b.] by A26, INTEGRA5:def_3; then A28: ( ['a,b'] c= dom f & ['a,b'] c= dom g ) by A1, A25, XBOOLE_1:1; A29: ( f | ['a,b'] is bounded & g | ['a,b'] is bounded ) by A2, A3, A26, Def6; then (f + g) | (['a,b'] /\ ['a,b']) is bounded by RFUNCT_1:83; hence ( f + g is_integrable_on ['a,b'] & (f + g) | ['a,b'] is bounded ) by A28, A27, A29, INTEGRA6:11; ::_thesis: verum end; hence A30: f + g is_-infty_ext_Riemann_integrable_on b by A12, A24, Def6; ::_thesis: infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) lim_in-infty (Intf + Intg) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) by A10, A11, A6, A7, A20, LIMFUNC1:91; hence infty_ext_left_integral ((f + g),b) = (infty_ext_left_integral (f,b)) + (infty_ext_left_integral (g,b)) by A12, A24, A30, Def8; ::_thesis: verum end; theorem :: INTEGR10:11 for f being PartFunc of REAL,REAL for b being real number st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b holds for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for b being real number st left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b holds for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) let b be real number ; ::_thesis: ( left_closed_halfline b c= dom f & f is_-infty_ext_Riemann_integrable_on b implies for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) ) assume that A1: left_closed_halfline b c= dom f and A2: f is_-infty_ext_Riemann_integrable_on b ; ::_thesis: for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) proof let r be Real; ::_thesis: ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) consider Intf being PartFunc of REAL,REAL such that A3: dom Intf = left_closed_halfline b and A4: for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) and A5: Intf is convergent_in-infty and A6: infty_ext_left_integral (f,b) = lim_in-infty Intf by A2, Def8; set Intfg = r (#) Intf; A7: r (#) Intf is convergent_in-infty by A5, LIMFUNC1:89; A8: ( dom (r (#) Intf) = left_closed_halfline b & ( for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),x,b) ) ) proof thus A9: dom (r (#) Intf) = left_closed_halfline b by A3, VALUED_1:def_5; ::_thesis: for x being Real st x in dom (r (#) Intf) holds (r (#) Intf) . x = integral ((r (#) f),x,b) let x be Real; ::_thesis: ( x in dom (r (#) Intf) implies (r (#) Intf) . x = integral ((r (#) f),x,b) ) assume A10: x in dom (r (#) Intf) ; ::_thesis: (r (#) Intf) . x = integral ((r (#) f),x,b) then A11: x <= b by A9, XXREAL_1:234; then A12: ( ['x,b'] = [.x,b.] & f is_integrable_on ['x,b'] ) by A2, Def6, INTEGRA5:def_3; A13: ( [.x,b.] c= left_closed_halfline b & f | ['x,b'] is bounded ) by A2, A11, Def6, XXREAL_1:265; thus (r (#) Intf) . x = r * (Intf . x) by A10, VALUED_1:def_5 .= r * (integral (f,x,b)) by A3, A4, A9, A10 .= integral ((r (#) f),x,b) by A1, A11, A12, A13, INTEGRA6:10, XBOOLE_1:1 ; ::_thesis: verum end; for a being Real st a <= b holds ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) proof let a be Real; ::_thesis: ( a <= b implies ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) ) A14: [.a,b.] c= left_closed_halfline b by XXREAL_1:265; assume A15: a <= b ; ::_thesis: ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) then A16: ( f is_integrable_on ['a,b'] & f | ['a,b'] is bounded ) by A2, Def6; ['a,b'] = [.a,b.] by A15, INTEGRA5:def_3; then ['a,b'] c= dom f by A1, A14, XBOOLE_1:1; hence ( r (#) f is_integrable_on ['a,b'] & (r (#) f) | ['a,b'] is bounded ) by A16, INTEGRA6:9, RFUNCT_1:80; ::_thesis: verum end; hence A17: r (#) f is_-infty_ext_Riemann_integrable_on b by A8, A7, Def6; ::_thesis: infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) lim_in-infty (r (#) Intf) = r * (infty_ext_left_integral (f,b)) by A5, A6, LIMFUNC1:89; hence infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) by A8, A7, A17, Def8; ::_thesis: verum end; hence for r being Real holds ( r (#) f is_-infty_ext_Riemann_integrable_on b & infty_ext_left_integral ((r (#) f),b) = r * (infty_ext_left_integral (f,b)) ) ; ::_thesis: verum end; theorem :: INTEGR10:12 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_right_integral (f,a,b) = integral (f,a,b) proof let f be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_right_integral (f,a,b) = integral (f,a,b) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ext_right_integral (f,a,b) = integral (f,a,b) ) assume that A1: a < b and A2: ['a,b'] c= dom f and A3: f is_integrable_on ['a,b'] and A4: f | ['a,b'] is bounded ; ::_thesis: ext_right_integral (f,a,b) = integral (f,a,b) reconsider AB = [.a,b.[ as non empty Subset of REAL by A1, XXREAL_1:3; deffunc H1( Element of AB) -> Element of REAL = integral (f,a,\$1); consider Intf being Function of AB,REAL such that A5: for x being Element of AB holds Intf . x = H1(x) from FUNCT_2:sch_4(); A6: dom Intf = AB by FUNCT_2:def_1; then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5; consider M0 being real number such that A7: for x being set st x in ['a,b'] /\ (dom f) holds abs (f . x) <= M0 by A4, RFUNCT_1:73; reconsider M = M0 + 1 as Real ; A8: for x being Real st x in ['a,b'] holds abs (f . x) < M proof A9: ['a,b'] /\ (dom f) = ['a,b'] by A2, XBOOLE_1:28; let x be Real; ::_thesis: ( x in ['a,b'] implies abs (f . x) < M ) assume x in ['a,b'] ; ::_thesis: abs (f . x) < M hence abs (f . x) < M by A7, A9, XREAL_1:39; ::_thesis: verum end; a in { r where r is Real : ( a <= r & r <= b ) } by A1; then a in [.a,b.] by RCOMP_1:def_1; then a in ['a,b'] by A1, INTEGRA5:def_3; then abs (f . a) < M by A8; then A10: 0 < M by COMPLEX1:46; A11: for g1 being Real st 0 < g1 holds ex r being Real st ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) proof let g1 be Real; ::_thesis: ( 0 < g1 implies ex r being Real st ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) ) assume 0 < g1 ; ::_thesis: ex r being Real st ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) then consider r being Real such that A12: a < r and A13: r < b and A14: (b - r) * M < g1 by A1, A10, Th1; take r ; ::_thesis: ( r < b & ( for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) thus r < b by A13; ::_thesis: for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 now__::_thesis:_for_r1_being_Real_st_r_<_r1_&_r1_<_b_&_r1_in_dom_Intf_holds_ abs_((Intf_._r1)_-_(integral_(f,a,b)))_<_g1 let r1 be Real; ::_thesis: ( r < r1 & r1 < b & r1 in dom Intf implies abs ((Intf . r1) - (integral (f,a,b))) < g1 ) assume that A15: r < r1 and A16: r1 < b and A17: r1 in dom Intf ; ::_thesis: abs ((Intf . r1) - (integral (f,a,b))) < g1 A18: Intf . r1 = integral (f,a,r1) by A5, A6, A17; A19: a <= r1 by A12, A15, XXREAL_0:2; then r1 in [.a,b.] by A16, XXREAL_1:1; then A20: r1 in ['a,b'] by A1, INTEGRA5:def_3; b - r1 < b - r by A15, XREAL_1:15; then A21: M * (b - r1) < M * (b - r) by A10, XREAL_1:68; A22: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; [.r1,b.] = ['r1,b'] by A16, INTEGRA5:def_3; then ['r1,b'] c= ['a,b'] by A22, A19, XXREAL_1:34; then A23: for x being real number st x in ['r1,b'] holds abs (f . x) <= M by A8; b in ['a,b'] by A1, A22, XXREAL_1:1; then abs (integral (f,r1,b)) <= M * (b - r1) by A1, A2, A3, A4, A16, A20, A23, INTEGRA6:23; then A24: abs (integral (f,r1,b)) < M * (b - r) by A21, XXREAL_0:2; abs ((Intf . r1) - (integral (f,a,b))) = abs ((integral (f,a,b)) - (Intf . r1)) by COMPLEX1:60 .= abs (((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,a,r1))) by A1, A2, A3, A4, A18, A20, INTEGRA6:17 .= abs (integral (f,r1,b)) ; hence abs ((Intf . r1) - (integral (f,a,b))) < g1 by A14, A24, XXREAL_0:2; ::_thesis: verum end; hence for r1 being Real st r < r1 & r1 < b & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ; ::_thesis: verum end; A25: for x being Real st x in dom Intf holds Intf . x = integral (f,a,x) by A5, A6; for r being Real st r < b holds ex g being Real st ( r < g & g < b & g in dom Intf ) proof let r be Element of REAL ; ::_thesis: ( r < b implies ex g being Real st ( r < g & g < b & g in dom Intf ) ) assume A26: r < b ; ::_thesis: ex g being Real st ( r < g & g < b & g in dom Intf ) percases ( r < a or not r < a ) ; supposeA27: r < a ; ::_thesis: ex g being Real st ( r < g & g < b & g in dom Intf ) reconsider g = a as Real ; take g ; ::_thesis: ( r < g & g < b & g in dom Intf ) thus ( r < g & g < b & g in dom Intf ) by A1, A6, A27, XXREAL_1:3; ::_thesis: verum end; suppose not r < a ; ::_thesis: ex g being Real st ( r < g & g < b & g in dom Intf ) then A28: a - a <= r - a by XREAL_1:9; reconsider g = r + ((b - r) / 2) as Real ; take g ; ::_thesis: ( r < g & g < b & g in dom Intf ) A29: 0 < b - r by A26, XREAL_1:50; then (b - r) / 2 < b - r by XREAL_1:216; then A30: ((b - r) / 2) + r < (b - r) + r by XREAL_1:8; r < g by A29, XREAL_1:29, XREAL_1:215; then A31: r - (r - a) < g - 0 by A28, XREAL_1:14; 0 < (b - r) / 2 by A29, XREAL_1:215; hence ( r < g & g < b & g in dom Intf ) by A6, A31, A30, XREAL_1:8, XXREAL_1:3; ::_thesis: verum end; end; end; then A32: Intf is_left_convergent_in b by A11, LIMFUNC2:7; then A33: integral (f,a,b) = lim_left (Intf,b) by A11, LIMFUNC2:41; for d being Real st a <= d & d < b holds ( f is_integrable_on ['a,d'] & f | ['a,d'] is bounded ) by A2, A3, A4, INTEGRA6:18; then f is_right_ext_Riemann_integrable_on a,b by A6, A25, A32, Def1; hence ext_right_integral (f,a,b) = integral (f,a,b) by A6, A25, A32, A33, Def3; ::_thesis: verum end; theorem :: INTEGR10:13 for f being PartFunc of REAL,REAL for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_left_integral (f,a,b) = integral (f,a,b) proof let f be PartFunc of REAL,REAL; ::_thesis: for a, b being Real st a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded holds ext_left_integral (f,a,b) = integral (f,a,b) let a, b be Real; ::_thesis: ( a < b & ['a,b'] c= dom f & f is_integrable_on ['a,b'] & f | ['a,b'] is bounded implies ext_left_integral (f,a,b) = integral (f,a,b) ) assume that A1: a < b and A2: ['a,b'] c= dom f and A3: f is_integrable_on ['a,b'] and A4: f | ['a,b'] is bounded ; ::_thesis: ext_left_integral (f,a,b) = integral (f,a,b) reconsider AB = ].a,b.] as non empty Subset of REAL by A1, XXREAL_1:2; deffunc H1( Element of AB) -> Element of REAL = integral (f,\$1,b); consider Intf being Function of AB,REAL such that A5: for x being Element of AB holds Intf . x = H1(x) from FUNCT_2:sch_4(); A6: dom Intf = AB by FUNCT_2:def_1; then reconsider Intf = Intf as PartFunc of REAL,REAL by RELSET_1:5; consider M0 being real number such that A7: for x being set st x in ['a,b'] /\ (dom f) holds abs (f . x) <= M0 by A4, RFUNCT_1:73; reconsider M = M0 + 1 as Real ; A8: for x being Real st x in ['a,b'] holds abs (f . x) < M proof A9: ['a,b'] /\ (dom f) = ['a,b'] by A2, XBOOLE_1:28; let x be Real; ::_thesis: ( x in ['a,b'] implies abs (f . x) < M ) assume x in ['a,b'] ; ::_thesis: abs (f . x) < M hence abs (f . x) < M by A7, A9, XREAL_1:39; ::_thesis: verum end; a in { r where r is Real : ( a <= r & r <= b ) } by A1; then a in [.a,b.] by RCOMP_1:def_1; then a in ['a,b'] by A1, INTEGRA5:def_3; then abs (f . a) < M by A8; then A10: 0 < M by COMPLEX1:46; A11: for g1 being Real st 0 < g1 holds ex r being Real st ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) proof let g1 be Real; ::_thesis: ( 0 < g1 implies ex r being Real st ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) ) assume 0 < g1 ; ::_thesis: ex r being Real st ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) then consider r being Real such that A12: a < r and A13: r < b and A14: (r - a) * M < g1 by A1, A10, Th2; take r ; ::_thesis: ( a < r & ( for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ) ) thus a < r by A12; ::_thesis: for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 now__::_thesis:_for_r1_being_Real_st_a_<_r1_&_r1_<_r_&_r1_in_dom_Intf_holds_ abs_((Intf_._r1)_-_(integral_(f,a,b)))_<_g1 let r1 be Real; ::_thesis: ( a < r1 & r1 < r & r1 in dom Intf implies abs ((Intf . r1) - (integral (f,a,b))) < g1 ) assume that A15: a < r1 and A16: r1 < r and A17: r1 in dom Intf ; ::_thesis: abs ((Intf . r1) - (integral (f,a,b))) < g1 A18: Intf . r1 = integral (f,r1,b) by A5, A6, A17; r1 - a < r - a by A16, XREAL_1:14; then A19: M * (r1 - a) < M * (r - a) by A10, XREAL_1:68; A20: ['a,b'] = [.a,b.] by A1, INTEGRA5:def_3; A21: r1 <= b by A13, A16, XXREAL_0:2; then A22: r1 in ['a,b'] by A15, A20, XXREAL_1:1; [.a,r1.] = ['a,r1'] by A15, INTEGRA5:def_3; then ['a,r1'] c= ['a,b'] by A20, A21, XXREAL_1:34; then A23: for x being real number st x in ['a,r1'] holds abs (f . x) <= M by A8; a in ['a,b'] by A1, A20, XXREAL_1:1; then abs (integral (f,a,r1)) <= M * (r1 - a) by A1, A2, A3, A4, A15, A22, A23, INTEGRA6:23; then A24: abs (integral (f,a,r1)) < M * (r - a) by A19, XXREAL_0:2; abs ((Intf . r1) - (integral (f,a,b))) = abs ((integral (f,a,b)) - (Intf . r1)) by COMPLEX1:60 .= abs (((integral (f,a,r1)) + (integral (f,r1,b))) - (integral (f,r1,b))) by A1, A2, A3, A4, A18, A22, INTEGRA6:17 .= abs (integral (f,a,r1)) ; hence abs ((Intf . r1) - (integral (f,a,b))) < g1 by A14, A24, XXREAL_0:2; ::_thesis: verum end; hence for r1 being Real st r1 < r & a < r1 & r1 in dom Intf holds abs ((Intf . r1) - (integral (f,a,b))) < g1 ; ::_thesis: verum end; A25: for x being Real st x in dom Intf holds Intf . x = integral (f,x,b) by A5, A6; for r being Real st a < r holds ex g being Real st ( g < r & a < g & g in dom Intf ) proof let r be Element of REAL ; ::_thesis: ( a < r implies ex g being Real st ( g < r & a < g & g in dom Intf ) ) assume A26: a < r ; ::_thesis: ex g being Real st ( g < r & a < g & g in dom Intf ) percases ( b < r or not b < r ) ; supposeA27: b < r ; ::_thesis: ex g being Real st ( g < r & a < g & g in dom Intf ) reconsider g = b as Real ; take g ; ::_thesis: ( g < r & a < g & g in dom Intf ) g in ].a,b.] by A1, XXREAL_1:2; hence ( g < r & a < g & g in dom Intf ) by A1, A27, FUNCT_2:def_1; ::_thesis: verum end; supposeA28: not b < r ; ::_thesis: ex g being Real st ( g < r & a < g & g in dom Intf ) reconsider g = a + ((r - a) / 2) as Real ; take g ; ::_thesis: ( g < r & a < g & g in dom Intf ) A29: 0 < r - a by A26, XREAL_1:50; then A30: a < g by XREAL_1:29, XREAL_1:215; (r - a) / 2 < r - a by A29, XREAL_1:216; then A31: ((r - a) / 2) + a < (r - a) + a by XREAL_1:8; then g < b by A28, XXREAL_0:2; hence ( g < r & a < g & g in dom Intf ) by A6, A30, A31, XXREAL_1:2; ::_thesis: verum end; end; end; then A32: Intf is_right_convergent_in a by A11, LIMFUNC2:10; then A33: integral (f,a,b) = lim_right (Intf,a) by A11, LIMFUNC2:42; for d being Real st a < d & d <= b holds ( f is_integrable_on ['d,b'] & f | ['d,b'] is bounded ) by A2, A3, A4, INTEGRA6:18; then f is_left_ext_Riemann_integrable_on a,b by A6, A25, A32, Def2; hence ext_left_integral (f,a,b) = integral (f,a,b) by A6, A25, A32, A33, Def4; ::_thesis: verum end; begin definition let s be real number ; func exp*- s -> Function of REAL,REAL means :: INTEGR10:def 11 for t being Real holds it . t = exp_R . (- (s * t)); existence ex b1 being Function of REAL,REAL st for t being Real holds b1 . t = exp_R . (- (s * t)) proof deffunc H1( Real) -> Element of REAL = exp_R . (- (s * \$1)); consider g being Function of REAL,REAL such that A1: for x being Element of REAL holds g . x = H1(x) from FUNCT_2:sch_4(); take g ; ::_thesis: for t being Real holds g . t = exp_R . (- (s * t)) thus for t being Real holds g . t = exp_R . (- (s * t)) by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of REAL,REAL st ( for t being Real holds b1 . t = exp_R . (- (s * t)) ) & ( for t being Real holds b2 . t = exp_R . (- (s * t)) ) holds b1 = b2 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for t being Real holds f1 . t = exp_R . (- (s * t)) ) & ( for t being Real holds f2 . t = exp_R . (- (s * t)) ) implies f1 = f2 ) assume that A2: for d being Real holds f1 . d = exp_R . (- (s * d)) and A3: for d being Real holds f2 . d = exp_R . (- (s * d)) ; ::_thesis: f1 = f2 for d being Element of REAL holds f1 . d = f2 . d proof let d be Element of REAL ; ::_thesis: f1 . d = f2 . d thus f1 . d = exp_R . (- (s * d)) by A2 .= f2 . d by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem defines exp*- INTEGR10:def_11_:_ for s being real number for b2 being Function of REAL,REAL holds ( b2 = exp*- s iff for t being Real holds b2 . t = exp_R . (- (s * t)) ); definition let f be PartFunc of REAL,REAL; func One-sided_Laplace_transform f -> PartFunc of REAL,REAL means :Def12: :: INTEGR10:def 12 ( dom it = right_open_halfline 0 & ( for s being Real st s in dom it holds it . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ); existence ex b1 being PartFunc of REAL,REAL st ( dom b1 = right_open_halfline 0 & ( for s being Real st s in dom b1 holds b1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) proof defpred S1[ Element of REAL , Element of REAL ] means ( \$1 in right_open_halfline 0 & \$2 = infty_ext_right_integral ((f (#) (exp*- \$1)),0) ); consider g being PartFunc of REAL,REAL such that A1: ( ( for d being Element of REAL holds ( d in dom g iff ex c being Element of REAL st S1[d,c] ) ) & ( for d being Element of REAL st d in dom g holds S1[d,g /. d] ) ) from PARTFUN2:sch_1(); A2: dom g = right_open_halfline 0 proof let s1 be real number ; :: according to MEMBERED:def_15 ::_thesis: ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) ) reconsider s = s1 as Real by XREAL_0:def_1; ( s in right_open_halfline 0 implies s in dom g ) proof assume s in right_open_halfline 0 ; ::_thesis: s in dom g then ex y being Element of REAL st ( s in right_open_halfline 0 & y = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ; hence s in dom g by A1; ::_thesis: verum end; hence ( ( not s1 in dom g or s1 in right_open_halfline 0 ) & ( not s1 in right_open_halfline 0 or s1 in dom g ) ) by A1; ::_thesis: verum end; take g ; ::_thesis: ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) for s being Real st s in dom g holds g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) proof let s be Real; ::_thesis: ( s in dom g implies g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) assume A3: s in dom g ; ::_thesis: g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) then g /. s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A1; hence g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A3, PARTFUN1:def_6; ::_thesis: verum end; hence ( dom g = right_open_halfline 0 & ( for s being Real st s in dom g holds g . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) by A2; ::_thesis: verum end; uniqueness for b1, b2 being PartFunc of REAL,REAL st dom b1 = right_open_halfline 0 & ( for s being Real st s in dom b1 holds b1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom b2 = right_open_halfline 0 & ( for s being Real st s in dom b2 holds b2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) holds b1 = b2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( dom f1 = right_open_halfline 0 & ( for s being Real st s in dom f1 holds f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) & dom f2 = right_open_halfline 0 & ( for s being Real st s in dom f2 holds f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) implies f1 = f2 ) assume that A4: dom f1 = right_open_halfline 0 and A5: for s being Real st s in dom f1 holds f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; ::_thesis: ( not dom f2 = right_open_halfline 0 or ex s being Real st ( s in dom f2 & not f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) or f1 = f2 ) assume that A6: dom f2 = right_open_halfline 0 and A7: for s being Real st s in dom f2 holds f2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ; ::_thesis: f1 = f2 for s being Element of REAL st s in dom f1 holds f1 . s = f2 . s proof let s be Element of REAL ; ::_thesis: ( s in dom f1 implies f1 . s = f2 . s ) assume A8: s in dom f1 ; ::_thesis: f1 . s = f2 . s f1 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) by A5, A8; hence f1 . s = f2 . s by A4, A6, A7, A8; ::_thesis: verum end; hence f1 = f2 by A4, A6, PARTFUN1:5; ::_thesis: verum end; end; :: deftheorem Def12 defines One-sided_Laplace_transform INTEGR10:def_12_:_ for f, b2 being PartFunc of REAL,REAL holds ( b2 = One-sided_Laplace_transform f iff ( dom b2 = right_open_halfline 0 & ( for s being Real st s in dom b2 holds b2 . s = infty_ext_right_integral ((f (#) (exp*- s)),0) ) ) ); begin theorem :: INTEGR10:14 for f, g being PartFunc of REAL,REAL st dom f = right_closed_halfline 0 & dom g = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds ( ( for s being Real st s in right_open_halfline 0 holds (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) proof let f, g be PartFunc of REAL,REAL; ::_thesis: ( dom f = right_closed_halfline 0 & dom g = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) implies ( ( for s being Real st s in right_open_halfline 0 holds (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) ) assume that A1: dom f = right_closed_halfline 0 and A2: dom g = right_closed_halfline 0 and A3: ( ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & ( for s being Real st s in right_open_halfline 0 holds g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) ) ; ::_thesis: ( ( for s being Real st s in right_open_halfline 0 holds (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) set Intg = One-sided_Laplace_transform g; set Intf = One-sided_Laplace_transform f; set F = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g); A4: dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) = (dom (One-sided_Laplace_transform f)) /\ (dom (One-sided_Laplace_transform g)) by VALUED_1:def_1 .= (right_open_halfline 0) /\ (dom (One-sided_Laplace_transform g)) by Def12 .= (right_open_halfline 0) /\ (right_open_halfline 0) by Def12 .= right_open_halfline 0 ; A5: for s being Real st s in right_open_halfline 0 holds ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) proof let s be Real; ::_thesis: ( s in right_open_halfline 0 implies ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) ) A6: (f + g) (#) (exp*- s) = (f (#) (exp*- s)) + (g (#) (exp*- s)) by RFUNCT_1:10; A7: dom (g (#) (exp*- s)) = (dom g) /\ (dom (exp*- s)) by VALUED_1:def_4 .= (right_closed_halfline 0) /\ REAL by A2, FUNCT_2:def_1 .= right_closed_halfline 0 by XBOOLE_1:28 ; assume s in right_open_halfline 0 ; ::_thesis: ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) then A8: ( f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & g (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) by A3; dom (f (#) (exp*- s)) = (dom f) /\ (dom (exp*- s)) by VALUED_1:def_4 .= (right_closed_halfline 0) /\ REAL by A1, FUNCT_2:def_1 .= right_closed_halfline 0 by XBOOLE_1:28 ; hence ( (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) ) by A8, A6, A7, Th8; ::_thesis: verum end; for s being Real st s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) holds ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0) proof let s be Real; ::_thesis: ( s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) implies ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0) ) assume A9: s in dom ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) ; ::_thesis: ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s = infty_ext_right_integral (((f + g) (#) (exp*- s)),0) then A10: s in dom (One-sided_Laplace_transform f) by A4, Def12; A11: s in dom (One-sided_Laplace_transform g) by A4, A9, Def12; thus infty_ext_right_integral (((f + g) (#) (exp*- s)),0) = (infty_ext_right_integral ((f (#) (exp*- s)),0)) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) by A5, A4, A9 .= ((One-sided_Laplace_transform f) . s) + (infty_ext_right_integral ((g (#) (exp*- s)),0)) by A10, Def12 .= ((One-sided_Laplace_transform f) . s) + ((One-sided_Laplace_transform g) . s) by A11, Def12 .= ((One-sided_Laplace_transform f) + (One-sided_Laplace_transform g)) . s by A9, VALUED_1:def_1 ; ::_thesis: verum end; hence ( ( for s being Real st s in right_open_halfline 0 holds (f + g) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (f + g) = (One-sided_Laplace_transform f) + (One-sided_Laplace_transform g) ) by A5, A4, Def12; ::_thesis: verum end; theorem :: INTEGR10:15 for f being PartFunc of REAL,REAL for a being Real st dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) proof let f be PartFunc of REAL,REAL; ::_thesis: for a being Real st dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) holds ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) let a be Real; ::_thesis: ( dom f = right_closed_halfline 0 & ( for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) implies ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) ) assume that A1: dom f = right_closed_halfline 0 and A2: for s being Real st s in right_open_halfline 0 holds f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ; ::_thesis: ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) set Intf = One-sided_Laplace_transform f; set F = a (#) (One-sided_Laplace_transform f); A3: dom (a (#) (One-sided_Laplace_transform f)) = dom (One-sided_Laplace_transform f) by VALUED_1:def_5 .= right_open_halfline 0 by Def12 ; A4: for s being Real st s in right_open_halfline 0 holds ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) proof let s be Real; ::_thesis: ( s in right_open_halfline 0 implies ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) ) A5: (a (#) f) (#) (exp*- s) = a (#) (f (#) (exp*- s)) by RFUNCT_1:12; assume s in right_open_halfline 0 ; ::_thesis: ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) then A6: f (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 by A2; dom (f (#) (exp*- s)) = (dom f) /\ (dom (exp*- s)) by VALUED_1:def_4 .= (right_closed_halfline 0) /\ REAL by A1, FUNCT_2:def_1 .= right_closed_halfline 0 by XBOOLE_1:28 ; hence ( (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 & infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) ) by A6, A5, Th9; ::_thesis: verum end; for s being Real st s in dom (a (#) (One-sided_Laplace_transform f)) holds (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) proof let s be Real; ::_thesis: ( s in dom (a (#) (One-sided_Laplace_transform f)) implies (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) ) assume A7: s in dom (a (#) (One-sided_Laplace_transform f)) ; ::_thesis: (a (#) (One-sided_Laplace_transform f)) . s = infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) then A8: s in dom (One-sided_Laplace_transform f) by A3, Def12; thus infty_ext_right_integral (((a (#) f) (#) (exp*- s)),0) = a * (infty_ext_right_integral ((f (#) (exp*- s)),0)) by A4, A3, A7 .= a * ((One-sided_Laplace_transform f) . s) by A8, Def12 .= (a (#) (One-sided_Laplace_transform f)) . s by VALUED_1:6 ; ::_thesis: verum end; hence ( ( for s being Real st s in right_open_halfline 0 holds (a (#) f) (#) (exp*- s) is_+infty_ext_Riemann_integrable_on 0 ) & One-sided_Laplace_transform (a (#) f) = a (#) (One-sided_Laplace_transform f) ) by A4, A3, Def12; ::_thesis: verum end;