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

begin

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 ))) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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) ) )

proof end;

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)) ) )

proof end;

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)) ) )

proof end;

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) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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)) ) )

proof end;

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)) ) )

proof end;

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 ) ) )

proof end;

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)) ) )

proof end;

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)) ) )

proof end;

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)) ) )

proof end;

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) ) )

proof end;

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) ) )

proof end;

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 ) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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 ) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 ) ) )

proof end;

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 ) ) )

proof end;

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 ) ) )

proof end;

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 ) ) )

proof end;

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 ))) ) )

proof end;

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 ))) ) )

proof end;

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 )))) ) )

proof end;

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 )))) ) )

proof end;

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 ))) ) )

proof end;

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 ))) ) )

proof end;

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) ) )

proof end;

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) ) )

proof end;

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 ) ) )

proof end;

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 )) ) )

proof end;

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 )) ) )

proof end;

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 ) ) )

proof end;