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