:: Several Integrability Formulas of Special Functions -- Part {II}
::  by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang
::
:: Received October 14, 2008
:: Copyright (c) 2008-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies REAL_1, SUBSET_1, NUMBERS, INTEGRA1, RCOMP_1, RELAT_1, JGRAPH_2,
      ARYTM_3, CARD_1, SIN_COS, VALUED_1, ARYTM_1, FDIFF_1, FUNCT_1, SQUARE_1,
      PREPOWER, SIN_COS2, ORDINAL2, XXREAL_2, XXREAL_1, INTEGRA5, XBOOLE_0,
      PARTFUN1, TARSKI, ORDINAL4, SIN_COS4, SIN_COS9, XXREAL_0, TAYLOR_1,
      SIN_COS6, SEQ_4, MEASURE5;
 notations TARSKI, XBOOLE_0, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS,
      RELAT_1, VALUED_1, XXREAL_0, XCMPLX_0, REAL_1, XREAL_0, PARTFUN1,
      PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
      PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS2, FDIFF_9, SIN_COS4,
      SIN_COS6, SIN_COS9, SEQ_4;
 constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
      INTEGRA5, SIN_COS2, SEQ_4, SIN_COS9, PARTFUN2, SIN_COS6, RFUNCT_1,
      FDIFF_9, SIN_COS4, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, SERIES_1,
      BINOP_2;
 registrations VALUED_1, NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1,
      ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1, TOPREALB, FCONT_3, MEASURE5,
      XREAL_0, SIN_COS, PREPOWER, SQUARE_1;
 requirements NUMERALS, BOOLE, SUBSET, ARITHM;


begin :: Differentiation Formulas

reserve r,x,x0,a,b for Real;
reserve n,m for Element of NAT;
reserve A for non empty closed_interval Subset of REAL;
reserve Z for open Subset of REAL;

:: f.x = (1/2)*x-(1/4)*sin(2*x)

theorem :: INTEGR11:1
  AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)-(1/4)(#)(sin*
  AffineMap(2,0)))`|REAL).x = (sin.x)^2;

:: f.x = (1/2)*x+(1/4)*sin(2*x)

theorem :: INTEGR11:2
  AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))
  is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)+(1/4)(#)(sin*
  AffineMap(2,0)))`|REAL).x = (cos.x)^2;

:: f.x = (1/(n+1))*(sin.x)^(n+1)

theorem :: INTEGR11:3
  (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL & for x
  holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x = ((sin.x) #Z n)*cos.x;

:: f.x = (-1/(n+1))*(cos.x)^(n+1)

theorem :: INTEGR11:4
  (-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL & for x
  holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x = ((cos.x) #Z n)*sin.x;

:: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n))

theorem :: INTEGR11:5
  m+n<>0 & m-n<>0 implies ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
(1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)
  ))`|REAL).x = cos.(m*x) *cos.(n*x);

:: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n))

theorem :: INTEGR11:6
  m+n<>0 & m-n<>0 implies ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
(1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL & for x holds
(((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)
  ))`|REAL).x = sin.(m*x)*sin.(n*x);

:: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n))

theorem :: INTEGR11:7
  m+n<>0 & m-n<>0 implies ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))
  ) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL & for x
  holds ((-((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
  AffineMap(m-n,0)))`|REAL).x = sin.(m*x) * cos.(n*x);

:: f.x = (1/(n^2))*sin.(n*x)-(1/n)*x*cos.(n*x)

theorem :: INTEGR11:8
  n<>0 implies ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)
  )(#)(cos*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x=x*
  sin.(n*x);

:: f.x = (1/(n^2))*cos.(n*x)+(1/n)*x*sin.(n*x)

theorem :: INTEGR11:9
  n<>0 implies ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)
  )(#)(sin*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2))
(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x=x*
  cos.(n*x);

:: f.x = x*cosh.x-sinh.x

theorem :: INTEGR11:10
  (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL & for x
  holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x=x*sinh.x;

:: f.x = x*sinh.x-cosh.x

theorem :: INTEGR11:11
  (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL & for x
  holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x=x*cosh.x;

:: f.x = (1/(a*(n+1)))*(a*x+b)^(n+1)

theorem :: INTEGR11:12
  a*(n+1) <> 0 implies (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))
is_differentiable_on REAL & for x holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(
  a,b)))`|REAL).x = (a*x+b) #Z n;

begin :: Integrability Formulas
:: f.x = (sin.x)^2

theorem :: INTEGR11:13
  integral(sin^2,A) = (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0
  ))).(upper_bound A) -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).
  (lower_bound A);

theorem :: INTEGR11:14
  A = [.0,PI.] implies integral(sin^2,A) = PI/2;

theorem :: INTEGR11:15
  A = [.0,2*PI.] implies integral(sin^2,A) = PI;

:: f.x = (cos.x)^2

theorem :: INTEGR11:16
  integral(cos^2,A) = (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0
  ))).(upper_bound A) -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).
  (lower_bound A);

theorem :: INTEGR11:17
  A = [.0,PI.] implies integral(cos^2,A) = PI/2;

theorem :: INTEGR11:18
  A = [.0,2*PI.] implies integral(cos^2,A) = PI;

:: f.x = (sin.x)^n*(cos.x)

theorem :: INTEGR11:19
  integral(( #Z n*sin)(#)cos,A) = ((1/(n+1))(#)( #Z (n+1)*sin)).(
  upper_bound A) -((1/(n+1))(#)( #Z (n+1)*sin)).(lower_bound A);

theorem :: INTEGR11:20
  A = [.0,PI.] implies integral(( #Z n*sin)(#)cos,A) = 0;

theorem :: INTEGR11:21
  A = [.0,2*PI.] implies integral(( #Z n*sin)(#)cos,A) = 0;

:: f.x = (cos.x)^n*(sin.x)

theorem :: INTEGR11:22
  integral(( #Z n*cos)(#)sin,A) = ((-1/(n+1))(#)( #Z (n+1)*cos)).(
  upper_bound A) -((-1/(n+1))(#)( #Z (n+1)*cos)).(lower_bound A);

theorem :: INTEGR11:23
  A = [.0,2*PI.] implies integral(( #Z n*cos)(#)sin,A) = 0;

theorem :: INTEGR11:24
  A = [.-PI/2,PI/2.] implies integral(( #Z n*cos)(#)sin,A) = 0;

:: f.x = cos.(m*x)*cos.(n*x)

theorem :: INTEGR11:25
  m+n<>0 & m-n<>0 implies integral((cos*AffineMap(m,0))(#)(cos*AffineMap
  (n,0)),A) = ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*
AffineMap(m-n,0))).(upper_bound A) -((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+
 (1/(2*(m-n
  )))(#)(sin*AffineMap(m-n,0))).(lower_bound A);

:: f.x = sin.(m*x)*sin.(n*x)

theorem :: INTEGR11:26
  m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(sin*AffineMap
  (n,0)),A) = ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*
AffineMap(m+n,0))).(upper_bound A) -((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))-
 (1/(2*(m+n
  )))(#)(sin*AffineMap(m+n,0))).(lower_bound A);

:: f.x = sin.(m*x)*cos.(n*x)

theorem :: INTEGR11:27
  m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(cos*AffineMap
  (n,0)),A) = ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos*
AffineMap(m-n,0))).(upper_bound A) -((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))
- (1/(2*(
  m-n)))(#)(cos*AffineMap(m-n,0))).(lower_bound A);

:: f.x = x*sin.(n*x)

theorem :: INTEGR11:28
  n<>0 implies integral((AffineMap(1,0))(#)(sin*AffineMap(n,0)),A) = ((1
/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)
  )).(lower_bound A);

:: f.x = x*cos.(n*x)

theorem :: INTEGR11:29
  n<>0 implies integral((AffineMap(1,0))(#)(cos*AffineMap(n,0)),A) = ((1
/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0))).
(upper_bound
A) -((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)
  )).(lower_bound A);

theorem :: INTEGR11:30
  integral((AffineMap(1,0))(#)sinh,A) = ((AffineMap(1,0))(#)cosh-sinh).(
  upper_bound A) -((AffineMap(1,0))(#)cosh-sinh).(lower_bound A);

theorem :: INTEGR11:31
  integral((AffineMap(1,0))(#)cosh,A) = ((AffineMap(1,0))(#)sinh-cosh).(
  upper_bound A) -((AffineMap(1,0))(#)sinh-cosh).(lower_bound A);

:: f.x = (a*x+b)^n

theorem :: INTEGR11:32
  a*(n+1) <> 0 implies integral( #Z n*AffineMap(a,b),A) = ((1/(a*(n+1)))
(#)( #Z (n+1)*AffineMap(a,b))).(upper_bound A) -
((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a
  ,b))).(lower_bound A);

begin :: Addenda

reserve f, f1, f2, f3 for PartFunc of REAL, REAL;

:: f.x = (1/2)*x^2

theorem :: INTEGR11:33
  Z c= dom ((1/2)(#)f) & f=#Z 2 implies (1/2)(#)f
  is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x = x;

:: f.x = x

theorem :: INTEGR11:34
  A c= Z & f=#Z 2 & Z = dom ((1/2)(#)f) implies integral(id Z,A) = ((1/2
  )(#)f).(upper_bound A)-((1/2)(#)f).(lower_bound A);

:: f.x = -1/x^2 :: INTEGRA9

theorem :: INTEGR11:35
  not 0 in Z & A c= Z & (for x st x in Z holds x<>0 & f.x = -1/x^2) &
dom f = Z & f|A is continuous implies integral(f,A) =
 ((id Z)^).(upper_bound A)-((id Z)
  ^).(lower_bound A);

:: f.x = 2*x/(1+x^2)^2

theorem :: INTEGR11:36
  A c= Z & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x
^2)^2) & dom (f1/(f2+f1))=Z & Z = dom f & f|A is continuous implies integral(f,
  A) = (f1/(f2+f1)).(upper_bound A)-(f1/(f2+f1)).(lower_bound A);

theorem :: INTEGR11:37
  (Z c= dom (tan+sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan+sec is_differentiable_on Z & for x st x in Z holds ((tan
  +sec)`|Z).x = 1/(1-sin.x);

:: f.x = 1/(1-sin.x)

theorem :: INTEGR11:38
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1-sin.x)) & dom (tan+sec)=Z & Z = dom f & f|A is continuous implies integral(f
  ,A) = (tan+sec).(upper_bound A)-(tan+sec).(lower_bound A);

theorem :: INTEGR11:39
  (Z c= dom (tan-sec) & for x st x in Z holds (1+sin.x)<>0 & (1-
sin.x)<>0) implies tan-sec is_differentiable_on Z & for x st x in Z holds ((tan
  -sec)`|Z).x = 1/(1+sin.x);

:: f.x = 1/(1+sin.x)

theorem :: INTEGR11:40
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/
(1+sin.x)) & dom (tan-sec)=Z & Z = dom f & f|A is continuous implies integral(f
  ,A) = (tan-sec).(upper_bound A)-(tan-sec).(lower_bound A);

theorem :: INTEGR11:41
  (Z c= dom (-cot+cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot+cosec is_differentiable_on Z & for x st x in Z holds (
  (-cot+cosec)`|Z).x = 1/(1+cos.x);

:: f.x = 1/(1+cos.x)

theorem :: INTEGR11:42
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
  (1+cos.x)) & dom (-cot+cosec)=Z & Z = dom f & f|A is continuous implies
  integral(f,A) = (-cot+cosec).(upper_bound A)-(-cot+cosec).(lower_bound A);

theorem :: INTEGR11:43
  (Z c= dom (-cot-cosec) & for x st x in Z holds (1+cos.x)<>0 & (1
-cos.x)<>0) implies -cot-cosec is_differentiable_on Z & for x st x in Z holds (
  (-cot-cosec)`|Z).x = 1/(1-cos.x);

:: f.x = 1/(1-cos.x)

theorem :: INTEGR11:44
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/
  (1-cos.x)) & dom (-cot-cosec)=Z & Z = dom f & f|A is continuous implies
  integral(f,A) = (-cot-cosec).(upper_bound A)-(-cot-cosec).(lower_bound A);

:: f.x = 1/(1+x^2)

theorem :: INTEGR11:45
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=1/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A)
 = arctan.(upper_bound A) - arctan.(lower_bound
  A);

:: f.x = r/(1+x^2)

theorem :: INTEGR11:46
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=r/(1+x^2)) & Z =
dom f & f|A is continuous implies integral(f,A) = (r(#)arctan).(upper_bound A)
 - (r(#)
  arctan).(lower_bound A);

:: f.x = -1/(1+x^2)

theorem :: INTEGR11:47
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-1/(1+x^2)) & Z
  = dom f & f|A is continuous implies integral(f,A) = arccot.(upper_bound A)
   - arccot.(
  lower_bound A);

:: f.x = -r/(1+x^2)

theorem :: INTEGR11:48
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-r/(1+x^2)) & Z
  = dom f & f|A is continuous implies integral(f,A)
   = (r(#)arccot).(upper_bound A) - (r
  (#)arccot).(lower_bound A);

:: f.x = x+cot.x-cosec.x

theorem :: INTEGR11:49
  (Z c= dom ((id Z)+cot-cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot-cosec is_differentiable_on Z & for x st x
  in Z holds ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x);

:: f.x = cos.x/(1+cos.x)

theorem :: INTEGR11:50
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
  cos.x/(1+cos.x)) & dom (id Z+cot-cosec)=Z & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z+cot-cosec).(upper_bound A)-(id Z+cot-cosec).(lower_bound A);

:: f.x = x+cot.x+cosec.x

theorem :: INTEGR11:51
  (Z c= dom ((id Z)+cot+cosec) & for x st x in Z holds (1+cos.x)<>
0 & (1-cos.x)<>0) implies (id Z)+cot+cosec is_differentiable_on Z & for x st x
  in Z holds ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1);

:: f.x = cos.x/(cos.x-1)

theorem :: INTEGR11:52
  A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x =
  cos.x/(cos.x-1)) & dom (id Z+cot+cosec)=Z & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z+cot+cosec).(upper_bound A)-(id Z+cot+cosec).(lower_bound A);

:: f.x = x-tan.x+sec.x

theorem :: INTEGR11:53
  (Z c= dom (id Z-tan+sec) & for x st x in Z holds (1+sin.x)<>0 &
  (1-sin.x)<>0) implies (id Z)-tan+sec is_differentiable_on Z & for x st x in Z
  holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1);

:: f.x = sin.x/(1+sin.x)

theorem :: INTEGR11:54
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
  sin.x/(1+sin.x)) & Z c= dom (id Z-tan+sec) & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z-tan+sec).(upper_bound A)-(id Z-tan+sec).(lower_bound A);

:: f.x = x-tan.x-sec.x

theorem :: INTEGR11:55
  (Z c= dom (id Z-tan-sec) & for x st x in Z holds (1+sin.x)<>0 &
  (1-sin.x)<>0) implies id Z-tan-sec is_differentiable_on Z & for x st x in Z
  holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1);

:: f.x = sin.x/(sin.x-1)

theorem :: INTEGR11:56
  A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x =
  sin.x/(sin.x-1)) & Z c= dom (id Z-tan-sec) & Z = dom f & f|A is continuous
  implies integral(f,A) =
   (id Z-tan-sec).(upper_bound A)-(id Z-tan-sec).(lower_bound A);

:: f.x = tan.x-x

theorem :: INTEGR11:57
  Z c= dom (tan-id Z) implies tan-id Z is_differentiable_on Z &
  for x st x in Z holds ((tan-id Z)`|Z).x=(tan.x)^2;

:: f.x = (tan.x)^2

theorem :: INTEGR11:58
  A c= Z & (for x st x in Z holds cos.x >0 & f.x = (tan.x)^2) & Z c= dom
(tan-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (tan-id Z).(
  upper_bound A)-(tan-id Z).(lower_bound A);

:: f.x = -cot.x-x

theorem :: INTEGR11:59
  Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z &
  for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2;

:: f.x = (cot.x)^2

theorem :: INTEGR11:60
  A c= Z & (for x st x in Z holds sin.x >0 & f.x = (cot.x)^2) & Z c= dom
(-cot-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (-cot-id Z)
  .(upper_bound A)-(-cot-id Z).(lower_bound A);

:: f.x = 1/(cos.x)^2

theorem :: INTEGR11:61
  A c= Z & (for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0) & dom
tan=Z & Z = dom f & f|A is continuous implies
 integral(f,A) = tan.(upper_bound A)-tan.(
  lower_bound A);

:: f.x = -1/(sin.x)^2

theorem :: INTEGR11:62
  A c= Z & (for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0) & dom
cot=Z & Z = dom f & f|A is continuous implies
 integral(f,A) = cot.(upper_bound A)-cot.(
  lower_bound A);

:: f.x = (sin.x-(cos.x)^2)/(cos.x)^2

theorem :: INTEGR11:63
  A c= Z & (for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2) & Z
c= dom (sec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) = (sec-
  id Z).(upper_bound A)-(sec-id Z).(lower_bound A);

:: f.x = (cos.x-(sin.x)^2)/(sin.x)^2

theorem :: INTEGR11:64
  A c= Z & (for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2) & Z
c= dom (-cosec-id Z) & Z = dom f & f|A is continuous implies integral(f,A) =(-
  cosec-id Z).(upper_bound A)-(-cosec-id Z).(lower_bound A);

:: f.x = cot(x)

theorem :: INTEGR11:65
  A c= Z & (for x st x in Z holds sin.x >0) & Z c= dom (ln*sin) & Z =
  dom cot & cot|A is continuous implies
   integral(cot,A) = (ln*sin).(upper_bound A)-(ln*
  sin).(lower_bound A);

:: f.x = arcsin.x / sqrt(1-x^2)

theorem :: INTEGR11:66
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=arcsin.x/sqrt(1-
  x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) & Z = dom f & f|A is continuous
implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arcsin))).(upper_bound A)
 -((1/2)(#)(( #Z 2)
  *(arcsin))).(lower_bound A);

:: f.x = -arccos.x / sqrt(1-x^2)

theorem :: INTEGR11:67
  A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-arccos.x / sqrt
  (1-x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) & Z = dom f & f|A is
continuous implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arccos))).(upper_bound A)
 -((1/2)
  (#)(( #Z 2)*(arccos))).(lower_bound A);

:: f.x = arcsin.x

theorem :: INTEGR11:68
  A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arcsin=Z & Z c= dom ((id Z)(#)(arcsin)+( #R (1/2)
)*f) implies integral(arcsin,A) =
 ((id Z)(#)(arcsin)+( #R (1/2))*f).(upper_bound A) -((
  id Z)(#)(arcsin) + ( #R (1/2))*f).(lower_bound A);

:: f.x = arcsin.(x/a)

theorem :: INTEGR11:69
  A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
  & f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arcsin)*f3)=Z & Z c=
  dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) & ((arcsin)*f3)|A is continuous
implies integral((arcsin)*f3,A) =
 ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(upper_bound A
  ) -((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(lower_bound A);

:: f.x = arccos.x

theorem :: INTEGR11:70
  A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=1 & f.x >0 & x<>0) & dom arccos=Z & Z c= dom ((id Z)(#)(arccos)-( #R (1/2)
)*f) implies integral(arccos,A)
 = ((id Z)(#)(arccos)-( #R (1/2))*f).(upper_bound A) -((
  id Z)(#)(arccos)-( #R (1/2))*f).(lower_bound A);

:: f.x = arccos.(x/a)

theorem :: INTEGR11:71
  A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0
& f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arccos)*f3)=Z & Z = dom
((id Z)(#)((arccos)*f3)-( #R (1/2))*f) & ((arccos)*f3)|A is continuous implies
integral((arccos)*f3,A) =
 ((id Z)(#)((arccos)*f3)-( #R (1/2))*f).(upper_bound A) -((id
  Z)(#)((arccos)*f3)-( #R (1/2))*f).(lower_bound A);

:: f.x = arctan.x

theorem :: INTEGR11:72
  A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1 ) &
  Z = dom arctan & Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) implies
integral(arctan,A) =
 ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
  (#)(arctan)-(1/2)(#)(ln*(f1+f2))).(lower_bound A);

:: f.x = arccot.x

theorem :: INTEGR11:73
  A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1) &
  dom arccot=Z & Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) implies
integral(arccot,A) =
 ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z)
  (#)(arccot)+(1/2)(#)(ln*(f1+f2))).(lower_bound A);