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

begin

theorem :: FDIFF_11:1

for Z being open Subset of REAL st Z c= dom (arctan * sin) & ( 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
((arctan * sin) `| Z) . x = (cos . x) / (1 + ((sin . x) ^2)) ) )

proof end;

theorem :: FDIFF_11:2

for Z being open Subset of REAL st Z c= dom (arccot * sin) & ( 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
((arccot * sin) `| Z) . x = - ((cos . x) / (1 + ((sin . x) ^2))) ) )

proof end;

theorem :: FDIFF_11:3

for Z being open Subset of REAL st Z c= dom (arctan * cos) & ( 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
((arctan * cos) `| Z) . x = - ((sin . x) / (1 + ((cos . x) ^2))) ) )

proof end;

theorem :: FDIFF_11:4

for Z being open Subset of REAL st Z c= dom (arccot * cos) & ( 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
((arccot * cos) `| Z) . x = (sin . x) / (1 + ((cos . x) ^2)) ) )

proof end;

theorem :: FDIFF_11:5

for Z being open Subset of REAL st Z c= dom (arctan * tan) & ( 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
((arctan * tan) `| Z) . x = 1 ) )

proof end;

theorem :: FDIFF_11:6

for Z being open Subset of REAL st Z c= dom (arccot * tan) & ( 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
((arccot * tan) `| Z) . x = - 1 ) )

proof end;

theorem :: FDIFF_11:7

for Z being open Subset of REAL st Z c= dom (arctan * cot) & ( 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
((arctan * cot) `| Z) . x = - 1 ) )

proof end;

theorem :: FDIFF_11:8

for Z being open Subset of REAL st Z c= dom (arccot * cot) & ( 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
((arccot * cot) `| Z) . x = 1 ) )

proof end;

theorem :: FDIFF_11:9

for Z being open Subset of REAL st Z c= dom (arctan * arctan) & 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
((arctan * arctan) `| Z) . x = 1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2))) ) )

proof end;

theorem :: FDIFF_11:10

for Z being open Subset of REAL st Z c= dom (arccot * arctan) & 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
((arccot * arctan) `| Z) . x = - (1 / ((1 + (x ^2)) * (1 + ((arctan . x) ^2)))) ) )

proof end;

theorem :: FDIFF_11:11

for Z being open Subset of REAL st Z c= dom (arctan * arccot) & 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
((arctan * arccot) `| Z) . x = - (1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2)))) ) )

proof end;

theorem :: FDIFF_11:12

for Z being open Subset of REAL st Z c= dom (arccot * arccot) & 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
((arccot * arccot) `| Z) . x = 1 / ((1 + (x ^2)) * (1 + ((arccot . x) ^2))) ) )

proof end;

theorem :: FDIFF_11:13

for Z being open Subset of REAL st Z c= dom (sin * arctan) & Z c= ].(- 1),1.[ holds
( sin * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * arctan) `| Z) . x = (cos . (arctan . x)) / (1 + (x ^2)) ) )

proof end;

theorem :: FDIFF_11:14

for Z being open Subset of REAL st Z c= dom (sin * arccot) & Z c= ].(- 1),1.[ holds
( sin * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * arccot) `| Z) . x = - ((cos . (arccot . x)) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:15

for Z being open Subset of REAL st Z c= dom (cos * arctan) & Z c= ].(- 1),1.[ holds
( cos * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * arctan) `| Z) . x = - ((sin . (arctan . x)) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:16

for Z being open Subset of REAL st Z c= dom (cos * arccot) & Z c= ].(- 1),1.[ holds
( cos * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * arccot) `| Z) . x = (sin . (arccot . x)) / (1 + (x ^2)) ) )

proof end;

theorem :: FDIFF_11:17

for Z being open Subset of REAL st Z c= dom (tan * arctan) & Z c= ].(- 1),1.[ holds
( tan * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * arctan) `| Z) . x = 1 / (((cos . (arctan . x)) ^2) * (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:18

for Z being open Subset of REAL st Z c= dom (tan * arccot) & Z c= ].(- 1),1.[ holds
( tan * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan * arccot) `| Z) . x = - (1 / (((cos . (arccot . x)) ^2) * (1 + (x ^2)))) ) )

proof end;

theorem :: FDIFF_11:19

for Z being open Subset of REAL st Z c= dom (cot * arctan) & Z c= ].(- 1),1.[ holds
( cot * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * arctan) `| Z) . x = - (1 / (((sin . (arctan . x)) ^2) * (1 + (x ^2)))) ) )

proof end;

theorem :: FDIFF_11:20

for Z being open Subset of REAL st Z c= dom (cot * arccot) & Z c= ].(- 1),1.[ holds
( cot * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((cot * arccot) `| Z) . x = 1 / (((sin . (arccot . x)) ^2) * (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:21

for Z being open Subset of REAL st Z c= dom (sec * arctan) & Z c= ].(- 1),1.[ holds
( sec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * arctan) `| Z) . x = (sin . (arctan . x)) / (((cos . (arctan . x)) ^2) * (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:22

for Z being open Subset of REAL st Z c= dom (sec * arccot) & Z c= ].(- 1),1.[ holds
( sec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((sec * arccot) `| Z) . x = - ((sin . (arccot . x)) / (((cos . (arccot . x)) ^2) * (1 + (x ^2)))) ) )

proof end;

theorem :: FDIFF_11:23

for Z being open Subset of REAL st Z c= dom (cosec * arctan) & Z c= ].(- 1),1.[ holds
( cosec * arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * arctan) `| Z) . x = - ((cos . (arctan . x)) / (((sin . (arctan . x)) ^2) * (1 + (x ^2)))) ) )

proof end;

theorem :: FDIFF_11:24

for Z being open Subset of REAL st Z c= dom (cosec * arccot) & Z c= ].(- 1),1.[ holds
( cosec * arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((cosec * arccot) `| Z) . x = (cos . (arccot . x)) / (((sin . (arccot . x)) ^2) * (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:25

for Z being open Subset of REAL st Z c= dom (sin (#) arctan) & Z c= ].(- 1),1.[ holds
( sin (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) arctan) `| Z) . x = ((cos . x) * (arctan . x)) + ((sin . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:26

for Z being open Subset of REAL st Z c= dom (sin (#) arccot) & Z c= ].(- 1),1.[ holds
( sin (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) arccot) `| Z) . x = ((cos . x) * (arccot . x)) - ((sin . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:27

for Z being open Subset of REAL st Z c= dom (cos (#) arctan) & Z c= ].(- 1),1.[ holds
( cos (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) arctan) `| Z) . x = (- ((sin . x) * (arctan . x))) + ((cos . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:28

for Z being open Subset of REAL st Z c= dom (cos (#) arccot) & Z c= ].(- 1),1.[ holds
( cos (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) arccot) `| Z) . x = (- ((sin . x) * (arccot . x))) - ((cos . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:29

for Z being open Subset of REAL st Z c= dom (tan (#) arctan) & Z c= ].(- 1),1.[ holds
( tan (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) arctan) `| Z) . x = ((arctan . x) / ((cos . x) ^2)) + ((tan . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:30

for Z being open Subset of REAL st Z c= dom (tan (#) arccot) & Z c= ].(- 1),1.[ holds
( tan (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) arccot) `| Z) . x = ((arccot . x) / ((cos . x) ^2)) - ((tan . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:31

for Z being open Subset of REAL st Z c= dom (cot (#) arctan) & Z c= ].(- 1),1.[ holds
( cot (#) arctan is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) arctan) `| Z) . x = (- ((arctan . x) / ((sin . x) ^2))) + ((cot . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:32

for Z being open Subset of REAL st Z c= dom (cot (#) arccot) & Z c= ].(- 1),1.[ holds
( cot (#) arccot is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) arccot) `| Z) . x = (- ((arccot . x) / ((sin . x) ^2))) - ((cot . x) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:33

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

proof end;

theorem :: FDIFF_11:34

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

proof end;

theorem :: FDIFF_11:35

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

proof end;

theorem :: FDIFF_11:36

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

proof end;

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
((arctan + arccot) `| Z) . x = 0 ) )

proof end;

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
((arctan - arccot) `| Z) . x = 2 / (1 + (x ^2)) ) )

proof end;

theorem :: FDIFF_11:39

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( sin (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (arctan + arccot)) `| Z) . x = (cos . x) * ((arctan . x) + (arccot . x)) ) )

proof end;

theorem :: FDIFF_11:40

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( sin (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) (arctan - arccot)) `| Z) . x = ((cos . x) * ((arctan . x) - (arccot . x))) + ((2 * (sin . x)) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:41

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( cos (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (arctan + arccot)) `| Z) . x = - ((sin . x) * ((arctan . x) + (arccot . x))) ) )

proof end;

theorem :: FDIFF_11:42

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( cos (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos (#) (arctan - arccot)) `| Z) . x = (- ((sin . x) * ((arctan . x) - (arccot . x)))) + ((2 * (cos . x)) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:43

for Z being open Subset of REAL st Z c= dom tan & Z c= ].(- 1),1.[ holds
( tan (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((tan (#) (arctan + arccot)) `| Z) . x = ((arctan . x) + (arccot . x)) / ((cos . x) ^2) ) )

proof end;

theorem :: FDIFF_11:44

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

proof end;

theorem :: FDIFF_11:45

for Z being open Subset of REAL st Z c= dom cot & Z c= ].(- 1),1.[ holds
( cot (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cot (#) (arctan + arccot)) `| Z) . x = - (((arctan . x) + (arccot . x)) / ((sin . x) ^2)) ) )

proof end;

theorem :: FDIFF_11:46

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

proof end;

theorem :: FDIFF_11:47

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

proof end;

theorem :: FDIFF_11:48

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

proof end;

theorem :: FDIFF_11:49

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

proof end;

theorem :: FDIFF_11:50

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

proof end;

theorem :: FDIFF_11:51

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (arctan + arccot)) `| Z) . x = (exp_R . x) * ((arctan . x) + (arccot . x)) ) )

proof end;

theorem :: FDIFF_11:52

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( exp_R (#) (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (arctan - arccot)) `| Z) . x = ((exp_R . x) * ((arctan . x) - (arccot . x))) + ((2 * (exp_R . x)) / (1 + (x ^2))) ) )

proof end;

theorem :: FDIFF_11:53

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( (arctan + arccot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((arctan + arccot) / exp_R) `| Z) . x = - (((arctan . x) + (arccot . x)) / (exp_R . x)) ) )

proof end;

theorem :: FDIFF_11:54

for Z being open Subset of REAL st Z c= ].(- 1),1.[ holds
( (arctan - arccot) / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(((arctan - arccot) / exp_R) `| Z) . x = (((2 / (1 + (x ^2))) - (arctan . x)) + (arccot . x)) / (exp_R . x) ) )

proof end;

theorem :: FDIFF_11:55

for Z being open Subset of REAL st Z c= dom (exp_R * (arctan + arccot)) & Z c= ].(- 1),1.[ holds
( exp_R * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (arctan + arccot)) `| Z) . x = 0 ) )

proof end;

theorem :: FDIFF_11:56

for Z being open Subset of REAL st Z c= dom (exp_R * (arctan - arccot)) & Z c= ].(- 1),1.[ holds
( exp_R * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (arctan - arccot)) `| Z) . x = (2 * (exp_R . ((arctan . x) - (arccot . x)))) / (1 + (x ^2)) ) )

proof end;

theorem :: FDIFF_11:57

for Z being open Subset of REAL st Z c= dom (sin * (arctan + arccot)) & Z c= ].(- 1),1.[ holds
( sin * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (arctan + arccot)) `| Z) . x = 0 ) )

proof end;

theorem :: FDIFF_11:58

for Z being open Subset of REAL st Z c= dom (sin * (arctan - arccot)) & Z c= ].(- 1),1.[ holds
( sin * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((sin * (arctan - arccot)) `| Z) . x = (2 * (cos . ((arctan . x) - (arccot . x)))) / (1 + (x ^2)) ) )

proof end;

theorem :: FDIFF_11:59

for Z being open Subset of REAL st Z c= dom (cos * (arctan + arccot)) & Z c= ].(- 1),1.[ holds
( cos * (arctan + arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (arctan + arccot)) `| Z) . x = 0 ) )

proof end;

theorem :: FDIFF_11:60

for Z being open Subset of REAL st Z c= dom (cos * (arctan - arccot)) & Z c= ].(- 1),1.[ holds
( cos * (arctan - arccot) is_differentiable_on Z & ( for x being Real st x in Z holds
((cos * (arctan - arccot)) `| Z) . x = - ((2 * (sin . ((arctan . x) - (arccot . x)))) / (1 + (x ^2))) ) )

proof end;

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
((arctan (#) arccot) `| Z) . x = ((arccot . x) - (arctan . x)) / (1 + (x ^2)) ) )

proof end;

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;

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;

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;

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;

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;

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
((arctan ^) `| Z) . x = - (1 / (((arctan . x) ^2) * (1 + (x ^2)))) ) )

proof end;

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
((arccot ^) `| Z) . x = 1 / (((arccot . x) ^2) * (1 + (x ^2))) ) )

proof end;

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) * (arctan ^))) & Z c= ].(- 1),1.[ & n > 0 & ( for x being Real st x in Z holds
arctan . x <> 0 ) holds
( (1 / n) (#) ((#Z n) * (arctan ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arctan ^))) `| Z) . x = - (1 / (((arctan . x) #Z (n + 1)) * (1 + (x ^2)))) ) )

proof end;

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) * (arccot ^))) & Z c= ].(- 1),1.[ & n > 0 holds
( (1 / n) (#) ((#Z n) * (arccot ^)) is_differentiable_on Z & ( for x being Real st x in Z holds
(((1 / n) (#) ((#Z n) * (arccot ^))) `| Z) . x = 1 / (((arccot . x) #Z (n + 1)) * (1 + (x ^2))) ) )

proof end;

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 = ((arctan . x) #R (- (1 / 2))) / (1 + (x ^2)) ) )

proof end;

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 = - (((arccot . x) #R (- (1 / 2))) / (1 + (x ^2))) ) )

proof end;

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 = ((arctan . x) #R (1 / 2)) / (1 + (x ^2)) ) )

proof end;

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 = - (((arccot . x) #R (1 / 2)) / (1 + (x ^2))) ) )

proof end;