:: INTEGRA8 semantic presentation begin Lm1: sin (PI / 4) > 0 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then PI / 4 < PI / 1 by XREAL_1:76; then A2: PI / 4 < PI + ((2 * PI) * 0) ; 0 / 4 < PI / 4 by A1, XREAL_1:74; hence sin (PI / 4) > 0 by A2, SIN_COS6:11; ::_thesis: verum end; Lm2: sin (- (PI / 4)) < 0 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then 0 / 4 < PI / 4 by XREAL_1:74; then A2: (PI / 4) * (- 1) < 0 * (- 1) by XREAL_1:69; PI / 4 < PI / 1 by A1, XREAL_1:76; then A3: PI * (- 1) < (PI / 4) * (- 1) by XREAL_1:69; for r being Real st PI + ((2 * PI) * (- 1)) < r & r < (2 * PI) + ((2 * PI) * (- 1)) holds sin r < 0 by SIN_COS6:12; hence sin (- (PI / 4)) < 0 by A2, A3; ::_thesis: verum end; theorem Th1: :: INTEGRA8:1 for x being Real for n being Element of NAT holds sin (x + ((2 * n) * PI)) = sin x proof let x be Real; ::_thesis: for n being Element of NAT holds sin (x + ((2 * n) * PI)) = sin x let n be Element of NAT ; ::_thesis: sin (x + ((2 * n) * PI)) = sin x sin . x = sin . (((2 * PI) * n) + x) by SIN_COS2:10; hence sin (x + ((2 * n) * PI)) = sin x ; ::_thesis: verum end; theorem Th2: :: INTEGRA8:2 for x being Real for n being Element of NAT holds sin (x + (((2 * n) + 1) * PI)) = - (sin x) proof let x be Real; ::_thesis: for n being Element of NAT holds sin (x + (((2 * n) + 1) * PI)) = - (sin x) let n be Element of NAT ; ::_thesis: sin (x + (((2 * n) + 1) * PI)) = - (sin x) defpred S1[ Element of NAT ] means sin (x + (((2 * \$1) + 1) * PI)) = - (sin x); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: sin (x + (((2 * n) + 1) * PI)) = - (sin x) ; ::_thesis: S1[n + 1] sin (x + (((2 * (n + 1)) + 1) * PI)) = sin ((x + (((2 * n) + 1) * PI)) + (2 * PI)) .= ((sin (x + (((2 * n) + 1) * PI))) * (cos (2 * PI))) + ((cos (x + (((2 * n) + 1) * PI))) * (sin (2 * PI))) by SIN_COS:75 .= - (sin x) by A2, SIN_COS:77 ; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by SIN_COS:79; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence sin (x + (((2 * n) + 1) * PI)) = - (sin x) ; ::_thesis: verum end; theorem Th3: :: INTEGRA8:3 for x being Real for n being Element of NAT holds cos (x + ((2 * n) * PI)) = cos x proof let x be Real; ::_thesis: for n being Element of NAT holds cos (x + ((2 * n) * PI)) = cos x let n be Element of NAT ; ::_thesis: cos (x + ((2 * n) * PI)) = cos x cos . x = cos . (x + ((2 * PI) * n)) by SIN_COS6:10; hence cos (x + ((2 * n) * PI)) = cos x ; ::_thesis: verum end; theorem Th4: :: INTEGRA8:4 for x being Real for n being Element of NAT holds cos (x + (((2 * n) + 1) * PI)) = - (cos x) proof let x be Real; ::_thesis: for n being Element of NAT holds cos (x + (((2 * n) + 1) * PI)) = - (cos x) let n be Element of NAT ; ::_thesis: cos (x + (((2 * n) + 1) * PI)) = - (cos x) defpred S1[ Element of NAT ] means cos (x + (((2 * \$1) + 1) * PI)) = - (cos x); A1: for n being Element of NAT st S1[n] holds S1[n + 1] proof let n be Element of NAT ; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A2: cos (x + (((2 * n) + 1) * PI)) = - (cos x) ; ::_thesis: S1[n + 1] cos (x + (((2 * (n + 1)) + 1) * PI)) = cos ((x + (((2 * n) + 1) * PI)) + (2 * PI)) .= ((cos (x + (((2 * n) + 1) * PI))) * (cos (2 * PI))) - ((sin (x + (((2 * n) + 1) * PI))) * (sin (2 * PI))) by SIN_COS:75 .= - (cos x) by A2, SIN_COS:77 ; hence S1[n + 1] ; ::_thesis: verum end; A3: S1[ 0 ] by SIN_COS:79; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A3, A1); hence cos (x + (((2 * n) + 1) * PI)) = - (cos x) ; ::_thesis: verum end; theorem Th5: :: INTEGRA8:5 for x being Real st sin (x / 2) >= 0 holds sin (x / 2) = sqrt ((1 - (cos x)) / 2) proof let x be Real; ::_thesis: ( sin (x / 2) >= 0 implies sin (x / 2) = sqrt ((1 - (cos x)) / 2) ) assume A1: sin (x / 2) >= 0 ; ::_thesis: sin (x / 2) = sqrt ((1 - (cos x)) / 2) sqrt ((1 - (cos x)) / 2) = sqrt ((1 - (cos (2 * (x / 2)))) / 2) .= sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2) by SIN_COS5:7 .= abs (sin (x / 2)) by COMPLEX1:72 .= sin (x / 2) by A1, ABSVALUE:def_1 ; hence sin (x / 2) = sqrt ((1 - (cos x)) / 2) ; ::_thesis: verum end; theorem Th6: :: INTEGRA8:6 for x being Real st sin (x / 2) < 0 holds sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) proof let x be Real; ::_thesis: ( sin (x / 2) < 0 implies sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) ) assume A1: sin (x / 2) < 0 ; ::_thesis: sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) sqrt ((1 - (cos x)) / 2) = sqrt ((1 - (cos (2 * (x / 2)))) / 2) .= sqrt ((1 - (1 - (2 * ((sin (x / 2)) ^2)))) / 2) by SIN_COS5:7 .= abs (sin (x / 2)) by COMPLEX1:72 .= - (sin (x / 2)) by A1, ABSVALUE:def_1 ; hence sin (x / 2) = - (sqrt ((1 - (cos x)) / 2)) ; ::_thesis: verum end; theorem Th7: :: INTEGRA8:7 sin (PI / 4) = (sqrt 2) / 2 proof A1: sqrt 2 > 0 by SQUARE_1:25; sin ((PI / 2) / 2) = sqrt ((1 - (cos (PI / 2))) / 2) by Lm1, Th5; then sin (PI / 4) = 1 / (sqrt 2) by SIN_COS:77, SQUARE_1:18, SQUARE_1:30 .= ((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) by A1, XCMPLX_1:91 .= ((sqrt 2) * 1) / ((sqrt 2) ^2) ; hence sin (PI / 4) = (sqrt 2) / 2 by SQUARE_1:def_2; ::_thesis: verum end; theorem Th8: :: INTEGRA8:8 sin (- (PI / 4)) = - ((sqrt 2) / 2) proof A1: cos (- (PI / 2)) = sin ((PI / 2) - (- (PI / 2))) by SIN_COS:79 .= 0 by SIN_COS:77 ; A2: sqrt 2 > 0 by SQUARE_1:25; sin ((- (PI / 2)) / 2) = - (sqrt ((1 - (cos (- (PI / 2)))) / 2)) by Lm2, Th6; then sin (- (PI / 4)) = - (1 / (sqrt 2)) by A1, SQUARE_1:18, SQUARE_1:30 .= - (((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2))) by A2, XCMPLX_1:91 .= - (((sqrt 2) * 1) / ((sqrt 2) ^2)) ; hence sin (- (PI / 4)) = - ((sqrt 2) / 2) by SQUARE_1:def_2; ::_thesis: verum end; theorem Th9: :: INTEGRA8:9 [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[ proof A1: sqrt 2 > 0 by SQUARE_1:25; sqrt 2 < sqrt 4 by SQUARE_1:27; then A2: (sqrt 2) / 2 < 2 / 2 by SQUARE_1:20, XREAL_1:74; then ((sqrt 2) / 2) * (- 1) > 1 * (- 1) by XREAL_1:69; then A3: - ((sqrt 2) / 2) in ].(- 1),1.[ by A1, XXREAL_1:4; (sqrt 2) / 2 > 0 by A1, XREAL_1:139; then (sqrt 2) / 2 in ].(- 1),1.[ by A2, XXREAL_1:4; hence [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] c= ].(- 1),1.[ by A3, XXREAL_2:def_12; ::_thesis: verum end; theorem Th10: :: INTEGRA8:10 arcsin ((sqrt 2) / 2) = PI / 4 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then PI / 4 < PI / 2 by XREAL_1:76; hence arcsin ((sqrt 2) / 2) = PI / 4 by A1, Th7, SIN_COS6:69; ::_thesis: verum end; theorem Th11: :: INTEGRA8:11 arcsin (- ((sqrt 2) / 2)) = - (PI / 4) proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then PI / 4 < PI / 2 by XREAL_1:76; then (PI / 4) * (- 1) > (PI / 2) * (- 1) by XREAL_1:69; hence arcsin (- ((sqrt 2) / 2)) = - (PI / 4) by A1, Th8, SIN_COS6:69; ::_thesis: verum end; theorem Th12: :: INTEGRA8:12 for x being Real st cos (x / 2) >= 0 holds cos (x / 2) = sqrt ((1 + (cos x)) / 2) proof let x be Real; ::_thesis: ( cos (x / 2) >= 0 implies cos (x / 2) = sqrt ((1 + (cos x)) / 2) ) assume A1: cos (x / 2) >= 0 ; ::_thesis: cos (x / 2) = sqrt ((1 + (cos x)) / 2) sqrt ((1 + (cos x)) / 2) = sqrt ((1 + (cos (2 * (x / 2)))) / 2) .= sqrt ((1 + ((2 * ((cos (x / 2)) ^2)) - 1)) / 2) by SIN_COS5:7 .= abs (cos (x / 2)) by COMPLEX1:72 .= cos (x / 2) by A1, ABSVALUE:def_1 ; hence cos (x / 2) = sqrt ((1 + (cos x)) / 2) ; ::_thesis: verum end; Lm3: cos (PI / 4) > 0 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then 0 / 2 < PI / 2 by XREAL_1:74; then (PI / 2) * (- 1) < 0 * (- 1) by XREAL_1:69; then A2: (- (PI / 2)) + ((2 * PI) * 0) < PI / 4 by A1; PI / 4 < (PI / 2) + ((2 * PI) * 0) by A1, XREAL_1:76; hence cos (PI / 4) > 0 by A2, SIN_COS6:13; ::_thesis: verum end; theorem Th13: :: INTEGRA8:13 cos (PI / 4) = (sqrt 2) / 2 proof A1: sqrt 2 > 0 by SQUARE_1:25; cos ((PI / 2) / 2) = sqrt ((1 + (cos (PI / 2))) / 2) by Lm3, Th12 .= 1 / (sqrt 2) by SIN_COS:77, SQUARE_1:18, SQUARE_1:30 .= ((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) by A1, XCMPLX_1:91 .= ((sqrt 2) * 1) / ((sqrt 2) ^2) ; hence cos (PI / 4) = (sqrt 2) / 2 by SQUARE_1:def_2; ::_thesis: verum end; theorem Th14: :: INTEGRA8:14 cos ((3 * PI) / 4) = - ((sqrt 2) / 2) proof cos ((3 * PI) / 4) = cos ((PI / 2) + (PI / 4)) .= - ((sqrt 2) / 2) by Th7, SIN_COS:79 ; hence cos ((3 * PI) / 4) = - ((sqrt 2) / 2) ; ::_thesis: verum end; theorem Th15: :: INTEGRA8:15 arccos ((sqrt 2) / 2) = PI / 4 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then PI / 4 < PI / 1 by XREAL_1:76; hence arccos ((sqrt 2) / 2) = PI / 4 by A1, Th13, SIN_COS6:92; ::_thesis: verum end; theorem Th16: :: INTEGRA8:16 arccos (- ((sqrt 2) / 2)) = (3 * PI) / 4 proof PI in ].0,4.[ by SIN_COS:def_28; then A1: 0 < PI by XXREAL_1:4; then (3 / 4) * PI < 1 * PI by XREAL_1:68; hence arccos (- ((sqrt 2) / 2)) = (3 * PI) / 4 by A1, Th14, SIN_COS6:92; ::_thesis: verum end; theorem Th17: :: INTEGRA8:17 sinh . 1 = ((number_e ^2) - 1) / (2 * number_e) proof sinh . 1 = (number_e - (exp_R (- 1))) / 2 by IRRAT_1:def_7, SIN_COS2:def_1 .= ((number_e / 1) - (1 / number_e)) / 2 by IRRAT_1:def_7, TAYLOR_1:4 .= (((number_e * number_e) / (1 * number_e)) - (1 / number_e)) / 2 by TAYLOR_1:11, XCMPLX_1:91 .= (((number_e ^2) / number_e) - (1 / number_e)) / 2 .= (((number_e ^2) - 1) / number_e) / 2 by XCMPLX_1:120 .= ((number_e ^2) - 1) / (2 * number_e) by XCMPLX_1:78 ; hence sinh . 1 = ((number_e ^2) - 1) / (2 * number_e) ; ::_thesis: verum end; theorem Th18: :: INTEGRA8:18 cosh . 0 = 1 proof cosh . 0 = ((exp_R . 0) + (exp_R . (- 0))) / 2 by SIN_COS2:def_3 .= 1 by SIN_COS:51 ; hence cosh . 0 = 1 ; ::_thesis: verum end; theorem Th19: :: INTEGRA8:19 cosh . 1 = ((number_e ^2) + 1) / (2 * number_e) proof cosh . 1 = (number_e + (exp_R (- 1))) / 2 by IRRAT_1:def_7, SIN_COS2:def_3 .= ((number_e / 1) + (1 / number_e)) / 2 by IRRAT_1:def_7, TAYLOR_1:4 .= (((number_e * number_e) / (1 * number_e)) + (1 / number_e)) / 2 by TAYLOR_1:11, XCMPLX_1:91 .= (((number_e ^2) / number_e) + (1 / number_e)) / 2 .= (((number_e ^2) + 1) / number_e) / 2 by XCMPLX_1:62 .= ((number_e ^2) + 1) / (2 * number_e) by XCMPLX_1:78 ; hence cosh . 1 = ((number_e ^2) + 1) / (2 * number_e) ; ::_thesis: verum end; Lm4: for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: (- f1) (#) (- f2) = f1 (#) f2 (- f1) (#) (- f2) = (- 1) (#) (f1 (#) (- f2)) by RFUNCT_1:12 .= f1 (#) (- (- f2)) by RFUNCT_1:13 ; hence (- f1) (#) (- f2) = f1 (#) f2 ; ::_thesis: verum end; theorem Th20: :: INTEGRA8:20 for L1 being LinearFunc holds - L1 is LinearFunc proof let L1 be LinearFunc; ::_thesis: - L1 is LinearFunc consider g1 being Real such that A1: for p being Real holds L1 . p = g1 * p by FDIFF_1:def_3; A2: L1 is total by FDIFF_1:def_3; now__::_thesis:_for_p_being_Real_holds_(-_L1)_._p_=_(-_g1)_*_p let p be Real; ::_thesis: (- L1) . p = (- g1) * p thus (- L1) . p = - (L1 . p) by A2, RFUNCT_1:58 .= - (g1 * p) by A1 .= (- g1) * p ; ::_thesis: verum end; hence - L1 is LinearFunc by A2, FDIFF_1:def_3; ::_thesis: verum end; theorem Th21: :: INTEGRA8:21 for R1 being RestFunc holds - R1 is RestFunc proof let R1 be RestFunc; ::_thesis: - R1 is RestFunc A1: R1 is total by FDIFF_1:def_2; then A2: dom R1 = REAL by PARTFUN1:def_2; A3: for h being non-zero 0 -convergent Real_Sequence holds - (R1 /* h) = (- R1) /* h proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: - (R1 /* h) = (- R1) /* h rng h c= dom R1 by A2, VALUED_0:def_3; hence - (R1 /* h) = (- R1) /* h by RFUNCT_2:10; ::_thesis: verum end; now__::_thesis:_for_h_being_non-zero_0_-convergent_Real_Sequence_holds_ (_(h_")_(#)_((-_R1)_/*_h)_is_convergent_&_lim_((h_")_(#)_((-_R1)_/*_h))_=_0_) let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) ((- R1) /* h) is convergent & lim ((h ") (#) ((- R1) /* h)) = 0 ) A4: (h ") (#) (R1 /* h) is convergent by FDIFF_1:def_2; A5: (h ") (#) ((- R1) /* h) = (h ") (#) (- (R1 /* h)) by A3 .= - ((h ") (#) (R1 /* h)) by SEQ_1:19 ; hence (h ") (#) ((- R1) /* h) is convergent by A4, SEQ_2:9; ::_thesis: lim ((h ") (#) ((- R1) /* h)) = 0 A6: lim ((h ") (#) (R1 /* h)) = 0 by FDIFF_1:def_2; thus lim ((h ") (#) ((- R1) /* h)) = - (lim ((h ") (#) (R1 /* h))) by A4, A5, SEQ_2:10 .= 0 by A6 ; ::_thesis: verum end; hence - R1 is RestFunc by A1, FDIFF_1:def_2; ::_thesis: verum end; theorem Th22: :: INTEGRA8:22 for f1 being PartFunc of REAL,REAL for x0 being Real st f1 is_differentiable_in x0 holds ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) proof let f1 be PartFunc of REAL,REAL; ::_thesis: for x0 being Real st f1 is_differentiable_in x0 holds ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) let x0 be Real; ::_thesis: ( f1 is_differentiable_in x0 implies ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) ) assume A1: f1 is_differentiable_in x0 ; ::_thesis: ( - f1 is_differentiable_in x0 & diff ((- f1),x0) = - (diff (f1,x0)) ) then consider N1 being Neighbourhood of x0 such that A2: N1 c= dom f1 and A3: ex L being LinearFunc ex R being RestFunc st for x being Real st x in N1 holds (f1 . x) - (f1 . x0) = (L . (x - x0)) + (R . (x - x0)) by FDIFF_1:def_4; consider L1 being LinearFunc, R1 being RestFunc such that A4: for x being Real st x in N1 holds (f1 . x) - (f1 . x0) = (L1 . (x - x0)) + (R1 . (x - x0)) by A3; reconsider R = - R1 as RestFunc by Th21; reconsider L = - L1 as LinearFunc by Th20; A5: L1 is total by FDIFF_1:def_3; consider N being Neighbourhood of x0 such that A6: N c= N1 ; A7: R1 is total by FDIFF_1:def_2; A8: now__::_thesis:_for_x_being_Real_st_x_in_N_holds_ ((-_f1)_._x)_-_((-_f1)_._x0)_=_(L_._(x_-_x0))_+_(R_._(x_-_x0)) let x be Real; ::_thesis: ( x in N implies ((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0)) ) assume A9: x in N ; ::_thesis: ((- f1) . x) - ((- f1) . x0) = (L . (x - x0)) + (R . (x - x0)) thus ((- f1) . x) - ((- f1) . x0) = (- (f1 . x)) - ((- f1) . x0) by VALUED_1:8 .= (- (f1 . x)) - (- (f1 . x0)) by VALUED_1:8 .= - ((f1 . x) - (f1 . x0)) .= - ((L1 . (x - x0)) + (R1 . (x - x0))) by A4, A6, A9 .= (- (L1 . (x - x0))) + (- (R1 . (x - x0))) .= (L . (x - x0)) + (- (R1 . (x - x0))) by A5, RFUNCT_1:58 .= (L . (x - x0)) + (R . (x - x0)) by A7, RFUNCT_1:58 ; ::_thesis: verum end; N c= dom f1 by A2, A6, XBOOLE_1:1; then A10: N c= dom (- f1) by VALUED_1:8; hence - f1 is_differentiable_in x0 by A8, FDIFF_1:def_4; ::_thesis: diff ((- f1),x0) = - (diff (f1,x0)) hence diff ((- f1),x0) = L . 1 by A10, A8, FDIFF_1:def_5 .= - (L1 . 1) by A5, RFUNCT_1:58 .= - (diff (f1,x0)) by A1, A2, A4, FDIFF_1:def_5 ; ::_thesis: verum end; theorem Th23: :: INTEGRA8:23 for f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st Z c= dom (- f1) & f1 is_differentiable_on Z holds ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) ) ) proof let f1 be PartFunc of REAL,REAL; ::_thesis: for Z being open Subset of REAL st Z c= dom (- f1) & f1 is_differentiable_on Z holds ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom (- f1) & f1 is_differentiable_on Z implies ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) ) ) ) assume that A1: Z c= dom (- f1) and A2: f1 is_differentiable_on Z ; ::_thesis: ( - f1 is_differentiable_on Z & ( for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) ) ) now__::_thesis:_for_x0_being_Real_st_x0_in_Z_holds_ -_f1_is_differentiable_in_x0 let x0 be Real; ::_thesis: ( x0 in Z implies - f1 is_differentiable_in x0 ) assume x0 in Z ; ::_thesis: - f1 is_differentiable_in x0 then f1 is_differentiable_in x0 by A2, FDIFF_1:9; hence - f1 is_differentiable_in x0 by Th22; ::_thesis: verum end; hence A3: - f1 is_differentiable_on Z by A1, FDIFF_1:9; ::_thesis: for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((-_f1)_`|_Z)_._x_=_-_(diff_(f1,x)) let x be Real; ::_thesis: ( x in Z implies ((- f1) `| Z) . x = - (diff (f1,x)) ) assume A4: x in Z ; ::_thesis: ((- f1) `| Z) . x = - (diff (f1,x)) then A5: f1 is_differentiable_in x by A2, FDIFF_1:9; thus ((- f1) `| Z) . x = diff ((- f1),x) by A3, A4, FDIFF_1:def_7 .= - (diff (f1,x)) by A5, Th22 ; ::_thesis: verum end; hence for x being Real st x in Z holds ((- f1) `| Z) . x = - (diff (f1,x)) ; ::_thesis: verum end; theorem :: INTEGRA8:24 - sin is_differentiable_on REAL proof dom (- sin) = [#] REAL by FUNCT_2:def_1; hence - sin is_differentiable_on REAL by Th23, SIN_COS:68; ::_thesis: verum end; theorem Th25: :: INTEGRA8:25 for x being Real holds ( - cos is_differentiable_in x & diff ((- cos),x) = sin . x ) proof let x be Real; ::_thesis: ( - cos is_differentiable_in x & diff ((- cos),x) = sin . x ) A1: cos is_differentiable_in x by SIN_COS:63; then diff ((- cos),x) = - (diff (cos,x)) by Th22 .= - (- (sin . x)) by SIN_COS:63 ; hence ( - cos is_differentiable_in x & diff ((- cos),x) = sin . x ) by A1, Th22; ::_thesis: verum end; theorem Th26: :: INTEGRA8:26 ( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds diff ((- cos),x) = sin . x ) ) proof dom (- cos) = [#] REAL by FUNCT_2:def_1; hence ( - cos is_differentiable_on REAL & ( for x being Real st x in REAL holds diff ((- cos),x) = sin . x ) ) by Th23, Th25, SIN_COS:67; ::_thesis: verum end; theorem Th27: :: INTEGRA8:27 sin `| REAL = cos proof for x being Real st x in REAL holds diff (sin,x) = cos . x by SIN_COS:68; hence sin `| REAL = cos by FDIFF_1:def_7, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem Th28: :: INTEGRA8:28 cos `| REAL = - sin proof A1: for x being Element of REAL st x in dom (cos `| REAL) holds (cos `| REAL) . x = (- sin) . x proof let x be Element of REAL ; ::_thesis: ( x in dom (cos `| REAL) implies (cos `| REAL) . x = (- sin) . x ) assume x in dom (cos `| REAL) ; ::_thesis: (cos `| REAL) . x = (- sin) . x (cos `| REAL) . x = diff (cos,x) by FDIFF_1:def_7, SIN_COS:67 .= - (sin . x) by SIN_COS:63 ; hence (cos `| REAL) . x = (- sin) . x by VALUED_1:8; ::_thesis: verum end; dom (- sin) = REAL by FUNCT_2:def_1; then dom (cos `| REAL) = dom (- sin) by FDIFF_1:def_7, SIN_COS:67; hence cos `| REAL = - sin by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th29: :: INTEGRA8:29 (- cos) `| REAL = sin by Th26, FDIFF_1:def_7, SIN_COS:24; theorem Th30: :: INTEGRA8:30 sinh `| REAL = cosh proof for x being Real st x in REAL holds diff (sinh,x) = cosh . x by SIN_COS2:34; hence sinh `| REAL = cosh by FDIFF_1:def_7, SIN_COS2:30, SIN_COS2:34; ::_thesis: verum end; theorem Th31: :: INTEGRA8:31 cosh `| REAL = sinh proof for x being Real st x in REAL holds diff (cosh,x) = sinh . x by SIN_COS2:35; hence cosh `| REAL = sinh by FDIFF_1:def_7, SIN_COS2:30, SIN_COS2:35; ::_thesis: verum end; theorem Th32: :: INTEGRA8:32 exp_R `| REAL = exp_R proof for x being Real st x in REAL holds diff (exp_R,x) = exp_R . x by SIN_COS:66; hence exp_R `| REAL = exp_R by FDIFF_1:def_7, SIN_COS:47, SIN_COS:66; ::_thesis: verum end; theorem Th33: :: INTEGRA8:33 for Z being open Subset of REAL st Z c= dom tan holds ( tan is_differentiable_on Z & ( for x being Real st x in Z holds (tan `| Z) . x = 1 / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom tan implies ( tan is_differentiable_on Z & ( for x being Real st x in Z holds (tan `| Z) . x = 1 / ((cos . x) ^2) ) ) ) assume A1: Z c= dom tan ; ::_thesis: ( tan is_differentiable_on Z & ( for x being Real st x in Z holds (tan `| Z) . x = 1 / ((cos . x) ^2) ) ) A2: for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then x in dom tan by A1; then A3: cos . x <> 0 by FDIFF_8:1; ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; hence tan is_differentiable_in x by A3, FDIFF_2:14; ::_thesis: verum end; then A4: tan is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (tan `| Z) . x = 1 / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies (tan `| Z) . x = 1 / ((cos . x) ^2) ) A5: ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; assume A6: x in Z ; ::_thesis: (tan `| Z) . x = 1 / ((cos . x) ^2) then x in dom tan by A1; then cos . x <> 0 by FDIFF_8:1; then diff (tan,x) = (((diff (sin,x)) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) by A5, FDIFF_2:14 .= (((cos . x) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) by SIN_COS:64 .= (((cos . x) * (cos . x)) - ((- (sin . x)) * (sin . x))) / ((cos . x) ^2) by SIN_COS:63 .= (((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) / ((cos . x) ^2) .= 1 / ((cos . x) ^2) by SIN_COS:28 ; hence (tan `| Z) . x = 1 / ((cos . x) ^2) by A4, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( tan is_differentiable_on Z & ( for x being Real st x in Z holds (tan `| Z) . x = 1 / ((cos . x) ^2) ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum end; theorem Th34: :: INTEGRA8:34 for Z being open Subset of REAL st Z c= dom cot holds ( cot is_differentiable_on Z & ( for x being Real st x in Z holds (cot `| Z) . x = - (1 / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom cot implies ( cot is_differentiable_on Z & ( for x being Real st x in Z holds (cot `| Z) . x = - (1 / ((sin . x) ^2)) ) ) ) assume A1: Z c= dom cot ; ::_thesis: ( cot is_differentiable_on Z & ( for x being Real st x in Z holds (cot `| Z) . x = - (1 / ((sin . x) ^2)) ) ) A2: for x being Real st x in Z holds cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x ) assume x in Z ; ::_thesis: cot is_differentiable_in x then x in dom cot by A1; then A3: sin . x <> 0 by FDIFF_8:2; ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; hence cot is_differentiable_in x by A3, FDIFF_2:14; ::_thesis: verum end; then A4: cot is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (cot `| Z) . x = - (1 / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies (cot `| Z) . x = - (1 / ((sin . x) ^2)) ) A5: ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; assume A6: x in Z ; ::_thesis: (cot `| Z) . x = - (1 / ((sin . x) ^2)) then x in dom cot by A1; then sin . x <> 0 by FDIFF_8:2; then diff (cot,x) = (((diff (cos,x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by A5, FDIFF_2:14 .= (((- (sin . x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) by SIN_COS:63 .= ((- ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) / ((sin . x) ^2) by SIN_COS:64 .= (- (((sin . x) * (sin . x)) + ((cos . x) * (cos . x)))) / ((sin . x) ^2) .= (- (((sin . x) * (sin . x)) + ((cos . x) ^2))) / ((sin . x) ^2) .= (- (((sin . x) ^2) + ((cos . x) ^2))) / ((sin . x) ^2) .= - ((((cos . x) ^2) + ((sin . x) ^2)) / ((sin . x) ^2)) by XCMPLX_1:187 .= - (1 / ((sin . x) ^2)) by SIN_COS:28 ; hence (cot `| Z) . x = - (1 / ((sin . x) ^2)) by A4, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( cot is_differentiable_on Z & ( for x being Real st x in Z holds (cot `| Z) . x = - (1 / ((sin . x) ^2)) ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum end; theorem :: INTEGRA8:35 for r being Real holds rng (REAL --> r) c= REAL proof let r be Real; ::_thesis: rng (REAL --> r) c= REAL rng (REAL --> r) c= {r} by FUNCOP_1:13; hence rng (REAL --> r) c= REAL by XBOOLE_1:1; ::_thesis: verum end; definition let r be Real; func Cst r -> Function of REAL,REAL equals :: INTEGRA8:def 1 REAL --> r; coherence REAL --> r is Function of REAL,REAL ; end; :: deftheorem defines Cst INTEGRA8:def_1_:_ for r being Real holds Cst r = REAL --> r; theorem Th36: :: INTEGRA8:36 for a, b being Real for A being non empty closed_interval Subset of REAL holds chi (A,A) = (Cst 1) | A proof let a, b be Real; ::_thesis: for A being non empty closed_interval Subset of REAL holds chi (A,A) = (Cst 1) | A let A be non empty closed_interval Subset of REAL; ::_thesis: chi (A,A) = (Cst 1) | A ( dom ((Cst 1) | A) = A & ( for x being set st x in A holds ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) ) ) proof A1: ( dom (Cst 1) = REAL & dom ((Cst 1) | A) = (dom (Cst 1)) /\ A ) by FUNCOP_1:13, RELAT_1:61; hence dom ((Cst 1) | A) = A by XBOOLE_1:28; ::_thesis: for x being set st x in A holds ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) let x be set ; ::_thesis: ( x in A implies ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) ) assume A2: x in A ; ::_thesis: ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) then x in dom ((Cst 1) | A) by A1, XBOOLE_0:def_4; then ((Cst 1) | A) . x = (REAL --> 1) . x by FUNCT_1:47 .= 1 by A2, FUNCOP_1:7 ; hence ( ( x in A implies ((Cst 1) | A) . x = 1 ) & ( not x in A implies ((Cst 1) | A) . x = 0 ) ) by A2; ::_thesis: verum end; hence chi (A,A) = (Cst 1) | A by FUNCT_3:def_3; ::_thesis: verum end; theorem Th37: :: INTEGRA8:37 for a, b being Real for A being non empty closed_interval Subset of REAL st A = [.a,b.] holds ( upper_bound A = b & lower_bound A = a ) proof let a, b be Real; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.a,b.] holds ( upper_bound A = b & lower_bound A = a ) let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.a,b.] implies ( upper_bound A = b & lower_bound A = a ) ) A1: A = [.(lower_bound A),(upper_bound A).] by INTEGRA1:4; assume A = [.a,b.] ; ::_thesis: ( upper_bound A = b & lower_bound A = a ) hence ( upper_bound A = b & lower_bound A = a ) by A1, INTEGRA1:5; ::_thesis: verum end; begin theorem :: INTEGRA8:38 for a, b being Real st a <= b holds integral ((Cst 1),a,b) = b - a proof let a, b be Real; ::_thesis: ( a <= b implies integral ((Cst 1),a,b) = b - a ) assume a <= b ; ::_thesis: integral ((Cst 1),a,b) = b - a then [.a,b.] = ['a,b'] by INTEGRA5:def_3; then reconsider A = [.a,b.] as non empty closed_interval Subset of REAL ; ( upper_bound A = b & lower_bound A = a ) by Th37; then A1: vol A = b - a by INTEGRA1:def_5; ( integral ((Cst 1),a,b) = integral ((Cst 1),A) & (Cst 1) || A = chi (A,A) ) by Th36, INTEGRA5:19; hence integral ((Cst 1),a,b) = b - a by A1, INTEGRA4:2; ::_thesis: verum end; Lm5: dom sin = REAL by FUNCT_2:def_1; Lm6: dom cos = REAL by FUNCT_2:def_1; Lm7: dom (- sin) = REAL by FUNCT_2:def_1; Lm8: dom exp_R = REAL by FUNCT_2:def_1; Lm9: dom sinh = REAL by FUNCT_2:def_1; Lm10: dom cosh = REAL by FUNCT_2:def_1; Lm11: for A being non empty closed_interval Subset of REAL holds ( cos is_integrable_on A & cos | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( cos is_integrable_on A & cos | A is bounded ) cos | A is continuous ; hence ( cos is_integrable_on A & cos | A is bounded ) by Lm6, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th39: :: INTEGRA8:39 for A being non empty closed_interval Subset of REAL holds integral (cos,A) = (sin . (upper_bound A)) - (sin . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral (cos,A) = (sin . (upper_bound A)) - (sin . (lower_bound A)) A1: for x being Element of REAL st x in dom (sin `| REAL) holds (sin `| REAL) . x = cos . x proof let x be Element of REAL ; ::_thesis: ( x in dom (sin `| REAL) implies (sin `| REAL) . x = cos . x ) assume x in dom (sin `| REAL) ; ::_thesis: (sin `| REAL) . x = cos . x (sin `| REAL) . x = diff (sin,x) by FDIFF_1:def_7, SIN_COS:68; hence (sin `| REAL) . x = cos . x by SIN_COS:64; ::_thesis: verum end; A2: ( cos is_integrable_on A & cos | A is bounded ) by Lm11; dom (sin `| REAL) = dom cos by FDIFF_1:def_7, SIN_COS:24, SIN_COS:68; then sin `| REAL = cos by A1, PARTFUN1:5; hence integral (cos,A) = (sin . (upper_bound A)) - (sin . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS:68; ::_thesis: verum end; theorem :: INTEGRA8:40 for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds integral (cos,A) = 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI / 2).] implies integral (cos,A) = 1 ) assume A = [.0,(PI / 2).] ; ::_thesis: integral (cos,A) = 1 then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37; then integral (cos,A) = 1 - (sin . 0) by Th39, SIN_COS:77 .= 1 - (cos . ((PI / 2) - 0)) by SIN_COS:78 .= 1 - 0 by SIN_COS:77 ; hence integral (cos,A) = 1 ; ::_thesis: verum end; theorem :: INTEGRA8:41 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral (cos,A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies integral (cos,A) = 0 ) assume A = [.0,PI.] ; ::_thesis: integral (cos,A) = 0 then ( upper_bound A = PI & lower_bound A = 0 ) by Th37; then integral (cos,A) = 0 - (sin . 0) by Th39, SIN_COS:76 .= 0 - (sin . (0 + (2 * PI))) by SIN_COS:78 .= 0 - 0 by SIN_COS:76 ; hence integral (cos,A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:42 for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds integral (cos,A) = - 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,((PI * 3) / 2).] implies integral (cos,A) = - 1 ) assume A = [.0,((PI * 3) / 2).] ; ::_thesis: integral (cos,A) = - 1 then ( upper_bound A = (PI * 3) / 2 & lower_bound A = 0 ) by Th37; then integral (cos,A) = (- 1) - (sin . 0) by Th39, SIN_COS:76 .= (- 1) - (sin . (0 + (2 * PI))) by SIN_COS:78 .= (- 1) - 0 by SIN_COS:76 ; hence integral (cos,A) = - 1 ; ::_thesis: verum end; theorem :: INTEGRA8:43 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds integral (cos,A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies integral (cos,A) = 0 ) assume A = [.0,(PI * 2).] ; ::_thesis: integral (cos,A) = 0 then ( upper_bound A = PI * 2 & lower_bound A = 0 ) by Th37; then integral (cos,A) = 0 - (sin . 0) by Th39, SIN_COS:76 .= 0 - (sin . (0 + (2 * PI))) by SIN_COS:78 .= 0 - 0 by SIN_COS:76 ; hence integral (cos,A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:44 for A being non empty closed_interval Subset of REAL for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral (cos,A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral (cos,A) = 0 let n be Element of NAT ; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral (cos,A) = 0 ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: integral (cos,A) = 0 then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37; then integral (cos,A) = (sin (0 + (((2 * n) + 1) * PI))) - (sin (0 + ((2 * n) * PI))) by Th39 .= (- (sin 0)) - (sin (0 + ((2 * n) * PI))) by Th2 .= (- (sin 0)) - (sin 0) by Th1 .= (- (sin (0 + (2 * PI)))) - (sin 0) by SIN_COS:79 .= 0 - 0 by SIN_COS:77, SIN_COS:79 ; hence integral (cos,A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:45 for A being non empty closed_interval Subset of REAL for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral (cos,A) = - (2 * (sin x)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral (cos,A) = - (2 * (sin x)) let x be Real; ::_thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral (cos,A) = - (2 * (sin x)) let n be Element of NAT ; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral (cos,A) = - (2 * (sin x)) ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: integral (cos,A) = - (2 * (sin x)) then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37; then integral (cos,A) = (sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI))) by Th39 .= (- (sin x)) - (sin (x + ((2 * n) * PI))) by Th2 .= (- (sin x)) - (sin x) by Th1 .= - (2 * (sin x)) ; hence integral (cos,A) = - (2 * (sin x)) ; ::_thesis: verum end; Lm12: for A being non empty closed_interval Subset of REAL holds ( - sin is_integrable_on A & (- sin) | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( - sin is_integrable_on A & (- sin) | A is bounded ) (- sin) | A is continuous ; hence ( - sin is_integrable_on A & (- sin) | A is bounded ) by Lm7, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th46: :: INTEGRA8:46 for A being non empty closed_interval Subset of REAL holds integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A)) A1: for x being Element of REAL st x in dom (cos `| REAL) holds (cos `| REAL) . x = (- sin) . x proof let x be Element of REAL ; ::_thesis: ( x in dom (cos `| REAL) implies (cos `| REAL) . x = (- sin) . x ) assume x in dom (cos `| REAL) ; ::_thesis: (cos `| REAL) . x = (- sin) . x (cos `| REAL) . x = diff (cos,x) by FDIFF_1:def_7, SIN_COS:67 .= - (sin . x) by SIN_COS:63 ; hence (cos `| REAL) . x = (- sin) . x by VALUED_1:8; ::_thesis: verum end; A2: ( - sin is_integrable_on A & (- sin) | A is bounded ) by Lm12; dom (- sin) = REAL by FUNCT_2:def_1; then dom (cos `| REAL) = dom (- sin) by FDIFF_1:def_7, SIN_COS:67; then cos `| REAL = - sin by A1, PARTFUN1:5; hence integral ((- sin),A) = (cos . (upper_bound A)) - (cos . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS:67; ::_thesis: verum end; theorem :: INTEGRA8:47 for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds integral ((- sin),A) = - 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI / 2).] implies integral ((- sin),A) = - 1 ) assume A = [.0,(PI / 2).] ; ::_thesis: integral ((- sin),A) = - 1 then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37; then integral ((- sin),A) = 0 - (cos . 0) by Th46, SIN_COS:76 .= 0 - (sin . ((PI / 2) - 0)) by SIN_COS:78 .= 0 - 1 by SIN_COS:76 ; hence integral ((- sin),A) = - 1 ; ::_thesis: verum end; theorem :: INTEGRA8:48 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((- sin),A) = - 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies integral ((- sin),A) = - 2 ) assume A = [.0,PI.] ; ::_thesis: integral ((- sin),A) = - 2 then ( upper_bound A = PI & lower_bound A = 0 ) by Th37; then integral ((- sin),A) = (- 1) - (cos . 0) by Th46, SIN_COS:76 .= (- 1) - (sin . ((PI / 2) - 0)) by SIN_COS:78 .= (- 1) - 1 by SIN_COS:76 ; hence integral ((- sin),A) = - 2 ; ::_thesis: verum end; theorem :: INTEGRA8:49 for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds integral ((- sin),A) = - 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,((PI * 3) / 2).] implies integral ((- sin),A) = - 1 ) assume A = [.0,((PI * 3) / 2).] ; ::_thesis: integral ((- sin),A) = - 1 then ( upper_bound A = (PI * 3) / 2 & lower_bound A = 0 ) by Th37; then integral ((- sin),A) = 0 - (cos . 0) by Th46, SIN_COS:76 .= 0 - (sin . ((PI / 2) - 0)) by SIN_COS:78 .= 0 - 1 by SIN_COS:76 ; hence integral ((- sin),A) = - 1 ; ::_thesis: verum end; theorem :: INTEGRA8:50 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds integral ((- sin),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies integral ((- sin),A) = 0 ) assume A = [.0,(PI * 2).] ; ::_thesis: integral ((- sin),A) = 0 then ( upper_bound A = PI * 2 & lower_bound A = 0 ) by Th37; then integral ((- sin),A) = 1 - (cos . 0) by Th46, SIN_COS:76 .= 1 - (sin . ((PI / 2) - 0)) by SIN_COS:78 .= 1 - 1 by SIN_COS:76 ; hence integral ((- sin),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:51 for A being non empty closed_interval Subset of REAL for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((- sin),A) = - 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((- sin),A) = - 2 let n be Element of NAT ; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral ((- sin),A) = - 2 ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: integral ((- sin),A) = - 2 then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37; then integral ((- sin),A) = (cos (0 + (((2 * n) + 1) * PI))) - (cos (0 + ((2 * n) * PI))) by Th46 .= (- (cos 0)) - (cos (0 + ((2 * n) * PI))) by Th4 .= (- (cos 0)) - (cos 0) by Th3 .= (- (cos (0 + (2 * PI)))) - (cos 0) by SIN_COS:79 .= (- 1) - 1 by SIN_COS:77, SIN_COS:79 ; hence integral ((- sin),A) = - 2 ; ::_thesis: verum end; theorem :: INTEGRA8:52 for A being non empty closed_interval Subset of REAL for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((- sin),A) = - (2 * (cos x)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((- sin),A) = - (2 * (cos x)) let x be Real; ::_thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((- sin),A) = - (2 * (cos x)) let n be Element of NAT ; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral ((- sin),A) = - (2 * (cos x)) ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: integral ((- sin),A) = - (2 * (cos x)) then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37; then integral ((- sin),A) = (cos (x + (((2 * n) + 1) * PI))) - (cos (x + ((2 * n) * PI))) by Th46 .= (- (cos x)) - (cos (x + ((2 * n) * PI))) by Th4 .= (- (cos x)) - (cos x) by Th3 .= - (2 * (cos x)) ; hence integral ((- sin),A) = - (2 * (cos x)) ; ::_thesis: verum end; Lm13: for A being non empty closed_interval Subset of REAL holds ( exp_R is_integrable_on A & exp_R | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( exp_R is_integrable_on A & exp_R | A is bounded ) exp_R | A is continuous ; hence ( exp_R is_integrable_on A & exp_R | A is bounded ) by Lm8, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th53: :: INTEGRA8:53 for A being non empty closed_interval Subset of REAL holds integral (exp_R,A) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral (exp_R,A) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound A)) A1: for x being Element of REAL st x in dom (exp_R `| REAL) holds (exp_R `| REAL) . x = exp_R . x proof let x be Element of REAL ; ::_thesis: ( x in dom (exp_R `| REAL) implies (exp_R `| REAL) . x = exp_R . x ) assume x in dom (exp_R `| REAL) ; ::_thesis: (exp_R `| REAL) . x = exp_R . x (exp_R `| REAL) . x = diff (exp_R,x) by FDIFF_1:def_7, SIN_COS:66; hence (exp_R `| REAL) . x = exp_R . x by SIN_COS:65; ::_thesis: verum end; A2: ( exp_R is_integrable_on A & exp_R | A is bounded ) by Lm13; dom (exp_R `| REAL) = dom exp_R by FDIFF_1:def_7, SIN_COS:47, SIN_COS:66; then exp_R `| REAL = exp_R by A1, PARTFUN1:5; hence integral (exp_R,A) = (exp_R . (upper_bound A)) - (exp_R . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS:66; ::_thesis: verum end; theorem :: INTEGRA8:54 for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds integral (exp_R,A) = number_e - 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,1.] implies integral (exp_R,A) = number_e - 1 ) assume A = [.0,1.] ; ::_thesis: integral (exp_R,A) = number_e - 1 then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37; hence integral (exp_R,A) = number_e - 1 by Th53, IRRAT_1:def_7, SIN_COS:51; ::_thesis: verum end; Lm14: for A being non empty closed_interval Subset of REAL holds sinh | A is continuous proof let A be non empty closed_interval Subset of REAL; ::_thesis: sinh | A is continuous sinh | REAL is continuous by FDIFF_1:25, SIN_COS2:34; hence sinh | A is continuous by FCONT_1:16; ::_thesis: verum end; Lm15: for A being non empty closed_interval Subset of REAL holds ( sinh is_integrable_on A & sinh | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( sinh is_integrable_on A & sinh | A is bounded ) sinh | A is continuous by Lm14; hence ( sinh is_integrable_on A & sinh | A is bounded ) by Lm9, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th55: :: INTEGRA8:55 for A being non empty closed_interval Subset of REAL holds integral (sinh,A) = (cosh . (upper_bound A)) - (cosh . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral (sinh,A) = (cosh . (upper_bound A)) - (cosh . (lower_bound A)) A1: for x being Element of REAL st x in dom (cosh `| REAL) holds (cosh `| REAL) . x = sinh . x proof let x be Element of REAL ; ::_thesis: ( x in dom (cosh `| REAL) implies (cosh `| REAL) . x = sinh . x ) assume x in dom (cosh `| REAL) ; ::_thesis: (cosh `| REAL) . x = sinh . x (cosh `| REAL) . x = diff (cosh,x) by FDIFF_1:def_7, SIN_COS2:35; hence (cosh `| REAL) . x = sinh . x by SIN_COS2:35; ::_thesis: verum end; A2: ( sinh is_integrable_on A & sinh | A is bounded ) by Lm15; dom (cosh `| REAL) = dom sinh by FDIFF_1:def_7, SIN_COS2:30, SIN_COS2:35; then cosh `| REAL = sinh by A1, PARTFUN1:5; hence integral (sinh,A) = (cosh . (upper_bound A)) - (cosh . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS2:35; ::_thesis: verum end; theorem :: INTEGRA8:56 for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,1.] implies integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) ) exp_R 1 > 0 by SIN_COS:55; then A1: 2 * number_e > 0 by IRRAT_1:def_7, XREAL_1:129; assume A = [.0,1.] ; ::_thesis: integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37; then integral (sinh,A) = (((number_e ^2) + 1) / (2 * number_e)) - 1 by Th18, Th19, Th55 .= (((number_e ^2) + 1) / (2 * number_e)) - ((2 * number_e) / (2 * number_e)) by A1, XCMPLX_1:60 .= (((number_e ^2) + 1) - (2 * number_e)) / (2 * number_e) by XCMPLX_1:120 .= (((number_e ^2) - ((2 * number_e) * 1)) + (1 ^2)) / (2 * number_e) .= ((number_e - 1) ^2) / (2 * number_e) ; hence integral (sinh,A) = ((number_e - 1) ^2) / (2 * number_e) ; ::_thesis: verum end; Lm16: for A being non empty closed_interval Subset of REAL holds cosh | A is continuous proof let A be non empty closed_interval Subset of REAL; ::_thesis: cosh | A is continuous cosh | REAL is continuous by FDIFF_1:25, SIN_COS2:35; hence cosh | A is continuous by FCONT_1:16; ::_thesis: verum end; Lm17: for A being non empty closed_interval Subset of REAL holds ( cosh is_integrable_on A & cosh | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( cosh is_integrable_on A & cosh | A is bounded ) cosh | A is continuous by Lm16; hence ( cosh is_integrable_on A & cosh | A is bounded ) by Lm10, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th57: :: INTEGRA8:57 for A being non empty closed_interval Subset of REAL holds integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A)) A1: for x being Element of REAL st x in dom (sinh `| REAL) holds (sinh `| REAL) . x = cosh . x proof let x be Element of REAL ; ::_thesis: ( x in dom (sinh `| REAL) implies (sinh `| REAL) . x = cosh . x ) assume x in dom (sinh `| REAL) ; ::_thesis: (sinh `| REAL) . x = cosh . x (sinh `| REAL) . x = diff (sinh,x) by FDIFF_1:def_7, SIN_COS2:34; hence (sinh `| REAL) . x = cosh . x by SIN_COS2:34; ::_thesis: verum end; A2: ( cosh is_integrable_on A & cosh | A is bounded ) by Lm17; dom (sinh `| REAL) = dom cosh by FDIFF_1:def_7, SIN_COS2:30, SIN_COS2:34; then sinh `| REAL = cosh by A1, PARTFUN1:5; hence integral (cosh,A) = (sinh . (upper_bound A)) - (sinh . (lower_bound A)) by A2, INTEGRA5:13, SIN_COS2:34; ::_thesis: verum end; theorem :: INTEGRA8:58 for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,1.] implies integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) ) assume A = [.0,1.] ; ::_thesis: integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37; then integral (cosh,A) = (sinh . 1) - 0 by Th57, SIN_COS2:16 .= ((number_e ^2) - 1) / (2 * number_e) by Th17 ; hence integral (cosh,A) = ((number_e ^2) - 1) / (2 * number_e) ; ::_thesis: verum end; theorem :: INTEGRA8:59 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds ( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds ( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds ( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom tan = Z & dom tan = dom f2 & ( for x being Real st x in Z holds ( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & f2 | A is continuous implies integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) ) assume that A1: A c= Z and A2: dom tan = Z and A3: dom tan = dom f2 and A4: for x being Real st x in Z holds ( f2 . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) A6: f2 is_integrable_on A by A1, A2, A3, A5, INTEGRA5:11; A7: tan is_differentiable_on Z by A2, Th33; A8: for x being Real st x in dom (tan `| Z) holds (tan `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (tan `| Z) implies (tan `| Z) . x = f2 . x ) assume x in dom (tan `| Z) ; ::_thesis: (tan `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (tan `| Z) . x = 1 / ((cos . x) ^2) by A2, Th33 .= f2 . x by A4, A9 ; hence (tan `| Z) . x = f2 . x ; ::_thesis: verum end; dom (tan `| Z) = dom f2 by A2, A3, A7, FDIFF_1:def_7; then tan `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (tan . (upper_bound A)) - (tan . (lower_bound A)) by A1, A2, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA8:60 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & dom cot = Z & dom cot = dom f2 & ( for x being Real st x in Z holds ( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & dom cot = Z & dom cot = dom f2 & ( for x being Real st x in Z holds ( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st A c= Z & dom cot = Z & dom cot = dom f2 & ( for x being Real st x in Z holds ( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & f2 | A is continuous holds integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( A c= Z & dom cot = Z & dom cot = dom f2 & ( for x being Real st x in Z holds ( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & f2 | A is continuous implies integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) ) assume that A1: A c= Z and A2: dom cot = Z and A3: dom cot = dom f2 and A4: for x being Real st x in Z holds ( f2 . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) and A5: f2 | A is continuous ; ::_thesis: integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) A6: f2 is_integrable_on A by A1, A2, A3, A5, INTEGRA5:11; A7: cot is_differentiable_on Z by A2, Th34; A8: for x being Real st x in dom (cot `| Z) holds (cot `| Z) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (cot `| Z) implies (cot `| Z) . x = f2 . x ) assume x in dom (cot `| Z) ; ::_thesis: (cot `| Z) . x = f2 . x then A9: x in Z by A7, FDIFF_1:def_7; then (cot `| Z) . x = - (1 / ((sin . x) ^2)) by A2, Th34 .= f2 . x by A4, A9 ; hence (cot `| Z) . x = f2 . x ; ::_thesis: verum end; dom (cot `| Z) = dom f2 by A2, A3, A7, FDIFF_1:def_7; then cot `| Z = f2 by A8, PARTFUN1:5; hence integral (f2,A) = (cot . (upper_bound A)) - (cot . (lower_bound A)) by A1, A2, A3, A5, A6, A7, INTEGRA5:10, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA8:61 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st dom tanh = dom f2 & ( for x being Real st x in REAL holds f2 . x = 1 / ((cosh . x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st dom tanh = dom f2 & ( for x being Real st x in REAL holds f2 . x = 1 / ((cosh . x) ^2) ) & f2 | A is continuous holds integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( dom tanh = dom f2 & ( for x being Real st x in REAL holds f2 . x = 1 / ((cosh . x) ^2) ) & f2 | A is continuous implies integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) ) assume that A1: dom tanh = dom f2 and A2: for x being Real st x in REAL holds f2 . x = 1 / ((cosh . x) ^2) and A3: f2 | A is continuous ; ::_thesis: integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) A4: for x being Real st x in dom (tanh `| REAL) holds (tanh `| REAL) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (tanh `| REAL) implies (tanh `| REAL) . x = f2 . x ) assume x in dom (tanh `| REAL) ; ::_thesis: (tanh `| REAL) . x = f2 . x (tanh `| REAL) . x = diff (tanh,x) by FDIFF_1:def_7, SIN_COS2:36 .= 1 / ((cosh . x) ^2) by SIN_COS2:33 .= f2 . x by A2 ; hence (tanh `| REAL) . x = f2 . x ; ::_thesis: verum end; dom (tanh `| REAL) = dom f2 by A1, FDIFF_1:def_7, SIN_COS2:30, SIN_COS2:36; then A5: tanh `| REAL = f2 by A4, PARTFUN1:5; A6: dom tanh = REAL by FUNCT_2:def_1; then f2 is_integrable_on A by A1, A3, INTEGRA5:11; hence integral (f2,A) = (tanh . (upper_bound A)) - (tanh . (lower_bound A)) by A1, A3, A6, A5, INTEGRA5:10, INTEGRA5:13, SIN_COS2:36; ::_thesis: verum end; Lm18: dom (arcsin `| ].(- 1),1.[) = ].(- 1),1.[ by FDIFF_1:def_7, SIN_COS6:83; theorem Th62: :: INTEGRA8:62 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( A c= ].(- 1),1.[ & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous implies integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) ) assume that A1: A c= ].(- 1),1.[ and A2: dom (arcsin `| ].(- 1),1.[) = dom f2 and A3: for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) and A4: f2 | A is continuous ; ::_thesis: integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) for x being Real st x in dom (arcsin `| ].(- 1),1.[) holds (arcsin `| ].(- 1),1.[) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (arcsin `| ].(- 1),1.[) implies (arcsin `| ].(- 1),1.[) . x = f2 . x ) assume A5: x in dom (arcsin `| ].(- 1),1.[) ; ::_thesis: (arcsin `| ].(- 1),1.[) . x = f2 . x then A6: ( - 1 < x & x < 1 ) by Lm18, XXREAL_1:4; (arcsin `| ].(- 1),1.[) . x = diff (arcsin,x) by A5, Lm18, FDIFF_1:def_7, SIN_COS6:83 .= 1 / (sqrt (1 - (x ^2))) by A6, SIN_COS6:83 .= f2 . x by A3 ; hence (arcsin `| ].(- 1),1.[) . x = f2 . x ; ::_thesis: verum end; then A7: arcsin `| ].(- 1),1.[ = f2 by A2, PARTFUN1:5; ( A c= dom f2 & f2 is_integrable_on A ) by A1, A2, A4, Lm18, INTEGRA5:11; hence integral (f2,A) = (arcsin . (upper_bound A)) - (arcsin . (lower_bound A)) by A1, A4, A7, INTEGRA5:10, INTEGRA5:13, SIN_COS6:83; ::_thesis: verum end; theorem Th63: :: INTEGRA8:63 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds integral (f2,A) = (arccos . (upper_bound A)) - (arccos . (lower_bound A)) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st A c= ].(- 1),1.[ & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds integral (f2,A) = (arccos . (upper_bound A)) - (arccos . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: ( A c= ].(- 1),1.[ & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous implies integral (f2,A) = (arccos . (upper_bound A)) - (arccos . (lower_bound A)) ) assume that A1: A c= ].(- 1),1.[ and A2: dom (arccos `| ].(- 1),1.[) = dom f2 and A3: for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) and A4: f2 | A is continuous ; ::_thesis: integral (f2,A) = (arccos . (upper_bound A)) - (arccos . (lower_bound A)) A5: A c= dom f2 by A1, A2, FDIFF_1:def_7, SIN_COS6:106; A6: dom (arccos `| ].(- 1),1.[) = ].(- 1),1.[ by FDIFF_1:def_7, SIN_COS6:106; for x being Real st x in dom (arccos `| ].(- 1),1.[) holds (arccos `| ].(- 1),1.[) . x = f2 . x proof let x be Real; ::_thesis: ( x in dom (arccos `| ].(- 1),1.[) implies (arccos `| ].(- 1),1.[) . x = f2 . x ) assume A7: x in dom (arccos `| ].(- 1),1.[) ; ::_thesis: (arccos `| ].(- 1),1.[) . x = f2 . x then A8: ( - 1 < x & x < 1 ) by A6, XXREAL_1:4; (arccos `| ].(- 1),1.[) . x = diff (arccos,x) by A6, A7, FDIFF_1:def_7, SIN_COS6:106 .= - (1 / (sqrt (1 - (x ^2)))) by A8, SIN_COS6:106 .= f2 . x by A3 ; hence (arccos `| ].(- 1),1.[) . x = f2 . x ; ::_thesis: verum end; then A9: arccos `| ].(- 1),1.[ = f2 by A2, PARTFUN1:5; f2 is_integrable_on A by A6, A1, A2, A4, INTEGRA5:11; hence integral (f2,A) = (arccos . (upper_bound A)) - (arccos . (lower_bound A)) by A1, A4, A5, A9, INTEGRA5:10, INTEGRA5:13, SIN_COS6:106; ::_thesis: verum end; theorem :: INTEGRA8:64 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds integral (f2,A) = PI / 2 proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous holds integral (f2,A) = PI / 2 let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous implies integral (f2,A) = PI / 2 ) assume that A1: A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] and A2: ( dom (arcsin `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = 1 / (sqrt (1 - (x ^2))) ) ) & f2 | A is continuous ) ; ::_thesis: integral (f2,A) = PI / 2 ( upper_bound A = (sqrt 2) / 2 & lower_bound A = - ((sqrt 2) / 2) ) by A1, Th37; then integral (f2,A) = (arcsin . ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) by A1, A2, Th9, Th62 .= (arcsin ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) by SIN_COS6:def_2 .= (arcsin ((sqrt 2) / 2)) - (arcsin (- ((sqrt 2) / 2))) by SIN_COS6:def_2 .= (2 * PI) / 4 by Th10, Th11 ; hence integral (f2,A) = PI / 2 ; ::_thesis: verum end; theorem :: INTEGRA8:65 for f2 being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds integral (f2,A) = - (PI / 2) proof let f2 be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL st A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous holds integral (f2,A) = - (PI / 2) let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] & dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous implies integral (f2,A) = - (PI / 2) ) assume that A1: A = [.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] and A2: ( dom (arccos `| ].(- 1),1.[) = dom f2 & ( for x being Real holds ( x in ].(- 1),1.[ & f2 . x = - (1 / (sqrt (1 - (x ^2)))) ) ) & f2 | A is continuous ) ; ::_thesis: integral (f2,A) = - (PI / 2) ( upper_bound A = (sqrt 2) / 2 & lower_bound A = - ((sqrt 2) / 2) ) by A1, Th37; then integral (f2,A) = (arccos . ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) by A1, A2, Th9, Th63 .= (arccos ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) by SIN_COS6:def_4 .= (arccos ((sqrt 2) / 2)) - (arccos (- ((sqrt 2) / 2))) by SIN_COS6:def_4 .= (- (2 * PI)) / 4 by Th15, Th16 ; hence integral (f2,A) = - (PI / 2) ; ::_thesis: verum end; theorem Th66: :: INTEGRA8:66 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) let Z be open Subset of REAL; ::_thesis: ( f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded implies integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) ) assume that A1: f is_differentiable_on Z and A2: g is_differentiable_on Z and A3: A c= Z and A4: f `| Z is_integrable_on A and A5: (f `| Z) | A is bounded and A6: g `| Z is_integrable_on A and A7: (g `| Z) | A is bounded ; ::_thesis: integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) A8: ( (f `| Z) || A is integrable & (g `| Z) || A is integrable ) by A4, A6, INTEGRA5:def_1; A c= dom (g `| Z) by A2, A3, FDIFF_1:def_7; then A9: (g `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; A c= dom (f `| Z) by A1, A3, FDIFF_1:def_7; then A10: (f `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; A11: ( ((f `| Z) || A) | A is bounded & ((g `| Z) || A) | A is bounded ) by A5, A7, INTEGRA5:9; integral (((f `| Z) + (g `| Z)),A) = integral (((f `| Z) || A) + ((g `| Z) || A)) by INTEGRA5:5 .= (integral ((f `| Z),A)) + (integral ((g `| Z),A)) by A8, A10, A9, A11, INTEGRA1:57 .= ((f . (upper_bound A)) - (f . (lower_bound A))) + (integral ((g `| Z),A)) by A1, A3, A4, A5, INTEGRA5:13 .= ((f . (upper_bound A)) - (f . (lower_bound A))) + ((g . (upper_bound A)) - (g . (lower_bound A))) by A2, A3, A6, A7, INTEGRA5:13 ; hence integral (((f `| Z) + (g `| Z)),A) = (((f . (upper_bound A)) - (f . (lower_bound A))) + (g . (upper_bound A))) - (g . (lower_bound A)) ; ::_thesis: verum end; theorem Th67: :: INTEGRA8:67 for f, g being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) proof let f, g be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) let A be non empty closed_interval Subset of REAL; ::_thesis: for Z being open Subset of REAL st f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded holds integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) let Z be open Subset of REAL; ::_thesis: ( f is_differentiable_on Z & g is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded & g `| Z is_integrable_on A & (g `| Z) | A is bounded implies integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) ) assume that A1: f is_differentiable_on Z and A2: g is_differentiable_on Z and A3: A c= Z and A4: f `| Z is_integrable_on A and A5: (f `| Z) | A is bounded and A6: g `| Z is_integrable_on A and A7: (g `| Z) | A is bounded ; ::_thesis: integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) A8: ( (f `| Z) || A is integrable & (g `| Z) || A is integrable ) by A4, A6, INTEGRA5:def_1; A c= dom (g `| Z) by A2, A3, FDIFF_1:def_7; then A9: (g `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; A c= dom (f `| Z) by A1, A3, FDIFF_1:def_7; then A10: (f `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; A11: ( ((f `| Z) || A) | A is bounded & ((g `| Z) || A) | A is bounded ) by A5, A7, INTEGRA5:9; integral (((f `| Z) - (g `| Z)),A) = integral (((f `| Z) || A) - ((g `| Z) || A)) by RFUNCT_1:47 .= (integral ((f `| Z),A)) - (integral ((g `| Z) || A)) by A8, A10, A9, A11, INTEGRA2:33 .= ((f . (upper_bound A)) - (f . (lower_bound A))) - (integral ((g `| Z),A)) by A1, A3, A4, A5, INTEGRA5:13 .= ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) by A2, A3, A6, A7, INTEGRA5:13 ; hence integral (((f `| Z) - (g `| Z)),A) = ((f . (upper_bound A)) - (f . (lower_bound A))) - ((g . (upper_bound A)) - (g . (lower_bound A))) ; ::_thesis: verum end; theorem Th68: :: INTEGRA8:68 for f being PartFunc of REAL,REAL for A being non empty closed_interval Subset of REAL for r being Real for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) proof let f be PartFunc of REAL,REAL; ::_thesis: for A being non empty closed_interval Subset of REAL for r being Real for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) let r be Real; ::_thesis: for Z being open Subset of REAL st f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded holds integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) let Z be open Subset of REAL; ::_thesis: ( f is_differentiable_on Z & A c= Z & f `| Z is_integrable_on A & (f `| Z) | A is bounded implies integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) ) assume that A1: ( f is_differentiable_on Z & A c= Z ) and A2: ( f `| Z is_integrable_on A & (f `| Z) | A is bounded ) ; ::_thesis: integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) A3: ( (f `| Z) || A is integrable & ((f `| Z) || A) | A is bounded ) by A2, INTEGRA5:9, INTEGRA5:def_1; A c= dom (f `| Z) by A1, FDIFF_1:def_7; then A4: (f `| Z) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; integral ((r (#) (f `| Z)),A) = integral (r (#) ((f `| Z) || A)) by RFUNCT_1:49 .= r * (integral ((f `| Z),A)) by A4, A3, INTEGRA2:31 .= r * ((f . (upper_bound A)) - (f . (lower_bound A))) by A1, A2, INTEGRA5:13 ; hence integral ((r (#) (f `| Z)),A) = (r * (f . (upper_bound A))) - (r * (f . (lower_bound A))) ; ::_thesis: verum end; Lm19: for A being non empty closed_interval Subset of REAL holds ( sin is_integrable_on A & sin | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( sin is_integrable_on A & sin | A is bounded ) sin | A is continuous ; hence ( sin is_integrable_on A & sin | A is bounded ) by Lm5, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem Th69: :: INTEGRA8:69 for A being non empty closed_interval Subset of REAL holds integral ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) A1: [#] REAL is open Subset of REAL ; A2: ( sin is_integrable_on A & sin | A is bounded ) by Lm19; ( cos is_integrable_on A & cos | A is bounded ) by Lm11; hence integral ((sin + cos),A) = ((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) by A2, A1, Th26, Th27, Th29, Th66, SIN_COS:68; ::_thesis: verum end; theorem :: INTEGRA8:70 for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds integral ((sin + cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI / 2).] implies integral ((sin + cos),A) = 2 ) assume A = [.0,(PI / 2).] ; ::_thesis: integral ((sin + cos),A) = 2 then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37; then integral ((sin + cos),A) = ((((- cos) . (PI / 2)) - ((- cos) . 0)) + (sin . (PI / 2))) - (sin . 0) by Th69 .= (((- (cos . (PI / 2))) - ((- cos) . 0)) + (sin . (PI / 2))) - (sin . 0) by VALUED_1:8 .= (((- 0) - (- (cos . 0))) + 1) - (sin . 0) by SIN_COS:76, VALUED_1:8 .= ((- (- (cos . 0))) + 1) - (sin . (0 + (2 * PI))) by SIN_COS:78 .= ((- (- (cos . (0 + (2 * PI))))) + 1) - 0 by SIN_COS:76, SIN_COS:78 .= 2 by SIN_COS:76 ; hence integral ((sin + cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:71 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((sin + cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies integral ((sin + cos),A) = 2 ) assume A = [.0,PI.] ; ::_thesis: integral ((sin + cos),A) = 2 then ( upper_bound A = PI & lower_bound A = 0 ) by Th37; then integral ((sin + cos),A) = ((((- cos) . PI) - ((- cos) . 0)) + (sin . PI)) - (sin . 0) by Th69 .= (((- (cos . PI)) - ((- cos) . 0)) + (sin . PI)) - (sin . 0) by VALUED_1:8 .= (((- (cos . PI)) - (- (cos . 0))) + (sin . PI)) - (sin . 0) by VALUED_1:8 .= ((- (- (cos . 0))) + 1) - (sin . (0 + (2 * PI))) by SIN_COS:76, SIN_COS:78 .= ((- (- (cos . (0 + (2 * PI))))) + 1) - 0 by SIN_COS:76, SIN_COS:78 .= 2 by SIN_COS:76 ; hence integral ((sin + cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:72 for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds integral ((sin + cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,((PI * 3) / 2).] implies integral ((sin + cos),A) = 0 ) assume A = [.0,((PI * 3) / 2).] ; ::_thesis: integral ((sin + cos),A) = 0 then ( upper_bound A = (PI * 3) / 2 & lower_bound A = 0 ) by Th37; then integral ((sin + cos),A) = ((((- cos) . ((PI * 3) / 2)) - ((- cos) . 0)) + (sin . ((PI * 3) / 2))) - (sin . 0) by Th69 .= (((- (cos . ((PI * 3) / 2))) - ((- cos) . 0)) + (sin . ((PI * 3) / 2))) - (sin . 0) by VALUED_1:8 .= (((- (cos . ((PI * 3) / 2))) - (- (cos . 0))) + (sin . ((PI * 3) / 2))) - (sin . 0) by VALUED_1:8 .= (((- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI))))) + (sin . ((PI * 3) / 2))) - (sin . 0) by SIN_COS:78 .= (((- 0) + 1) + (- 1)) - 0 by SIN_COS:76, SIN_COS:78 ; hence integral ((sin + cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:73 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds integral ((sin + cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies integral ((sin + cos),A) = 0 ) assume A = [.0,(PI * 2).] ; ::_thesis: integral ((sin + cos),A) = 0 then ( upper_bound A = PI * 2 & lower_bound A = 0 ) by Th37; then integral ((sin + cos),A) = ((((- cos) . (PI * 2)) - ((- cos) . 0)) + (sin . (PI * 2))) - (sin . 0) by Th69 .= (((- (cos . (PI * 2))) - ((- cos) . 0)) + (sin . (PI * 2))) - (sin . 0) by VALUED_1:8 .= (((- (cos . (PI * 2))) - (- (cos . 0))) + (sin . (PI * 2))) - (sin . 0) by VALUED_1:8 .= (((- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI))))) + (sin . (PI * 2))) - (sin . 0) by SIN_COS:78 .= (((- 1) + 1) + 0) - 0 by SIN_COS:76, SIN_COS:78 ; hence integral ((sin + cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:74 for A being non empty closed_interval Subset of REAL for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin + cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin + cos),A) = 2 let n be Element of NAT ; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral ((sin + cos),A) = 2 ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: integral ((sin + cos),A) = 2 then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37; then integral ((sin + cos),A) = ((((- cos) . (((2 * n) + 1) * PI)) - ((- cos) . ((2 * n) * PI))) + (sin . (((2 * n) + 1) * PI))) - (sin . ((2 * n) * PI)) by Th69 .= (((- (cos . (((2 * n) + 1) * PI))) - ((- cos) . ((2 * n) * PI))) + (sin . (((2 * n) + 1) * PI))) - (sin . ((2 * n) * PI)) by VALUED_1:8 .= (((- (cos . (((2 * n) + 1) * PI))) - (- (cos (0 + ((2 * n) * PI))))) + (sin . (((2 * n) + 1) * PI))) - (sin . (0 + ((2 * n) * PI))) by VALUED_1:8 .= (((- (cos . (((2 * n) + 1) * PI))) - (- (cos 0))) + (sin . (((2 * n) + 1) * PI))) - (sin . (0 + ((2 * n) * PI))) by Th3 .= (((- (cos . (((2 * n) + 1) * PI))) + (cos 0)) + (sin . (((2 * n) + 1) * PI))) - (sin . (0 + ((2 * n) * PI))) .= (((- (cos . (((2 * n) + 1) * PI))) + (cos (0 + (2 * PI)))) + (sin . (((2 * n) + 1) * PI))) - (sin . (0 + ((2 * n) * PI))) by SIN_COS:79 .= (((- (cos . (((2 * n) + 1) * PI))) + 1) + (sin . (((2 * n) + 1) * PI))) - (sin (0 + ((2 * n) * PI))) by SIN_COS:77 .= (((- (cos . (((2 * n) + 1) * PI))) + 1) + (sin . (((2 * n) + 1) * PI))) - (sin 0) by Th1 .= (((- (cos . (((2 * n) + 1) * PI))) + 1) + (sin . (((2 * n) + 1) * PI))) - (sin (0 + (2 * PI))) by SIN_COS:79 .= ((- (cos (0 + (((2 * n) + 1) * PI)))) + 1) + (sin (0 + (((2 * n) + 1) * PI))) by SIN_COS:77 .= ((- (cos (0 + (((2 * n) + 1) * PI)))) + 1) + (- (sin 0)) by Th2 .= ((- (- (cos 0))) + 1) + (- (sin 0)) by Th4 .= ((cos 0) + 1) - (sin 0) .= ((cos (0 + (2 * PI))) + 1) - (sin 0) by SIN_COS:79 .= ((cos (0 + (2 * PI))) + 1) - (sin (0 + (2 * PI))) by SIN_COS:79 .= 2 by SIN_COS:77 ; hence integral ((sin + cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:75 for A being non empty closed_interval Subset of REAL for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) let x be Real; ::_thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) let n be Element of NAT ; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37; then integral ((sin + cos),A) = ((((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI)))) - (sin . (x + ((2 * n) * PI))) by Th69 .= (((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI)))) - (sin . (x + ((2 * n) * PI))) by VALUED_1:8 .= (((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) by VALUED_1:8 .= (((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) by Th4 .= (((- (- (cos x))) - (- (cos x))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) by Th3 .= (((- (- (cos x))) - (- (cos x))) + (- (sin x))) - (sin (x + ((2 * n) * PI))) by Th2 .= (((cos x) + (cos x)) - (sin x)) - (sin x) by Th1 .= (2 * (cos x)) - (2 * (sin x)) ; hence integral ((sin + cos),A) = (2 * (cos x)) - (2 * (sin x)) ; ::_thesis: verum end; theorem Th76: :: INTEGRA8:76 for A being non empty closed_interval Subset of REAL holds integral ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A)) A1: [#] REAL is open Subset of REAL ; cosh | A is continuous by Lm16; then A2: cosh is_integrable_on A by Lm10, INTEGRA5:11; sinh | A is continuous by Lm14; then A3: sinh is_integrable_on A by Lm9, INTEGRA5:11; ( cosh | A is bounded & sinh | A is bounded ) by Lm9, Lm10, Lm14, Lm16, INTEGRA5:10; hence integral ((sinh + cosh),A) = (((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A)) by A2, A3, A1, Th30, Th31, Th66, SIN_COS2:34, SIN_COS2:35; ::_thesis: verum end; theorem :: INTEGRA8:77 for A being non empty closed_interval Subset of REAL st A = [.0,1.] holds integral ((sinh + cosh),A) = number_e - 1 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,1.] implies integral ((sinh + cosh),A) = number_e - 1 ) A1: number_e > 0 by IRRAT_1:def_7, SIN_COS:55; assume A = [.0,1.] ; ::_thesis: integral ((sinh + cosh),A) = number_e - 1 then ( upper_bound A = 1 & lower_bound A = 0 ) by Th37; then integral ((sinh + cosh),A) = (((cosh . 1) - (cosh . 0)) + (sinh . 1)) - (sinh . 0) by Th76 .= ((((number_e ^2) + 1) / (2 * number_e)) + (((number_e ^2) - 1) / (2 * number_e))) - 1 by Th17, Th18, Th19, SIN_COS2:16 .= ((((number_e ^2) + 1) + ((number_e ^2) - 1)) / (2 * number_e)) - 1 by XCMPLX_1:62 .= ((2 * (number_e ^2)) / (2 * number_e)) - 1 .= ((number_e ^2) / number_e) - 1 by XCMPLX_1:91 .= ((number_e * number_e) / number_e) - 1 .= number_e - 1 by A1, XCMPLX_1:89 ; hence integral ((sinh + cosh),A) = number_e - 1 ; ::_thesis: verum end; theorem Th78: :: INTEGRA8:78 for A being non empty closed_interval Subset of REAL holds integral ((sin - cos),A) = (((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sin - cos),A) = (((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A))) A1: [#] REAL is open Subset of REAL ; A2: ( sin is_integrable_on A & sin | A is bounded ) by Lm19; ( cos is_integrable_on A & cos | A is bounded ) by Lm11; hence integral ((sin - cos),A) = (((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A))) by A2, A1, Th26, Th27, Th29, Th67, SIN_COS:68; ::_thesis: verum end; theorem :: INTEGRA8:79 for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds integral ((sin - cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI / 2).] implies integral ((sin - cos),A) = 0 ) assume A = [.0,(PI / 2).] ; ::_thesis: integral ((sin - cos),A) = 0 then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37; then integral ((sin - cos),A) = (((- cos) . (PI / 2)) - ((- cos) . 0)) - ((sin . (PI / 2)) - (sin . 0)) by Th78 .= ((- (cos . (PI / 2))) - ((- cos) . 0)) - ((sin . (PI / 2)) - (sin . 0)) by VALUED_1:8 .= ((- 0) - (- (cos . 0))) - (1 - (sin . 0)) by SIN_COS:76, VALUED_1:8 .= (- (- (cos . 0))) - (1 - (sin . (0 + (2 * PI)))) by SIN_COS:78 .= (- (- (cos . (0 + (2 * PI))))) - (1 - 0) by SIN_COS:76, SIN_COS:78 .= 0 by SIN_COS:76 ; hence integral ((sin - cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:80 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((sin - cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies integral ((sin - cos),A) = 2 ) assume A = [.0,PI.] ; ::_thesis: integral ((sin - cos),A) = 2 then ( upper_bound A = PI & lower_bound A = 0 ) by Th37; then integral ((sin - cos),A) = (((- cos) . PI) - ((- cos) . 0)) - ((sin . PI) - (sin . 0)) by Th78 .= ((- (cos . PI)) - ((- cos) . 0)) - ((sin . PI) - (sin . 0)) by VALUED_1:8 .= ((- (cos . PI)) - (- (cos . 0))) - ((sin . PI) - (sin . 0)) by VALUED_1:8 .= ((- (- (cos . 0))) + 1) - ((sin . (0 + (2 * PI))) - 0) by SIN_COS:76, SIN_COS:78 .= ((- (- (cos . (0 + (2 * PI))))) + 1) - 0 by SIN_COS:76, SIN_COS:78 .= 2 by SIN_COS:76 ; hence integral ((sin - cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:81 for A being non empty closed_interval Subset of REAL st A = [.0,((PI * 3) / 2).] holds integral ((sin - cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,((PI * 3) / 2).] implies integral ((sin - cos),A) = 2 ) assume A = [.0,((PI * 3) / 2).] ; ::_thesis: integral ((sin - cos),A) = 2 then ( upper_bound A = (PI * 3) / 2 & lower_bound A = 0 ) by Th37; then integral ((sin - cos),A) = (((- cos) . ((PI * 3) / 2)) - ((- cos) . 0)) - ((sin . ((PI * 3) / 2)) - (sin . 0)) by Th78 .= ((- (cos . ((PI * 3) / 2))) - ((- cos) . 0)) - ((sin . ((PI * 3) / 2)) - (sin . 0)) by VALUED_1:8 .= ((- (cos . ((PI * 3) / 2))) - (- (cos . 0))) - ((sin . ((PI * 3) / 2)) - (sin . 0)) by VALUED_1:8 .= ((- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI))))) - ((sin . ((PI * 3) / 2)) - (sin . 0)) by SIN_COS:78 .= ((- 0) + 1) - ((- 1) - 0) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin - cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:82 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds integral ((sin - cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies integral ((sin - cos),A) = 0 ) assume A = [.0,(PI * 2).] ; ::_thesis: integral ((sin - cos),A) = 0 then ( upper_bound A = PI * 2 & lower_bound A = 0 ) by Th37; then integral ((sin - cos),A) = (((- cos) . (PI * 2)) - ((- cos) . 0)) - ((sin . (PI * 2)) - (sin . 0)) by Th78 .= ((- (cos . (PI * 2))) - ((- cos) . 0)) - ((sin . (PI * 2)) - (sin . 0)) by VALUED_1:8 .= ((- (cos . (PI * 2))) - (- (cos . 0))) - ((sin . (PI * 2)) - (sin . 0)) by VALUED_1:8 .= ((- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI))))) - ((sin . (PI * 2)) - (sin . 0)) by SIN_COS:78 .= ((- 1) + 1) - (0 - 0) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin - cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:83 for A being non empty closed_interval Subset of REAL for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin - cos),A) = 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin - cos),A) = 2 let n be Element of NAT ; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral ((sin - cos),A) = 2 ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: integral ((sin - cos),A) = 2 then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37; then integral ((sin - cos),A) = (((- cos) . (((2 * n) + 1) * PI)) - ((- cos) . ((2 * n) * PI))) - ((sin . (((2 * n) + 1) * PI)) - (sin . ((2 * n) * PI))) by Th78 .= ((- (cos . (((2 * n) + 1) * PI))) - ((- cos) . ((2 * n) * PI))) - ((sin . (((2 * n) + 1) * PI)) - (sin . ((2 * n) * PI))) by VALUED_1:8 .= ((- (cos . (((2 * n) + 1) * PI))) - (- (cos (0 + ((2 * n) * PI))))) - ((sin . (((2 * n) + 1) * PI)) - (sin . (0 + ((2 * n) * PI)))) by VALUED_1:8 .= ((- (cos . (((2 * n) + 1) * PI))) - (- (cos 0))) - ((sin . (((2 * n) + 1) * PI)) - (sin . (0 + ((2 * n) * PI)))) by Th3 .= ((- (cos . (((2 * n) + 1) * PI))) + (cos 0)) - ((sin . (((2 * n) + 1) * PI)) - (sin . (0 + ((2 * n) * PI)))) .= ((- (cos . (((2 * n) + 1) * PI))) + (cos (0 + (2 * PI)))) - ((sin . (((2 * n) + 1) * PI)) - (sin . (0 + ((2 * n) * PI)))) by SIN_COS:79 .= ((- (cos . (((2 * n) + 1) * PI))) + 1) - ((sin . (((2 * n) + 1) * PI)) - (sin (0 + ((2 * n) * PI)))) by SIN_COS:77 .= ((- (cos . (((2 * n) + 1) * PI))) + 1) - ((sin . (((2 * n) + 1) * PI)) - (sin 0)) by Th1 .= ((- (cos . (((2 * n) + 1) * PI))) + 1) - ((sin . (((2 * n) + 1) * PI)) - (sin (0 + (2 * PI)))) by SIN_COS:79 .= ((- (cos (0 + (((2 * n) + 1) * PI)))) + 1) - (sin (0 + (((2 * n) + 1) * PI))) by SIN_COS:77 .= ((- (cos (0 + (((2 * n) + 1) * PI)))) + 1) - (- (sin 0)) by Th2 .= ((- (- (cos 0))) + 1) - (- (sin 0)) by Th4 .= ((cos 0) + 1) + (sin 0) .= ((cos (0 + (2 * PI))) + 1) + (sin 0) by SIN_COS:79 .= ((cos (0 + (2 * PI))) + 1) + (sin (0 + (2 * PI))) by SIN_COS:79 .= 2 by SIN_COS:77 ; hence integral ((sin - cos),A) = 2 ; ::_thesis: verum end; theorem :: INTEGRA8:84 for A being non empty closed_interval Subset of REAL for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) let x be Real; ::_thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) let n be Element of NAT ; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37; then integral ((sin - cos),A) = (((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) by Th78 .= ((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) by VALUED_1:8 .= ((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by VALUED_1:8 .= ((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by Th4 .= ((- (- (cos x))) - (- (cos x))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) by Th3 .= ((- (- (cos x))) - (- (cos x))) - ((- (sin x)) - (sin (x + ((2 * n) * PI)))) by Th2 .= ((cos x) + (cos x)) - ((- (sin x)) - (sin x)) by Th1 .= (2 * (cos x)) + (2 * (sin x)) ; hence integral ((sin - cos),A) = (2 * (cos x)) + (2 * (sin x)) ; ::_thesis: verum end; theorem :: INTEGRA8:85 for A being non empty closed_interval Subset of REAL for r being Real holds integral ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real holds integral ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A))) let r be Real; ::_thesis: integral ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A))) ( sin | A is bounded & [#] REAL is open Subset of REAL ) by Lm5, INTEGRA5:10; hence integral ((r (#) sin),A) = (r * ((- cos) . (upper_bound A))) - (r * ((- cos) . (lower_bound A))) by Lm5, Th26, Th29, Th68, INTEGRA5:11; ::_thesis: verum end; theorem :: INTEGRA8:86 for A being non empty closed_interval Subset of REAL for r being Real holds integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real holds integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A))) let r be Real; ::_thesis: integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A))) A1: [#] REAL is open Subset of REAL ; ( cos is_integrable_on A & cos | A is bounded ) by Lm11; hence integral ((r (#) cos),A) = (r * (sin . (upper_bound A))) - (r * (sin . (lower_bound A))) by A1, Th27, Th68, SIN_COS:68; ::_thesis: verum end; theorem :: INTEGRA8:87 for A being non empty closed_interval Subset of REAL for r being Real holds integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real holds integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A))) let r be Real; ::_thesis: integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A))) A1: [#] REAL is open Subset of REAL ; ( sinh | A is continuous & sinh | A is bounded ) by Lm9, Lm14, INTEGRA5:10; hence integral ((r (#) sinh),A) = (r * (cosh . (upper_bound A))) - (r * (cosh . (lower_bound A))) by A1, Lm9, Th31, Th68, INTEGRA5:11, SIN_COS2:35; ::_thesis: verum end; theorem :: INTEGRA8:88 for A being non empty closed_interval Subset of REAL for r being Real holds integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real holds integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A))) let r be Real; ::_thesis: integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A))) A1: [#] REAL is open Subset of REAL ; ( cosh | A is continuous & cosh | A is bounded ) by Lm10, Lm16, INTEGRA5:10; hence integral ((r (#) cosh),A) = (r * (sinh . (upper_bound A))) - (r * (sinh . (lower_bound A))) by A1, Lm10, Th30, Th68, INTEGRA5:11, SIN_COS2:34; ::_thesis: verum end; theorem :: INTEGRA8:89 for A being non empty closed_interval Subset of REAL for r being Real holds integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: for r being Real holds integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A))) let r be Real; ::_thesis: integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A))) ( exp_R | A is bounded & [#] REAL is open Subset of REAL ) by Lm8, INTEGRA5:10; hence integral ((r (#) exp_R),A) = (r * (exp_R . (upper_bound A))) - (r * (exp_R . (lower_bound A))) by Lm8, Th32, Th68, INTEGRA5:11, SIN_COS:66; ::_thesis: verum end; theorem Th90: :: INTEGRA8:90 for A being non empty closed_interval Subset of REAL holds integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) A1: [#] REAL is open Subset of REAL ; sin | A is continuous ; then A2: (- cos) `| REAL is_integrable_on A by Lm5, Th29, INTEGRA5:11; (- sin) | A is continuous ; then A3: cos `| REAL is_integrable_on A by Lm7, Th28, INTEGRA5:11; ( ((- cos) `| REAL) | A is bounded & (cos `| REAL) | A is bounded ) by Lm5, Lm7, Th28, Th29, INTEGRA5:10; then integral ((sin (#) cos),A) = ((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral (((- cos) (#) (- sin)),A)) by A2, A3, A1, Th26, Th28, Th29, INTEGRA5:21, SIN_COS:67 .= ((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by Lm4 .= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by VALUED_1:8 .= (((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - ((- (cos . (lower_bound A))) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) by VALUED_1:8 .= (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) - (integral ((sin (#) cos),A)) ; hence integral ((sin (#) cos),A) = (1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) ; ::_thesis: verum end; theorem :: INTEGRA8:91 for A being non empty closed_interval Subset of REAL st A = [.0,(PI / 2).] holds integral ((sin (#) cos),A) = 1 / 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI / 2).] implies integral ((sin (#) cos),A) = 1 / 2 ) assume A = [.0,(PI / 2).] ; ::_thesis: integral ((sin (#) cos),A) = 1 / 2 then ( upper_bound A = PI / 2 & lower_bound A = 0 ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by Th90 .= (1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2)))) by SIN_COS:78 .= (1 / 2) * ((1 * 1) - (0 * 0)) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin (#) cos),A) = 1 / 2 ; ::_thesis: verum end; theorem :: INTEGRA8:92 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((sin (#) cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,PI.] implies integral ((sin (#) cos),A) = 0 ) assume A = [.0,PI.] ; ::_thesis: integral ((sin (#) cos),A) = 0 then ( upper_bound A = PI & lower_bound A = 0 ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . PI) * (cos . PI))) by Th90 .= (1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . PI) * (cos . PI))) by SIN_COS:78 .= (1 / 2) * ((1 * 1) - ((- 1) * (- 1))) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin (#) cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:93 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * (3 / 2)).] holds integral ((sin (#) cos),A) = 1 / 2 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * (3 / 2)).] implies integral ((sin (#) cos),A) = 1 / 2 ) assume A = [.0,(PI * (3 / 2)).] ; ::_thesis: integral ((sin (#) cos),A) = 1 / 2 then ( upper_bound A = PI * (3 / 2) & lower_bound A = 0 ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2))))) by Th90 .= (1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2))))) by SIN_COS:78 .= (1 / 2) * ((1 * 1) - (0 * 0)) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin (#) cos),A) = 1 / 2 ; ::_thesis: verum end; theorem :: INTEGRA8:94 for A being non empty closed_interval Subset of REAL st A = [.0,(PI * 2).] holds integral ((sin (#) cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( A = [.0,(PI * 2).] implies integral ((sin (#) cos),A) = 0 ) assume A = [.0,(PI * 2).] ; ::_thesis: integral ((sin (#) cos),A) = 0 then ( upper_bound A = PI * 2 & lower_bound A = 0 ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2)))) by Th90 .= (1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2)))) by SIN_COS:78 .= (1 / 2) * ((1 * 1) - (1 * 1)) by SIN_COS:76, SIN_COS:78 ; hence integral ((sin (#) cos),A) = 0 ; ::_thesis: verum end; theorem :: INTEGRA8:95 for A being non empty closed_interval Subset of REAL for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin (#) cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for n being Element of NAT st A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] holds integral ((sin (#) cos),A) = 0 let n be Element of NAT ; ::_thesis: ( A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] implies integral ((sin (#) cos),A) = 0 ) assume A = [.((2 * n) * PI),(((2 * n) + 1) * PI).] ; ::_thesis: integral ((sin (#) cos),A) = 0 then ( upper_bound A = ((2 * n) + 1) * PI & lower_bound A = (2 * n) * PI ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . ((2 * n) * PI)) * (cos . ((2 * n) * PI))) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by Th90 .= (1 / 2) * (((cos 0) * (cos (0 + ((2 * n) * PI)))) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by Th3 .= (1 / 2) * (((cos 0) * (cos 0)) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by Th3 .= (1 / 2) * (((cos (0 + (2 * PI))) * (cos 0)) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by SIN_COS:79 .= (1 / 2) * ((1 * 1) - ((cos . (((2 * n) + 1) * PI)) * (cos . (((2 * n) + 1) * PI)))) by SIN_COS:77, SIN_COS:79 .= (1 / 2) * ((1 * 1) - ((- (cos 0)) * (cos (0 + (((2 * n) + 1) * PI))))) by Th4 .= (1 / 2) * ((1 * 1) - ((- (cos 0)) * (- (cos 0)))) by Th4 .= (1 / 2) * ((1 * 1) - ((cos 0) * (cos 0))) .= (1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI))) * (cos 0))) by SIN_COS:79 .= (1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI))) * (cos (0 + (2 * PI))))) by SIN_COS:79 ; hence integral ((sin (#) cos),A) = 0 by SIN_COS:77; ::_thesis: verum end; theorem :: INTEGRA8:96 for A being non empty closed_interval Subset of REAL for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin (#) cos),A) = 0 proof let A be non empty closed_interval Subset of REAL; ::_thesis: for x being Real for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin (#) cos),A) = 0 let x be Real; ::_thesis: for n being Element of NAT st A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] holds integral ((sin (#) cos),A) = 0 let n be Element of NAT ; ::_thesis: ( A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] implies integral ((sin (#) cos),A) = 0 ) assume A = [.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] ; ::_thesis: integral ((sin (#) cos),A) = 0 then ( upper_bound A = x + (((2 * n) + 1) * PI) & lower_bound A = x + ((2 * n) * PI) ) by Th37; then integral ((sin (#) cos),A) = (1 / 2) * (((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI)))) - ((cos . (x + (((2 * n) + 1) * PI))) * (cos . (x + (((2 * n) + 1) * PI))))) by Th90 .= (1 / 2) * (((cos x) * (cos (x + ((2 * n) * PI)))) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI))))) by Th3 .= (1 / 2) * (((cos x) * (cos x)) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI))))) by Th3 .= (1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (cos (x + (((2 * n) + 1) * PI))))) by Th4 .= (1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (- (cos x)))) by Th4 .= 0 ; hence integral ((sin (#) cos),A) = 0 ; ::_thesis: verum end; Lm20: for A being non empty closed_interval Subset of REAL holds ( cos (#) cos is_integrable_on A & (cos (#) cos) | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( cos (#) cos is_integrable_on A & (cos (#) cos) | A is bounded ) dom cos = REAL by FUNCT_2:def_1; then A c= (dom cos) /\ (dom cos) ; then A1: A c= dom (cos (#) cos) by VALUED_1:def_4; (cos (#) cos) | A is continuous ; hence ( cos (#) cos is_integrable_on A & (cos (#) cos) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem :: INTEGRA8:97 for A being non empty closed_interval Subset of REAL holds integral ((sin (#) sin),A) = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sin (#) sin),A) = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A)) A1: [#] REAL is open Subset of REAL ; A2: ((cos (#) cos) || A) | A is bounded by Lm20, INTEGRA5:9; sin | A is continuous ; then A3: (- cos) `| REAL is_integrable_on A by Lm5, Th29, INTEGRA5:11; dom (cos (#) cos) = REAL by FUNCT_2:def_1; then A4: (cos (#) cos) || A is Function of A,REAL by FUNCT_2:68, INTEGRA5:6; cos | A is continuous ; then A5: sin `| REAL is_integrable_on A by Lm6, Th27, INTEGRA5:11; cos (#) cos is_integrable_on A by Lm20; then A6: (cos (#) cos) || A is integrable by INTEGRA5:def_1; ( ((- cos) `| REAL) | A is bounded & (sin `| REAL) | A is bounded ) by Lm5, Lm6, Th27, Th29, INTEGRA5:10; then integral ((sin (#) sin),A) = ((((- cos) . (upper_bound A)) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) by A3, A5, A1, Th26, Th27, Th29, INTEGRA5:21, SIN_COS:68 .= (((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) by VALUED_1:8 .= (((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - ((- (cos . (lower_bound A))) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) by VALUED_1:8 .= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- (cos (#) cos)),A)) by RFUNCT_1:12 .= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- 1) (#) ((cos (#) cos) || A))) by RFUNCT_1:49 .= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - ((- 1) * (integral ((cos (#) cos),A))) by A6, A2, A4, INTEGRA2:31 .= (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A)) ; hence integral ((sin (#) sin),A) = (((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A)) ; ::_thesis: verum end; theorem :: INTEGRA8:98 for A being non empty closed_interval Subset of REAL holds integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A)) A1: [#] REAL is open Subset of REAL ; A2: ( sinh `| REAL is_integrable_on A & (sinh `| REAL) | A is bounded ) by Lm17, Th30; ( cosh `| REAL is_integrable_on A & (cosh `| REAL) | A is bounded ) by Lm15, Th31; hence integral ((sinh (#) sinh),A) = (((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A)) by A2, A1, Th30, Th31, INTEGRA5:21, SIN_COS2:34, SIN_COS2:35; ::_thesis: verum end; theorem :: INTEGRA8:99 for A being non empty closed_interval Subset of REAL holds integral ((sinh (#) cosh),A) = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((sinh (#) cosh),A) = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) sinh | A is continuous by Lm14; then A1: cosh `| REAL is_integrable_on A by Lm9, Th31, INTEGRA5:11; ( (cosh `| REAL) | A is bounded & [#] REAL is open Subset of REAL ) by Lm9, Lm14, Th31, INTEGRA5:10; then integral ((sinh (#) cosh),A) = (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) - (integral ((sinh (#) cosh),A)) by A1, Th31, INTEGRA5:21, SIN_COS2:35; hence integral ((sinh (#) cosh),A) = (1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) ; ::_thesis: verum end; theorem :: INTEGRA8:100 for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) exp_R),A) = (1 / 2) * (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((exp_R (#) exp_R),A) = (1 / 2) * (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) exp_R | A is continuous ; then A1: exp_R `| REAL is_integrable_on A by Lm8, Th32, INTEGRA5:11; ( (exp_R `| REAL) | A is bounded & [#] REAL is open Subset of REAL ) by Lm8, Th32, INTEGRA5:10; then integral ((exp_R (#) exp_R),A) = (((exp_R . (upper_bound A)) * (exp_R . (upper_bound A))) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral ((exp_R (#) exp_R),A)) by A1, Th32, INTEGRA5:21, SIN_COS:66 .= (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral ((exp_R (#) exp_R),A)) .= (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) - (integral ((exp_R (#) exp_R),A)) ; hence integral ((exp_R (#) exp_R),A) = (1 / 2) * (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) ; ::_thesis: verum end; Lm21: for A being non empty closed_interval Subset of REAL holds ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) A1: dom (sin + cos) = (dom sin) /\ (dom cos) by VALUED_1:def_1; ( dom sin = REAL & dom cos = REAL ) by FUNCT_2:def_1; then A c= (dom exp_R) /\ (dom (sin + cos)) by A1, SIN_COS:47; then A2: A c= dom (exp_R (#) (sin + cos)) by VALUED_1:def_4; (exp_R (#) (sin + cos)) | A is continuous ; hence ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) by A2, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; Lm22: for A being non empty closed_interval Subset of REAL holds ( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded ) proof let A be non empty closed_interval Subset of REAL; ::_thesis: ( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded ) ( dom exp_R = REAL & dom (cos - sin) = REAL ) by FUNCT_2:def_1; then A c= (dom exp_R) /\ (dom (cos - sin)) ; then A1: A c= dom (exp_R (#) (cos - sin)) by VALUED_1:def_4; (exp_R (#) (cos - sin)) | A is continuous ; hence ( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded ) by A1, INTEGRA5:10, INTEGRA5:11; ::_thesis: verum end; theorem :: INTEGRA8:101 for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) A1: dom (sin + cos) = REAL by FUNCT_2:def_1; A2: dom (exp_R (#) (sin + cos)) = (dom exp_R) /\ (dom (sin + cos)) by VALUED_1:def_4 .= REAL /\ (dom (sin + cos)) by SIN_COS:47 .= REAL by A1 ; A3: ( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded ) by Lm21; A4: ( dom (exp_R (#) sin) = REAL & [#] REAL is open Subset of REAL ) by FUNCT_2:def_1; A5: for x being Real st x in dom ((exp_R (#) sin) `| REAL) holds ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x proof let x be Real; ::_thesis: ( x in dom ((exp_R (#) sin) `| REAL) implies ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x ) assume x in dom ((exp_R (#) sin) `| REAL) ; ::_thesis: ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x (exp_R (#) (sin + cos)) . x = (exp_R . x) * ((sin + cos) . x) by VALUED_1:5 .= (exp_R . x) * ((sin . x) + (cos . x)) by VALUED_1:1 ; hence ((exp_R (#) sin) `| REAL) . x = (exp_R (#) (sin + cos)) . x by A4, FDIFF_7:44; ::_thesis: verum end; exp_R (#) sin is_differentiable_on REAL by A4, FDIFF_7:44; then dom ((exp_R (#) sin) `| REAL) = dom (exp_R (#) (sin + cos)) by A2, FDIFF_1:def_7; then (exp_R (#) sin) `| REAL = exp_R (#) (sin + cos) by A5, PARTFUN1:5; hence integral ((exp_R (#) (sin + cos)),A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) by A3, A4, FDIFF_7:44, INTEGRA5:13; ::_thesis: verum end; theorem :: INTEGRA8:102 for A being non empty closed_interval Subset of REAL holds integral ((exp_R (#) (cos - sin)),A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) proof let A be non empty closed_interval Subset of REAL; ::_thesis: integral ((exp_R (#) (cos - sin)),A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) A1: ( dom (exp_R (#) cos) = REAL & [#] REAL is open Subset of REAL ) by FUNCT_2:def_1; A2: dom (cos - sin) = REAL by FUNCT_2:def_1; A3: for x being Real st x in dom ((exp_R (#) cos) `| REAL) holds ((exp_R (#) cos) `| REAL) . x = (exp_R (#) (cos - sin)) . x proof let x be Real; ::_thesis: ( x in dom ((exp_R (#) cos) `| REAL) implies ((exp_R (#) cos) `| REAL) . x = (exp_R (#) (cos - sin)) . x ) assume x in dom ((exp_R (#) cos) `| REAL) ; ::_thesis: ((exp_R (#) cos) `| REAL) . x = (exp_R (#) (cos - sin)) . x (exp_R (#) (cos - sin)) . x = (exp_R . x) * ((cos - sin) . x) by VALUED_1:5 .= (exp_R . x) * ((cos . x) - (sin . x)) by A2, VALUED_1:13 ; hence ((exp_R (#) cos) `| REAL) . x = (exp_R (#) (cos - sin)) . x by A1, FDIFF_7:45; ::_thesis: verum end; A4: ( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded ) by Lm22; A5: dom (exp_R (#) (cos - sin)) = (dom exp_R) /\ (dom (cos - sin)) by VALUED_1:def_4 .= REAL /\ (dom (cos - sin)) by SIN_COS:47 .= REAL by A2 ; exp_R (#) cos is_differentiable_on REAL by A1, FDIFF_7:45; then dom ((exp_R (#) cos) `| REAL) = dom (exp_R (#) (cos - sin)) by A5, FDIFF_1:def_7; then (exp_R (#) cos) `| REAL = exp_R (#) (cos - sin) by A3, PARTFUN1:5; hence integral ((exp_R (#) (cos - sin)),A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) by A4, A1, FDIFF_7:45, INTEGRA5:13; ::_thesis: verum end;