:: Several Differentiation Formulas of Special Functions -- Part {VII}
:: by Fuguo Ge and Bing Xie
::
:: Copyright (c) 2008-2019 Association of Mizar Users

::f.x=arctan.(sin.x)
theorem :: FDIFF_11:1
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( sin . x > - 1 & sin . x < 1 ) ) holds
( arctan * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . x) / (1 + ((sin . x) ^2)) ) )
proof end;

::f.x=arccot.(sin.x)
theorem :: FDIFF_11:2
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( sin . x > - 1 & sin . x < 1 ) ) holds
( arccot * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((cos . x) / (1 + ((sin . x) ^2))) ) )
proof end;

::f.x=arctan.(cos.x)
theorem :: FDIFF_11:3
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( cos . x > - 1 & cos . x < 1 ) ) holds
( arctan * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin . x) / (1 + ((cos . x) ^2))) ) )
proof end;

::f.x=arccot.(cos.x)
theorem :: FDIFF_11:4
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( cos . x > - 1 & cos . x < 1 ) ) holds
( arccot * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin . x) / (1 + ((cos . x) ^2)) ) )
proof end;

::f.x=arctan.(tan.x)
theorem :: FDIFF_11:5
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( tan . x > - 1 & tan . x < 1 ) ) holds
( arctan * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 ) )
proof end;

::f.x=arccot.(tan.x)
theorem :: FDIFF_11:6
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( tan . x > - 1 & tan . x < 1 ) ) holds
( arccot * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - 1 ) )
proof end;

::f.x=arctan.(cot.x)
theorem :: FDIFF_11:7
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( cot . x > - 1 & cot . x < 1 ) ) holds
( arctan * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - 1 ) )
proof end;

::f.x=arccot.(cot.x)
theorem :: FDIFF_11:8
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
( cot . x > - 1 & cot . x < 1 ) ) holds
( arccot * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 ) )
proof end;

::f.x=arctan.(arctan.x)
theorem :: FDIFF_11:9
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arctan . x > - 1 & arctan . x < 1 ) ) holds
( arctan * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / ((1 + (x ^2)) * (1 + (() ^2))) ) )
proof end;

::f.x=arccot.(arctan.x)
theorem :: FDIFF_11:10
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arctan . x > - 1 & arctan . x < 1 ) ) holds
( arccot * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / ((1 + (x ^2)) * (1 + (() ^2)))) ) )
proof end;

::f.x=arctan.(arccot.x)
theorem :: FDIFF_11:11
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arccot . x > - 1 & arccot . x < 1 ) ) holds
( arctan * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / ((1 + (x ^2)) * (1 + (() ^2)))) ) )
proof end;

::f.x=arccot.(arccot.x)
theorem :: FDIFF_11:12
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
( arccot . x > - 1 & arccot . x < 1 ) ) holds
( arccot * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / ((1 + (x ^2)) * (1 + (() ^2))) ) )
proof end;

::f.x=sin.(arctan.x)
theorem :: FDIFF_11:13
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . ()) / (1 + (x ^2)) ) )
proof end;

::f.x=sin.(arccot.x)
theorem :: FDIFF_11:14
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((cos . ()) / (1 + (x ^2))) ) )
proof end;

::f.x=cos.(arctan.x)
theorem :: FDIFF_11:15
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin . ()) / (1 + (x ^2))) ) )
proof end;

::f.x=cos.(arccot.x)
theorem :: FDIFF_11:16
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin . ()) / (1 + (x ^2)) ) )
proof end;

::f.x=tan.(arctan.x)
theorem :: FDIFF_11:17
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( tan * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / (((cos . ()) ^2) * (1 + (x ^2))) ) )
proof end;

::f.x=tan.(arccot.x)
theorem :: FDIFF_11:18
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( tan * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / (((cos . ()) ^2) * (1 + (x ^2)))) ) )
proof end;

::f.x=cot.(arctan.x)
theorem :: FDIFF_11:19
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cot * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / (((sin . ()) ^2) * (1 + (x ^2)))) ) )
proof end;

::f.x=cot.(arccot.x)
theorem :: FDIFF_11:20
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cot * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / (((sin . ()) ^2) * (1 + (x ^2))) ) )
proof end;

::f.x=sec.(arctan.x)
theorem :: FDIFF_11:21
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin . ()) / (((cos . ()) ^2) * (1 + (x ^2))) ) )
proof end;

::f.x=sec.(arccot.x)
theorem :: FDIFF_11:22
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin . ()) / (((cos . ()) ^2) * (1 + (x ^2)))) ) )
proof end;

::f.x=cosec.(arctan.x)
theorem :: FDIFF_11:23
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cosec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((cos . ()) / (((sin . ()) ^2) * (1 + (x ^2)))) ) )
proof end;

::f.x=cosec.(arccot.x)
theorem :: FDIFF_11:24
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cosec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . ()) / (((sin . ()) ^2) * (1 + (x ^2))) ) )
proof end;

::f.x=sin.x*arctan.x
theorem :: FDIFF_11:25
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) * ()) + ((sin . x) / (1 + (x ^2))) ) )
proof end;

::f.x=sin.x*arccot.x
theorem :: FDIFF_11:26
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) * ()) - ((sin . x) / (1 + (x ^2))) ) )
proof end;

::f.x=cos.x*arctan.x
theorem :: FDIFF_11:27
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- ((sin . x) * ())) + ((cos . x) / (1 + (x ^2))) ) )
proof end;

::f.x=cos.x*arccot.x
theorem :: FDIFF_11:28
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- ((sin . x) * ())) - ((cos . x) / (1 + (x ^2))) ) )
proof end;

::f.x=tan.x*arctan.x
theorem :: FDIFF_11:29
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( tan (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() / ((cos . x) ^2)) + ((tan . x) / (1 + (x ^2))) ) )
proof end;

::f.x=tan.x*arccot.x
theorem :: FDIFF_11:30
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( tan (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() / ((cos . x) ^2)) - ((tan . x) / (1 + (x ^2))) ) )
proof end;

::f.x=cot.x*arctan.x
theorem :: FDIFF_11:31
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cot (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (() / ((sin . x) ^2))) + ((cot . x) / (1 + (x ^2))) ) )
proof end;

::f.x=cot.x*arccot.x
theorem :: FDIFF_11:32
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cot (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (() / ((sin . x) ^2))) - ((cot . x) / (1 + (x ^2))) ) )
proof end;

::f.x=sec.x*arctan.x
theorem :: FDIFF_11:33
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sec (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (((sin . x) * ()) / ((cos . x) ^2)) + (1 / ((cos . x) * (1 + (x ^2)))) ) )
proof end;

::f.x=sec.x*arccot.x
theorem :: FDIFF_11:34
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sec (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (((sin . x) * ()) / ((cos . x) ^2)) - (1 / ((cos . x) * (1 + (x ^2)))) ) )
proof end;

::f.x=cosec.x*arctan.x
theorem :: FDIFF_11:35
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cosec (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (((cos . x) * ()) / ((sin . x) ^2))) + (1 / ((sin . x) * (1 + (x ^2)))) ) )
proof end;

::f.x=cosec.x*arccot.x
theorem :: FDIFF_11:36
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cosec (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (((cos . x) * ()) / ((sin . x) ^2))) - (1 / ((sin . x) * (1 + (x ^2)))) ) )
proof end;

::f.x=arctan.x+arccot.x
theorem Th37: :: FDIFF_11:37
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( arctan + arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 0 ) )
proof end;

::f.x=arctan.x-arccot.x
theorem Th38: :: FDIFF_11:38
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( arctan - arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 2 / (1 + (x ^2)) ) )
proof end;

::f.x=sin.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:39
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( sin (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . x) * (() + ()) ) )
proof end;

::f.x=sin.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:40
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( sin (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) * (() - ())) + ((2 * (sin . x)) / (1 + (x ^2))) ) )
proof end;

::f.x=cos.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:41
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( cos (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin . x) * (() + ())) ) )
proof end;

::f.x=cos.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:42
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( cos (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- ((sin . x) * (() - ()))) + ((2 * (cos . x)) / (1 + (x ^2))) ) )
proof end;

::f.x=tan.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:43
for Z being open Subset of REAL st Z c= dom tan & Z c= ].(- 1),1.[ holds
( tan (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() + ()) / ((cos . x) ^2) ) )
proof end;

::f.x=tan.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:44
for Z being open Subset of REAL st Z c= dom tan & Z c= ].(- 1),1.[ holds
( tan (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((() - ()) / ((cos . x) ^2)) + ((2 * (tan . x)) / (1 + (x ^2))) ) )
proof end;

::f.x=cot.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:45
for Z being open Subset of REAL st Z c= dom cot & Z c= ].(- 1),1.[ holds
( cot (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((() + ()) / ((sin . x) ^2)) ) )
proof end;

::f.x=cot.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:46
for Z being open Subset of REAL st Z c= dom cot & Z c= ].(- 1),1.[ holds
( cot (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- ((() - ()) / ((sin . x) ^2))) + ((2 * (cot . x)) / (1 + (x ^2))) ) )
proof end;

::f.x=sec.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:47
for Z being open Subset of REAL st Z c= dom sec & Z c= ].(- 1),1.[ holds
( sec (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((() + ()) * (sin . x)) / ((cos . x) ^2) ) )
proof end;

::f.x=sec.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:48
for Z being open Subset of REAL st Z c= dom sec & Z c= ].(- 1),1.[ holds
( sec (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (((() - ()) * (sin . x)) / ((cos . x) ^2)) + ((2 * (sec . x)) / (1 + (x ^2))) ) )
proof end;

::f.x=cosec.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:49
for Z being open Subset of REAL st Z c= dom cosec & Z c= ].(- 1),1.[ holds
( cosec (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (((() + ()) * (cos . x)) / ((sin . x) ^2)) ) )
proof end;

::f.x=cosec.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:50
for Z being open Subset of REAL st Z c= dom cosec & Z c= ].(- 1),1.[ holds
( cosec (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (((() - ()) * (cos . x)) / ((sin . x) ^2))) + ((2 * ()) / (1 + (x ^2))) ) )
proof end;

::f.x=exp_R.x*(arctan.x+arccot.x)
theorem :: FDIFF_11:51
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = () * (() + ()) ) )
proof end;

::f.x=exp_R.x*(arctan.x-arccot.x)
theorem :: FDIFF_11:52
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() * (() - ())) + ((2 * ()) / (1 + (x ^2))) ) )
proof end;

::f.x=(arctan.x+arccot.x)/exp_R.x
theorem :: FDIFF_11:53
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((() + ()) / ()) ) )
proof end;

::f.x=(arctan.x-arccot.x)/exp_R.x
theorem :: FDIFF_11:54
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (((2 / (1 + (x ^2))) - ()) + ()) / () ) )
proof end;

::f.x=exp_R.(arctan.x+arccot.x)
theorem :: FDIFF_11:55
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( exp_R * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 0 ) )
proof end;

::f.x=exp_R.(arctan.x-arccot.x)
theorem :: FDIFF_11:56
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( exp_R * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (2 * (exp_R . (() - ()))) / (1 + (x ^2)) ) )
proof end;

::f.x=sin.(arctan.x+arccot.x)
theorem :: FDIFF_11:57
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 0 ) )
proof end;

::f.x=sin.(arctan.x-arccot.x)
theorem :: FDIFF_11:58
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( sin * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (2 * (cos . (() - ()))) / (1 + (x ^2)) ) )
proof end;

::f.x=cos.(arctan.x+arccot.x)
theorem :: FDIFF_11:59
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 0 ) )
proof end;

::f.x=cos.(arctan.x-arccot.x)
theorem :: FDIFF_11:60
for Z being open Subset of REAL st Z c= dom () & Z c= ].(- 1),1.[ holds
( cos * () is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((2 * (sin . (() - ()))) / (1 + (x ^2))) ) )
proof end;

::f.x=arctan.x*arccot.x
theorem :: FDIFF_11:61
for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( arctan (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() - ()) / (1 + (x ^2)) ) )
proof end;

::f.x=arctan.(1/x)*arccot.(1/x)
theorem :: FDIFF_11:62
for Z being open Subset of REAL st not 0 in Z & Z c= dom ((arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^))) & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( (arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((arctan * ((id Z) ^)) (#) (arccot * ((id Z) ^))) | Z) . x = ((arctan . (1 / x)) - (arccot . (1 / x))) / (1 + (x ^2)) ) )
proof end;

::f.x=x*arctan(1/x)
theorem :: FDIFF_11:63
for Z being open Subset of REAL st not 0 in Z & Z c= dom ((id Z) (#) (arctan * ((id Z) ^))) & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( (id Z) (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (arctan * ((id Z) ^))) | Z) . x = (arctan . (1 / x)) - (x / (1 + (x ^2))) ) )
proof end;

::f.x=x*arccot(1/x)
theorem :: FDIFF_11:64
for Z being open Subset of REAL st not 0 in Z & Z c= dom ((id Z) (#) (arccot * ((id Z) ^))) & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( (id Z) (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((id Z) (#) (arccot * ((id Z) ^))) | Z) . x = (arccot . (1 / x)) + (x / (1 + (x ^2))) ) )
proof end;

::f.x=x^2*arctan(1/x)
theorem :: FDIFF_11:65
for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (arctan * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( g (#) (arctan * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arctan * ((id Z) ^))) | Z) . x = ((2 * x) * (arctan . (1 / x))) - ((x ^2) / (1 + (x ^2))) ) )
proof end;

::f.x=x^2*arccot(1/x)
theorem :: FDIFF_11:66
for Z being open Subset of REAL
for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (arccot * ((id Z) ^))) & g = #Z 2 & ( for x being Real st x in Z holds
( ((id Z) ^) . x > - 1 & ((id Z) ^) . x < 1 ) ) holds
( g (#) (arccot * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
((g (#) (arccot * ((id Z) ^))) | Z) . x = ((2 * x) * (arccot . (1 / x))) + ((x ^2) / (1 + (x ^2))) ) )
proof end;

::f.x=1/arctan.x
theorem Th67: :: FDIFF_11:67
for Z being open Subset of REAL st Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arctan . x <> 0 ) holds
( arctan ^ is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (1 / ((() ^2) * (1 + (x ^2)))) ) )
proof end;

::f.x=1/arccot.x
theorem Th68: :: FDIFF_11:68
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
(() | Z) . x = 1 / ((() ^2) * (1 + (x ^2))) ) )
proof end;

::f.x=1/(n*(arctan.x)|^n)
theorem :: FDIFF_11:69
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * ())) & Z c= ].(- 1),1.[ & n > 0 & ( for x being Real st x in Z holds
arctan . x <> 0 ) holds
( (1 / n) (#) ((#Z n) * ()) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * ())) | Z) . x = - (1 / ((() #Z (n + 1)) * (1 + (x ^2)))) ) )
proof end;

::f.x=1/(n*(arccot.x)|^n)
theorem :: FDIFF_11:70
for n being Element of NAT
for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * ())) & Z c= ].(- 1),1.[ & n > 0 holds
( (1 / n) (#) ((#Z n) * ()) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * ())) | Z) . x = 1 / ((() #Z (n + 1)) * (1 + (x ^2))) ) )
proof end;

::f.x=2*(arctan #R (1/2))
theorem :: FDIFF_11:71
for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * arctan)) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arctan . x > 0 ) holds
( 2 (#) ((#R (1 / 2)) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * arctan)) | Z) . x = (() #R (- (1 / 2))) / (1 + (x ^2)) ) )
proof end;

::f.x=2*(arccot #R (1/2))
theorem :: FDIFF_11:72
for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * arccot)) & Z c= ].(- 1),1.[ holds
( 2 (#) ((#R (1 / 2)) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((2 (#) ((#R (1 / 2)) * arccot)) | Z) . x = - ((() #R (- (1 / 2))) / (1 + (x ^2))) ) )
proof end;

::f.x=(2/3)*(arctan #R (3/2))
theorem :: FDIFF_11:73
for Z being open Subset of REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arctan)) & Z c= ].(- 1),1.[ & ( for x being Real st x in Z holds
arctan . x > 0 ) holds
( (2 / 3) (#) ((#R (3 / 2)) * arctan) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * arctan)) | Z) . x = (() #R (1 / 2)) / (1 + (x ^2)) ) )
proof end;

::f.x=(2/3)*(arccot #R (3/2))
theorem :: FDIFF_11:74
for Z being open Subset of REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * arccot)) & Z c= ].(- 1),1.[ holds
( (2 / 3) (#) ((#R (3 / 2)) * arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
(((2 / 3) (#) ((#R (3 / 2)) * arccot)) | Z) . x = - ((() #R (1 / 2)) / (1 + (x ^2))) ) )
proof end;