:: 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


Lm1: [#] REAL = dom (AffineMap ((1 / 2),0))
by FUNCT_2:def 1;

Lm2: [#] REAL = dom (sin * (AffineMap (2,0)))
by FUNCT_2:def 1;

Lm3: dom ((1 / 4) (#) (sin * (AffineMap (2,0)))) = [#] REAL
by FUNCT_2:def 1;

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

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

:: f.x = (1/(n+1))*(sin.x)^(n+1)
theorem Th3: :: INTEGR11:3
for n being Element of NAT holds
( (1 / (n + 1)) (#) ((#Z (n + 1)) * sin) is_differentiable_on REAL & ( for x being Real holds (((1 / (n + 1)) (#) ((#Z (n + 1)) * sin)) `| REAL) . x = ((sin . x) #Z n) * (cos . x) ) )
proof end;

:: f.x = (-1/(n+1))*(cos.x)^(n+1)
theorem Th4: :: INTEGR11:4
for n being Element of NAT holds
( (- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos) is_differentiable_on REAL & ( for x being Real holds (((- (1 / (n + 1))) (#) ((#Z (n + 1)) * cos)) `| REAL) . x = ((cos . x) #Z n) * (sin . x) ) )
proof end;

:: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n))
theorem Th5: :: INTEGR11:5
for n, m being Element of NAT st m + n <> 0 & m - n <> 0 holds
( ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) + ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real 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)) ) )
proof end;

:: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n))
theorem Th6: :: INTEGR11:6
for n, m being Element of NAT st m + n <> 0 & m - n <> 0 holds
( ((1 / (2 * (m - n))) (#) (sin * (AffineMap ((m - n),0)))) - ((1 / (2 * (m + n))) (#) (sin * (AffineMap ((m + n),0)))) is_differentiable_on REAL & ( for x being Real 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)) ) )
proof end;

:: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n))
theorem Th7: :: INTEGR11:7
for n, m being Element of NAT st m + n <> 0 & m - n <> 0 holds
( (- ((1 / (2 * (m + n))) (#) (cos * (AffineMap ((m + n),0))))) - ((1 / (2 * (m - n))) (#) (cos * (AffineMap ((m - n),0)))) is_differentiable_on REAL & ( for x being Real 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)) ) )
proof end;

:: f.x = (1/(n^2))*sin.(n*x)-(1/n)*x*cos.(n*x)
theorem Th8: :: INTEGR11:8
for n being Element of NAT st n <> 0 holds
( ((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (sin * (AffineMap (n,0)))) - ((AffineMap ((1 / n),0)) (#) (cos * (AffineMap (n,0))))) `| REAL) . x = x * (sin . (n * x)) ) )
proof end;

:: f.x = (1/(n^2))*cos.(n*x)+(1/n)*x*sin.(n*x)
theorem Th9: :: INTEGR11:9
for n being Element of NAT st n <> 0 holds
( ((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0)))) is_differentiable_on REAL & ( for x being Real holds ((((1 / (n ^2)) (#) (cos * (AffineMap (n,0)))) + ((AffineMap ((1 / n),0)) (#) (sin * (AffineMap (n,0))))) `| REAL) . x = x * (cos . (n * x)) ) )
proof end;

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

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

:: f.x = (1/(a*(n+1)))*(a*x+b)^(n+1)
theorem Th12: :: INTEGR11:12
for a, b being Real
for n being Element of NAT st a * (n + 1) <> 0 holds
( (1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b))) is_differentiable_on REAL & ( for x being Real holds (((1 / (a * (n + 1))) (#) ((#Z (n + 1)) * (AffineMap (a,b)))) `| REAL) . x = ((a * x) + b) #Z n ) )
proof end;

:: f.x = (sin.x)^2
theorem Th13: :: INTEGR11:13
for A being non empty closed_interval Subset of REAL holds 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))
proof end;

Lm4: dom (AffineMap (2,0)) = [#] REAL
by FUNCT_2:def 1;

Lm5: dom ((AffineMap ((1 / 2),0)) - ((1 / 4) (#) (sin * (AffineMap (2,0))))) = REAL
by FUNCT_2:def 1;

reconsider pp = PI as Element of REAL by XREAL_0:def 1;

Lm6: 0 in REAL
by XREAL_0:def 1;

theorem :: INTEGR11:14
for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
integral ((sin ^2),A) = PI / 2
proof end;

reconsider dp = 2 * PI, ddp = (2 * (2 * PI)) + 0 as Element of REAL by XREAL_0:def 1;

theorem :: INTEGR11:15
for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((sin ^2),A) = PI
proof end;

:: f.x = (cos.x)^2
theorem Th16: :: INTEGR11:16
for A being non empty closed_interval Subset of REAL holds 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))
proof end;

theorem :: INTEGR11:17
for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
integral ((cos ^2),A) = PI / 2
proof end;

theorem :: INTEGR11:18
for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((cos ^2),A) = PI
proof end;

:: f.x = (sin.x)^n*(cos.x)
theorem Th19: :: INTEGR11:19
for n being Element of NAT
for A being non empty closed_interval Subset of REAL holds 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))
proof end;

theorem :: INTEGR11:20
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds
integral ((((#Z n) * sin) (#) cos),A) = 0
proof end;

theorem :: INTEGR11:21
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((((#Z n) * sin) (#) cos),A) = 0
proof end;

:: f.x = (cos.x)^n*(sin.x)
theorem Th22: :: INTEGR11:22
for n being Element of NAT
for A being non empty closed_interval Subset of REAL holds 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))
proof end;

theorem :: INTEGR11:23
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0
proof end;

reconsider pd = PI / 2, mpd = - (PI / 2) as Element of REAL by XREAL_0:def 1;

theorem :: INTEGR11:24
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st A = [.(- (PI / 2)),(PI / 2).] holds
integral ((((#Z n) * cos) (#) sin),A) = 0
proof end;

:: f.x = cos.(m*x)*cos.(n*x)
theorem :: INTEGR11:25
for n, m being Element of NAT
for A being non empty closed_interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
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))
proof end;

:: f.x = sin.(m*x)*sin.(n*x)
theorem :: INTEGR11:26
for n, m being Element of NAT
for A being non empty closed_interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
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))
proof end;

:: f.x = sin.(m*x)*cos.(n*x)
theorem :: INTEGR11:27
for n, m being Element of NAT
for A being non empty closed_interval Subset of REAL st m + n <> 0 & m - n <> 0 holds
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))
proof end;

:: f.x = x*sin.(n*x)
theorem :: INTEGR11:28
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
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))
proof end;

:: f.x = x*cos.(n*x)
theorem :: INTEGR11:29
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st n <> 0 holds
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))
proof end;

theorem :: INTEGR11:30
for A being non empty closed_interval Subset of REAL holds integral (((AffineMap (1,0)) (#) sinh),A) = ((((AffineMap (1,0)) (#) cosh) - sinh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) cosh) - sinh) . (lower_bound A))
proof end;

theorem :: INTEGR11:31
for A being non empty closed_interval Subset of REAL holds integral (((AffineMap (1,0)) (#) cosh),A) = ((((AffineMap (1,0)) (#) sinh) - cosh) . (upper_bound A)) - ((((AffineMap (1,0)) (#) sinh) - cosh) . (lower_bound A))
proof end;

:: f.x = (a*x+b)^n
theorem :: INTEGR11:32
for a, b being Real
for n being Element of NAT
for A being non empty closed_interval Subset of REAL st a * (n + 1) <> 0 holds
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))
proof end;

:: f.x = (1/2)*x^2
theorem Th33: :: INTEGR11:33
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) f) & f = #Z 2 holds
( (1 / 2) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / 2) (#) f) `| Z) . x = x ) )
proof end;

:: f.x = x
theorem :: INTEGR11:34
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & f = #Z 2 & Z = dom ((1 / 2) (#) f) holds
integral ((id Z),A) = (((1 / 2) (#) f) . (upper_bound A)) - (((1 / 2) (#) f) . (lower_bound A))
proof end;

:: f.x = -1/x^2 :: INTEGRA9
theorem :: INTEGR11:35
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st not 0 in Z & A c= Z & ( for x being Real st x in Z holds
( x <> 0 & f . x = - (1 / (x ^2)) ) ) & dom f = Z & f | A is continuous holds
integral (f,A) = (((id Z) ^) . (upper_bound A)) - (((id Z) ^) . (lower_bound A))
proof end;

:: f.x = 2*x/(1+x^2)^2
theorem :: INTEGR11:36
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st A c= Z & f1 = #Z 2 & ( for x being Real 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 holds
integral (f,A) = ((f1 / (f2 + f1)) . (upper_bound A)) - ((f1 / (f2 + f1)) . (lower_bound A))
proof end;

theorem Th37: :: INTEGR11:37
for Z being open Subset of REAL st Z c= dom (tan + sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( tan + sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan + sec) `| Z) . x = 1 / (1 - (sin . x)) ) )
proof end;

:: f.x = 1/(1-sin.x)
theorem :: INTEGR11:38
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((tan + sec) . (upper_bound A)) - ((tan + sec) . (lower_bound A))
proof end;

theorem Th39: :: INTEGR11:39
for Z being open Subset of REAL st Z c= dom (tan - sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( tan - sec is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - sec) `| Z) . x = 1 / (1 + (sin . x)) ) )
proof end;

:: f.x = 1/(1+sin.x)
theorem :: INTEGR11:40
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((tan - sec) . (upper_bound A)) - ((tan - sec) . (lower_bound A))
proof end;

theorem Th41: :: INTEGR11:41
for Z being open Subset of REAL st Z c= dom ((- cot) + cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( (- cot) + cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) + cosec) `| Z) . x = 1 / (1 + (cos . x)) ) )
proof end;

:: f.x = 1/(1+cos.x)
theorem :: INTEGR11:42
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = (((- cot) + cosec) . (upper_bound A)) - (((- cot) + cosec) . (lower_bound A))
proof end;

theorem Th43: :: INTEGR11:43
for Z being open Subset of REAL st Z c= dom ((- cot) - cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( (- cot) - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - cosec) `| Z) . x = 1 / (1 - (cos . x)) ) )
proof end;

:: f.x = 1/(1-cos.x)
theorem :: INTEGR11:44
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = (((- cot) - cosec) . (upper_bound A)) - (((- cot) - cosec) . (lower_bound A))
proof end;

:: f.x = 1/(1+x^2)
theorem :: INTEGR11:45
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = 1 / (1 + (x ^2)) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (arctan . (upper_bound A)) - (arctan . (lower_bound A))
proof end;

:: f.x = r/(1+x^2)
theorem :: INTEGR11:46
for r being Real
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = r / (1 + (x ^2)) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((r (#) arctan) . (upper_bound A)) - ((r (#) arctan) . (lower_bound A))
proof end;

:: f.x = -1/(1+x^2)
theorem :: INTEGR11:47
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = - (1 / (1 + (x ^2))) ) & Z = dom f & f | A is continuous holds
integral (f,A) = (arccot . (upper_bound A)) - (arccot . (lower_bound A))
proof end;

:: f.x = -r/(1+x^2)
theorem :: INTEGR11:48
for r being Real
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
f . x = - (r / (1 + (x ^2))) ) & Z = dom f & f | A is continuous holds
integral (f,A) = ((r (#) arccot) . (upper_bound A)) - ((r (#) arccot) . (lower_bound A))
proof end;

:: f.x = x+cot.x-cosec.x
theorem Th49: :: INTEGR11:49
for Z being open Subset of REAL st Z c= dom (((id Z) + cot) - cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( ((id Z) + cot) - cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) + cot) - cosec) `| Z) . x = (cos . x) / (1 + (cos . x)) ) )
proof end;

:: f.x = cos.x/(1+cos.x)
theorem :: INTEGR11:50
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((((id Z) + cot) - cosec) . (upper_bound A)) - ((((id Z) + cot) - cosec) . (lower_bound A))
proof end;

:: f.x = x+cot.x+cosec.x
theorem Th51: :: INTEGR11:51
for Z being open Subset of REAL st Z c= dom (((id Z) + cot) + cosec) & ( for x being Real st x in Z holds
( 1 + (cos . x) <> 0 & 1 - (cos . x) <> 0 ) ) holds
( ((id Z) + cot) + cosec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) + cot) + cosec) `| Z) . x = (cos . x) / ((cos . x) - 1) ) )
proof end;

:: f.x = cos.x/(cos.x-1)
theorem :: INTEGR11:52
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((((id Z) + cot) + cosec) . (upper_bound A)) - ((((id Z) + cot) + cosec) . (lower_bound A))
proof end;

:: f.x = x-tan.x+sec.x
theorem Th53: :: INTEGR11:53
for Z being open Subset of REAL st Z c= dom (((id Z) - tan) + sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( ((id Z) - tan) + sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) - tan) + sec) `| Z) . x = (sin . x) / ((sin . x) + 1) ) )
proof end;

:: f.x = sin.x/(1+sin.x)
theorem :: INTEGR11:54
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((((id Z) - tan) + sec) . (upper_bound A)) - ((((id Z) - tan) + sec) . (lower_bound A))
proof end;

:: f.x = x-tan.x-sec.x
theorem Th55: :: INTEGR11:55
for Z being open Subset of REAL st Z c= dom (((id Z) - tan) - sec) & ( for x being Real st x in Z holds
( 1 + (sin . x) <> 0 & 1 - (sin . x) <> 0 ) ) holds
( ((id Z) - tan) - sec is_differentiable_on Z & ( for x being Real st x in Z holds
((((id Z) - tan) - sec) `| Z) . x = (sin . x) / ((sin . x) - 1) ) )
proof end;

:: f.x = sin.x/(sin.x-1)
theorem :: INTEGR11:56
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((((id Z) - tan) - sec) . (upper_bound A)) - ((((id Z) - tan) - sec) . (lower_bound A))
proof end;

:: f.x = tan.x-x
theorem Th57: :: INTEGR11:57
for Z being open Subset of REAL st Z c= dom (tan - (id Z)) holds
( tan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan - (id Z)) `| Z) . x = (tan . x) ^2 ) )
proof end;

:: f.x = (tan.x)^2
theorem :: INTEGR11:58
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((tan - (id Z)) . (upper_bound A)) - ((tan - (id Z)) . (lower_bound A))
proof end;

:: f.x = -cot.x-x
theorem Th59: :: INTEGR11:59
for Z being open Subset of REAL st Z c= dom ((- cot) - (id Z)) holds
( (- cot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds
(((- cot) - (id Z)) `| Z) . x = (cot . x) ^2 ) )
proof end;

:: f.x = (cot.x)^2
theorem :: INTEGR11:60
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = (((- cot) - (id Z)) . (upper_bound A)) - (((- cot) - (id Z)) . (lower_bound A))
proof end;

:: f.x = 1/(cos.x)^2
theorem :: INTEGR11:61
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = 1 / ((cos . x) ^2) & cos . x <> 0 ) ) & dom tan = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (tan . (upper_bound A)) - (tan . (lower_bound A))
proof end;

:: f.x = -1/(sin.x)^2
theorem :: INTEGR11:62
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real st x in Z holds
( f . x = - (1 / ((sin . x) ^2)) & sin . x <> 0 ) ) & dom cot = Z & Z = dom f & f | A is continuous holds
integral (f,A) = (cot . (upper_bound A)) - (cot . (lower_bound A))
proof end;

:: f.x = (sin.x-(cos.x)^2)/(cos.x)^2
theorem :: INTEGR11:63
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = ((sec - (id Z)) . (upper_bound A)) - ((sec - (id Z)) . (lower_bound A))
proof end;

:: f.x = (cos.x-(sin.x)^2)/(sin.x)^2
theorem :: INTEGR11:64
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & ( for x being Real 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 holds
integral (f,A) = (((- cosec) - (id Z)) . (upper_bound A)) - (((- cosec) - (id Z)) . (lower_bound A))
proof end;

:: f.x = cot(x)
theorem :: INTEGR11:65
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds
sin . x > 0 ) & Z c= dom (ln * sin) & Z = dom cot & cot | A is continuous holds
integral (cot,A) = ((ln * sin) . (upper_bound A)) - ((ln * sin) . (lower_bound A))
proof end;

:: f.x = arcsin.x / sqrt(1-x^2)
theorem :: INTEGR11:66
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real 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 holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arcsin)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arcsin)) . (lower_bound A))
proof end;

:: f.x = -arccos.x / sqrt(1-x^2)
theorem :: INTEGR11:67
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & ( for x being Real 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 holds
integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccos)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccos)) . (lower_bound A))
proof end;

:: f.x = arcsin.x
theorem :: INTEGR11:68
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real 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)) holds
integral (arcsin,A) = ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arcsin) + ((#R (1 / 2)) * f)) . (lower_bound A))
proof end;

:: f.x = arcsin.(x/a)
theorem :: INTEGR11:69
for a being Real
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2, f3 being PartFunc of REAL,REAL st A c= Z & f = f1 - f2 & f2 = #Z 2 & ( for x being Real 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 holds
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))
proof end;

:: f.x = arccos.x
theorem :: INTEGR11:70
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f = f1 - f2 & f2 = #Z 2 & ( for x being Real 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)) holds
integral (arccos,A) = ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) . (upper_bound A)) - ((((id Z) (#) arccos) - ((#R (1 / 2)) * f)) . (lower_bound A))
proof end;

:: f.x = arccos.(x/a)
theorem :: INTEGR11:71
for a being Real
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f, f1, f2, f3 being PartFunc of REAL,REAL st A c= Z & f = f1 - f2 & f2 = #Z 2 & ( for x being Real 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 holds
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))
proof end;

:: f.x = arctan.x
theorem :: INTEGR11:72
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) & Z = dom arctan & Z = dom (((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) holds
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))
proof end;

:: f.x = arccot.x
theorem :: INTEGR11:73
for A being non empty closed_interval Subset of REAL
for Z being open Subset of REAL
for f1, f2 being PartFunc of REAL,REAL st A c= Z & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds
f1 . x = 1 ) & dom arccot = Z & Z = dom (((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) holds
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))
proof end;