:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Bo Li and Pan Wang
::
:: Copyright (c) 2007-2018 Association of Mizar Users

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

::f.x=tan.(tan.x)
theorem :: FDIFF_10:2
for Z being open Subset of REAL st Z c= dom () holds
( tan * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) ) )
proof end;

::f.x=cot.(cot.x)
theorem :: FDIFF_10:3
for Z being open Subset of REAL st Z c= dom () holds
( cot * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) ) )
proof end;

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

::f.x= tan.x - cot.x
theorem Th5: :: FDIFF_10:5
for Z being open Subset of REAL st Z c= dom () holds
( tan - cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) ) )
proof end;

::f.x= tan.x + cot.x
theorem Th6: :: FDIFF_10:6
for Z being open Subset of REAL st Z c= dom () holds
( tan + cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) ) )
proof end;

::f.x=sin.(sin.x)
theorem :: FDIFF_10:7
for Z being open Subset of REAL holds
( sin * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos . (sin . x)) * (cos . x) ) )
proof end;

::f.x=sin.(cos.x)
theorem :: FDIFF_10:8
for Z being open Subset of REAL holds
( sin * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((cos . (cos . x)) * (sin . x)) ) )
proof end;

::f.x=cos.(sin.x)
theorem :: FDIFF_10:9
for Z being open Subset of REAL holds
( cos * sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin . (sin . x)) * (cos . x)) ) )
proof end;

::f.x=cos.(cos.x)
theorem :: FDIFF_10:10
for Z being open Subset of REAL holds
( cos * cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin . (cos . x)) * (sin . x) ) )
proof end;

:: f.x=cos.x * cot.x
theorem :: FDIFF_10:11
for Z being open Subset of REAL st Z c= dom () holds
( cos (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (- (cos . x)) - ((cos . x) / ((sin . x) ^2)) ) )
proof end;

:: f.x=sin.x * tan.x
theorem :: FDIFF_10:12
for Z being open Subset of REAL st Z c= dom () holds
( sin (#) tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin . x) + ((sin . x) / ((cos . x) ^2)) ) )
proof end;

:: f.x=sin.x * cot.x
theorem :: FDIFF_10:13
for Z being open Subset of REAL st Z c= dom () holds
( sin (#) cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) * (cot . x)) - (1 / (sin . x)) ) )
proof end;

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

:: f.x=sin.x * cos.x
theorem :: FDIFF_10:15
for Z being open Subset of REAL st Z c= dom () holds
( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) ^2) - ((sin . x) ^2) ) )
proof end;

:: f.x=ln.x * sin.x
theorem :: FDIFF_10:16
for Z being open Subset of REAL st Z c= dom () holds
( ln (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((sin . x) / x) + ((ln . x) * (cos . x)) ) )
proof end;

:: f.x=ln.x * cos.x
theorem :: FDIFF_10:17
for Z being open Subset of REAL st Z c= dom () holds
( ln (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . x) / x) - ((ln . x) * (sin . x)) ) )
proof end;

:: f.x=ln.x * exp_R.x
theorem :: FDIFF_10:18
for Z being open Subset of REAL st Z c= dom () holds
( ln (#) exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (() / x) + ((ln . x) * ()) ) )
proof end;

::f.x=ln.(ln.x)
theorem :: FDIFF_10:19
for Z being open Subset of REAL st Z c= dom () & ( for x being Real st x in Z holds
x > 0 ) holds
( ln * ln is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = 1 / ((ln . x) * x) ) )
proof end;

::f.x=exp_R.(exp_R.x)
theorem :: FDIFF_10:20
for Z being open Subset of REAL st Z c= dom () holds
( exp_R * exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (exp_R . ()) * () ) )
proof end;

::f.x=sin.(tan.x)
theorem :: FDIFF_10:21
for Z being open Subset of REAL st Z c= dom () holds
( sin * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (cos (tan . x)) / ((cos . x) ^2) ) )
proof end;

::f.x=sin.(cot.x)
theorem :: FDIFF_10:22
for Z being open Subset of REAL st Z c= dom () holds
( sin * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((cos (cot . x)) / ((sin . x) ^2)) ) )
proof end;

::f.x=cos.(tan.x)
theorem :: FDIFF_10:23
for Z being open Subset of REAL st Z c= dom () holds
( cos * tan is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - ((sin (tan . x)) / ((cos . x) ^2)) ) )
proof end;

::f.x=cos.(cot.x)
theorem :: FDIFF_10:24
for Z being open Subset of REAL st Z c= dom () holds
( cos * cot is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = (sin (cot . x)) / ((sin . x) ^2) ) )
proof end;

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

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

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

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

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

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

::f.x=sin.x*(sin.x+cos.x)
theorem :: FDIFF_10:31
for Z being open Subset of REAL st Z c= dom (sin (#) ()) holds
( sin (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) ()) | Z) . x = (((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) ) )
proof end;

::f.x=sin.x*(sin.x-cos.x)
theorem :: FDIFF_10:32
for Z being open Subset of REAL st Z c= dom (sin (#) ()) holds
( sin (#) () is_differentiable_on Z & ( for x being Real st x in Z holds
((sin (#) ()) | Z) . x = (((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) ) )
proof end;

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

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

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

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

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

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

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

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

::f.x=(tan.x-cot.x)/exp_.x
theorem :: FDIFF_10:41
for Z being open Subset of REAL st Z c= dom (() / exp_R) holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) | Z) . x = ((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / () ) )
proof end;

::f.x=(tan.x+cot.x)/exp_.x
theorem :: FDIFF_10:42
for Z being open Subset of REAL st Z c= dom (() / exp_R) holds
( () / exp_R is_differentiable_on Z & ( for x being Real st x in Z holds
((() / exp_R) | Z) . x = ((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / () ) )
proof end;

:: f.x = sin.(sec.x)
theorem :: FDIFF_10:43
for Z being open Subset of REAL st Z c= dom () holds
( sin * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) ) )
proof end;

:: f.x = cos.(sec.x)
theorem :: FDIFF_10:44
for Z being open Subset of REAL st Z c= dom () holds
( cos * sec is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) ) )
proof end;

:: f.x = sin.(cosec.x)
theorem :: FDIFF_10:45
for Z being open Subset of REAL st Z c= dom () holds
( sin * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = - (((cos . ()) * (cos . x)) / ((sin . x) ^2)) ) )
proof end;

:: f.x = cos.(cose.x)
theorem :: FDIFF_10:46
for Z being open Subset of REAL st Z c= dom () holds
( cos * cosec is_differentiable_on Z & ( for x being Real st x in Z holds
(() | Z) . x = ((sin . ()) * (cos . x)) / ((sin . x) ^2) ) )
proof end;