:: Inverse Trigonometric Functions Arctan and Arccot :: by Xiquan Liang and Bing Xie :: :: Received March 18, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin theorem Th1: :: SIN_COS9:1 ].(- (PI / 2)),(PI / 2).[ c= dom tan proofend; theorem Th2: :: SIN_COS9:2 ].0,PI.[ c= dom cot proofend; Lm1: tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ proofend; Lm2: cot is_differentiable_on ].0,PI.[ proofend; Lm3: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds diff (tan,x) = 1 / ((cos . x) ^2) proofend; Lm4: for x being Real st x in ].0,PI.[ holds diff (cot,x) = - (1 / ((sin . x) ^2)) proofend; theorem :: SIN_COS9:3 ( tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[ & ( for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds diff (tan,x) = 1 / ((cos . x) ^2) ) ) by Lm1, Lm3; theorem :: SIN_COS9:4 ( cot is_differentiable_on ].0,PI.[ & ( for x being Real st x in ].0,PI.[ holds diff (cot,x) = - (1 / ((sin . x) ^2)) ) ) by Lm2, Lm4; theorem :: SIN_COS9:5 tan | ].(- (PI / 2)),(PI / 2).[ is continuous by Lm1, FDIFF_1:25; theorem :: SIN_COS9:6 cot | ].0,PI.[ is continuous by Lm2, FDIFF_1:25; theorem Th7: :: SIN_COS9:7 tan | ].(- (PI / 2)),(PI / 2).[ is increasing proofend; theorem Th8: :: SIN_COS9:8 cot | ].0,PI.[ is decreasing proofend; theorem :: SIN_COS9:9 tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:8; theorem :: SIN_COS9:10 cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:8; registration clusterK77(tan,].(- (PI / 2)),(PI / 2).[) -> one-to-one ; coherence tan | ].(- (PI / 2)),(PI / 2).[ is one-to-one by Th7, FCONT_3:8; clusterK77(cot,].0,PI.[) -> one-to-one ; coherence cot | ].0,PI.[ is one-to-one by Th8, FCONT_3:8; end; definition func arctan -> PartFunc of REAL,REAL equals :: SIN_COS9:def 1 (tan | ].(- (PI / 2)),(PI / 2).[) " ; coherence (tan | ].(- (PI / 2)),(PI / 2).[) " is PartFunc of REAL,REAL ; func arccot -> PartFunc of REAL,REAL equals :: SIN_COS9:def 2 (cot | ].0,PI.[) " ; coherence (cot | ].0,PI.[) " is PartFunc of REAL,REAL ; end; :: deftheorem defines arctan SIN_COS9:def_1_:_ arctan = (tan | ].(- (PI / 2)),(PI / 2).[) " ; :: deftheorem defines arccot SIN_COS9:def_2_:_ arccot = (cot | ].0,PI.[) " ; definition let r be Real; func arctan r -> set equals :: SIN_COS9:def 3 arctan . r; coherence arctan . r is set ; func arccot r -> set equals :: SIN_COS9:def 4 arccot . r; coherence arccot . r is set ; end; :: deftheorem defines arctan SIN_COS9:def_3_:_ for r being Real holds arctan r = arctan . r; :: deftheorem defines arccot SIN_COS9:def_4_:_ for r being Real holds arccot r = arccot . r; definition let r be Real; :: original:arctan redefine func arctan r -> Real; coherence arctan r is Real ; :: original:arccot redefine func arccot r -> Real; coherence arccot r is Real ; end; Lm5: arctan " = tan | ].(- (PI / 2)),(PI / 2).[ by FUNCT_1:43; Lm6: arccot " = cot | ].0,PI.[ by FUNCT_1:43; theorem Th11: :: SIN_COS9:11 rng arctan = ].(- (PI / 2)),(PI / 2).[ proofend; theorem Th12: :: SIN_COS9:12 rng arccot = ].0,PI.[ proofend; registration cluster arctan -> one-to-one ; coherence arctan is one-to-one ; cluster arccot -> one-to-one ; coherence arccot is one-to-one ; end; Lm7: - (PI / 4) in ].(- (PI / 2)),(PI / 2).[ proofend; Lm8: PI / 4 in ].(- (PI / 2)),(PI / 2).[ proofend; Lm9: PI / 4 in ].0,PI.[ proofend; Lm10: (3 / 4) * PI in ].0,PI.[ proofend; Lm11: dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).] proofend; Lm12: dom (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(PI / 4),((3 / 4) * PI).] proofend; theorem Th13: :: SIN_COS9:13 for x being real number st x in ].(- (PI / 2)),(PI / 2).[ holds tan . x = tan x proofend; theorem Th14: :: SIN_COS9:14 for x being real number st x in ].0,PI.[ holds cot . x = cot x proofend; theorem :: SIN_COS9:15 for x being Real st cos . x <> 0 holds tan . x = tan x proofend; theorem :: SIN_COS9:16 for x being Real st sin . x <> 0 holds cot . x = cot x proofend; theorem Th17: :: SIN_COS9:17 ( tan . (- (PI / 4)) = - 1 & tan (- (PI / 4)) = - 1 ) proofend; theorem Th18: :: SIN_COS9:18 ( cot . (PI / 4) = 1 & cot (PI / 4) = 1 & cot . ((3 / 4) * PI) = - 1 & cot ((3 / 4) * PI) = - 1 ) proofend; theorem Th19: :: SIN_COS9:19 for x being set st x in [.(- (PI / 4)),(PI / 4).] holds tan . x in [.(- 1),1.] proofend; theorem Th20: :: SIN_COS9:20 for x being set st x in [.(PI / 4),((3 / 4) * PI).] holds cot . x in [.(- 1),1.] proofend; theorem Th21: :: SIN_COS9:21 rng (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- 1),1.] proofend; theorem Th22: :: SIN_COS9:22 rng (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(- 1),1.] proofend; theorem Th23: :: SIN_COS9:23 [.(- 1),1.] c= dom arctan proofend; theorem Th24: :: SIN_COS9:24 [.(- 1),1.] c= dom arccot proofend; Lm13: (tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] is increasing proofend; Lm14: (cot | [.(PI / 4),((3 / 4) * PI).]) | [.(PI / 4),((3 / 4) * PI).] is decreasing proofend; Lm15: tan | [.(- (PI / 4)),(PI / 4).] is one-to-one proofend; Lm16: cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one proofend; registration clusterK77(tan,[.(- (PI / 4)),(PI / 4).]) -> one-to-one ; coherence tan | [.(- (PI / 4)),(PI / 4).] is one-to-one by Lm15; clusterK77(cot,[.(PI / 4),((3 / 4) * PI).]) -> one-to-one ; coherence cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one by Lm16; end; theorem Th25: :: SIN_COS9:25 arctan | [.(- 1),1.] = (tan | [.(- (PI / 4)),(PI / 4).]) " proofend; theorem Th26: :: SIN_COS9:26 arccot | [.(- 1),1.] = (cot | [.(PI / 4),((3 / 4) * PI).]) " proofend; theorem :: SIN_COS9:27 (tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by Th21, Th25, FUNCT_1:39; theorem :: SIN_COS9:28 (cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by Th22, Th26, FUNCT_1:39; theorem :: SIN_COS9:29 (tan | [.(- (PI / 4)),(PI / 4).]) * (arctan | [.(- 1),1.]) = id [.(- 1),1.] by Th21, Th25, FUNCT_1:39; theorem :: SIN_COS9:30 (cot | [.(PI / 4),((3 / 4) * PI).]) * (arccot | [.(- 1),1.]) = id [.(- 1),1.] by Th22, Th26, FUNCT_1:39; theorem Th31: :: SIN_COS9:31 arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by Lm5, Th11, FUNCT_1:39; theorem Th32: :: SIN_COS9:32 arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6, Th12, FUNCT_1:39; theorem :: SIN_COS9:33 arctan * (tan | ].(- (PI / 2)),(PI / 2).[) = id ].(- (PI / 2)),(PI / 2).[ by Lm5, Th11, FUNCT_1:39; theorem :: SIN_COS9:34 arccot * (cot | ].0,PI.[) = id ].0,PI.[ by Lm6, Th12, FUNCT_1:39; theorem Th35: :: SIN_COS9:35 for r being Real st - (PI / 2) < r & r < PI / 2 holds ( arctan (tan . r) = r & arctan (tan r) = r ) proofend; theorem Th36: :: SIN_COS9:36 for r being Real st 0 < r & r < PI holds ( arccot (cot . r) = r & arccot (cot r) = r ) proofend; theorem Th37: :: SIN_COS9:37 ( arctan (- 1) = - (PI / 4) & arctan . (- 1) = - (PI / 4) ) proofend; theorem Th38: :: SIN_COS9:38 ( arccot (- 1) = (3 / 4) * PI & arccot . (- 1) = (3 / 4) * PI ) proofend; theorem Th39: :: SIN_COS9:39 ( arctan 1 = PI / 4 & arctan . 1 = PI / 4 ) proofend; theorem Th40: :: SIN_COS9:40 ( arccot 1 = PI / 4 & arccot . 1 = PI / 4 ) proofend; theorem Th41: :: SIN_COS9:41 ( tan . 0 = 0 & tan 0 = 0 ) proofend; theorem Th42: :: SIN_COS9:42 ( cot . (PI / 2) = 0 & cot (PI / 2) = 0 ) proofend; theorem :: SIN_COS9:43 ( arctan 0 = 0 & arctan . 0 = 0 ) proofend; theorem :: SIN_COS9:44 ( arccot 0 = PI / 2 & arccot . 0 = PI / 2 ) proofend; theorem Th45: :: SIN_COS9:45 arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is increasing proofend; theorem Th46: :: SIN_COS9:46 arccot | (cot .: ].0,PI.[) is decreasing proofend; theorem Th47: :: SIN_COS9:47 arctan | [.(- 1),1.] is increasing proofend; theorem Th48: :: SIN_COS9:48 arccot | [.(- 1),1.] is decreasing proofend; theorem Th49: :: SIN_COS9:49 for x being set st x in [.(- 1),1.] holds arctan . x in [.(- (PI / 4)),(PI / 4).] proofend; theorem Th50: :: SIN_COS9:50 for x being set st x in [.(- 1),1.] holds arccot . x in [.(PI / 4),((3 / 4) * PI).] proofend; theorem Th51: :: SIN_COS9:51 for r being Real st - 1 <= r & r <= 1 holds tan (arctan r) = r proofend; theorem Th52: :: SIN_COS9:52 for r being Real st - 1 <= r & r <= 1 holds cot (arccot r) = r proofend; theorem Th53: :: SIN_COS9:53 arctan | [.(- 1),1.] is continuous proofend; theorem Th54: :: SIN_COS9:54 arccot | [.(- 1),1.] is continuous proofend; theorem Th55: :: SIN_COS9:55 rng (arctan | [.(- 1),1.]) = [.(- (PI / 4)),(PI / 4).] proofend; theorem Th56: :: SIN_COS9:56 rng (arccot | [.(- 1),1.]) = [.(PI / 4),((3 / 4) * PI).] proofend; theorem :: SIN_COS9:57 for r being Real st - 1 <= r & r <= 1 & arctan r = - (PI / 4) holds r = - 1 by Th17, Th51; theorem :: SIN_COS9:58 for r being Real st - 1 <= r & r <= 1 & arccot r = (3 / 4) * PI holds r = - 1 by Th18, Th52; theorem :: SIN_COS9:59 for r being Real st - 1 <= r & r <= 1 & arctan r = 0 holds r = 0 by Th41, Th51; theorem :: SIN_COS9:60 for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 2 holds r = 0 by Th42, Th52; theorem :: SIN_COS9:61 for r being Real st - 1 <= r & r <= 1 & arctan r = PI / 4 holds r = 1 proofend; theorem :: SIN_COS9:62 for r being Real st - 1 <= r & r <= 1 & arccot r = PI / 4 holds r = 1 by Th18, Th52; theorem Th63: :: SIN_COS9:63 for r being Real st - 1 <= r & r <= 1 holds ( - (PI / 4) <= arctan r & arctan r <= PI / 4 ) proofend; theorem Th64: :: SIN_COS9:64 for r being Real st - 1 <= r & r <= 1 holds ( PI / 4 <= arccot r & arccot r <= (3 / 4) * PI ) proofend; theorem :: SIN_COS9:65 for r being Real st - 1 < r & r < 1 holds ( - (PI / 4) < arctan r & arctan r < PI / 4 ) proofend; theorem :: SIN_COS9:66 for r being Real st - 1 < r & r < 1 holds ( PI / 4 < arccot r & arccot r < (3 / 4) * PI ) proofend; theorem :: SIN_COS9:67 for r being Real st - 1 <= r & r <= 1 holds arctan r = - (arctan (- r)) proofend; theorem :: SIN_COS9:68 for r being Real st - 1 <= r & r <= 1 holds arccot r = PI - (arccot (- r)) proofend; theorem :: SIN_COS9:69 for r being Real st - 1 <= r & r <= 1 holds cot (arctan r) = 1 / r proofend; theorem :: SIN_COS9:70 for r being Real st - 1 <= r & r <= 1 holds tan (arccot r) = 1 / r proofend; theorem Th71: :: SIN_COS9:71 arctan is_differentiable_on tan .: ].(- (PI / 2)),(PI / 2).[ proofend; theorem Th72: :: SIN_COS9:72 arccot is_differentiable_on cot .: ].0,PI.[ proofend; theorem Th73: :: SIN_COS9:73 arctan is_differentiable_on ].(- 1),1.[ proofend; theorem Th74: :: SIN_COS9:74 arccot is_differentiable_on ].(- 1),1.[ proofend; theorem Th75: :: SIN_COS9:75 for r being Real st - 1 <= r & r <= 1 holds diff (arctan,r) = 1 / (1 + (r ^2)) proofend; theorem Th76: :: SIN_COS9:76 for r being Real st - 1 <= r & r <= 1 holds diff (arccot,r) = - (1 / (1 + (r ^2))) proofend; theorem :: SIN_COS9:77 arctan | (tan .: ].(- (PI / 2)),(PI / 2).[) is continuous by Th71, FDIFF_1:25; theorem :: SIN_COS9:78 arccot | (cot .: ].0,PI.[) is continuous by Th72, FDIFF_1:25; theorem :: SIN_COS9:79 dom arctan is open proofend; theorem :: SIN_COS9:80 dom arccot is open proofend; begin :: f.x=arctan.x theorem Th81: :: SIN_COS9:81 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arctan is_differentiable_on Z & ( for x being Real st x in Z holds (arctan `| Z) . x = 1 / (1 + (x ^2)) ) ) proofend; :: f.x=arccot.x theorem Th82: :: SIN_COS9:82 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( arccot is_differentiable_on Z & ( for x being Real st x in Z holds (arccot `| Z) . x = - (1 / (1 + (x ^2))) ) ) proofend; ::f.x=r*arctanx theorem :: SIN_COS9:83 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( r (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arctan) `| Z) . x = r / (1 + (x ^2)) ) ) proofend; ::f.x=r*arccotx theorem :: SIN_COS9:84 for r being Real for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( r (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((r (#) arccot) `| Z) . x = - (r / (1 + (x ^2))) ) ) proofend; theorem Th85: :: SIN_COS9:85 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arctan * f is_differentiable_in x & diff ((arctan * f),x) = (diff (f,x)) / (1 + ((f . x) ^2)) ) proofend; theorem Th86: :: SIN_COS9:86 for x being Real for f being PartFunc of REAL,REAL st f is_differentiable_in x & f . x > - 1 & f . x < 1 holds ( arccot * f is_differentiable_in x & diff ((arccot * f),x) = - ((diff (f,x)) / (1 + ((f . x) ^2))) ) proofend; ::f.x=arctan.(r*x+s) theorem Th87: :: SIN_COS9:87 for r, s being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arctan * f) & ( for x being Real st x in Z holds ( f . x = (r * x) + s & f . x > - 1 & f . x < 1 ) ) holds ( arctan * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * f) `| Z) . x = r / (1 + (((r * x) + s) ^2)) ) ) proofend; ::f.x=arccot.(r*x+s) theorem Th88: :: SIN_COS9:88 for r, s being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (arccot * f) & ( for x being Real st x in Z holds ( f . x = (r * x) + s & f . x > - 1 & f . x < 1 ) ) holds ( arccot * f is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * f) `| Z) . x = - (r / (1 + (((r * x) + s) ^2))) ) ) proofend; ::f.x=ln(arctan.x) theorem :: SIN_COS9:89 for Z being open Subset of REAL st Z c= dom (ln * arctan) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arctan . x > 0 ) holds ( ln * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arctan) `| Z) . x = 1 / ((1 + (x ^2)) * (arctan . x)) ) ) proofend; ::f.x=ln(arccot.x) theorem :: SIN_COS9:90 for Z being open Subset of REAL st Z c= dom (ln * arccot) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds arccot . x > 0 ) holds ( ln * arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * arccot) `| Z) . x = - (1 / ((1 + (x ^2)) * (arccot . x))) ) ) proofend; ::f.x=(arctan)|^n theorem Th91: :: SIN_COS9:91 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((#Z n) * arctan) & Z c= ].(- 1),1.[ holds ( (#Z n) * arctan is_differentiable_on Z & ( for x being Real st x in Z holds (((#Z n) * arctan) `| Z) . x = (n * ((arctan . x) #Z (n - 1))) / (1 + (x ^2)) ) ) proofend; ::f.x=(arccot)|^n theorem Th92: :: SIN_COS9:92 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=(1/2)*(arctan)|^2 theorem :: SIN_COS9:93 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * arctan)) & Z c= ].(- 1),1.[ holds ( (1 / 2) (#) ((#Z 2) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * arctan)) `| Z) . x = (arctan . x) / (1 + (x ^2)) ) ) proofend; ::f.x=(1/2)*(arccot)|^2 theorem :: SIN_COS9:94 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#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=x*arctan.x theorem Th95: :: SIN_COS9:95 for Z being open Subset of REAL st 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 / (1 + (x ^2))) ) ) proofend; ::f.x=x*arccot.x theorem Th96: :: SIN_COS9:96 for Z being open Subset of REAL st 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 / (1 + (x ^2))) ) ) proofend; ::f.x=(r*x+s)*arctan.x theorem :: SIN_COS9:97 for r, s being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arctan) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (r * x) + s ) holds ( f (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arctan) `| Z) . x = (r * (arctan . x)) + (((r * x) + s) / (1 + (x ^2))) ) ) proofend; ::f.x=(r*x+s)*arccot.x theorem :: SIN_COS9:98 for r, s being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (f (#) arccot) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds f . x = (r * x) + s ) holds ( f (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((f (#) arccot) `| Z) . x = (r * (arccot . x)) - (((r * x) + s) / (1 + (x ^2))) ) ) proofend; ::f.x=(1/2)*arctan(2*x) theorem :: SIN_COS9:99 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arctan * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arctan * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arctan * f)) `| Z) . x = 1 / (1 + ((2 * x) ^2)) ) ) proofend; ::f.x=(1/2)*arccot(2*x) theorem :: SIN_COS9:100 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (arccot * f)) & ( for x being Real st x in Z holds ( f . x = 2 * x & f . x > - 1 & f . x < 1 ) ) holds ( (1 / 2) (#) (arccot * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (arccot * f)) `| Z) . x = - (1 / (1 + ((2 * x) ^2))) ) ) proofend; ::f.x=1+x|^2 theorem Th101: :: SIN_COS9:101 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = 1 ) & f2 = #Z 2 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) proofend; ::f.x=(1/2)ln(1+x|^2) theorem Th102: :: SIN_COS9:102 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / 2) (#) (ln * (f1 + f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( (1 / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (1 + (x ^2)) ) ) proofend; ::f.x=x*arctan.x-(1/2)ln(1+x|^2) theorem :: SIN_COS9:103 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( ((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arctan) - ((1 / 2) (#) (ln * (f1 + f2)))) `| Z) . x = arctan . x ) ) proofend; ::f.x=x*arccot.x+(1/2)ln(1+x|^2) theorem :: SIN_COS9:104 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) & Z c= ].(- 1),1.[ & f2 = #Z 2 & ( for x being Real st x in Z holds f1 . x = 1 ) holds ( ((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) arccot) + ((1 / 2) (#) (ln * (f1 + f2)))) `| Z) . x = arccot . x ) ) proofend; ::f.x=x*arctan(x/r) theorem Th105: :: SIN_COS9:105 for r being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arctan * f)) & ( for x being Real st x in Z holds ( f . x = x / r & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arctan * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arctan * f)) `| Z) . x = (arctan . (x / r)) + (x / (r * (1 + ((x / r) ^2)))) ) ) proofend; ::f.x=x*arccot(x/r) theorem Th106: :: SIN_COS9:106 for r being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((id Z) (#) (arccot * f)) & ( for x being Real st x in Z holds ( f . x = x / r & f . x > - 1 & f . x < 1 ) ) holds ( (id Z) (#) (arccot * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (arccot * f)) `| Z) . x = (arccot . (x / r)) - (x / (r * (1 + ((x / r) ^2)))) ) ) proofend; ::f.x=1+(x/r)^2 theorem Th107: :: SIN_COS9:107 for r being Real for Z being open Subset of REAL for f1, f2, f being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds f . x = x / r ) holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = (2 * x) / (r ^2) ) ) proofend; ::f.x=(r/2)ln(1+(x/r)^2) theorem Th108: :: SIN_COS9:108 for r being Real for Z being open Subset of REAL for f1, f2, f being PartFunc of REAL,REAL st Z c= dom ((r / 2) (#) (ln * (f1 + f2))) & ( for x being Real st x in Z holds f1 . x = 1 ) & r <> 0 & f2 = (#Z 2) * f & ( for x being Real st x in Z holds f . x = x / r ) holds ( (r / 2) (#) (ln * (f1 + f2)) is_differentiable_on Z & ( for x being Real st x in Z holds (((r / 2) (#) (ln * (f1 + f2))) `| Z) . x = x / (r * (1 + ((x / r) ^2))) ) ) proofend; ::f.x=x*arctan.(x/r)-(r/2)ln(1+(x/r)^2) theorem :: SIN_COS9:109 for r being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arctan * f)) - ((r / 2) (#) (ln * (f1 + f2)))) & r <> 0 & ( for x being Real st x in Z holds ( f . x = x / r & f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds f . x = x / r ) holds ( ((id Z) (#) (arctan * f)) - ((r / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arctan * f)) - ((r / 2) (#) (ln * (f1 + f2)))) `| Z) . x = arctan . (x / r) ) ) proofend; ::f.x=x*arccot.(x/r)+(r/2)ln(1+(x/r)^2) theorem :: SIN_COS9:110 for r being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (((id Z) (#) (arccot * f)) + ((r / 2) (#) (ln * (f1 + f2)))) & r <> 0 & ( for x being Real st x in Z holds ( f . x = x / r & f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds f1 . x = 1 ) & f2 = (#Z 2) * f & ( for x being Real st x in Z holds f . x = x / r ) holds ( ((id Z) (#) (arccot * f)) + ((r / 2) (#) (ln * (f1 + f2))) is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) (arccot * f)) + ((r / 2) (#) (ln * (f1 + f2)))) `| Z) . x = arccot . (x / r) ) ) proofend; ::f.x=arctan.(1/x) theorem :: SIN_COS9:111 for Z being open Subset of REAL st not 0 in Z & Z c= dom (arctan * ((id Z) ^)) & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( arctan * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * ((id Z) ^)) `| Z) . x = - (1 / (1 + (x ^2))) ) ) proofend; ::f.x=arccot.(1/x) theorem :: SIN_COS9:112 for Z being open Subset of REAL st not 0 in Z & Z c= dom (arccot * ((id Z) ^)) & ( for x being Real st x in Z holds ( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds ( arccot * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * ((id Z) ^)) `| Z) . x = 1 / (1 + (x ^2)) ) ) proofend; ::f.x=arctan.(r+s*x+h*x^2) theorem :: SIN_COS9:113 for h, r, s being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (arctan * f) & f = f1 + (h (#) f2) & ( for x being Real st x in Z holds ( f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds f1 . x = r + (s * x) ) & f2 = #Z 2 holds ( arctan * (f1 + (h (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * (f1 + (h (#) f2))) `| Z) . x = (s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2))) ^2)) ) ) proofend; ::f.x=arccot.(r+s*x+h*x^2) theorem :: SIN_COS9:114 for h, r, s being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (arccot * f) & f = f1 + (h (#) f2) & ( for x being Real st x in Z holds ( f . x > - 1 & f . x < 1 ) ) & ( for x being Real st x in Z holds f1 . x = r + (s * x) ) & f2 = #Z 2 holds ( arccot * (f1 + (h (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * (f1 + (h (#) f2))) `| Z) . x = - ((s + ((2 * h) * x)) / (1 + (((r + (s * x)) + (h * (x ^2))) ^2))) ) ) proofend; ::f.x=arctan.(exp_R.x) theorem :: SIN_COS9:115 for Z being open Subset of REAL st Z c= dom (arctan * exp_R) & ( for x being Real st x in Z holds exp_R . x < 1 ) holds ( arctan * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * exp_R) `| Z) . x = (exp_R . x) / (1 + ((exp_R . x) ^2)) ) ) proofend; ::f.x=arccot.(exp_R.x) theorem :: SIN_COS9:116 for Z being open Subset of REAL st Z c= dom (arccot * exp_R) & ( for x being Real st x in Z holds exp_R . x < 1 ) holds ( arccot * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * exp_R) `| Z) . x = - ((exp_R . x) / (1 + ((exp_R . x) ^2))) ) ) proofend; ::f.x=arctan.(ln.x) theorem :: SIN_COS9:117 for Z being open Subset of REAL st Z c= dom (arctan * ln) & ( for x being Real st x in Z holds ( ln . x > - 1 & ln . x < 1 ) ) holds ( arctan * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan * ln) `| Z) . x = 1 / (x * (1 + ((ln . x) ^2))) ) ) proofend; ::f.x=arccot.(ln.x) theorem :: SIN_COS9:118 for Z being open Subset of REAL st Z c= dom (arccot * ln) & ( for x being Real st x in Z holds ( ln . x > - 1 & ln . x < 1 ) ) holds ( arccot * ln is_differentiable_on Z & ( for x being Real st x in Z holds ((arccot * ln) `| Z) . x = - (1 / (x * (1 + ((ln . x) ^2)))) ) ) proofend; ::f.x=exp_R.(arctan.x) theorem :: SIN_COS9:119 for Z being open Subset of REAL st Z c= dom (exp_R * arctan) & Z c= ].(- 1),1.[ holds ( exp_R * arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R * arctan) `| Z) . x = (exp_R . (arctan . x)) / (1 + (x ^2)) ) ) proofend; ::f.x=exp_R.(arccot.x) theorem :: SIN_COS9:120 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=arctan.x-x theorem :: SIN_COS9:121 for Z being open Subset of REAL st Z c= dom (arctan - (id Z)) & Z c= ].(- 1),1.[ holds ( arctan - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((arctan - (id Z)) `| Z) . x = - ((x ^2) / (1 + (x ^2))) ) ) proofend; ::f.x=-arccot.x-x theorem :: SIN_COS9:122 for Z being open Subset of REAL st Z c= dom ((- arccot) - (id Z)) & Z c= ].(- 1),1.[ holds ( (- arccot) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds (((- arccot) - (id Z)) `| Z) . x = - ((x ^2) / (1 + (x ^2))) ) ) proofend; ::f.x=exp_R.x*arctan.x theorem :: SIN_COS9:123 for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds ( exp_R (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) arctan) `| Z) . x = ((exp_R . x) * (arctan . x)) + ((exp_R . x) / (1 + (x ^2))) ) ) proofend; ::f.x=exp_R.x*arccot.x theorem :: SIN_COS9:124 for Z being open Subset of REAL st 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 . x) * (arccot . x)) - ((exp_R . x) / (1 + (x ^2))) ) ) proofend; ::f.x=(1/r)*arctan.(r*x)-x theorem :: SIN_COS9:125 for r being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((1 / r) (#) (arctan * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds ( ((1 / r) (#) (arctan * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / r) (#) (arctan * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ) ) proofend; ::f.x=(-1/r)*arccot.(r*x)-x theorem :: SIN_COS9:126 for r being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (((- (1 / r)) (#) (arccot * f)) - (id Z)) & ( for x being Real st x in Z holds ( f . x = r * x & r <> 0 & f . x > - 1 & f . x < 1 ) ) holds ( ((- (1 / r)) (#) (arccot * f)) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (1 / r)) (#) (arccot * f)) - (id Z)) `| Z) . x = - (((r * x) ^2) / (1 + ((r * x) ^2))) ) ) proofend; ::f.x=ln.x*arctan.x theorem :: SIN_COS9:127 for Z being open Subset of REAL st Z c= dom (ln (#) arctan) & Z c= ].(- 1),1.[ holds ( ln (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) arctan) `| Z) . x = ((arctan . x) / x) + ((ln . x) / (1 + (x ^2))) ) ) proofend; ::f.x=ln.x*arccot.x theorem :: SIN_COS9:128 for Z being open Subset of REAL st Z c= dom (ln (#) arccot) & Z c= ].(- 1),1.[ holds ( ln (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds ((ln (#) arccot) `| Z) . x = ((arccot . x) / x) - ((ln . x) / (1 + (x ^2))) ) ) proofend; ::f.x=1/x*arctan.x theorem :: SIN_COS9:129 for Z being open Subset of REAL st not 0 in Z & 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; ::f.x=1/x*arccot.x theorem :: SIN_COS9:130 for Z being open Subset of REAL st not 0 in Z & 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;