:: Several Differentiation Formulas of Special Functions -- Part {III}
::  by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006-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 REAL_1, SUBSET_1, NUMBERS, RCOMP_1, PARTFUN1, PREPOWER, SQUARE_1,
      NEWTON, XXREAL_0, CARD_1, ARYTM_3, RELAT_1, POWER, ARYTM_1, SIN_COS,
      FUNCT_1, TARSKI, XXREAL_1, VALUED_1, SIN_COS6, FDIFF_1, TAYLOR_1,
      XBOOLE_0, ORDINAL4, LIMFUNC1;
 notations TARSKI, SUBSET_1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2,
      RCOMP_1, ORDINAL1, XCMPLX_0, XREAL_0, NEWTON, TAYLOR_1, SIN_COS,
      RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, VALUED_1, FDIFF_1, PREPOWER, POWER,
      SIN_COS6, LIMFUNC1;
 constructors PARTFUN1, REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, RFUNCT_1,
      LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, SIN_COS6, TAYLOR_1,
      VALUED_1, RELSET_1, NEWTON;
 registrations RELSET_1, NUMBERS, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0,
      SIN_COS, SQUARE_1, PREPOWER;
 requirements SUBSET, NUMERALS, ARITHM;


begin

reserve y for set,
  x,r,a,b for Real,
  n for Element of NAT,
  Z for open Subset of REAL,
  f,f1,f2,f3 for PartFunc of REAL,REAL;

theorem :: FDIFF_7:1
  x #Z 2=x^2;

theorem :: FDIFF_7:2
  x>0 implies x #R (1/2)=sqrt x;

theorem :: FDIFF_7:3
  x>0 implies x #R (-1/2)=1/sqrt x;

::f.x=r*arcsinx

theorem :: FDIFF_7:4
  Z c=]. -1,1 .[ & Z c= dom (r(#)arcsin) implies r(#)arcsin
is_differentiable_on Z & for x st x in Z holds ((r(#)arcsin)`|Z).x = r / sqrt(1
  -x^2);

::f.x=r*arccosx

theorem :: FDIFF_7:5
  Z c=]. -1,1 .[ & Z c= dom (r(#)arccos) implies r(#)arccos
is_differentiable_on Z & for x st x in Z holds ((r(#)arccos)`|Z).x =- r / sqrt(
  1-x^2);

theorem :: FDIFF_7:6
  f is_differentiable_in x & f.x > -1 & f.x < 1 implies (arcsin)*f
  is_differentiable_in x & diff((arcsin)*f,x) = diff(f,x)/sqrt(1-(f.x)^2);

theorem :: FDIFF_7:7
  f is_differentiable_in x & f.x > -1 & f.x < 1 implies (arccos)*f
  is_differentiable_in x & diff((arccos)*f,x) = -diff(f,x)/sqrt(1-(f.x)^2);

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

theorem :: FDIFF_7:8
  Z c= dom (ln*(arcsin)) & Z c= ]. -1,1 .[ & (for x st x in Z holds
arcsin.x>0) implies ln*(arcsin) is_differentiable_on Z & for x st x in Z holds
  ((ln*(arcsin))`|Z).x=1 / (sqrt(1-x^2)*arcsin.x);

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

theorem :: FDIFF_7:9
  Z c= dom (ln*arccos) & Z c= ]. -1,1 .[ & (for x st x in Z holds arccos
.x>0) implies ln*(arccos) is_differentiable_on Z & for x st x in Z holds ((ln*(
  arccos))`|Z).x=-1 / (sqrt(1-x^2)*arccos.x);

::f.x=(arcsin)^n

theorem :: FDIFF_7:10
  Z c= dom (( #Z n)*(arcsin)) & Z c=]. -1,1 .[ implies ( #Z n)*(
arcsin) is_differentiable_on Z & for x st x in Z holds ((( #Z n)*arcsin)`|Z).x
  =n*(arcsin.x) #Z (n-1) / sqrt(1-x^2);

::f.x=(arccos)^n

theorem :: FDIFF_7:11
  Z c= dom (( #Z n)*(arccos)) & Z c=]. -1,1 .[ implies ( #Z n)*(
arccos) is_differentiable_on Z & for x st x in Z holds ((( #Z n)*(arccos))`|Z).
  x =-n*(arccos.x) #Z (n-1) / sqrt(1-x^2);

::f.x=(1/2)*(arcsin)^2

theorem :: FDIFF_7:12
  Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) & Z c=]. -1,1 .[ implies (1/2)
(#)(( #Z 2)*(arcsin)) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)
  (( #Z 2)*(arcsin)))`|Z).x =arcsin.x / sqrt(1-x^2);

::f.x=(1/2)*(arccos)^2

theorem :: FDIFF_7:13
  Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) & Z c=]. -1,1 .[ implies (1/2)
(#)(( #Z 2)*(arccos)) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)
  (( #Z 2)*(arccos)))`|Z).x =-arccos.x / sqrt(1-x^2);

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

theorem :: FDIFF_7:14
  Z c= dom ((arcsin)*f) & (for x st x in Z holds f.x=a*x+b & f.x >
-1 & f.x < 1) implies (arcsin)*f is_differentiable_on Z & for x st x in Z holds
  (((arcsin)*f)`|Z).x=a / sqrt(1-(a*x+b)^2);

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

theorem :: FDIFF_7:15
  Z c= dom ((arccos)*f) & (for x st x in Z holds f.x=a*x+b & f.x >
-1 & f.x < 1) implies (arccos)*f is_differentiable_on Z & for x st x in Z holds
  (((arccos)*f)`|Z).x=-a / sqrt(1-(a*x+b)^2);

::f.x=x*arcsin.x

theorem :: FDIFF_7:16
  Z c= dom ((id Z)(#)(arcsin)) & Z c= ]. -1,1 .[ implies (id Z)(#)
(arcsin) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arcsin))`|Z
  ).x =arcsin.x+x/sqrt(1-x^2);

::f.x=x*arccos.x

theorem :: FDIFF_7:17
  Z c= dom ((id Z)(#)(arccos)) & Z c= ]. -1,1 .[ implies (id Z)(#)
(arccos) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccos))`|Z
  ).x =arccos.x-x/sqrt(1-x^2);

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

theorem :: FDIFF_7:18
  Z c= dom (f(#)(arcsin)) & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x
=a*x+b) implies f(#)(arcsin) is_differentiable_on Z & for x st x in Z holds ((f
  (#)(arcsin))`|Z).x =a*arcsin.x+(a*x+b)/sqrt(1-x^2);

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

theorem :: FDIFF_7:19
  Z c= dom (f(#)(arccos)) & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x
=a*x+b) implies f(#)(arccos) is_differentiable_on Z & for x st x in Z holds ((f
  (#)(arccos))`|Z).x =a*arccos.x-(a*x+b)/sqrt(1-x^2);

::f.x=(1/2)*arcsin(2*x)

theorem :: FDIFF_7:20
  Z c= dom ((1/2)(#)((arcsin)*f)) & (for x st x in Z holds f.x=2*x & f.x
> -1 & f.x < 1) implies (1/2)(#)((arcsin)*f) is_differentiable_on Z & for x st
  x in Z holds (((1/2)(#)((arcsin)*f))`|Z).x=1/sqrt(1-(2*x)^2);

::f.x=(1/2)*arccos(2*x)

theorem :: FDIFF_7:21
  Z c= dom ((1/2)(#)((arccos)*f)) & (for x st x in Z holds f.x=2*x & f.x
> -1 & f.x < 1) implies (1/2)(#)((arccos)*f) is_differentiable_on Z & for x st
  x in Z holds (((1/2)(#)((arccos)*f))`|Z).x=-1/sqrt(1-(2*x)^2);

::f.x=(1-x|^2) ^ (1/2)

theorem :: FDIFF_7:22
  Z c= dom (( #R (1/2))*f) & f=f1-f2 & f2=#Z 2 & (for x st x in Z
  holds f1.x=1 & f.x >0) implies (( #R (1/2))*f) is_differentiable_on Z & for x
  st x in Z holds ((( #R (1/2))*f)`|Z).x =-x*(1-x #Z 2) #R (-1/2);

::f.x=x*arcsin.x+(1-x^2) ^ (1/2)

theorem :: FDIFF_7:23
  Z c= dom ((id Z)(#)(arcsin)+( #R (1/2))*f) & Z c= ]. -1,1 .[ & f=f1-f2
  & f2=#Z 2 & (for x st x in Z holds f1.x=1 & f.x >0 & x<>0) implies (id Z)(#)(
  arcsin)+( #R (1/2))*f is_differentiable_on Z & for x st x in Z holds (((id Z)
  (#)(arcsin)+( #R (1/2))*f)`|Z).x =arcsin.x;

::f.x=x*arccos.x-(1-x^2) ^ (1/2)

theorem :: FDIFF_7:24
  Z c= dom ((id Z)(#)(arccos)-( #R (1/2))*f) & Z c= ]. -1,1 .[ & f=f1-f2
  & f2=#Z 2 & (for x st x in Z holds f1.x=1 & f.x >0 & x<>0) implies (id Z)(#)(
  arccos)-( #R (1/2))*f is_differentiable_on Z & for x st x in Z holds (((id Z)
  (#)(arccos)-( #R (1/2))*f)`|Z).x =arccos.x;

::f.x=x*arcsin(x/a)

theorem :: FDIFF_7:25
  Z c= dom ((id Z)(#)((arcsin)*f)) & (for x st x in Z holds f.x=x/
a & f.x > -1 & f.x < 1) implies (id Z)(#)((arcsin)*f) is_differentiable_on Z &
for x st x in Z holds (((id Z)(#)((arcsin)*f))`|Z).x =arcsin.(x/a)+x/(a*sqrt(1-
  (x/a)^2));

::f.x=x*arccos(x/a)

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

::f.x=(a^2-x^2) ^ (1/2)

theorem :: FDIFF_7:27
  Z c= dom (( #R (1/2))*f) & f=f1-f2 & f2=#Z 2 & (for x st x in Z
  holds f1.x=a^2 & f.x >0) implies ( #R (1/2))*f is_differentiable_on Z & for x
  st x in Z holds ((( #R (1/2))*f)`|Z).x = -x*(a^2-x #Z 2) #R (-1/2);

::f.x=x*arcsin(x/a)+(a^2-x^2) ^ (1/2)

theorem :: FDIFF_7:28
  Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) & f=f1-f2 & f2=#Z 2 &
(for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3.x < 1 & x
<>0 & a>0) implies (id Z)(#)((arcsin)*f3)+( #R (1/2))*f is_differentiable_on Z
& for x st x in Z holds (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = arcsin.
  (x/a);

::f.x=x*arccos(x/a)-(a^2-x^2) ^ (1/2)

theorem :: FDIFF_7:29
  Z c= dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) & f=f1-f2 & f2=#Z 2 &
(for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3.x < 1 & x
<>0 & a>0) implies (id Z)(#)((arccos)*f3)-( #R (1/2))*f is_differentiable_on Z
& for x st x in Z holds (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = arccos.
  (x/a);

::f.x=-1/(n*(sin.x)^n)

theorem :: FDIFF_7:30
  Z c= dom ((-1/n)(#)(( #Z n)*(sin^))) & n>0 & (for x st x in Z holds
sin.x<>0) implies (-1/n)(#)(( #Z n)*(sin^)) is_differentiable_on Z & for x st x
  in Z holds (((-1/n)(#)(( #Z n)*(sin^)))`|Z).x=cos.x/((sin.x) #Z (n+1));

::f.x=1/(n*(cos.x)^n)

theorem :: FDIFF_7:31
  Z c= dom ((1/n)(#)(( #Z n)*(cos^))) & n>0 & (for x st x in Z holds cos
.x<>0) implies (1/n)(#)(( #Z n)*(cos^)) is_differentiable_on Z & for x st x in
  Z holds (((1/n)(#)(( #Z n)*(cos^)))`|Z).x=sin.x/((cos.x) #Z (n+1));

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

theorem :: FDIFF_7:32
  Z c= dom (sin*ln) & (for x st x in Z holds x>0) implies sin*ln
  is_differentiable_on Z & for x st x in Z holds ((sin*ln)`|Z).x =cos.(ln.x)/x;

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

theorem :: FDIFF_7:33
  Z c= dom (cos*ln) & (for x st x in Z holds x>0) implies cos*ln
  is_differentiable_on Z & for x st x in Z holds ((cos*ln)`|Z).x =-sin.(ln.x)/x
;

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

theorem :: FDIFF_7:34
  Z c= dom (sin*exp_R) implies sin*exp_R is_differentiable_on Z & for x
  st x in Z holds ((sin*exp_R)`|Z).x = exp_R.x * cos.(exp_R.x);

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

theorem :: FDIFF_7:35
  Z c= dom (cos*exp_R) implies cos*exp_R is_differentiable_on Z & for x
  st x in Z holds ((cos*exp_R)`|Z).x = -exp_R.x * sin.(exp_R.x);

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

theorem :: FDIFF_7:36
  Z c= dom (exp_R*cos) implies exp_R*cos is_differentiable_on Z & for x
  st x in Z holds ((exp_R*cos)`|Z).x = -exp_R.(cos.x) * sin.x;

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

theorem :: FDIFF_7:37
  Z c= dom (exp_R*sin) implies exp_R*sin is_differentiable_on Z & for x
  st x in Z holds ((exp_R*sin)`|Z).x = exp_R.(sin.x) * cos.x;

::f.x=sin.x+cos.x

theorem :: FDIFF_7:38
  Z c= dom (sin+cos) implies sin+cos is_differentiable_on Z & for
  x st x in Z holds ((sin+cos)`|Z).x =cos.x-sin.x;

::f.x=sin.x-cos.x

theorem :: FDIFF_7:39
  Z c= dom (sin-cos) implies sin-cos is_differentiable_on Z & for
  x st x in Z holds ((sin-cos)`|Z).x =cos.x+sin.x;

::f.x=exp_R.x*(sin.x-cos.x)

theorem :: FDIFF_7:40
  Z c= dom (exp_R(#)(sin-cos)) implies exp_R(#)(sin-cos)
is_differentiable_on Z & for x st x in Z holds ((exp_R(#)(sin-cos))`|Z).x =2 *
  exp_R.x * sin.x;

::f.x=exp_R.x*(sin.x+cos.x)

theorem :: FDIFF_7:41
  Z c= dom (exp_R(#)(sin+cos)) implies exp_R(#)(sin+cos)
is_differentiable_on Z & for x st x in Z holds ((exp_R(#)(sin+cos))`|Z).x =2 *
  exp_R.x * cos.x;

::f.x=(sin.x+cos.x)/exp_R.x

theorem :: FDIFF_7:42
  Z c= dom ((sin+cos)/exp_R) implies (sin+cos)/exp_R
is_differentiable_on Z & for x st x in Z holds (((sin+cos)/exp_R)`|Z).x =-2*sin
  .x/exp_R.x;

::f.x=(sin.x-cos.x)/exp_R.x

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

::f.x=exp_R.x*sin.x

theorem :: FDIFF_7:44
  Z c= dom (exp_R(#)sin) implies exp_R(#)sin is_differentiable_on Z &
  for x st x in Z holds ((exp_R(#)sin)`|Z).x = exp_R.x*(sin.x+cos.x);

::f.x=exp_R.x*cos.x

theorem :: FDIFF_7:45
  Z c= dom (exp_R(#)cos) implies exp_R(#)cos is_differentiable_on Z &
  for x st x in Z holds ((exp_R(#)cos)`|Z).x = exp_R.x*(cos.x-sin.x);

:: f.x=tan.x

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

::f.x=cot.x

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

::f.x=(tan.x) ^ 2

theorem :: FDIFF_7:48
  Z c= dom (( #Z 2)*(sin/cos)) & (for x st x in Z holds cos.x<>0)
implies ( #Z 2)*(sin/cos) is_differentiable_on Z & for x st x in Z holds ((( #Z
  2)*(sin/cos))`|Z).x =2*sin.x/((cos.x) #Z 3);

::f.x=(cot.x) ^ 2

theorem :: FDIFF_7:49
  Z c= dom (( #Z 2)*(cos/sin)) & (for x st x in Z holds sin.x<>0)
implies ( #Z 2)*(cos/sin) is_differentiable_on Z & for x st x in Z holds ((( #Z
  2)*(cos/sin))`|Z).x =-2*cos.x/((sin.x) #Z 3);

::f.x=tan.(x/2)

theorem :: FDIFF_7:50
  Z c= dom ((sin/cos)*f) & (for x st x in Z holds f.x=x/2 & cos.(f.x)<>0
) implies (sin/cos)*f is_differentiable_on Z & for x st x in Z holds (((sin/cos
  )*f)`|Z).x = 1/(1+cos.x);

::f.x=cot.(x/2)

theorem :: FDIFF_7:51
  Z c= dom ((cos/sin)*f) & (for x st x in Z holds f.x=x/2 & sin.(f.x)<>0
) implies (cos/sin)*f is_differentiable_on Z & for x st x in Z holds (((cos/sin
  )*f)`|Z).x = -1/(1-cos.x);