:: Integrability Formulas -- Part {II} :: by Bo Li , Na Ma and Xiquan Liang :: :: Received February 4, 2010 :: Copyright (c) 2010-2012 Association of Mizar Users begin Lm1: for Z being open Subset of REAL st 0 in Z holds (id Z) " {0} = {0} proofend; Lm2: right_open_halfline 0 = { g where g is Real : 0 < g } by XXREAL_1:230; Lm3: ( - 1 is Real & - (1 / 2) is Real & 1 / 2 is Real ) ; :: f.x = 1/(sin.x*cos.x) theorem :: INTEGR13:1 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (sin (#) cos) ^ & Z c= dom (ln * tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln * tan) . (upper_bound A)) - ((ln * tan) . (lower_bound A)) proofend; :: f.x = -1/(sin.x*cos.x) theorem :: INTEGR13:2 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = - ((sin (#) cos) ^) & Z c= dom (ln * cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln * cot) . (upper_bound A)) - ((ln * cot) . (lower_bound A)) proofend; ::f.x=2 * exp_R.x * sin.x theorem :: INTEGR13:3 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) sin) & Z c= dom (exp_R (#) (sin - cos)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) (sin - cos)) . (upper_bound A)) - ((exp_R (#) (sin - cos)) . (lower_bound A)) proofend; ::f.x=2 * exp_R.x * cos.x theorem :: INTEGR13:4 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = 2 (#) (exp_R (#) cos) & Z c= dom (exp_R (#) (sin + cos)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) (sin + cos)) . (upper_bound A)) - ((exp_R (#) (sin + cos)) . (lower_bound A)) proofend; ::f.x=cos.x-sin.x theorem :: INTEGR13:5 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & Z = dom (cos - sin) & (cos - sin) | A is continuous holds integral ((cos - sin),A) = ((sin + cos) . (upper_bound A)) - ((sin + cos) . (lower_bound A)) proofend; ::f.x=cos.x+sin.x theorem :: INTEGR13:6 for A being non empty closed_interval Subset of REAL for Z being open Subset of REAL st A c= Z & Z = dom (cos + sin) & (cos + sin) | A is continuous holds integral ((cos + sin),A) = ((sin - cos) . (upper_bound A)) - ((sin - cos) . (lower_bound A)) proofend; theorem Th7: :: INTEGR13:7 for Z being open Subset of REAL st Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) holds ( (- (1 / 2)) (#) ((sin + cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (1 / 2)) (#) ((sin + cos) / exp_R)) `| Z) . x = (sin . x) / (exp_R . x) ) ) proofend; ::f.x=sin.x/exp_R.x theorem :: INTEGR13:8 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = sin / exp_R & Z c= dom ((- (1 / 2)) (#) ((sin + cos) / exp_R)) & Z = dom f & f | A is continuous holds integral (f,A) = (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (upper_bound A)) - (((- (1 / 2)) (#) ((sin + cos) / exp_R)) . (lower_bound A)) proofend; theorem Th9: :: INTEGR13:9 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) holds ( (1 / 2) (#) ((sin - cos) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((sin - cos) / exp_R)) `| Z) . x = (cos . x) / (exp_R . x) ) ) proofend; ::f.x=cos.x/exp_R.x theorem :: INTEGR13:10 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = cos / exp_R & Z c= dom ((1 / 2) (#) ((sin - cos) / exp_R)) & Z = dom f & f | A is continuous holds integral (f,A) = (((1 / 2) (#) ((sin - cos) / exp_R)) . (upper_bound A)) - (((1 / 2) (#) ((sin - cos) / exp_R)) . (lower_bound A)) proofend; ::f.x=exp_R.x*(sin.x+cos.x) theorem :: INTEGR13:11 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = exp_R (#) (sin + cos) & Z c= dom (exp_R (#) sin) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) proofend; ::f.x=exp_R.x*(cos.x-sin.x) theorem :: INTEGR13:12 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = exp_R (#) (cos - sin) & Z c= dom (exp_R (#) cos) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) proofend; ::f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2 theorem :: INTEGR13:13 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f1 = #Z 2 & f = (- ((sin / cos) / f1)) + (((id Z) ^) / (cos ^2)) & Z c= dom (((id Z) ^) (#) tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((((id Z) ^) (#) tan) . (upper_bound A)) - ((((id Z) ^) (#) tan) . (lower_bound A)) proofend; ::f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2 theorem :: INTEGR13:14 for A being non empty closed_interval Subset of REAL for f, f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (- ((cos / sin) / f1)) - (((id Z) ^) / (sin ^2)) & f1 = #Z 2 & Z c= dom (((id Z) ^) (#) cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((((id Z) ^) (#) cot) . (upper_bound A)) - ((((id Z) ^) (#) cot) . (lower_bound A)) proofend; ::f.x=sin.x/cos.x/x+ln.x/(cos.x)^2 theorem :: INTEGR13:15 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ((sin / cos) / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) proofend; ::f.x=cos.x/sin.x/x-ln.x/(sin.x)^2 theorem :: INTEGR13:16 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ((cos / sin) / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) proofend; ::f.x=tan.x/x+ln.x/(cos.x)^2 theorem :: INTEGR13:17 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (tan / (id Z)) + (ln / (cos ^2)) & Z c= dom (ln (#) tan) & Z c= dom tan & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) tan) . (upper_bound A)) - ((ln (#) tan) . (lower_bound A)) proofend; ::f.x=cot.x/x-ln.x/(sin.x)^2 theorem :: INTEGR13:18 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (cot / (id Z)) - (ln / (sin ^2)) & Z c= dom (ln (#) cot) & Z c= dom cot & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) cot) . (upper_bound A)) - ((ln (#) cot) . (lower_bound A)) proofend; ::f.x=arctan.x/x+ln.x/(1+x^2) theorem :: INTEGR13:19 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = (arctan / (id Z)) + (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) arctan) . (upper_bound A)) - ((ln (#) arctan) . (lower_bound A)) proofend; ::f.x=arccot.x/x-ln.x/(1+x^2) theorem :: INTEGR13:20 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = (arccot / (id Z)) - (ln / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = ((ln (#) arccot) . (upper_bound A)) - ((ln (#) arccot) . (lower_bound A)) proofend; ::f.x=exp_R.(tan.x)/(cos.x)^2 theorem :: INTEGR13:21 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * tan) / (cos ^2) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * tan) . (upper_bound A)) - ((exp_R * tan) . (lower_bound A)) proofend; ::f.x=-exp_R.(cot.x)/(sin.x)^2 theorem :: INTEGR13:22 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = - ((exp_R * cot) / (sin ^2)) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * cot) . (upper_bound A)) - ((exp_R * cot) . (lower_bound A)) proofend; theorem Th23: :: INTEGR13:23 for Z being open Subset of REAL st Z c= dom (exp_R * cot) holds ( - (exp_R * cot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * cot)) `| Z) . x = (exp_R . (cot . x)) / ((sin . x) ^2) ) ) proofend; ::f.x=exp_R.(cot.x)/(sin.x)^2 theorem :: INTEGR13:24 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = (exp_R * cot) / (sin ^2) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (exp_R * cot)) . (upper_bound A)) - ((- (exp_R * cot)) . (lower_bound A)) proofend; ::f.x=1/(x*(cos.(ln.x))^2) theorem :: INTEGR13:25 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((cos * ln) ^2)) ^ & Z c= dom (tan * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan * ln) . (upper_bound A)) - ((tan * ln) . (lower_bound A)) proofend; ::f.x= -1/(x*(sin.(ln.x))^2) theorem :: INTEGR13:26 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = - (((id Z) (#) ((sin * ln) ^2)) ^) & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((cot * ln) . (upper_bound A)) - ((cot * ln) . (lower_bound A)) proofend; theorem Th27: :: INTEGR13:27 for Z being open Subset of REAL st Z c= dom (cot * ln) holds ( - (cot * ln) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot * ln)) `| Z) . x = 1 / (x * ((sin . (ln . x)) ^2)) ) ) proofend; ::f.x= 1/(x*(sin.(ln.x))^2) theorem :: INTEGR13:28 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = ((id Z) (#) ((sin * ln) ^2)) ^ & Z c= dom (cot * ln) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot * ln)) . (upper_bound A)) - ((- (cot * ln)) . (lower_bound A)) proofend; ::f.x=exp_R.x/(cos.(exp_R.x))^2 theorem :: INTEGR13:29 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = exp_R / ((cos * exp_R) ^2) & Z c= dom (tan * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((tan * exp_R) . (upper_bound A)) - ((tan * exp_R) . (lower_bound A)) proofend; ::f.x=-exp_R.x/(sin.(exp_R.x))^2 theorem :: INTEGR13:30 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = - (exp_R / ((sin * exp_R) ^2)) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((cot * exp_R) . (upper_bound A)) - ((cot * exp_R) . (lower_bound A)) proofend; theorem Th31: :: INTEGR13:31 for Z being open Subset of REAL st Z c= dom (cot * exp_R) holds ( - (cot * exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (cot * exp_R)) `| Z) . x = (exp_R . x) / ((sin . (exp_R . x)) ^2) ) ) proofend; ::f.x=exp_R.x/(sin.(exp_R.x))^2 theorem :: INTEGR13:32 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = exp_R / ((sin * exp_R) ^2) & Z c= dom (cot * exp_R) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (cot * exp_R)) . (upper_bound A)) - ((- (cot * exp_R)) . (lower_bound A)) proofend; ::f.x=-1/(x^2*(cos.(1/x))^2) theorem :: INTEGR13:33 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = - (1 / ((x ^2) * ((cos . (1 / 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; theorem Th34: :: INTEGR13:34 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 = 1 / ((x ^2) * ((cos . (1 / x)) ^2)) ) ) proofend; ::f.x=1/(x^2*(cos.(1/x))^2) theorem :: INTEGR13:35 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = 1 / ((x ^2) * ((cos . (1 / 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=1/(x^2*(sin.(1/x))^2) theorem :: INTEGR13:36 for A being non empty closed_interval Subset of REAL for f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f . x = 1 / ((x ^2) * ((sin . (1 / 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/((1+x^2)*arctan.x) theorem :: INTEGR13:37 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds ( f1 . x = 1 & arctan . x > 0 ) ) & f = ((f1 + (#Z 2)) (#) arctan) ^ & Z c= ].(- 1),1.[ & Z c= dom (ln * arctan) & Z = dom f & f | A is continuous holds integral (f,A) = ((ln * arctan) . (upper_bound A)) - ((ln * arctan) . (lower_bound A)) proofend; ::f.x=n*(arctan.x) #Z (n-1) / (1+x^2) theorem :: INTEGR13:38 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f, f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & f = n (#) (((#Z (n - 1)) * arctan) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds f1 . x = 1 ) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arctan) & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * arctan) . (upper_bound A)) - (((#Z n) * arctan) . (lower_bound A)) proofend; ::f.x=-n*(arccot.x) #Z (n-1) / (1+x^2) theorem :: INTEGR13:39 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = - (n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2)))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot) & Z = dom f & f | A is continuous holds integral (f,A) = (((#Z n) * arccot) . (upper_bound A)) - (((#Z n) * arccot) . (lower_bound A)) proofend; theorem Th40: :: INTEGR13:40 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arccot) & Z c= ].(- 1),1.[ holds ( - ((#Z n) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#Z n) * arccot)) `| Z) . x = (n * ((arccot . x) #Z (n - 1))) / (1 + (x ^2)) ) ) proofend; ::f.x=n*(arccot.x) #Z (n-1) / (1+x^2) theorem :: INTEGR13:41 for n being Element of NAT for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = n (#) (((#Z (n - 1)) * arccot) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z n) * arccot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((#Z n) * arccot)) . (upper_bound A)) - ((- ((#Z n) * arccot)) . (lower_bound A)) proofend; ::f.x=arctan.x / (1+x^2) theorem :: INTEGR13:42 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = arctan / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arctan) & Z = dom f & f | A is continuous holds integral (f,A) = (((1 / 2) (#) ((#Z 2) * arctan)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arctan)) . (lower_bound A)) proofend; ::f.x=-arccot.x / (1+x^2) theorem :: INTEGR13:43 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = - (arccot / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot) & Z = dom f & f | A is continuous holds integral (f,A) = (((1 / 2) (#) ((#Z 2) * arccot)) . (upper_bound A)) - (((1 / 2) (#) ((#Z 2) * arccot)) . (lower_bound A)) proofend; theorem Th44: :: INTEGR13:44 for Z being open Subset of REAL st Z c= dom ((#Z 2) * arccot) & Z c= ].(- 1),1.[ holds ( - ((1 / 2) (#) ((#Z 2) * arccot)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((1 / 2) (#) ((#Z 2) * arccot))) `| Z) . x = (arccot . x) / (1 + (x ^2)) ) ) proofend; ::f.x=arccot.x / (1+x^2) theorem :: INTEGR13:45 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = arccot / (f1 + (#Z 2)) & Z c= ].(- 1),1.[ & Z c= dom ((#Z 2) * arccot) & Z = dom f & f | A is continuous holds integral (f,A) = ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (upper_bound A)) - ((- ((1 / 2) (#) ((#Z 2) * arccot))) . (lower_bound A)) proofend; ::f.x=arctan.x + x/(1+x^2) theorem :: INTEGR13:46 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = arctan + ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = (((id Z) (#) arctan) . (upper_bound A)) - (((id Z) (#) arctan) . (lower_bound A)) proofend; ::f.x=arccot.x - x/(1+x^2) theorem :: INTEGR13:47 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = arccot - ((id Z) / (f1 + (#Z 2))) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = (((id Z) (#) arccot) . (upper_bound A)) - (((id Z) (#) arccot) . (lower_bound A)) proofend; ::f.x=exp_R.(arctan.x)/(1+x^2) theorem :: INTEGR13:48 for A being non empty closed_interval Subset of REAL for f, f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arctan) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds f1 . x = 1 ) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * arctan) . (upper_bound A)) - ((exp_R * arctan) . (lower_bound A)) proofend; ::f.x=-exp_R.(arccot.x)/(1+x^2) theorem :: INTEGR13:49 for A being non empty closed_interval Subset of REAL for f, f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = - ((exp_R * arccot) / (f1 + (#Z 2))) & ( for x being Real st x in Z holds f1 . x = 1 ) & Z = dom f & f | A is continuous holds integral (f,A) = ((exp_R * arccot) . (upper_bound A)) - ((exp_R * arccot) . (lower_bound A)) proofend; theorem Th50: :: INTEGR13:50 for Z being open Subset of REAL st Z c= dom (exp_R * arccot) & Z c= ].(- 1),1.[ holds ( - (exp_R * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (exp_R * arccot)) `| Z) . x = (exp_R . (arccot . x)) / (1 + (x ^2)) ) ) proofend; ::f.x=exp_R.(arccot.x)/(1+x^2) theorem :: INTEGR13:51 for A being non empty closed_interval Subset of REAL for f, f1 being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & Z c= ].(- 1),1.[ & f = (exp_R * arccot) / (f1 + (#Z 2)) & ( for x being Real st x in Z holds f1 . x = 1 ) & Z = dom f & f | A is continuous holds integral (f,A) = ((- (exp_R * arccot)) . (upper_bound A)) - ((- (exp_R * arccot)) . (lower_bound A)) proofend; ::f.x=x/(1+x^2) theorem :: INTEGR13:52 for A being non empty closed_interval Subset of REAL for f1, f2, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & f = (id Z) / (f1 + f2) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = 1 ) & Z = dom f & f | A is continuous holds integral (f,A) = (((1 / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((1 / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) proofend; ::f.x=x/(a*(1+(x/a)^2)) theorem :: INTEGR13:53 for a being Real for A being non empty closed_interval Subset of REAL for f1, f2, f, h being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & Z c= dom (ln * (f1 + f2)) & f = (id Z) / (a (#) (f1 + f2)) & ( for x being Real st x in Z holds ( h . x = x / a & f1 . x = 1 ) ) & a <> 0 & f2 = (#Z 2) * h & Z = dom f & f | A is continuous holds integral (f,A) = (((a / 2) (#) (ln * (f1 + f2))) . (upper_bound A)) - (((a / 2) (#) (ln * (f1 + f2))) . (lower_bound A)) proofend; theorem Th54: :: INTEGR13:54 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ holds ( - (((id Z) ^) (#) arctan) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) arctan)) `| Z) . x = ((arctan . x) / (x ^2)) - (1 / (x * (1 + (x ^2)))) ) ) proofend; theorem Th55: :: INTEGR13:55 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ holds ( - (((id Z) ^) (#) arccot) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (((id Z) ^) (#) arccot)) `| Z) . x = ((arccot . x) / (x ^2)) + (1 / (x * (1 + (x ^2)))) ) ) proofend; ::f.x=arctan.x/(x^2)-1/(x*(1+x^2)) theorem :: INTEGR13:56 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = (arctan / (#Z 2)) - (((id Z) (#) (f1 + (#Z 2))) ^) & Z c= dom (((id Z) ^) (#) arctan) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) arctan)) . (upper_bound A)) - ((- (((id Z) ^) (#) arctan)) . (lower_bound A)) proofend; ::f.x=arccot.x/(x^2)+1/(x*(1+x^2)) theorem :: INTEGR13:57 for A being non empty closed_interval Subset of REAL for f1, f being PartFunc of REAL,REAL for Z being open Subset of REAL st A c= Z & ( for x being Real st x in Z holds f1 . x = 1 ) & f = (arccot / (#Z 2)) + (((id Z) (#) (f1 + (#Z 2))) ^) & Z c= dom (((id Z) ^) (#) arccot) & Z c= ].(- 1),1.[ & Z = dom f & f | A is continuous holds integral (f,A) = ((- (((id Z) ^) (#) arccot)) . (upper_bound A)) - ((- (((id Z) ^) (#) arccot)) . (lower_bound A)) proofend;