:: Several Differentiation Formulas of Special Functions -- Part {V}
::  by Peng Wang and Bo Li
::
:: Received July 9, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SIN_COS4, PARTFUN1, SIN_COS, ORDINAL4, REAL_1, RCOMP_1,
      SUBSET_1, FUNCT_1, CARD_1, FDIFF_1, ARYTM_3, SQUARE_1, ARYTM_1, PREPOWER,
      NEWTON, TARSKI, RELAT_1, VALUED_1, XBOOLE_0, LIMFUNC1, TAYLOR_1,
      XXREAL_0, NAT_1;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1,
      PARTFUN2, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS,
      XCMPLX_0, XREAL_0, REAL_1, NAT_1, NEWTON, VALUED_1, FDIFF_1, PREPOWER,
      LIMFUNC1;
 constructors REAL_1, PARTFUN1, PARTFUN2, NAT_1, LIMFUNC1, RCOMP_1, TAYLOR_1,
      SIN_COS, FDIFF_1, RFUNCT_1, SQUARE_1, PREPOWER, VALUED_1, RELSET_1,
      NEWTON;
 registrations RELSET_1, XREAL_0, MEMBERED, RCOMP_1, INT_1, XXREAL_0, NUMBERS,
      ORDINAL1, VALUED_0, SQUARE_1, PREPOWER, NEWTON;
 requirements SUBSET, REAL, NUMERALS, ARITHM;


begin

definition
  func sec -> PartFunc of REAL,REAL equals
:: FDIFF_9:def 1
  cos^;
  func cosec -> PartFunc of REAL,REAL equals
:: FDIFF_9:def 2
  sin^;
end;

reserve x,a,b,c for Real,
  n for Nat,
  Z for open Subset of REAL,
  f, f1,f2 for PartFunc of REAL,REAL;

theorem :: FDIFF_9:1
  cos.x<>0 implies sec is_differentiable_in x & diff(sec, x) = sin. x/(cos.x)^2
;

theorem :: FDIFF_9:2
  sin.x<>0 implies cosec is_differentiable_in x & diff(cosec, x) =
  -cos.x/(sin.x)^2;

theorem :: FDIFF_9:3
  (1/x) #Z n = 1/(x #Z n);

:: f.x=sec.x

theorem :: FDIFF_9:4
  Z c= dom sec implies sec is_differentiable_on Z & for x st x in Z
  holds ( (sec)`|Z).x = sin.x/(cos.x)^2;

:: f.x=cosec.x

theorem :: FDIFF_9:5
  Z c= dom cosec implies cosec is_differentiable_on Z & for x st x in Z
  holds ( (cosec)`|Z).x = -cos.x/(sin.x)^2;

:: f.x=sec.(a*x+b)

theorem :: FDIFF_9:6
  Z c= dom (sec*f) & (for x st x in Z holds f.x = a*x+b) implies
sec*f is_differentiable_on Z & for x st x in Z holds ((sec*f)`|Z).x = a*sin.(a*
  x+b)/(cos.(a*x+b))^2;

:: f.x=cosec.(a*x+b)

theorem :: FDIFF_9:7
  Z c= dom (cosec*f) & (for x st x in Z holds f.x = a*x+b) implies
  cosec*f is_differentiable_on Z & for x st x in Z holds ((cosec*f)`|Z).x = -a*
  cos.(a*x+b)/(sin.(a*x+b))^2;

:: f.x = sec.(1/x)

theorem :: FDIFF_9:8
  not 0 in Z & Z c= dom (sec*((id Z)^)) implies (sec*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((sec*((id Z)^))`|Z).x = -sin.(1
  /x)/(x^2*(cos.(1/x))^2);

:: f.x = cosec.(1/x)

theorem :: FDIFF_9:9
  not 0 in Z & Z c= dom (cosec*((id Z)^)) implies (cosec*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((cosec*((id Z)^))`|Z).x = cos.(
  1/x)/(x^2*(sin.(1/x))^2);

:: f.x = sec.(a+b*x+c*x^2)

theorem :: FDIFF_9:10
  Z c= dom (sec*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x = a
+b*x) implies sec*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds ((
  sec*(f1+c(#)f2))`|Z).x = (b+2*c*x)*sin.(a+b*x+c*x^2)/(cos.(a+b*x+c*x^2))^2;

:: f.x = cosec.(a+b*x+c*x^2)

theorem :: FDIFF_9:11
  Z c= dom (cosec*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x =
a+b*x) implies cosec*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds
((cosec*(f1+c(#)f2))`|Z).x = -(b+2*c*x)*cos.(a+b*x+c*x^2)/(sin.(a+b*x+c*x^2))^2
;

:: f.x = sec.(exp_R.x)

theorem :: FDIFF_9:12
  Z c= dom (sec*exp_R) implies sec*exp_R is_differentiable_on Z & for x
  st x in Z holds ((sec*exp_R)`|Z).x = exp_R.x*sin.(exp_R.x)/(cos.(exp_R.x))^2;

:: f.x = cosec.(exp_R.x)

theorem :: FDIFF_9:13
  Z c= dom (cosec*exp_R) implies cosec*exp_R is_differentiable_on Z &
for x st x in Z holds ((cosec*exp_R)`|Z).x = -exp_R.x*cos.(exp_R.x)/(sin.(exp_R
  .x))^2;

:: f.x = sec.(ln.x)

theorem :: FDIFF_9:14
  Z c= dom (sec*ln) implies sec*ln is_differentiable_on Z & for x st x
  in Z holds ((sec*ln)`|Z).x = sin.(ln.x)/(x*(cos.(ln.x))^2);

:: f.x = cosec.(ln.x)

theorem :: FDIFF_9:15
  Z c= dom (cosec*ln) implies cosec*ln is_differentiable_on Z & for x st
  x in Z holds ((cosec*ln)`|Z).x = -cos.(ln.x)/(x*(sin.(ln.x))^2);

:: f.x = exp_R.(sec.x)

theorem :: FDIFF_9:16
  Z c= dom (exp_R*sec) implies exp_R*sec is_differentiable_on Z & for x
  st x in Z holds ((exp_R*sec)`|Z).x = exp_R.(sec.x)*sin.x/(cos.x)^2;

:: f.x = exp_R.(cosec.x)

theorem :: FDIFF_9:17
  Z c= dom (exp_R*cosec) implies exp_R*cosec is_differentiable_on Z &
  for x st x in Z holds ((exp_R*cosec)`|Z).x = -exp_R.(cosec.x)*cos.x/(sin.x)^2
;

:: f.x = ln.(sec.x)

theorem :: FDIFF_9:18
  Z c= dom (ln*sec) implies ln*sec is_differentiable_on Z & for x st x
  in Z holds ((ln*sec)`|Z).x = sin.x/cos.x;

:: f.x = ln.(cosec.x)

theorem :: FDIFF_9:19
  Z c= dom (ln*cosec) implies ln*cosec is_differentiable_on Z & for x st
  x in Z holds ((ln*cosec)`|Z).x = -cos.x/sin.x;

:: f.x=(sec.x) #Z n

theorem :: FDIFF_9:20
  Z c= dom (( #Z n)*sec) & 1<=n implies ( #Z n)*sec is_differentiable_on
  Z & for x st x in Z holds ((( #Z n)*sec)`|Z).x = n*sin.x/(cos.x) #Z (n+1);

:: f.x=(cosec.x) #Z n

theorem :: FDIFF_9:21
  Z c= dom (( #Z n)*cosec) & 1<=n implies ( #Z n)*cosec
is_differentiable_on Z & for x st x in Z holds ((( #Z n)*cosec)`|Z).x = -n*cos.
  x/(sin.x) #Z (n+1);

:: f.x = sec.x-x

theorem :: FDIFF_9:22
  Z c= dom (sec-id Z) implies sec-id Z is_differentiable_on Z & for x st
  x in Z holds ((sec-id Z)`|Z).x=(sin.x-(cos.x)^2)/(cos.x)^2;

:: f.x = -cosec.x-x

theorem :: FDIFF_9:23
  Z c= dom (-cosec-id Z) implies -cosec-id Z is_differentiable_on Z &
  for x st x in Z holds ((-cosec-id Z)`|Z).x = (cos.x-(sin.x)^2)/(sin.x)^2;

:: f.x = exp_R.x*sec.x

theorem :: FDIFF_9:24
  Z c= dom (exp_R(#)sec) implies (exp_R(#)sec) is_differentiable_on Z &
for x st x in Z holds ((exp_R(#)sec)`|Z).x = exp_R.x/cos.x+exp_R.x*sin.x/(cos.x
  )^2;

:: f.x = exp_R.x*cosec.x

theorem :: FDIFF_9:25
  Z c= dom (exp_R(#)cosec) implies (exp_R(#)cosec) is_differentiable_on
Z & for x st x in Z holds ((exp_R(#)cosec)`|Z).x = exp_R.x/sin.x-exp_R.x*cos.x/
  (sin.x)^2;

:: f.x = (1/a)*sec.(a*x)-x

theorem :: FDIFF_9:26
  (Z c= dom ((1/a)(#)(sec*f)-id Z) & for x st x in Z holds f.x=a*x & a<>
0) implies (1/a)(#)(sec*f)-id Z is_differentiable_on Z & for x st x in Z holds
  (((1/a)(#)(sec*f)-id Z)`|Z).x= (sin.(a*x)-(cos.(a*x))^2)/(cos.(a*x))^2;

:: f.x = (-1/a)*cosec.(a*x)-x

theorem :: FDIFF_9:27
  (Z c= dom ((-1/a)(#)(cosec*f)-id Z) & for x st x in Z holds f.x=a*x &
a<>0) implies (-1/a)(#)(cosec*f)-id Z is_differentiable_on Z & for x st x in Z
holds (((-1/a)(#)(cosec*f)-id Z)`|Z).x= (cos.(a*x)-(sin.(a*x))^2)/(sin.(a*x))^2
;

:: f.x = (a*x+b)*sec.x

theorem :: FDIFF_9:28
  (Z c= dom (f(#)sec) & for x st x in Z holds f.x=a*x+b) implies (f(#)
sec) is_differentiable_on Z & for x st x in Z holds ((f(#)sec)`|Z).x = a/cos.x+
  (a*x+b)*sin.x/(cos.x)^2;

:: f.x = (a*x+b)*cosec.x

theorem :: FDIFF_9:29
  (Z c= dom (f(#)cosec) & for x st x in Z holds f.x=a*x+b) implies (f(#)
  cosec) is_differentiable_on Z & for x st x in Z holds ((f(#)cosec)`|Z).x = a/
  sin.x-(a*x+b)*cos.x/(sin.x)^2;

:: f.x = ln.x*sec.x

theorem :: FDIFF_9:30
  Z c= dom (ln(#)sec) implies (ln(#)sec) is_differentiable_on Z & for x
  st x in Z holds ((ln(#)sec)`|Z).x = 1/cos.x/x+ln.x*sin.x/(cos.x)^2;

:: f.x = ln.x*cosec.x

theorem :: FDIFF_9:31
  Z c= dom (ln(#)cosec) implies (ln(#)cosec) is_differentiable_on Z &
  for x st x in Z holds ((ln(#)cosec)`|Z).x = 1/sin.x/x-ln.x*cos.x/(sin.x)^2;

:: f.x = 1/x*sec.x

theorem :: FDIFF_9:32
  not 0 in Z & Z c= dom ((id Z)^(#)sec) implies ((id Z)^(#)sec)
is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)sec)`|Z).x = -1/cos.
  x/x^2+sin.x/x/(cos.x)^2;

:: f.x = 1/x*cosec.x

theorem :: FDIFF_9:33
  not 0 in Z & Z c= dom ((id Z)^(#)cosec) implies ((id Z)^(#)cosec)
  is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)cosec)`|Z).x = -1/
  sin.x/x^2-cos.x/x/(sin.x)^2;

:: f.x = sec.(sin.x)

theorem :: FDIFF_9:34
  Z c= dom (sec*sin) implies sec*sin is_differentiable_on Z & for x st x
  in Z holds ((sec*sin)`|Z).x = cos.x*sin.(sin.x)/(cos.(sin.x))^2;

:: f.x = sec.(cos.x)

theorem :: FDIFF_9:35
  Z c= dom (sec*cos) implies sec*cos is_differentiable_on Z & for x st x
  in Z holds ((sec*cos)`|Z).x = -sin.x*sin.(cos.x)/(cos.(cos.x))^2;

:: f.x = cosec.(sin.x)

theorem :: FDIFF_9:36
  Z c= dom (cosec*sin) implies cosec*sin is_differentiable_on Z & for x
  st x in Z holds ((cosec*sin)`|Z).x = -cos.x*cos.(sin.x)/(sin.(sin.x))^2;

:: f.x = cosec.(cos.x)

theorem :: FDIFF_9:37
  Z c= dom (cosec*cos) implies cosec*cos is_differentiable_on Z & for x
  st x in Z holds ((cosec*cos)`|Z).x = sin.x*cos.(cos.x)/(sin.(cos.x))^2;

:: f.x = sec.(tan.x)

theorem :: FDIFF_9:38
  Z c= dom (sec*tan) implies sec*tan is_differentiable_on Z & for x st x
  in Z holds ((sec*tan)`|Z).x = sin.(tan.x)/(cos.x)^2/(cos.(tan.x))^2;

:: f.x = sec.(cot.x)

theorem :: FDIFF_9:39
  Z c= dom (sec*cot) implies sec*cot is_differentiable_on Z & for x st x
  in Z holds ((sec*cot)`|Z).x = -sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2;

:: f.x = cosec.(tan.x)

theorem :: FDIFF_9:40
  Z c= dom (cosec*tan) implies cosec*tan is_differentiable_on Z & for x
  st x in Z holds ((cosec*tan)`|Z).x = -cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2;

:: f.x = cosec.(cot.x)

theorem :: FDIFF_9:41
  Z c= dom (cosec*cot) implies cosec*cot is_differentiable_on Z & for x
  st x in Z holds ((cosec*cot)`|Z).x = cos.(cot.x)/(sin.x)^2/(sin.(cot.x))^2;

:: f.x = tan.x*sec.x

theorem :: FDIFF_9:42
  Z c= dom (tan(#)sec) implies (tan(#)sec) is_differentiable_on Z & for
x st x in Z holds ((tan(#)sec)`|Z).x = 1/(cos.x)^2/cos.x+tan.x*sin.x/(cos.x)^2;

:: f.x = cot.x*sec.x

theorem :: FDIFF_9:43
  Z c= dom (cot(#)sec) implies (cot(#)sec) is_differentiable_on Z & for
x st x in Z holds ((cot(#)sec)`|Z).x = -1/(sin.x)^2/cos.x+cot.x*sin.x/(cos.x)^2
;

:: f.x = tan.x*cosec.x

theorem :: FDIFF_9:44
  Z c= dom (tan(#)cosec) implies (tan(#)cosec) is_differentiable_on Z &
for x st x in Z holds ((tan(#)cosec)`|Z).x = 1/(cos.x)^2/sin.x-tan.x*cos.x/(sin
  .x)^2;

:: f.x = cot.x*cosec.x

theorem :: FDIFF_9:45
  Z c= dom (cot(#)cosec) implies (cot(#)cosec) is_differentiable_on Z &
  for x st x in Z holds ((cot(#)cosec)`|Z).x = -1/(sin.x)^2/sin.x-cot.x*cos.x/(
  sin.x)^2;