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