:: 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-2012 Association of Mizar Users begin 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 ) ) proofend; :: 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 ) ) proofend; :: 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) ) ) proofend; :: 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) ) ) proofend; :: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n)) theorem Th5: :: INTEGR11:5 for m, n 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)) ) ) proofend; :: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n)) theorem Th6: :: INTEGR11:6 for m, n 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)) ) ) proofend; :: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n)) theorem Th7: :: INTEGR11:7 for m, n 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)) ) ) proofend; :: 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)) ) ) proofend; :: 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)) ) ) proofend; :: 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) ) ) proofend; :: 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) ) ) proofend; :: 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 ) ) proofend; begin :: 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)) proofend; 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; theorem :: INTEGR11:14 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((sin ^2),A) = PI / 2 proofend; theorem :: INTEGR11:15 for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds integral ((sin ^2),A) = PI proofend; :: 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)) proofend; theorem :: INTEGR11:17 for A being non empty closed_interval Subset of REAL st A = [.0,PI.] holds integral ((cos ^2),A) = PI / 2 proofend; theorem :: INTEGR11:18 for A being non empty closed_interval Subset of REAL st A = [.0,(2 * PI).] holds integral ((cos ^2),A) = PI proofend; :: 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)) proofend; 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 proofend; 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 proofend; :: 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)) proofend; 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 proofend; 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 proofend; :: f.x = cos.(m*x)*cos.(n*x) theorem :: INTEGR11:25 for m, n 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)) proofend; :: f.x = sin.(m*x)*sin.(n*x) theorem :: INTEGR11:26 for m, n 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)) proofend; :: f.x = sin.(m*x)*cos.(n*x) theorem :: INTEGR11:27 for m, n 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)) proofend; :: 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)) proofend; :: 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)) proofend; 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)) proofend; 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)) proofend; :: 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)) proofend; begin :: 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 ) ) proofend; :: 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)) proofend; :: 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)) proofend; :: 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 f1, f2, f 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)) proofend; 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)) ) ) proofend; :: 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)) proofend; 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)) ) ) proofend; :: 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)) proofend; 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)) ) ) proofend; :: 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)) proofend; 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)) ) ) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) ) ) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend; :: 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) ) ) proofend; :: 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)) proofend; :: 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 ) ) proofend; :: 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)) proofend; :: 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 ) ) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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)) proofend; :: 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 f2, f1 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)) proofend; :: 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 f2, f1 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)) proofend;