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


begin

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

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

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

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

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

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

::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
((sin * sin) `| Z) . x = (cos . (sin . x)) * (cos . x) ) )
proofend;

::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
((sin * cos) `| Z) . x = - ((cos . (cos . x)) * (sin . x)) ) )
proofend;

::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
((cos * sin) `| Z) . x = - ((sin . (sin . x)) * (cos . x)) ) )
proofend;

::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
((cos * cos) `| Z) . x = (sin . (cos . x)) * (sin . x) ) )
proofend;

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

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

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

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

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

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

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

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

::f.x=ln.(ln.x)
theorem :: FDIFF_10:19
for Z being open Subset of REAL st Z c= dom (ln * ln) & ( 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
((ln * ln) `| Z) . x = 1 / ((ln . x) * x) ) )
proofend;

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

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

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

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

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

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

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

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

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

::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 (#) (tan + cot)) holds
( exp_R (#) (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan + cot)) `| Z) . x = ((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) ) )
proofend;

::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 (#) (tan - cot)) holds
( exp_R (#) (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R (#) (tan - cot)) `| Z) . x = ((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) ) )
proofend;

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

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

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

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

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

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

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

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

::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 * (tan + cot)) holds
( exp_R * (tan + cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan + cot)) `| Z) . x = (exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) ) )
proofend;

::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 * (tan - cot)) holds
( exp_R * (tan - cot) is_differentiable_on Z & ( for x being Real st x in Z holds
((exp_R * (tan - cot)) `| Z) . x = (exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) ) )
proofend;

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

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

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

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

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

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