:: Inverse Trigonometric Functions Arctan and Arccot :: by Xiquan Liang and Bing Xie :: :: Received March 18, 2008 :: Copyright (c) 2008-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XREAL_0, SUBSET_1, RCOMP_1, PARTFUN1, XXREAL_1, ARYTM_1, SIN_COS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, CARD_1, FUNCT_1, FDIFF_1, SQUARE_1, ORDINAL2, XXREAL_0, VALUED_0, VALUED_1, TAYLOR_1, PREPOWER, ORDINAL4, LIMFUNC1, SIN_COS9, ORDINAL1; notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, REAL_1, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, FCONT_1, XBOOLE_0, TAYLOR_1, PREPOWER, LIMFUNC1, RFUNCT_2; constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1, SIN_COS, PARTFUN2, SIN_COS4, TAYLOR_1, PREPOWER, LIMFUNC1, VALUED_1, XXREAL_2, PARTFUN1, SIN_COS6, RELSET_1, COMPLEX1; registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1, SIN_COS, FUNCT_1, SIN_COS6, RFUNCT_2, NUMBERS, INT_1, VALUED_0, XXREAL_2, ORDINAL1, SQUARE_1, PREPOWER; requirements SUBSET, NUMERALS, ARITHM, REAL; begin :: arctan,arccot reserve x,x0, r, s, h for Real, n for Element of NAT, rr, y for set, Z for open Subset of REAL, f, f1, f2 for PartFunc of REAL,REAL; theorem :: SIN_COS9:1 ].-PI/2,PI/2.[ c= dom tan; theorem :: SIN_COS9:2 ].0,PI.[ c= dom cot; theorem :: SIN_COS9:3 tan is_differentiable_on ].-PI/2,PI/2.[ & for x st x in ].-PI/2,PI/2.[ holds diff(tan,x) = 1/(cos.x)^2; theorem :: SIN_COS9:4 cot is_differentiable_on ].0,PI.[ & for x st x in ].0,PI.[ holds diff( cot,x) = -1/(sin.x)^2; theorem :: SIN_COS9:5 tan|].-PI/2,PI/2.[ is continuous; theorem :: SIN_COS9:6 cot|].0,PI.[ is continuous; theorem :: SIN_COS9:7 tan|].-PI/2,PI/2.[ is increasing; theorem :: SIN_COS9:8 cot|].0,PI.[ is decreasing; theorem :: SIN_COS9:9 tan | ].-PI/2,PI/2.[ is one-to-one; theorem :: SIN_COS9:10 cot | ].0,PI.[ is one-to-one; registration cluster tan | ].-PI/2,PI/2.[ -> one-to-one; cluster cot | ].0,PI.[ -> one-to-one; end; definition func arctan -> PartFunc of REAL,REAL equals :: SIN_COS9:def 1 (tan | ].-PI/2,PI/2.[)"; func arccot -> PartFunc of REAL, REAL equals :: SIN_COS9:def 2 (cot | ].0,PI.[)"; end; definition let r be Real; func arctan r -> number equals :: SIN_COS9:def 3 arctan.r; func arccot r -> number equals :: SIN_COS9:def 4 arccot.r; end; registration let r be Real; cluster arctan r -> real; cluster arccot r -> real; end; theorem :: SIN_COS9:11 rng arctan = ].-PI/2,PI/2.[; theorem :: SIN_COS9:12 rng arccot = ].0,PI.[; registration cluster arctan -> one-to-one; cluster arccot -> one-to-one; end; theorem :: SIN_COS9:13 for x be Real st x in ].-PI/2,PI/2.[ holds tan.x = tan x; theorem :: SIN_COS9:14 for x be Real st x in ].0,PI.[ holds cot.x = cot x; theorem :: SIN_COS9:15 for x be Real st cos.x <> 0 holds tan.x = tan x; theorem :: SIN_COS9:16 for x be Real st sin.x <> 0 holds cot.x = cot x; theorem :: SIN_COS9:17 tan.(-PI/4) = -1 & tan(-PI/4) = -1; theorem :: SIN_COS9:18 cot.(PI/4) = 1 & cot(PI/4) = 1 & cot.(3/4*PI) = -1 & cot(3/4*PI) = -1; theorem :: SIN_COS9:19 for x be set st x in [.-PI/4,PI/4.] holds tan.x in [.-1,1.]; theorem :: SIN_COS9:20 for x be set st x in [.PI/4,3/4*PI.] holds cot.x in [.-1,1.]; theorem :: SIN_COS9:21 rng (tan | [.-PI/4,PI/4.]) = [.-1,1.]; theorem :: SIN_COS9:22 rng (cot | [.PI/4,3/4*PI.]) = [.-1,1.]; theorem :: SIN_COS9:23 [.-1,1.] c= dom arctan; theorem :: SIN_COS9:24 [.-1,1.] c= dom arccot; registration cluster tan | [.-PI/4,PI/4.] -> one-to-one; cluster cot | [.PI/4,3/4*PI.] -> one-to-one; end; theorem :: SIN_COS9:25 arctan | [.-1,1.] = (tan | [.-PI/4,PI/4.])"; theorem :: SIN_COS9:26 arccot | [.-1,1.] = (cot | [.PI/4,3/4*PI.])"; theorem :: SIN_COS9:27 (tan | [.-PI/4,PI/4.]) qua Function * (arctan | [.-1,1.]) = id [.-1,1 .]; theorem :: SIN_COS9:28 (cot | [.PI/4,3/4*PI.]) qua Function * (arccot | [.-1,1.]) = id [.-1,1 .]; theorem :: SIN_COS9:29 (tan | [.-PI/4,PI/4.]) * (arctan | [.-1,1.]) = id [.-1,1.]; theorem :: SIN_COS9:30 (cot | [.PI/4,3/4*PI.]) * (arccot | [.-1,1.]) = id [.-1,1.]; theorem :: SIN_COS9:31 (arctan qua Function) * (tan | ].-PI/2,PI/2.[) = id ].-PI/2,PI/2 .[; theorem :: SIN_COS9:32 arccot * (cot | ].0,PI.[) = id ].0,PI.[; theorem :: SIN_COS9:33 arctan qua Function * (tan | ].-PI/2,PI/2.[) = id ].-PI/2,PI/2.[; theorem :: SIN_COS9:34 arccot qua Function * (cot | ].0,PI.[) = id ].0,PI.[; theorem :: SIN_COS9:35 -PI/2 < r & r < PI/2 implies arctan tan.r = r & arctan tan r = r; theorem :: SIN_COS9:36 0 < r & r < PI implies arccot cot.r = r & arccot cot r = r; theorem :: SIN_COS9:37 arctan (-1) = -PI/4 & arctan.(-1) = -PI/4; theorem :: SIN_COS9:38 arccot (-1) = 3/4*PI & arccot.(-1) = 3/4*PI; theorem :: SIN_COS9:39 arctan 1 = PI/4 & arctan.1 = PI/4; theorem :: SIN_COS9:40 arccot 1 = PI/4 & arccot.1 = PI/4; theorem :: SIN_COS9:41 tan.0 = 0 & tan 0 =0; theorem :: SIN_COS9:42 cot.(PI/2) = 0 & cot (PI/2) = 0; theorem :: SIN_COS9:43 arctan 0 = 0 & arctan.0 = 0; theorem :: SIN_COS9:44 arccot 0 = PI/2 & arccot.0 = PI/2; theorem :: SIN_COS9:45 arctan|(tan.:].-PI/2,PI/2.[) is increasing; theorem :: SIN_COS9:46 arccot|(cot.:].0,PI.[) is decreasing; theorem :: SIN_COS9:47 arctan|[.-1,1.] is increasing; theorem :: SIN_COS9:48 arccot|[.-1,1.] is decreasing; theorem :: SIN_COS9:49 for x be set st x in [.-1,1.] holds arctan.x in [.-PI/4,PI/4.]; theorem :: SIN_COS9:50 for x be set st x in [.-1,1.] holds arccot.x in [.PI/4,3/4*PI.]; theorem :: SIN_COS9:51 -1 <= r & r <= 1 implies tan arctan r = r; theorem :: SIN_COS9:52 -1 <= r & r <= 1 implies cot arccot r = r; theorem :: SIN_COS9:53 arctan|[.-1,1.] is continuous; theorem :: SIN_COS9:54 arccot|[.-1,1.] is continuous; theorem :: SIN_COS9:55 rng(arctan | [.-1,1.]) = [.-PI/4,PI/4.]; theorem :: SIN_COS9:56 rng(arccot | [.-1,1.]) = [.PI/4,3/4*PI.]; theorem :: SIN_COS9:57 -1 <= r & r <= 1 & arctan r = -PI/4 implies r = -1; theorem :: SIN_COS9:58 -1 <= r & r <= 1 & arccot r = 3/4*PI implies r = -1; theorem :: SIN_COS9:59 -1 <= r & r <= 1 & arctan r = 0 implies r = 0; theorem :: SIN_COS9:60 -1 <= r & r <= 1 & arccot r = PI/2 implies r = 0; theorem :: SIN_COS9:61 -1 <= r & r <= 1 & arctan r = PI/4 implies r = 1; theorem :: SIN_COS9:62 -1 <= r & r <= 1 & arccot r = PI/4 implies r = 1; theorem :: SIN_COS9:63 -1 <= r & r <= 1 implies -PI/4 <= arctan r & arctan r <= PI/4; theorem :: SIN_COS9:64 -1 <= r & r <= 1 implies PI/4 <= arccot r & arccot r <= 3/4*PI; theorem :: SIN_COS9:65 -1 < r & r < 1 implies -PI/4 < arctan r & arctan r < PI/4; theorem :: SIN_COS9:66 -1 < r & r < 1 implies PI/4 < arccot r & arccot r < 3/4*PI; theorem :: SIN_COS9:67 -1 <= r & r <= 1 implies arctan r = -arctan(-r); theorem :: SIN_COS9:68 -1 <= r & r <= 1 implies arccot r = PI - arccot(-r); theorem :: SIN_COS9:69 -1 <= r & r <= 1 implies cot arctan r = 1/r; theorem :: SIN_COS9:70 -1 <= r & r <= 1 implies tan arccot r = 1/r; theorem :: SIN_COS9:71 arctan is_differentiable_on tan.:].-PI/2,PI/2.[; theorem :: SIN_COS9:72 arccot is_differentiable_on cot.:].0,PI.[; theorem :: SIN_COS9:73 arctan is_differentiable_on ].-1,1.[; theorem :: SIN_COS9:74 arccot is_differentiable_on ].-1,1.[; theorem :: SIN_COS9:75 -1 <= r & r <= 1 implies diff(arctan,r) = 1/(1+r^2); theorem :: SIN_COS9:76 -1 <= r & r <= 1 implies diff(arccot,r) = -1/(1+r^2); theorem :: SIN_COS9:77 arctan|(tan.:].-PI/2,PI/2.[) is continuous; theorem :: SIN_COS9:78 arccot|(cot.:].0,PI.[) is continuous; theorem :: SIN_COS9:79 dom arctan is open; theorem :: SIN_COS9:80 dom arccot is open; begin :: Differentiation Formulas of arctan,arccot :: f.x=arctan.x theorem :: SIN_COS9:81 Z c= ].-1,1.[ implies arctan is_differentiable_on Z & for x st x in Z holds ((arctan)`|Z).x = 1/(1+x^2); :: f.x=arccot.x theorem :: SIN_COS9:82 Z c= ].-1,1.[ implies arccot is_differentiable_on Z & for x st x in Z holds ((arccot)`|Z).x = -1/(1+x^2); ::f.x=r*arctanx theorem :: SIN_COS9:83 Z c= ].-1,1.[ implies r(#)arctan is_differentiable_on Z & for x st x in Z holds ((r(#)arctan)`|Z).x = r/(1+x^2); ::f.x=r*arccotx theorem :: SIN_COS9:84 Z c= ].-1,1.[ implies r(#)arccot is_differentiable_on Z & for x st x in Z holds ((r(#)arccot)`|Z).x = -r/(1+x^2); theorem :: SIN_COS9:85 f is_differentiable_in x & f.x > -1 & f.x < 1 implies (arctan)*f is_differentiable_in x & diff((arctan)*f,x) = diff(f,x)/(1+(f.x)^2); theorem :: SIN_COS9:86 f is_differentiable_in x & f.x > -1 & f.x < 1 implies (arccot)*f is_differentiable_in x & diff((arccot)*f,x) = -diff(f,x)/(1+(f.x)^2); ::f.x=arctan.(r*x+s) theorem :: SIN_COS9:87 Z c= dom ((arctan)*f) & (for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1) implies (arctan)*f is_differentiable_on Z & for x st x in Z holds (((arctan)*f)`|Z).x = r/(1+(r*x+s)^2); ::f.x=arccot.(r*x+s) theorem :: SIN_COS9:88 Z c= dom ((arccot)*f) & (for x st x in Z holds f.x=r*x+s & f.x > -1 & f.x < 1) implies (arccot)*f is_differentiable_on Z & for x st x in Z holds (((arccot)*f)`|Z).x = -r/(1+(r*x+s)^2); ::f.x=ln(arctan.x) theorem :: SIN_COS9:89 Z c= dom (ln*(arctan)) & Z c= ].-1,1.[ & (for x st x in Z holds arctan .x>0) implies ln*(arctan) is_differentiable_on Z & for x st x in Z holds ((ln*( arctan))`|Z).x = 1/((1+x^2)*arctan.x); ::f.x=ln(arccot.x) theorem :: SIN_COS9:90 Z c= dom (ln*(arccot)) & Z c= ].-1,1.[ & (for x st x in Z holds arccot .x>0) implies ln*(arccot) is_differentiable_on Z & for x st x in Z holds ((ln*( arccot))`|Z).x = -1/((1+x^2)*arccot.x); ::f.x=(arctan)|^n theorem :: SIN_COS9:91 Z c= dom (( #Z n)*(arctan)) & Z c=].-1,1.[ implies ( #Z n)*( arctan) is_differentiable_on Z & for x st x in Z holds ((( #Z n)*arctan)`|Z).x = n*(arctan.x) #Z (n-1) / (1+x^2); ::f.x=(arccot)|^n theorem :: SIN_COS9:92 Z c= dom (( #Z n)*(arccot)) & Z c=].-1,1.[ implies ( #Z n)*( arccot) is_differentiable_on Z & for x st x in Z holds ((( #Z n)*arccot)`|Z).x = -n*(arccot.x) #Z (n-1) / (1+x^2); ::f.x=(1/2)*(arctan)|^2 theorem :: SIN_COS9:93 Z c= dom ((1/2)(#)(( #Z 2)*(arctan))) & Z c=].-1,1.[ implies (1/2)(#)( ( #Z 2)*(arctan)) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(( #Z 2)*(arctan)))`|Z).x = arctan.x / (1+x^2); ::f.x=(1/2)*(arccot)|^2 theorem :: SIN_COS9:94 Z c= dom ((1/2)(#)(( #Z 2)*(arccot))) & Z c=].-1,1.[ implies (1/2)(#)( ( #Z 2)*(arccot)) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(( #Z 2)*(arccot)))`|Z).x = -arccot.x / (1+x^2); ::f.x=x*arctan.x theorem :: SIN_COS9:95 Z c= ].-1,1.[ implies (id Z)(#)(arctan) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arctan))`|Z).x = arctan.x + x/(1+x^2); ::f.x=x*arccot.x theorem :: SIN_COS9:96 Z c= ].-1,1.[ implies (id Z)(#)(arccot) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccot))`|Z).x = arccot.x - x/(1+x^2); ::f.x=(r*x+s)*arctan.x theorem :: SIN_COS9:97 Z c= dom (f(#)(arctan)) & Z c= ].-1,1.[ & (for x st x in Z holds f.x=r *x+s) implies f(#)(arctan) is_differentiable_on Z & for x st x in Z holds ((f (#)(arctan))`|Z).x = r*arctan.x + (r*x+s)/(1+x^2); ::f.x=(r*x+s)*arccot.x theorem :: SIN_COS9:98 Z c= dom (f(#)(arccot)) & Z c= ].-1,1.[ & (for x st x in Z holds f.x=r *x+s) implies f(#)(arccot) is_differentiable_on Z & for x st x in Z holds ((f (#)(arccot))`|Z).x = r*arccot.x - (r*x+s)/(1+x^2); ::f.x=(1/2)*arctan(2*x) theorem :: SIN_COS9:99 Z c= dom ((1/2)(#)((arctan)*f)) & (for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1) implies (1/2)(#)((arctan)*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)((arctan)*f))`|Z).x = 1/(1+(2*x)^2); ::f.x=(1/2)*arccot(2*x) theorem :: SIN_COS9:100 Z c= dom ((1/2)(#)((arccot)*f)) & (for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1) implies (1/2)(#)((arccot)*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)((arccot)*f))`|Z).x = -1/(1+(2*x)^2); ::f.x=1+x|^2 theorem :: SIN_COS9:101 Z c= dom (f1+f2) & (for x st x in Z holds f1.x=1) & f2=#Z 2 implies f1+f2 is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x = 2 *x; ::f.x=(1/2)ln(1+x|^2) theorem :: SIN_COS9:102 Z c= dom ((1/2)(#)(ln*(f1+f2))) & f2=#Z 2 & (for x st x in Z holds f1.x=1 ) implies ((1/2)(#)(ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*(f1+f2)))`|Z).x = x/(1+x^2); ::f.x=x*arctan.x-(1/2)ln(1+x|^2) theorem :: SIN_COS9:103 Z c= dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) & Z c= ].-1,1.[ & f2 =#Z 2 & (for x st x in Z holds f1.x=1 ) implies (id Z)(#)(arctan)-(1/2)(#)(ln*( f1+f2)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arctan)-(1/2 )(#)(ln*(f1+f2)))`|Z).x = arctan.x; ::f.x=x*arccot.x+(1/2)ln(1+x|^2) theorem :: SIN_COS9:104 Z c= dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) & Z c= ].-1,1.[ & f2 =#Z 2 & (for x st x in Z holds f1.x=1 ) implies (id Z)(#)(arccot)+(1/2)(#)(ln*( f1+f2)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccot)+(1/2 )(#)(ln*(f1+f2)))`|Z).x = arccot.x; ::f.x=x*arctan(x/r) theorem :: SIN_COS9:105 Z c= dom ((id Z)(#)((arctan)*f)) & (for x st x in Z holds f.x=x /r & f.x > -1 & f.x < 1) implies (id Z)(#)((arctan)*f) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)((arctan)*f))`|Z).x = arctan.(x/r)+x/(r*(1+(x/ r)^2)); ::f.x=x*arccot(x/r) theorem :: SIN_COS9:106 Z c= dom ((id Z)(#)((arccot)*f)) & (for x st x in Z holds f.x=x /r & f.x > -1 & f.x < 1) implies (id Z)(#)((arccot)*f) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)((arccot)*f))`|Z).x = arccot.(x/r)-x/(r*(1+(x/ r)^2)); ::f.x=1+(x/r)^2 theorem :: SIN_COS9:107 Z c= dom (f1+f2) & (for x st x in Z holds f1.x=1) & f2=( #Z 2)* f & (for x st x in Z holds f.x=x/r) implies f1+f2 is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x = (2*x)/(r^2); ::f.x=(r/2)ln(1+(x/r)^2) theorem :: SIN_COS9:108 Z c= dom ((r/2)(#)(ln*(f1+f2))) & (for x st x in Z holds f1.x=1 ) & r <> 0 & f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r) implies ((r/2)(#)( ln*(f1+f2))) is_differentiable_on Z & for x st x in Z holds (((r/2)(#)(ln*(f1+ f2)))`|Z).x = x/(r*(1+(x/r)^2)); ::f.x=x*arctan.(x/r)-(r/2)ln(1+(x/r)^2) theorem :: SIN_COS9:109 Z c= dom ((id Z)(#)((arctan)*f)-(r/2)(#)(ln*(f1+f2))) & r <> 0 & (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) & (for x st x in Z holds f1.x=1 ) & f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r) implies (id Z)(#)((arctan)*f )-(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z & for x st x in Z holds (((id Z) (#)((arctan)*f)-(r/2)(#)(ln*(f1+f2)))`|Z).x = arctan.(x/r); ::f.x=x*arccot.(x/r)+(r/2)ln(1+(x/r)^2) theorem :: SIN_COS9:110 Z c= dom ((id Z)(#)((arccot)*f)+(r/2)(#)(ln*(f1+f2))) & r <> 0 & (for x st x in Z holds f.x=x/r & f.x > -1 & f.x < 1) & (for x st x in Z holds f1.x=1 ) & f2=( #Z 2)*f & (for x st x in Z holds f.x=x/r) implies (id Z)(#)((arccot)*f )+(r/2)(#)(ln*(f1+f2)) is_differentiable_on Z & for x st x in Z holds (((id Z) (#)((arccot)*f)+(r/2)(#)(ln*(f1+f2)))`|Z).x = arccot.(x/r); ::f.x=arctan.(1/x) theorem :: SIN_COS9:111 not 0 in Z & Z c= dom (arctan*((id Z)^)) & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (arctan*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((arctan*((id Z)^))`|Z).x = -1/(1+x^2); ::f.x=arccot.(1/x) theorem :: SIN_COS9:112 not 0 in Z & Z c= dom (arccot*((id Z)^)) & (for x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((arccot*((id Z)^))`|Z).x = 1/(1+x^2); ::f.x=arctan.(r+s*x+h*x^2) theorem :: SIN_COS9:113 Z c= dom (arctan*f) & f=f1+h(#)f2 & (for x st x in Z holds f.x > -1 & f.x < 1) & (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2 implies arctan*(f1+h (#)f2) is_differentiable_on Z & for x st x in Z holds ((arctan*(f1+h(#)f2))`|Z) .x = (s+2*h*x)/(1+(r+s*x+h*x^2)^2); ::f.x=arccot.(r+s*x+h*x^2) theorem :: SIN_COS9:114 Z c= dom (arccot*f) & f=f1+h(#)f2 & (for x st x in Z holds f.x > -1 & f.x < 1) & (for x st x in Z holds f1.x = r+s*x) & f2=#Z 2 implies arccot*(f1+h (#)f2) is_differentiable_on Z & for x st x in Z holds ((arccot*(f1+h(#)f2))`|Z) .x = -(s+2*h*x)/(1+(r+s*x+h*x^2)^2); ::f.x=arctan.(exp_R.x) theorem :: SIN_COS9:115 Z c= dom (arctan*exp_R) & (for x st x in Z holds exp_R.x < 1) implies arctan*exp_R is_differentiable_on Z & for x st x in Z holds ((arctan*exp_R)`|Z) .x = exp_R.x/(1+(exp_R.x)^2); ::f.x=arccot.(exp_R.x) theorem :: SIN_COS9:116 Z c= dom (arccot*exp_R) & (for x st x in Z holds exp_R.x < 1) implies arccot*exp_R is_differentiable_on Z & for x st x in Z holds ((arccot*exp_R)`|Z) .x = -exp_R.x/(1+(exp_R.x)^2); ::f.x=arctan.(ln.x) theorem :: SIN_COS9:117 Z c= dom (arctan*ln) & (for x st x in Z holds ln.x > -1 & ln.x < 1) implies arctan*ln is_differentiable_on Z & for x st x in Z holds ((arctan*ln)`| Z).x = 1/(x*(1+(ln.x)^2)); ::f.x=arccot.(ln.x) theorem :: SIN_COS9:118 Z c= dom (arccot*ln) & (for x st x in Z holds ln.x > -1 & ln.x < 1) implies arccot*ln is_differentiable_on Z & for x st x in Z holds ((arccot*ln)`| Z).x = -1/(x*(1+(ln.x)^2)); ::f.x=exp_R.(arctan.x) theorem :: SIN_COS9:119 Z c= dom (exp_R*arctan) & Z c= ].-1,1.[ implies exp_R*arctan is_differentiable_on Z & for x st x in Z holds ((exp_R*arctan)`|Z).x = exp_R.( arctan.x)/(1+x^2); ::f.x=exp_R.(arccot.x) theorem :: SIN_COS9:120 Z c= dom (exp_R*arccot) & Z c= ].-1,1.[ implies exp_R*arccot is_differentiable_on Z & for x st x in Z holds ((exp_R*arccot)`|Z).x = -exp_R.( arccot.x)/(1+x^2); ::f.x=arctan.x-x theorem :: SIN_COS9:121 Z c= dom (arctan-id Z) & Z c= ].-1,1.[ implies arctan-id Z is_differentiable_on Z & for x st x in Z holds ((arctan-id Z)`|Z).x = -x^2/(1+x ^2); ::f.x=-arccot.x-x theorem :: SIN_COS9:122 Z c= dom (-arccot-id Z) & Z c= ].-1,1.[ implies -arccot-id Z is_differentiable_on Z & for x st x in Z holds ((-arccot-id Z)`|Z).x = -x^2/(1+ x^2); ::f.x=exp_R.x*arctan.x theorem :: SIN_COS9:123 Z c= ].-1,1.[ implies (exp_R(#)arctan) is_differentiable_on Z & for x st x in Z holds ((exp_R(#)arctan)`|Z).x = exp_R.x*arctan.x+exp_R.x/(1+x^2); ::f.x=exp_R.x*arccot.x theorem :: SIN_COS9:124 Z c= ].-1,1.[ implies (exp_R(#)arccot) is_differentiable_on Z & for x st x in Z holds ((exp_R(#)arccot)`|Z).x = exp_R.x*arccot.x-exp_R.x/(1+x^2); ::f.x=(1/r)*arctan.(r*x)-x theorem :: SIN_COS9:125 Z c= dom ((1/r)(#)(arctan*f)-id Z) & (for x st x in Z holds f.x=r*x & r<>0 & f.x > -1 & f.x < 1) implies (1/r)(#)(arctan*f)-id Z is_differentiable_on Z & for x st x in Z holds (((1/r)(#)(arctan*f)-id Z)`|Z).x = -(r*x)^2/(1+(r*x) ^2); ::f.x=(-1/r)*arccot.(r*x)-x theorem :: SIN_COS9:126 Z c= dom ((-1/r)(#)(arccot*f)-id Z) & (for x st x in Z holds f.x=r*x & r<>0 & f.x > -1 & f.x < 1) implies (-1/r)(#)(arccot*f)-id Z is_differentiable_on Z & for x st x in Z holds (((-1/r)(#)(arccot*f)-id Z)`|Z). x = -(r*x)^2/(1+(r*x)^2); ::f.x=ln.x*arctan.x theorem :: SIN_COS9:127 Z c= dom (ln(#)arctan) & Z c= ].-1,1.[ implies (ln(#)arctan) is_differentiable_on Z & for x st x in Z holds ((ln(#)arctan)`|Z).x = arctan.x/ x+ln.x/(1+x^2); ::f.x=ln.x*arccot.x theorem :: SIN_COS9:128 Z c= dom (ln(#)arccot) & Z c= ].-1,1.[ implies (ln(#)arccot) is_differentiable_on Z & for x st x in Z holds ((ln(#)arccot)`|Z).x = arccot.x/ x-ln.x/(1+x^2); ::f.x=1/x*arctan.x theorem :: SIN_COS9:129 not 0 in Z & Z c= dom ((id Z)^(#)arctan) & Z c= ].-1,1.[ implies ((id Z)^(#)arctan) is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)arctan )`|Z).x = -arctan.x/(x^2)+1/(x*(1+x^2)); ::f.x=1/x*arccot.x theorem :: SIN_COS9:130 not 0 in Z & Z c= dom ((id Z)^(#)arccot) & Z c= ].-1,1.[ implies ((id Z)^(#)arccot) is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)arccot )`|Z).x = -arccot.x/(x^2)-1/(x*(1+x^2));