:: Several Differentiation Formulas of Special Functions -- Part {III}
:: by Bo Li , Yan Zhang and Xiquan Liang
::
:: Received March 22, 2006
:: Copyright (c) 2006-2026 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;
equalities SQUARE_1, RCOMP_1, LIMFUNC1, VALUED_1;
theorems FUNCT_1, SIN_COS6, FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_4,
POWER, SQUARE_1, FDIFF_1, TARSKI, PREPOWER, RFUNCT_1, XREAL_1, SIN_COS,
SIN_COS5, NEWTON, VALUED_1, XXREAL_1, XREAL_0;
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 Th1:
x #Z 2=x^2
proof
x #Z 2 = x |^ 2 by PREPOWER:36
.= x^2 by NEWTON:81;
hence thesis;
end;
theorem Th2:
x>0 implies x #R (1/2)=sqrt x
proof
assume
A1: x>0;
then
A2: x #R (1/2)>0 by PREPOWER:81;
x = x #R ((1/2)*2) by A1,PREPOWER:72
.=x #R (1/2) #R 2 by A1,PREPOWER:91
.=(x #R (1/2)) #Q 2 by A1,PREPOWER:74,81
.=(x #R (1/2)) to_power 2 by A1,POWER:44,PREPOWER:81
.=(x #R (1/2))^2 by POWER:46;
hence thesis by A1,A2,SQUARE_1:def 2;
end;
theorem Th3:
x>0 implies x #R (-1/2)=1/sqrt x
proof
assume
A1: x>0;
hence x #R (-1/2)=1 / x #R (1/2) by PREPOWER:76
.=1 / sqrt x by A1,Th2;
end;
Lm1: 2*(cos.(x/2))^2=1+cos.x
proof
(cos(x/2))^2=(1+cos(2*(x/2)))/2 by SIN_COS5:21
.=(1+cos(x))/2;
then 2*(cos.(x/2))^2 = 2*((1+cos(x))/2) by SIN_COS:def 19
.=1+cos.x by SIN_COS:def 19;
hence thesis;
end;
Lm2: 2*(sin.(x/2))^2=1-cos.x
proof
(sin(x/2))^2=(1-cos(2*(x/2)))/2 by SIN_COS5:20
.=(1-cos(x))/2;
then 2*(sin.(x/2))^2=2*((1-cos(x))/2) by SIN_COS:def 17
.=1-cos.x by SIN_COS:def 19;
hence thesis;
end;
::f.x=r*arcsinx
theorem
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)
proof
assume that
A1: Z c= ]. -1,1 .[ and
A2: Z c= dom (r(#)arcsin);
A3: arcsin is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:83;
for x st x in Z holds ((r(#)arcsin)`|Z).x = r / sqrt(1-x^2)
proof
let x;
assume
A4: x in Z;
then
A5: -1 < x & x < 1 by A1,XXREAL_1:4;
((r(#)arcsin)`|Z).x = r*diff(arcsin,x) by A2,A3,A4,FDIFF_1:20
.= r*(1 / sqrt(1-x^2)) by A5,SIN_COS6:83
.=r / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A2,A3,FDIFF_1:20;
end;
::f.x=r*arccosx
theorem
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)
proof
assume that
A1: Z c= ]. -1,1 .[ and
A2: Z c= dom (r(#)arccos);
A3: arccos is_differentiable_on Z by A1,FDIFF_1:26,SIN_COS6:106;
for x st x in Z holds ((r(#)arccos)`|Z).x = -r / sqrt(1-x^2)
proof
let x;
assume
A4: x in Z;
then
A5: -1 < x & x < 1 by A1,XXREAL_1:4;
((r(#)arccos)`|Z).x = r*diff(arccos,x) by A2,A3,A4,FDIFF_1:20
.= r*(-1 / sqrt(1-x^2)) by A5,SIN_COS6:106
.=-r*(1 / sqrt(1-x^2))
.=-r / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A2,A3,FDIFF_1:20;
end;
theorem Th6:
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)
proof
assume that
A1: f is_differentiable_in x and
A2: f.x > -1 & f.x < 1;
f.x in ]. -1,1 .[ by A2;
then
A3: arcsin is_differentiable_in f.x by FDIFF_1:9,SIN_COS6:83;
then diff((arcsin)*f,x) = diff((arcsin),f.x)*diff(f,x) by A1,FDIFF_2:13
.=diff(f,x)*(1 / sqrt(1-(f.x)^2)) by A2,SIN_COS6:83
.=diff(f,x)/sqrt(1-(f.x)^2) by XCMPLX_1:99;
hence thesis by A1,A3,FDIFF_2:13;
end;
theorem Th7:
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)
proof
assume that
A1: f is_differentiable_in x and
A2: f.x > -1 & f.x < 1;
f.x in ]. -1,1 .[ by A2;
then
A3: arccos is_differentiable_in f.x by FDIFF_1:9,SIN_COS6:106;
then diff(arccos*f,x) = diff(arccos,f.x)*diff(f,x) by A1,FDIFF_2:13
.=(-1 / sqrt(1-(f.x)^2))*diff(f,x) by A2,SIN_COS6:106
.=-diff(f,x)*(1 / sqrt(1-(f.x)^2))
.=-diff(f,x)/sqrt(1-(f.x)^2) by XCMPLX_1:99;
hence thesis by A1,A3,FDIFF_2:13;
end;
::f.x=ln(arcsin.x)
theorem
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)
proof
assume that
A1: Z c= dom (ln*arcsin) and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds arcsin.x > 0;
A4: for x st x in Z holds ln*arcsin is_differentiable_in x
proof
let x;
assume x in Z;
then arcsin is_differentiable_in x & arcsin.x >0 by A2,A3,FDIFF_1:9
,SIN_COS6:83;
hence thesis by TAYLOR_1:20;
end;
then
A5: ln*arcsin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(arcsin))`|Z).x = 1 / (sqrt(1-x^2)*arcsin.x)
proof
let x;
assume
A6: x in Z;
then
A7: -1 < x & x < 1 by A2,XXREAL_1:4;
arcsin is_differentiable_in x & arcsin.x >0 by A2,A3,A6,FDIFF_1:9
,SIN_COS6:83;
then diff(ln*arcsin,x) =diff(arcsin,x)/arcsin.x by TAYLOR_1:20
.=(1 / sqrt(1-x^2))/arcsin.x by A7,SIN_COS6:83
.=1 / (sqrt(1-x^2)*arcsin.x) by XCMPLX_1:78;
hence thesis by A5,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=ln(arccos.x)
theorem
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)
proof
assume that
A1: Z c= dom (ln*(arccos)) and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds arccos.x > 0;
A4: for x st x in Z holds ln*(arccos) is_differentiable_in x
proof
let x;
assume x in Z;
then arccos is_differentiable_in x & arccos.x >0 by A2,A3,FDIFF_1:9
,SIN_COS6:106;
hence thesis by TAYLOR_1:20;
end;
then
A5: ln*arccos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*arccos)`|Z).x = -1 / (sqrt(1-x^2)*arccos.x)
proof
let x;
assume
A6: x in Z;
then
A7: -1 < x & x < 1 by A2,XXREAL_1:4;
arccos is_differentiable_in x & arccos.x >0 by A2,A3,A6,FDIFF_1:9
,SIN_COS6:106;
then diff(ln*arccos,x) =diff(arccos,x)/arccos.x by TAYLOR_1:20
.=(-1 / sqrt(1-x^2))/arccos.x by A7,SIN_COS6:106
.=-(1 / sqrt(1-x^2))/arccos.x by XCMPLX_1:187
.=-1 / (sqrt(1-x^2)*arccos.x) by XCMPLX_1:78;
hence thesis by A5,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=(arcsin)^n
theorem Th10:
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)
proof
assume that
A1: Z c= dom (( #Z n)*arcsin) and
A2: Z c=]. -1,1 .[;
A3: for x st x in Z holds ( #Z n)*arcsin is_differentiable_in x
proof
let x;
assume x in Z;
then arcsin is_differentiable_in x by A2,FDIFF_1:9,SIN_COS6:83;
hence thesis by TAYLOR_1:3;
end;
then
A4: ( #Z n)*(arcsin) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*(arcsin))`|Z).x = n*(arcsin.x) #Z (n-1)
/ sqrt(1-x^2)
proof
let x;
assume
A5: x in Z;
then
A6: -1 < x & x < 1 by A2,XXREAL_1:4;
A7: arcsin is_differentiable_in x by A2,A5,FDIFF_1:9,SIN_COS6:83;
((( #Z n)*arcsin)`|Z).x = diff(( #Z n)*arcsin,x) by A4,A5,FDIFF_1:def 7
.=(n*((arcsin.x) #Z (n-1))) * diff(arcsin,x) by A7,TAYLOR_1:3
.=(n*((arcsin.x) #Z (n-1))) *(1 / sqrt(1-x^2)) by A6,SIN_COS6:83
.=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=(arccos)^n
theorem Th11:
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)
proof
assume that
A1: Z c= dom (( #Z n)*arccos) and
A2: Z c=]. -1,1 .[;
A3: for x st x in Z holds ( #Z n)*arccos is_differentiable_in x
proof
let x;
assume x in Z;
then arccos is_differentiable_in x by A2,FDIFF_1:9,SIN_COS6:106;
hence thesis by TAYLOR_1:3;
end;
then
A4: ( #Z n)*arccos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*arccos)`|Z).x =-n*(arccos.x) #Z (n-1) /
sqrt(1-x^2)
proof
let x;
assume
A5: x in Z;
then
A6: -1 < x & x < 1 by A2,XXREAL_1:4;
A7: arccos is_differentiable_in x by A2,A5,FDIFF_1:9,SIN_COS6:106;
((( #Z n)*(arccos))`|Z).x =diff(( #Z n)*(arccos),x) by A4,A5,FDIFF_1:def 7
.=(n*((arccos.x) #Z (n-1))) * diff(arccos,x) by A7,TAYLOR_1:3
.=(n*((arccos.x) #Z (n-1))) *(-(1 / sqrt(1-x^2))) by A6,SIN_COS6:106
.=-(n*(arccos.x) #Z (n-1)) *(1/ sqrt(1-x^2))
.=-n*(arccos.x) #Z (n-1) / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=(1/2)*(arcsin)^2
theorem
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)
proof
assume that
A1: Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) and
A2: Z c=]. -1,1 .[;
A3: Z c= dom (( #Z 2)*(arcsin)) by A1,VALUED_1:def 5;
then
A4: ( #Z 2)*(arcsin) is_differentiable_on Z by A2,Th10;
for x st x in Z holds (((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x =arcsin.x /
sqrt(1-x^2)
proof
let x;
assume
A5: x in Z;
then
(((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x =(1/2)*diff((( #Z 2)*arcsin),x) by A1
,A4,FDIFF_1:20
.=(1/2)*((( #Z 2)*(arcsin))`|Z).x by A4,A5,FDIFF_1:def 7
.=(1/2)*((2*(arcsin.x) #Z (2-1)) / sqrt(1-x^2)) by A2,A3,A5,Th10
.=((1/2)*(2*(arcsin.x) #Z (2-1))) / sqrt(1-x^2) by XCMPLX_1:74
.=arcsin.x / sqrt(1-x^2) by PREPOWER:35;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
::f.x=(1/2)*(arccos)^2
theorem
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)
proof
assume that
A1: Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) and
A2: Z c=]. -1,1 .[;
A3: Z c= dom (( #Z 2)*(arccos)) by A1,VALUED_1:def 5;
then
A4: ( #Z 2)*(arccos) is_differentiable_on Z by A2,Th11;
for x st x in Z holds (((1/2)(#)(( #Z 2)*(arccos)))`|Z).x =-arccos.x /
sqrt(1-x^2)
proof
let x;
assume
A5: x in Z;
then
(((1/2)(#)(( #Z 2)*(arccos)))`|Z).x =(1/2)*diff((( #Z 2)*arccos),x) by A1
,A4,FDIFF_1:20
.=(1/2)*((( #Z 2)*(arccos))`|Z).x by A4,A5,FDIFF_1:def 7
.=(1/2)*(-2*(arccos.x) #Z (2-1) / sqrt(1-x^2)) by A2,A3,A5,Th11
.=-(1/2)*((2*(arccos.x) #Z (2-1)) / sqrt(1-x^2))
.=-((1/2)*(2*(arccos.x) #Z (2-1))) / sqrt(1-x^2) by XCMPLX_1:74
.=-arccos.x / sqrt(1-x^2) by PREPOWER:35;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
::f.x=arcsin.(a*x+b)
theorem Th14:
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)
proof
assume that
A1: Z c= dom ((arcsin)*f) and
A2: for x st x in Z holds f.x=a*x+b & f.x > -1 & f.x < 1;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
A4: for x st x in Z holds f.x=a*x+b by A2;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds (arcsin)*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then
A8: f.x < 1 by A2;
f is_differentiable_in x & f.x > -1 by A2,A5,A7,FDIFF_1:9;
hence thesis by A8,Th6;
end;
then
A9: (arcsin)*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (((arcsin)*f)`|Z).x=a / sqrt(1-(a*x+b)^2)
proof
let x;
assume
A10: x in Z;
then
A11: f.x < 1 by A2;
f is_differentiable_in x & f.x > -1 by A2,A5,A10,FDIFF_1:9;
then diff((arcsin)*f,x) = diff(f,x)/sqrt(1-(f.x)^2) by A11,Th6
.=(f`|Z).x/sqrt(1-(f.x)^2) by A5,A10,FDIFF_1:def 7
.=a/sqrt(1-(f.x)^2) by A4,A3,A10,FDIFF_1:23
.=a / sqrt(1-(a*x+b)^2) by A2,A10;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
::f.x=arccos.(a*x+b)
theorem Th15:
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)
proof
assume that
A1: Z c= dom ((arccos)*f) and
A2: for x st x in Z holds f.x=a*x+b & f.x > -1 & f.x < 1;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
A4: for x st x in Z holds f.x=a*x+b by A2;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds (arccos)*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then
A8: f.x < 1 by A2;
f is_differentiable_in x & f.x > -1 by A2,A5,A7,FDIFF_1:9;
hence thesis by A8,Th7;
end;
then
A9: (arccos)*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (((arccos)*f)`|Z).x=-a / sqrt(1-(a*x+b)^2)
proof
let x;
assume
A10: x in Z;
then
A11: f.x < 1 by A2;
f is_differentiable_in x & f.x > -1 by A2,A5,A10,FDIFF_1:9;
then diff((arccos)*f,x) = -diff(f,x)/sqrt(1-(f.x)^2) by A11,Th7
.=-(f`|Z).x/sqrt(1-(f.x)^2) by A5,A10,FDIFF_1:def 7
.=-a/sqrt(1-(f.x)^2) by A4,A3,A10,FDIFF_1:23
.=-a / sqrt(1-(a*x+b)^2) by A2,A10;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
::f.x=x*arcsin.x
theorem Th16:
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)
proof
assume that
A1: Z c= dom ((id Z)(#)(arcsin)) and
A2: Z c= ]. -1,1 .[;
A3: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
Z c= dom (id Z) /\ dom (arcsin) by A1,VALUED_1:def 4;
then
A4: Z c= dom (id Z) by XBOOLE_1:18;
then
A5: id Z is_differentiable_on Z by A3,FDIFF_1:23;
A6: arcsin is_differentiable_on Z by A2,FDIFF_1:26,SIN_COS6:83;
for x st x in Z holds (((id Z)(#)(arcsin))`|Z).x =arcsin.x+x/sqrt(1-x^2)
proof
let x;
assume
A7: x in Z;
then
A8: -1 < x & x < 1 by A2,XXREAL_1:4;
(((id Z)(#)(arcsin))`|Z).x =(arcsin.x)*diff((id Z),x) + ((id Z).x)*
diff(arcsin,x) by A1,A5,A6,A7,FDIFF_1:21
.=(arcsin.x)*((id Z)`|Z).x+ ((id Z).x)*diff(arcsin,x) by A5,A7,
FDIFF_1:def 7
.=(arcsin.x)*1+ ((id Z).x)*diff(arcsin,x) by A4,A3,A7,FDIFF_1:23
.=(arcsin.x)*1+ ((id Z).x)*(1 / sqrt(1-x^2)) by A8,SIN_COS6:83
.=arcsin.x+ x*(1 / sqrt(1-x^2)) by A7,FUNCT_1:18
.=arcsin.x+x / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:21;
end;
::f.x=x*arccos.x
theorem Th17:
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)
proof
assume that
A1: Z c= dom ((id Z)(#)(arccos)) and
A2: Z c= ]. -1,1 .[;
A3: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
Z c= dom (id Z) /\ dom (arccos) by A1,VALUED_1:def 4;
then
A4: Z c= dom (id Z) by XBOOLE_1:18;
then
A5: id Z is_differentiable_on Z by A3,FDIFF_1:23;
A6: arccos is_differentiable_on Z by A2,FDIFF_1:26,SIN_COS6:106;
for x st x in Z holds (((id Z)(#)(arccos))`|Z).x =arccos.x-x/sqrt(1-x^2)
proof
let x;
assume
A7: x in Z;
then
A8: -1 < x & x < 1 by A2,XXREAL_1:4;
(((id Z)(#)(arccos))`|Z).x =(arccos.x)*diff((id Z),x) + ((id Z).x)*
diff(arccos,x) by A1,A5,A6,A7,FDIFF_1:21
.=(arccos.x)*((id Z)`|Z).x+ ((id Z).x)*diff(arccos,x) by A5,A7,
FDIFF_1:def 7
.=(arccos.x)*1+ ((id Z).x)*diff(arccos,x) by A4,A3,A7,FDIFF_1:23
.=(arccos.x)*1+ ((id Z).x)*(-1 / sqrt(1-x^2)) by A8,SIN_COS6:106
.=arccos.x+ x*(-1 / sqrt(1-x^2)) by A7,FUNCT_1:18
.=arccos.x-x*(1 / sqrt(1-x^2))
.=arccos.x-x / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:21;
end;
::f.x=(a*x+b)*arcsin.x
theorem
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)
proof
assume that
A1: Z c= dom (f(#)(arcsin)) and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=a*x+b;
Z c= dom f /\ dom arcsin by A1,VALUED_1:def 4;
then
A4: Z c= dom f by XBOOLE_1:18;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: arcsin is_differentiable_on Z by A2,FDIFF_1:26,SIN_COS6:83;
for x st x in Z holds ((f(#)(arcsin))`|Z).x =a*arcsin.x+(a*x+b)/sqrt(1-x ^2)
proof
let x;
assume
A7: x in Z;
then
A8: -1 < x & x < 1 by A2,XXREAL_1:4;
((f(#)(arcsin))`|Z).x =(arcsin.x)*diff(f,x) + (f.x)*diff(arcsin,x) by A1,A5
,A6,A7,FDIFF_1:21
.=(arcsin.x)*(f`|Z).x+ (f.x)*diff(arcsin,x) by A5,A7,FDIFF_1:def 7
.=(arcsin.x)*a+ (f.x)*diff(arcsin,x) by A3,A4,A7,FDIFF_1:23
.=(arcsin.x)*a+ (f.x)*(1 / sqrt(1-x^2)) by A8,SIN_COS6:83
.=a*arcsin.x+ (a*x+b)*(1 / sqrt(1-x^2)) by A3,A7
.=a*arcsin.x+(a*x+b) / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:21;
end;
::f.x=(a*x+b)*arccos.x
theorem
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)
proof
assume that
A1: Z c= dom (f(#)(arccos)) and
A2: Z c= ]. -1,1 .[ and
A3: for x st x in Z holds f.x=a*x+b;
Z c= dom f /\ dom arccos by A1,VALUED_1:def 4;
then
A4: Z c= dom f by XBOOLE_1:18;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: arccos is_differentiable_on Z by A2,FDIFF_1:26,SIN_COS6:106;
for x st x in Z holds ((f(#)(arccos))`|Z).x =a*arccos.x-(a*x+b)/sqrt(1-x ^2)
proof
let x;
assume
A7: x in Z;
then
A8: -1 < x & x < 1 by A2,XXREAL_1:4;
((f(#)(arccos))`|Z).x =(arccos.x)*diff(f,x) + (f.x)*diff(arccos,x) by A1,A5
,A6,A7,FDIFF_1:21
.=(arccos.x)*(f`|Z).x+ (f.x)*diff(arccos,x) by A5,A7,FDIFF_1:def 7
.=(arccos.x)*a+ (f.x)*diff(arccos,x) by A3,A4,A7,FDIFF_1:23
.=(arccos.x)*a+ (f.x)*(-1 / sqrt(1-x^2)) by A8,SIN_COS6:106
.=(arccos.x)*a-(f.x)*(1 / sqrt(1-x^2))
.=a*arccos.x-(a*x+b)*(1 / sqrt(1-x^2)) by A3,A7
.=a*arccos.x-(a*x+b) / sqrt(1-x^2) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:21;
end;
::f.x=(1/2)*arcsin(2*x)
theorem
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)
proof
assume that
A1: Z c= dom ((1/2)(#)((arcsin)*f)) and
A2: for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1;
A3: Z c= dom ((arcsin)*f) & for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x
< 1 by A1,A2,VALUED_1:def 5;
then
A4: (arcsin)*f is_differentiable_on Z by Th14;
for x st x in Z holds (((1/2)(#)((arcsin)*f))`|Z).x=1/sqrt(1-(2*x)^2)
proof
let x;
assume
A5: x in Z;
then (((1/2)(#)((arcsin)*f))`|Z).x =(1/2)*diff(((arcsin)*f),x) by A1,A4,
FDIFF_1:20
.=(1/2)*(((arcsin)*f)`|Z).x by A4,A5,FDIFF_1:def 7
.=(1/2)*(2 / sqrt(1-(2*x+0)^2)) by A3,A5,Th14
.=((1/2)*2 )/ sqrt(1-(2*x)^2) by XCMPLX_1:74
.=1/sqrt(1-(2*x)^2);
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
::f.x=(1/2)*arccos(2*x)
theorem
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)
proof
assume that
A1: Z c= dom ((1/2)(#)((arccos)*f)) and
A2: for x st x in Z holds f.x=2*x & f.x > -1 & f.x < 1;
A3: Z c= dom ((arccos)*f) & for x st x in Z holds f.x=2*x+0 & f.x > -1 & f.x
< 1 by A1,A2,VALUED_1:def 5;
then
A4: (arccos)*f is_differentiable_on Z by Th15;
for x st x in Z holds (((1/2)(#)((arccos)*f))`|Z).x=-1/sqrt(1-(2*x)^2)
proof
let x;
assume
A5: x in Z;
then (((1/2)(#)((arccos)*f))`|Z).x =(1/2)*diff(((arccos)*f),x) by A1,A4,
FDIFF_1:20
.=(1/2)*(((arccos)*f)`|Z).x by A4,A5,FDIFF_1:def 7
.=(1/2)*(-2 / sqrt(1-(2*x+0)^2)) by A3,A5,Th15
.=-(1/2)*(2 / sqrt(1-(2*x)^2))
.=-((1/2)*2)/sqrt(1-(2*x)^2) by XCMPLX_1:74
.=-1/sqrt(1-(2*x)^2);
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
::f.x=(1-x|^2) ^ (1/2)
theorem Th22:
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)
proof
assume that
A1: Z c= dom (( #R (1/2))*f) and
A2: f=f1-f2 and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=1 & f.x >0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A5: Z c= dom ((f1+(-1)(#)f2)) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=1+0*x by A4;
then
A7: f is_differentiable_on Z by A2,A3,A5,FDIFF_4:12;
A8: for x st x in Z holds ( #R (1/2))*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A4,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:22;
end;
then
A9: ( #R (1/2))*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #R (1/2))*f)`|Z).x =-x*(1-x #Z 2) #R (-1/2)
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x & f.x >0 by A4,A7,FDIFF_1:9;
x in dom (f1-f2) by A1,A2,A10,FUNCT_1:11;
then
A12: (f1-f2).x=f1.x - f2.x by VALUED_1:13
.=1 -(f2.x) by A4,A10
.=1 -(x #Z 2) by A3,TAYLOR_1:def 1;
((( #R (1/2))*f)`|Z).x =diff((( #R (1/2))*f),x) by A9,A10,FDIFF_1:def 7
.=(1/2)*((f.x) #R (1/2-1)) * diff(f,x) by A11,TAYLOR_1:22
.=(1/2)*((f.x) #R (1/2-1))*(f`|Z).x by A7,A10,FDIFF_1:def 7
.=(1/2)*((f.x) #R (1/2-1))*(0+2*(-1)*x) by A2,A3,A5,A6,A10,FDIFF_4:12
.=-x* (1-x #Z 2) #R (-1/2) by A2,A12;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
::f.x=x*arcsin.x+(1-x^2) ^ (1/2)
theorem
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
proof
assume that
A1: Z c= dom ((id Z)(#)(arcsin)+( #R (1/2))*f) and
A2: Z c= ]. -1,1 .[ and
A3: f=f1-f2 and
A4: f2=#Z 2 and
A5: for x st x in Z holds f1.x=1 & f.x >0 & x<>0;
A6: Z c= dom ((id Z)(#)(arcsin)) /\ dom (( #R (1/2))*f) by A1,VALUED_1:def 1;
then
A7: Z c= dom (( #R (1/2))*f) by XBOOLE_1:18;
A8: Z c= dom ((id Z)(#)(arcsin)) by A6,XBOOLE_1:18;
then
A9: (id Z)(#)(arcsin) is_differentiable_on Z by A2,Th16;
A10: for x st x in Z holds f1.x=1 & f.x >0 by A5;
then
A11: (( #R (1/2))*f) is_differentiable_on Z by A3,A4,A7,Th22;
A12: for x st x in Z holds x*(1-x #Z 2) #R (-1/2)=x/sqrt(1-x^2)
proof
let x;
assume
A13: x in Z;
then x in dom (f1-f2) by A3,A7,FUNCT_1:11;
then
A14: (f1-f2).x=f1.x - f2.x by VALUED_1:13
.=1 -(f2.x) by A5,A13
.=1 -(x #Z 2) by A4,TAYLOR_1:def 1;
f.x >0 by A5,A13;
then
A15: 1-x^2>0 by A3,A14,Th1;
(1-x #Z 2) #R (-1/2)=(1-x^2) #R (-1/2) by Th1
.=1/sqrt(1-x^2) by A15,Th3;
hence thesis by XCMPLX_1:99;
end;
for x st x in Z holds (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z).x =arcsin. x
proof
let x;
assume
A16: x in Z;
hence (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z).x =diff((id Z)(#)(arcsin),x)+
diff(( #R (1/2))*f,x) by A1,A9,A11,FDIFF_1:18
.=(((id Z)(#)(arcsin))`|Z).x+diff(( #R (1/2))*f,x) by A9,A16,
FDIFF_1:def 7
.=(((id Z)(#)(arcsin))`|Z).x+((( #R (1/2))*f)`|Z).x by A11,A16,
FDIFF_1:def 7
.=arcsin.x+x/sqrt(1-x^2)+((( #R (1/2))*f)`|Z).x by A2,A8,A16,Th16
.=arcsin.x+x/sqrt(1-x^2)+-x*(1-x #Z 2) #R (-1/2) by A3,A4,A10,A7,A16,Th22
.=arcsin.x+x/sqrt(1-x^2)-x*(1-x #Z 2) #R (-1/2)
.=arcsin.x+x/sqrt(1-x^2)-x/sqrt(1-x^2) by A12,A16
.=arcsin.x;
end;
hence thesis by A1,A9,A11,FDIFF_1:18;
end;
::f.x=x*arccos.x-(1-x^2) ^ (1/2)
theorem
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
proof
assume that
A1: Z c= dom ((id Z)(#)(arccos)-( #R (1/2))*f) and
A2: Z c= ]. -1,1 .[ and
A3: f=f1-f2 and
A4: f2=#Z 2 and
A5: for x st x in Z holds f1.x=1 & f.x >0 & x<>0;
A6: Z c= dom ((id Z)(#)(arccos)) /\ dom (( #R (1/2))*f) by A1,VALUED_1:12;
then
A7: Z c= dom (( #R (1/2))*f) by XBOOLE_1:18;
A8: Z c= dom ((id Z)(#)(arccos)) by A6,XBOOLE_1:18;
then
A9: (id Z)(#)(arccos) is_differentiable_on Z by A2,Th17;
A10: for x st x in Z holds f1.x=1 & f.x >0 by A5;
then
A11: (( #R (1/2))*f) is_differentiable_on Z by A3,A4,A7,Th22;
A12: for x st x in Z holds x*(1-x #Z 2) #R (-1/2)=x/sqrt(1-x^2)
proof
let x;
assume
A13: x in Z;
then x in dom (f1-f2) by A3,A7,FUNCT_1:11;
then
A14: (f1-f2).x=f1.x - f2.x by VALUED_1:13
.=1 -(f2.x) by A5,A13
.=1 -(x #Z 2) by A4,TAYLOR_1:def 1;
f.x >0 by A5,A13;
then
A15: 1-x^2>0 by A3,A14,Th1;
(1-x #Z 2) #R (-1/2)=(1-x^2) #R (-1/2) by Th1
.=1/sqrt(1-x^2) by A15,Th3;
hence thesis by XCMPLX_1:99;
end;
for x st x in Z holds (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z).x =arccos. x
proof
let x;
assume
A16: x in Z;
hence (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z).x =diff((id Z)(#)(arccos),x)-
diff(( #R (1/2))*f,x) by A1,A9,A11,FDIFF_1:19
.=(((id Z)(#)(arccos))`|Z).x-diff(( #R (1/2))*f,x) by A9,A16,
FDIFF_1:def 7
.=(((id Z)(#)(arccos))`|Z).x-((( #R (1/2))*f)`|Z).x by A11,A16,
FDIFF_1:def 7
.=arccos.x-x/sqrt(1-x^2)-((( #R (1/2))*f)`|Z).x by A2,A8,A16,Th17
.=arccos.x-x/sqrt(1-x^2)--x*(1-x #Z 2) #R (-1/2) by A3,A4,A10,A7,A16,Th22
.=arccos.x-x/sqrt(1-x^2)+x*(1-x #Z 2) #R (-1/2)
.=arccos.x-x/sqrt(1-x^2)+x/sqrt(1-x^2) by A12,A16
.=arccos.x;
end;
hence thesis by A1,A9,A11,FDIFF_1:19;
end;
::f.x=x*arcsin(x/a)
theorem Th25:
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))
proof
assume that
A1: Z c= dom ((id Z)(#)((arcsin)*f)) and
A2: for x st x in Z holds f.x=x/a & f.x > -1 & f.x < 1;
A3: Z c= dom (id Z) /\ dom ((arcsin)*f) by A1,VALUED_1:def 4;
then
A4: Z c= dom (id Z) by XBOOLE_1:18;
A5: Z c= dom ((arcsin)*f) by A3,XBOOLE_1:18;
for x st x in Z holds f.x=(1/a)*x+0
proof
let x;
assume x in Z;
then f.x=x/a by A2;
hence thesis by XCMPLX_1:99;
end;
then
A6: for x st x in Z holds f.x=(1/a)*x+0 & f.x > -1 & f.x < 1 by A2;
then
A7: (arcsin)*f is_differentiable_on Z by A5,Th14;
A8: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
then
A9: id Z is_differentiable_on Z by A4,FDIFF_1:23;
A10: for x st x in Z holds (((arcsin)*f)`|Z).x=1/(a*sqrt(1-(x/a)^2))
proof
let x;
assume x in Z;
then (((arcsin)*f)`|Z).x=(1/a)/sqrt(1-((1/a)*x+0)^2) by A6,A5,Th14
.=(1/a)/sqrt(1-(x/a)^2) by XCMPLX_1:99
.=1/(a*sqrt(1-(x/a)^2)) by XCMPLX_1:78;
hence thesis;
end;
for x st x in Z holds (((id Z)(#)((arcsin)*f))`|Z).x =arcsin.(x/a)+x/(a
*sqrt(1-(x/a)^2))
proof
let x;
assume
A11: x in Z;
then
A12: ((arcsin)*f).x=arcsin.(f.x) by A5,FUNCT_1:12
.=arcsin.(x/a) by A2,A11;
(((id Z)(#)((arcsin)*f))`|Z).x =((arcsin)*f).x*diff((id Z),x) + ((id
Z).x)*diff((arcsin)*f,x) by A1,A9,A7,A11,FDIFF_1:21
.=((arcsin)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arcsin)*f,x) by A9,A11,
FDIFF_1:def 7
.=((arcsin)*f).x*1+((id Z).x)*diff((arcsin)*f,x) by A4,A8,A11,FDIFF_1:23
.=((arcsin)*f).x*1+((id Z).x)*(((arcsin)*f)`|Z).x by A7,A11,FDIFF_1:def 7
.=((arcsin)*f).x+x*(((arcsin)*f)`|Z).x by A11,FUNCT_1:18
.=arcsin.(x/a)+x*(1/(a*sqrt(1-(x/a)^2))) by A10,A11,A12
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A9,A7,FDIFF_1:21;
end;
::f.x=x*arccos(x/a)
theorem Th26:
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))
proof
assume that
A1: Z c= dom ((id Z)(#)((arccos)*f)) and
A2: for x st x in Z holds f.x=x/a & f.x > -1 & f.x < 1;
A3: Z c= dom (id Z) /\ dom ((arccos)*f) by A1,VALUED_1:def 4;
then
A4: Z c= dom (id Z) by XBOOLE_1:18;
A5: Z c= dom ((arccos)*f) by A3,XBOOLE_1:18;
for x st x in Z holds f.x=(1/a)*x+0
proof
let x;
assume x in Z;
then f.x=x/a by A2;
hence thesis by XCMPLX_1:99;
end;
then
A6: for x st x in Z holds f.x=(1/a)*x+0 & f.x > -1 & f.x < 1 by A2;
then
A7: (arccos)*f is_differentiable_on Z by A5,Th15;
A8: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
then
A9: id Z is_differentiable_on Z by A4,FDIFF_1:23;
A10: for x st x in Z holds (((arccos)*f)`|Z).x=-1/(a*sqrt(1-(x/a)^2))
proof
let x;
assume x in Z;
then (((arccos)*f)`|Z).x=-(1/a)/sqrt(1-((1/a)*x+0)^2) by A6,A5,Th15
.=-(1/a)/sqrt(1-(x/a)^2) by XCMPLX_1:99
.=-1/(a*sqrt(1-(x/a)^2)) by XCMPLX_1:78;
hence thesis;
end;
for x st x in Z holds (((id Z)(#)((arccos)*f))`|Z).x =arccos.(x/a)-x/(a
*sqrt(1-(x/a)^2))
proof
let x;
assume
A11: x in Z;
then
A12: ((arccos)*f).x=arccos.(f.x) by A5,FUNCT_1:12
.=arccos.(x/a) by A2,A11;
(((id Z)(#)((arccos)*f))`|Z).x =((arccos)*f).x*diff((id Z),x) + ((id
Z).x)*diff((arccos)*f,x) by A1,A9,A7,A11,FDIFF_1:21
.=((arccos)*f).x*((id Z)`|Z).x + ((id Z).x)*diff((arccos)*f,x) by A9,A11,
FDIFF_1:def 7
.=((arccos)*f).x*1+((id Z).x)*diff((arccos)*f,x) by A4,A8,A11,FDIFF_1:23
.=((arccos)*f).x*1+((id Z).x)*(((arccos)*f)`|Z).x by A7,A11,FDIFF_1:def 7
.=((arccos)*f).x+x*(((arccos)*f)`|Z).x by A11,FUNCT_1:18
.=arccos.(x/a)+x*(-1/(a*sqrt(1-(x/a)^2))) by A10,A11,A12
.=arccos.(x/a)-x*(1/(a*sqrt(1-(x/a)^2)))
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A9,A7,FDIFF_1:21;
end;
::f.x=(a^2-x^2) ^ (1/2)
theorem Th27:
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)
proof
assume that
A1: Z c= dom (( #R (1/2))*f) and
A2: f=f1-f2 and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=a^2 & f.x >0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A5: Z c= dom ((f1+(-1)(#)f2)) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=a^2+0*x by A4;
then
A7: f is_differentiable_on Z by A2,A3,A5,FDIFF_4:12;
A8: for x st x in Z holds ( #R (1/2))*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A4,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:22;
end;
then
A9: ( #R (1/2))*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #R (1/2))*f)`|Z).x = -x*(a^2-x #Z 2) #R (-1/2 )
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x & f.x >0 by A4,A7,FDIFF_1:9;
x in dom (f1-f2) by A1,A2,A10,FUNCT_1:11;
then
A12: (f1-f2).x=f1.x - f2.x by VALUED_1:13
.=a^2 -(f2.x) by A4,A10
.=a^2 -(x #Z 2) by A3,TAYLOR_1:def 1;
((( #R (1/2))*f)`|Z).x = diff(( #R (1/2))*f,x) by A9,A10,FDIFF_1:def 7
.=(1/2)*((f.x) #R (1/2-1)) * diff(f,x) by A11,TAYLOR_1:22
.=(1/2)*((f.x) #R (1/2-1))*(f`|Z).x by A7,A10,FDIFF_1:def 7
.=(1/2)*((f.x) #R (1/2-1))*(0+2*(-1)*x) by A2,A3,A5,A6,A10,FDIFF_4:12
.=-x*(a^2-x #Z 2) #R (-1/2) by A2,A12;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
::f.x=x*arcsin(x/a)+(a^2-x^2) ^ (1/2)
theorem
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)
proof
assume that
A1: Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) and
A2: f=f1-f2 & f2=#Z 2 and
A3: 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;
A4: Z c= dom ((id Z)(#)((arcsin)*f3)) /\ dom (( #R (1/2))*f) by A1,
VALUED_1:def 1;
then
A5: Z c= dom (( #R (1/2))*f) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=a^2 & f.x >0 by A3;
then
A7: ( #R (1/2))*f is_differentiable_on Z by A2,A5,Th27;
A8: for x st x in Z holds f3.x=x/a & f3.x > -1 & f3.x < 1 by A3;
A9: Z c= dom ((id Z)(#)((arcsin)*f3)) by A4,XBOOLE_1:18;
then
A10: (id Z)(#)((arcsin)*f3) is_differentiable_on Z by A8,Th25;
A11: for x st x in Z holds (a^2-x #Z 2) #R (-1/2)=1/(a*sqrt(1-(x/a)^2))
proof
let x;
assume
A12: x in Z;
then
A13: f3.x=x/a by A3;
f3.x < 1 by A3,A12;
then
A14: 1-f3.x >1-1 by XREAL_1:10;
f3.x > -1 by A3,A12;
then 1+f3.x>1+(-1) by XREAL_1:6;
then
A15: (1+f3.x)*(1-f3.x)>0 by A14,XREAL_1:129;
A16: a>0 by A3,A12;
then
A17: a^2>0 by SQUARE_1:12;
1/(a*sqrt(1-(x/a)^2)) =1/((sqrt a^2)* sqrt (1-(x/a)^2)) by A16,SQUARE_1:22
.=1/sqrt ((a^2)*(1-(x/a)^2)) by A17,A13,A15,SQUARE_1:29
.=(a^2*1 - (a *(x/a))^2) #R (-1/2) by A17,A13,A15,Th3,XREAL_1:129
.=(a^2 - (x*a/a)^2) #R (-1/2) by XCMPLX_1:74
.=(a^2 - (x*(a/a))^2) #R (-1/2) by XCMPLX_1:74
.=(a^2 - (x*1)^2) #R (-1/2) by A16,XCMPLX_1:60
.=(a^2-x #Z 2) #R (-1/2) by Th1;
hence thesis;
end;
for x st x in Z holds (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x =
arcsin.(x/a)
proof
let x;
assume
A18: x in Z;
then (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = diff((id Z)(#)((
arcsin)*f3),x) + diff(( #R (1/2))*f,x) by A1,A10,A7,FDIFF_1:18
.=(((id Z)(#)((arcsin)*f3))`|Z).x+ diff(( #R (1/2))*f,x) by A10,A18,
FDIFF_1:def 7
.=(((id Z)(#)((arcsin)*f3))`|Z).x+ ((( #R (1/2))*f)`|Z).x by A7,A18,
FDIFF_1:def 7
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) + ((( #R (1/2))*f)`|Z).x by A9,A8
,A18,Th25
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) + -x*(a^2-x #Z 2) #R (-1/2) by A2,A5
,A6,A18,Th27
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) -x*(a^2-x #Z 2) #R (-1/2)
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) -x*(1/(a*sqrt(1-(x/a)^2))) by A11
,A18
.=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2)) -x/(a*sqrt(1-(x/a)^2)) by
XCMPLX_1:99
.=arcsin.(x/a);
hence thesis;
end;
hence thesis by A1,A10,A7,FDIFF_1:18;
end;
::f.x=x*arccos(x/a)-(a^2-x^2) ^ (1/2)
theorem
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)
proof
assume that
A1: Z c= dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) and
A2: f=f1-f2 & f2=#Z 2 and
A3: 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;
A4: Z c= dom ((id Z)(#)((arccos)*f3)) /\ dom (( #R (1/2))*f) by A1,VALUED_1:12;
then
A5: Z c= dom (( #R (1/2))*f) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=a^2 & f.x >0 by A3;
then
A7: ( #R (1/2))*f is_differentiable_on Z by A2,A5,Th27;
A8: for x st x in Z holds f3.x=x/a & f3.x > -1 & f3.x < 1 by A3;
A9: Z c= dom ((id Z)(#)((arccos)*f3)) by A4,XBOOLE_1:18;
then
A10: (id Z)(#)((arccos)*f3) is_differentiable_on Z by A8,Th26;
A11: for x st x in Z holds (a^2-x #Z 2) #R (-1/2)=1/(a*sqrt(1-(x/a)^2))
proof
let x;
assume
A12: x in Z;
then
A13: f3.x=x/a by A3;
f3.x < 1 by A3,A12;
then
A14: 1-f3.x >1-1 by XREAL_1:10;
f3.x > -1 by A3,A12;
then 1+f3.x>1+(-1) by XREAL_1:6;
then
A15: (1+f3.x)*(1-f3.x)>0 by A14,XREAL_1:129;
A16: a>0 by A3,A12;
then
A17: a^2>0 by SQUARE_1:12;
1/(a*sqrt(1-(x/a)^2)) =1/((sqrt a^2)* sqrt (1-(x/a)^2)) by A16,SQUARE_1:22
.=1/sqrt ((a^2)*(1-(x/a)^2)) by A17,A13,A15,SQUARE_1:29
.=(a^2*1 - (a *(x/a))^2) #R (-1/2) by A17,A13,A15,Th3,XREAL_1:129
.=(a^2 - (x*a/a)^2) #R (-1/2) by XCMPLX_1:74
.=(a^2 - (x*(a/a))^2) #R (-1/2) by XCMPLX_1:74
.=(a^2 - (x*1)^2) #R (-1/2) by A16,XCMPLX_1:60
.=(a^2-x #Z 2) #R (-1/2) by Th1;
hence thesis;
end;
for x st x in Z holds (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x =
arccos.(x/a)
proof
let x;
assume
A18: x in Z;
then (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = diff((id Z)(#)((
arccos)*f3),x) - diff(( #R (1/2))*f,x) by A1,A10,A7,FDIFF_1:19
.=(((id Z)(#)((arccos)*f3))`|Z).x- diff(( #R (1/2))*f,x) by A10,A18,
FDIFF_1:def 7
.=(((id Z)(#)((arccos)*f3))`|Z).x- ((( #R (1/2))*f)`|Z).x by A7,A18,
FDIFF_1:def 7
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) - ((( #R (1/2))*f)`|Z).x by A9,A8
,A18,Th26
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) - -x*(a^2-x #Z 2) #R (-1/2) by A2,A5
,A6,A18,Th27
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) +x*(a^2-x #Z 2) #R (-1/2)
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) +x*(1/(a*sqrt(1-(x/a)^2))) by A11
,A18
.=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2)) +x/(a*sqrt(1-(x/a)^2)) by
XCMPLX_1:99
.=arccos.(x/a);
hence thesis;
end;
hence thesis by A1,A10,A7,FDIFF_1:19;
end;
::f.x=-1/(n*(sin.x)^n)
theorem
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))
proof
assume that
A1: Z c= dom ((-1/n)(#)(( #Z n)*(sin^))) and
A2: n>0 and
A3: for x st x in Z holds sin.x<>0;
A4: Z c= dom (( #Z n)*(sin^)) by A1,VALUED_1:def 5;
A5: sin^ is_differentiable_on Z by A3,FDIFF_4:40;
now
let x;
assume x in Z;
then sin^ is_differentiable_in x by A5,FDIFF_1:9;
hence ( #Z n)*(sin^) is_differentiable_in x by TAYLOR_1:3;
end;
then
A6: ( #Z n)*(sin^) is_differentiable_on Z by A4,FDIFF_1:9;
for y being object st y in Z holds y in dom (sin^) by A4,FUNCT_1:11;
then
A7: Z c= dom (sin^) by TARSKI:def 3;
for x st x in Z holds (((-1/n)(#)(( #Z n)*(sin^)))`|Z).x =cos.x/((sin.x
) #Z (n+1))
proof
let x;
assume
A8: x in Z;
then
A9: sin^ is_differentiable_in x by A5,FDIFF_1:9;
A10: (sin^).x=(sin.x)" by A7,A8,RFUNCT_1:def 2
.=1/sin.x by XCMPLX_1:215;
(((-1/n)(#)(( #Z n)*(sin^)))`|Z).x =(-1/n)*diff((( #Z n)*(sin^)),x)
by A1,A6,A8,FDIFF_1:20
.=(-1/n)*(n*(((sin^).x) #Z (n-1)) * diff(sin^,x)) by A9,TAYLOR_1:3
.=(-1/n)*(n*(((sin^).x) #Z (n-1)) * ((sin^)`|Z).x) by A5,A8,FDIFF_1:def 7
.=(-1/n)*(n*(((sin^).x) #Z (n-1)) *(-cos.x/(sin.x)^2)) by A3,A8,
FDIFF_4:40
.=-((1/n)*n)*(((sin^).x) #Z (n-1)) *(-cos.x/(sin.x)^2)
.=-1*(((sin^).x) #Z (n-1)) * (-cos.x/(sin.x)^2) by A2,XCMPLX_1:106
.=-(1/sin.x) #Z (n-1) *(-cos.x/((sin.x) #Z 2)) by A10,Th1
.=-(-cos.x/((sin.x) #Z 2))*(1/((sin.x) #Z (n-1))) by PREPOWER:42
.=(cos.x/((sin.x) #Z 2))*(1/((sin.x) #Z (n-1)))
.=cos.x/((sin.x) #Z 2)/((sin.x) #Z (n-1)) by XCMPLX_1:99
.=cos.x/(((sin.x) #Z 2)*((sin.x) #Z (n-1))) by XCMPLX_1:78
.=cos.x/((sin.x) #Z (2+(n-1))) by A3,A8,PREPOWER:44
.=cos.x/((sin.x) #Z (n+1));
hence thesis;
end;
hence thesis by A1,A6,FDIFF_1:20;
end;
::f.x=1/(n*(cos.x)^n)
theorem
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))
proof
assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*(cos^))) and
A2: n>0 and
A3: for x st x in Z holds cos.x<>0;
A4: Z c= dom (( #Z n)*(cos^)) by A1,VALUED_1:def 5;
A5: cos^ is_differentiable_on Z by A3,FDIFF_4:39;
now
let x;
assume x in Z;
then cos^ is_differentiable_in x by A5,FDIFF_1:9;
hence ( #Z n)*(cos^) is_differentiable_in x by TAYLOR_1:3;
end;
then
A6: ( #Z n)*(cos^) is_differentiable_on Z by A4,FDIFF_1:9;
for y being object st y in Z holds y in dom (cos^) by A4,FUNCT_1:11;
then
A7: Z c= dom (cos^) by TARSKI:def 3;
for x st x in Z holds (((1/n)(#)(( #Z n)*(cos^)))`|Z).x=sin.x/((cos.x)
#Z (n+1))
proof
let x;
assume
A8: x in Z;
then
A9: cos^ is_differentiable_in x by A5,FDIFF_1:9;
A10: (cos^).x=(cos.x)" by A7,A8,RFUNCT_1:def 2
.=1/cos.x by XCMPLX_1:215;
(((1/n)(#)(( #Z n)*(cos^)))`|Z).x =(1/n)*diff((( #Z n)*(cos^)),x) by A1,A6
,A8,FDIFF_1:20
.=(1/n)*(n*(((cos^).x) #Z (n-1)) * diff(cos^,x)) by A9,TAYLOR_1:3
.=(1/n)*(n*(((cos^).x) #Z (n-1)) * ( (cos^)`|Z).x ) by A5,A8,
FDIFF_1:def 7
.=(1/n)*(n*(((cos^).x) #Z (n-1)) *(sin.x/(cos.x)^2)) by A3,A8,FDIFF_4:39
.=((1/n)*n)*(((cos^).x) #Z (n-1)) *(sin.x/(cos.x)^2)
.=1*(((cos^).x) #Z (n-1)) * (sin.x/(cos.x)^2) by A2,XCMPLX_1:106
.=(1/cos.x) #Z (n-1) *(sin.x/((cos.x) #Z 2)) by A10,Th1
.=(1/((cos.x) #Z (n-1))) *(sin.x/((cos.x) #Z 2)) by PREPOWER:42
.=(sin.x/((cos.x) #Z 2))/((cos.x) #Z (n-1)) by XCMPLX_1:99
.=sin.x/(((cos.x) #Z 2)*((cos.x) #Z (n-1))) by XCMPLX_1:78
.=sin.x/((cos.x) #Z (2+(n-1))) by A3,A8,PREPOWER:44
.=sin.x/((cos.x) #Z (n+1));
hence thesis;
end;
hence thesis by A1,A6,FDIFF_1:20;
end;
Lm3: right_open_halfline 0 = {g where g is Real: 0<g} by XXREAL_1:230;
::f.x=sin(ln.x)
theorem
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
proof
assume that
A1: Z c= dom (sin*ln) and
A2: for x st x in Z holds x>0;
A3: for x st x in Z holds sin*ln is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: ln is_differentiable_in x by A2,TAYLOR_1:18;
sin is_differentiable_in ln.x by SIN_COS:64;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: sin*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*ln)`|Z).x =cos.(ln.x)/x
proof
let x;
A6: sin is_differentiable_in ln.x by SIN_COS:64;
assume
A7: x in Z;
then x>0 by A2;
then
A8: x in right_open_halfline(0) by Lm3;
ln is_differentiable_in x by A2,A7,TAYLOR_1:18;
then diff(sin*ln,x) = diff(sin,ln.x)*diff(ln,x) by A6,FDIFF_2:13
.=cos.(ln.x)*diff(ln,x) by SIN_COS:64
.=cos.(ln.x)*(1/x) by A8,TAYLOR_1:18
.=cos.(ln.x)/x by XCMPLX_1:99;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cos(ln.x)
theorem
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
proof
assume that
A1: Z c= dom (cos*ln) and
A2: for x st x in Z holds x>0;
A3: for x st x in Z holds cos*ln is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: ln is_differentiable_in x by A2,TAYLOR_1:18;
cos is_differentiable_in ln.x by SIN_COS:63;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: cos*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*ln)`|Z).x =-sin.(ln.x)/x
proof
let x;
A6: cos is_differentiable_in ln.x by SIN_COS:63;
assume
A7: x in Z;
then x>0 by A2;
then
A8: x in right_open_halfline(0) by Lm3;
ln is_differentiable_in x by A2,A7,TAYLOR_1:18;
then diff(cos*ln,x) = diff(cos,ln.x)*diff(ln,x) by A6,FDIFF_2:13
.=(-sin.(ln.x))*diff(ln,x) by SIN_COS:63
.=(-sin.(ln.x))*(1/x) by A8,TAYLOR_1:18
.=(-sin.(ln.x))/x by XCMPLX_1:99
.=-sin.(ln.x)/x by XCMPLX_1:187;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=sin(exp.x)
theorem
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)
proof
A1: for x st x in Z holds sin*exp_R is_differentiable_in x
proof
let x;
assume x in Z;
exp_R is_differentiable_in x & sin is_differentiable_in exp_R.x by
SIN_COS:64,65;
hence thesis by FDIFF_2:13;
end;
assume
A2: Z c= dom (sin*exp_R);
then
A3: sin*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*exp_R)`|Z).x =exp_R.x * cos.(exp_R.x)
proof
let x;
exp_R is_differentiable_in x & sin is_differentiable_in exp_R.x by
SIN_COS:64,65;
then
A4: diff(sin*exp_R,x) = diff(sin,exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=cos.(exp_R.x)*diff(exp_R,x) by SIN_COS:64
.=exp_R.x*cos.(exp_R.x) by SIN_COS:65;
assume x in Z;
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A2,A1,FDIFF_1:9;
end;
::f.x=cos(exp_R.x)
theorem
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)
proof
A1: for x st x in Z holds cos*exp_R is_differentiable_in x
proof
let x;
assume x in Z;
exp_R is_differentiable_in x & cos is_differentiable_in exp_R.x by
SIN_COS:63,65;
hence thesis by FDIFF_2:13;
end;
assume
A2: Z c= dom (cos*exp_R);
then
A3: cos*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*exp_R)`|Z).x =-exp_R.x * sin.(exp_R.x)
proof
let x;
exp_R is_differentiable_in x & cos is_differentiable_in exp_R.x by
SIN_COS:63,65;
then
A4: diff(cos*exp_R,x) = diff(cos,exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=(-sin.(exp_R.x))*diff(exp_R,x) by SIN_COS:63
.=(-sin.(exp_R.x))*exp_R.x by SIN_COS:65
.=-exp_R.x*sin.(exp_R.x);
assume x in Z;
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A2,A1,FDIFF_1:9;
end;
::f.x=exp_R.(cos.x)
theorem
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
proof
A1: for x st x in Z holds exp_R*cos is_differentiable_in x
proof
let x;
assume x in Z;
cos is_differentiable_in x & exp_R is_differentiable_in cos.x by SIN_COS:63
,65;
hence thesis by FDIFF_2:13;
end;
assume
A2: Z c= dom (exp_R*cos);
then
A3: exp_R*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*cos)`|Z).x =-exp_R.(cos.x) * sin.x
proof
let x;
cos is_differentiable_in x & exp_R is_differentiable_in cos.x by SIN_COS:63
,65;
then
A4: diff(exp_R*cos,x) = diff(exp_R,cos.x)*diff(cos,x) by FDIFF_2:13
.=diff(exp_R,cos.x)*(-sin.x ) by SIN_COS:63
.=exp_R.(cos.x)*(-sin.x ) by SIN_COS:65
.=-exp_R.(cos.x) * sin.x;
assume x in Z;
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A2,A1,FDIFF_1:9;
end;
::f.x=exp_R.(sin.x)
theorem
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
proof
A1: for x st x in Z holds exp_R*sin is_differentiable_in x
proof
let x;
assume x in Z;
sin is_differentiable_in x & exp_R is_differentiable_in sin.x by SIN_COS:64
,65;
hence thesis by FDIFF_2:13;
end;
assume
A2: Z c= dom (exp_R*sin);
then
A3: exp_R*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*sin)`|Z).x = exp_R.(sin.x) * cos.x
proof
let x;
sin is_differentiable_in x & exp_R is_differentiable_in sin.x by SIN_COS:64
,65;
then
A4: diff(exp_R*sin,x) = diff(exp_R,sin.x)*diff(sin,x) by FDIFF_2:13
.=diff(exp_R,sin.x)*(cos.x ) by SIN_COS:64
.=exp_R.(sin.x) * cos.x by SIN_COS:65;
assume x in Z;
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A2,A1,FDIFF_1:9;
end;
::f.x=sin.x+cos.x
theorem Th38:
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
proof
A1: sin is_differentiable_on Z & cos is_differentiable_on Z by FDIFF_1:26
,SIN_COS:67,68;
assume
A2: Z c= dom (sin+cos);
now
let x;
assume x in Z;
hence ((sin+cos)`|Z).x =diff(sin,x) + diff(cos,x) by A2,A1,FDIFF_1:18
.=cos.x +diff(cos,x) by SIN_COS:64
.=cos.x +(-sin.x) by SIN_COS:63
.=cos.x-sin.x;
end;
hence thesis by A2,A1,FDIFF_1:18;
end;
::f.x=sin.x-cos.x
theorem Th39:
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
proof
A1: sin is_differentiable_on Z & cos is_differentiable_on Z by FDIFF_1:26
,SIN_COS:67,68;
assume
A2: Z c= dom (sin-cos);
now
let x;
assume x in Z;
hence ((sin-cos)`|Z).x =diff(sin,x) - diff(cos,x) by A2,A1,FDIFF_1:19
.=cos.x -diff(cos,x) by SIN_COS:64
.=cos.x -(-sin.x) by SIN_COS:63
.=cos.x+sin.x;
end;
hence thesis by A2,A1,FDIFF_1:19;
end;
::f.x=exp_R.x*(sin.x-cos.x)
theorem
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
proof
assume
A1: Z c= dom (exp_R(#)(sin-cos));
then Z c= dom (sin-cos) /\ dom exp_R by VALUED_1:def 4;
then
A2: Z c= dom (sin-cos) by XBOOLE_1:18;
then
A3: sin-cos is_differentiable_on Z by Th39;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds ((exp_R(#)(sin-cos))`|Z).x =2 * exp_R.x * sin.x
proof
let x;
assume
A5: x in Z;
then
((exp_R(#)(sin-cos))`|Z).x = ((sin-cos).x)*diff(exp_R,x) + (exp_R.x)*
diff((sin-cos),x) by A1,A3,A4,FDIFF_1:21
.=(sin.x-cos.x)*diff(exp_R,x)+ (exp_R.x)*diff((sin-cos),x) by A2,A5,
VALUED_1:13
.=(sin.x-cos.x)*(exp_R.x)+ (exp_R.x)*diff((sin-cos),x) by TAYLOR_1:16
.=(sin.x-cos.x)*(exp_R.x)+(exp_R.x)*((sin-cos)`|Z).x by A3,A5,
FDIFF_1:def 7
.=(sin.x-cos.x)*(exp_R.x)+(exp_R.x)*(cos.x+sin.x) by A2,A5,Th39
.=2 * exp_R.x * sin.x;
hence thesis;
end;
hence thesis by A1,A3,A4,FDIFF_1:21;
end;
::f.x=exp_R.x*(sin.x+cos.x)
theorem
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
proof
assume
A1: Z c= dom (exp_R(#)(sin+cos));
then Z c= dom (sin+cos) /\ dom exp_R by VALUED_1:def 4;
then
A2: Z c= dom (sin+cos) by XBOOLE_1:18;
then
A3: sin+cos is_differentiable_on Z by Th38;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds ((exp_R(#)(sin+cos))`|Z).x =2 * exp_R.x * cos.x
proof
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
assume
A5: x in Z;
then
((exp_R(#)(sin+cos))`|Z).x = ((sin+cos).xx)*diff(exp_R,x) + (exp_R.x)*
diff((sin+cos),x) by A1,A3,A4,FDIFF_1:21
.=(sin.xx+cos.xx)*diff(exp_R,x)+ (exp_R.x)*diff((sin+cos),x)
by VALUED_1:1
.=(sin.x+cos.x)*(exp_R.x)+ (exp_R.x)*diff((sin+cos),x) by TAYLOR_1:16
.=(sin.x+cos.x)*(exp_R.x)+(exp_R.x)*((sin+cos)`|Z).x by A3,A5,
FDIFF_1:def 7
.=(sin.x+cos.x)*(exp_R.x)+(exp_R.x)*(cos.x-sin.x) by A2,A5,Th38
.=2 * exp_R.x * cos.x;
hence thesis;
end;
hence thesis by A1,A3,A4,FDIFF_1:21;
end;
::f.x=(sin.x+cos.x)/exp_R.x
theorem
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
proof
assume Z c= dom ((sin+cos)/exp_R);
then Z c= dom (sin+cos) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A1: Z c= dom (sin+cos) by XBOOLE_1:18;
then
A2: sin+cos is_differentiable_on Z by Th38;
A3: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
then
A4: (sin+cos)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
for x st x in Z holds (((sin+cos)/exp_R)`|Z).x =-2*sin.x/exp_R.x
proof
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
A5: (sin+cos).xx=sin.xx+cos.xx by VALUED_1:1;
A6: exp_R.x <>0 by SIN_COS:54;
assume
A7: x in Z;
then exp_R is_differentiable_in x & sin+cos is_differentiable_in x by A2,
FDIFF_1:9,SIN_COS:65;
then
diff((sin+cos)/exp_R,x) =(diff(sin+cos,x) * exp_R.x - diff(exp_R,x) *
(sin+cos).x)/(exp_R.x)^2 by A6,FDIFF_2:14
.=(((sin+cos)`|Z).x* exp_R.x - diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2
by A2,A7,FDIFF_1:def 7
.=((cos.x-sin.x)* exp_R.x - diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2 by A1
,A7,Th38
.=((cos.x-sin.x)* exp_R.x - exp_R.x*(sin.x+cos.x))/(exp_R.x)^2 by A5,
SIN_COS:65
.=((-2*sin.x)*exp_R.x)/((exp_R.x)*(exp_R.x))
.=(-2*sin.x)*(exp_R.x/((exp_R.x)*(exp_R.x))) by XCMPLX_1:74
.=(-2*sin.x)*((exp_R.x)/(exp_R.x)/(exp_R.x)) by XCMPLX_1:78
.=(-2*sin.x)*(1/exp_R.x) by A6,XCMPLX_1:60
.=(-(2*sin.x))/exp_R.x by XCMPLX_1:99
.=-2*sin.x/exp_R.x by XCMPLX_1:187;
hence thesis by A4,A7,FDIFF_1:def 7;
end;
hence thesis by A2,A3,FDIFF_2:21;
end;
::f.x=(sin.x-cos.x)/exp_R.x
theorem
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
proof
assume Z c= dom ((sin-cos)/exp_R);
then Z c= dom (sin-cos) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A1: Z c= dom (sin-cos) by XBOOLE_1:18;
then
A2: sin-cos is_differentiable_on Z by Th39;
A3: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
then
A4: (sin-cos)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
for x st x in Z holds (((sin-cos)/exp_R)`|Z).x =2*cos.x/exp_R.x
proof
let x;
A5: exp_R.x <>0 by SIN_COS:54;
assume
A6: x in Z;
then
A7: (sin-cos).x=sin.x-cos.x by A1,VALUED_1:13;
exp_R is_differentiable_in x & sin-cos is_differentiable_in x by A2,A6,
FDIFF_1:9,SIN_COS:65;
then
diff((sin-cos)/exp_R,x) =(diff(sin-cos,x) * exp_R.x - diff(exp_R,x) *
(sin-cos).x)/(exp_R.x)^2 by A5,FDIFF_2:14
.=(((sin-cos)`|Z).x* exp_R.x - diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2
by A2,A6,FDIFF_1:def 7
.=((cos.x+sin.x)* exp_R.x - diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2 by A1
,A6,Th39
.=((cos.x+sin.x)* exp_R.x - exp_R.x*(sin.x-cos.x))/(exp_R.x)^2 by A7,
SIN_COS:65
.=((2*cos.x)*exp_R.x)/((exp_R.x)*(exp_R.x))
.=(2*cos.x)*(exp_R.x/((exp_R.x)*(exp_R.x))) by XCMPLX_1:74
.=(2*cos.x)*((exp_R.x)/(exp_R.x)/(exp_R.x)) by XCMPLX_1:78
.=(2*cos.x)*(1/exp_R.x) by A5,XCMPLX_1:60
.=2*cos.x/exp_R.x by XCMPLX_1:99;
hence thesis by A4,A6,FDIFF_1:def 7;
end;
hence thesis by A2,A3,FDIFF_2:21;
end;
::f.x=exp_R.x*sin.x
theorem
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)
proof
A1: sin is_differentiable_on Z & exp_R is_differentiable_on Z by FDIFF_1:26
,SIN_COS:68,TAYLOR_1:16;
assume
A2: Z c= dom (exp_R(#)sin);
now
let x;
assume x in Z;
hence ((exp_R(#)sin)`|Z).x = sin.x * diff(exp_R,x) + exp_R.x * diff(sin,x)
by A2,A1,FDIFF_1:21
.=sin.x*exp_R.x+ (exp_R.x)*diff(sin,x) by TAYLOR_1:16
.=sin.x*exp_R.x+ exp_R.x*cos.x by SIN_COS:64
.=exp_R.x*(sin.x+cos.x);
end;
hence thesis by A2,A1,FDIFF_1:21;
end;
::f.x=exp_R.x*cos.x
theorem
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)
proof
A1: cos is_differentiable_on Z & exp_R is_differentiable_on Z by FDIFF_1:26
,SIN_COS:67,TAYLOR_1:16;
assume
A2: Z c= dom (exp_R(#)cos);
now
let x;
assume x in Z;
hence ((exp_R(#)cos)`|Z).x = cos.x * diff(exp_R,x) + exp_R.x * diff(cos,x)
by A2,A1,FDIFF_1:21
.=cos.x*exp_R.x+ (exp_R.x)*diff(cos,x) by TAYLOR_1:16
.=cos.x*exp_R.x+ exp_R.x*(-sin.x) by SIN_COS:63
.=exp_R.x*(cos.x-sin.x);
end;
hence thesis by A2,A1,FDIFF_1:21;
end;
:: f.x=tan.x
theorem Th46:
cos.x<>0 implies sin/cos is_differentiable_in x & diff(sin/cos,
x)=1/(cos.x)^2
proof
assume
A1: cos.x<>0;
A2: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
then
diff(sin/cos,x) =(diff(sin,x) * cos.x - diff(cos,x)*sin.x)/(cos.x)^2 by A1,
FDIFF_2:14
.=((cos.x)*cos.x - diff(cos,x)*sin.x)/(cos.x)^2 by SIN_COS:64
.=((cos.x)*(cos.x)-(-sin.x)*(sin.x))/(cos.x)^2 by SIN_COS:63
.=((cos.x)*(cos.x) + (sin.x)*(sin.x))/(cos.x)^2
.=1/(cos.x)^2 by SIN_COS:28;
hence thesis by A2,A1,FDIFF_2:14;
end;
::f.x=cot.x
theorem Th47:
sin.x<>0 implies cos/sin is_differentiable_in x & diff(cos/sin,
x)=-1/(sin.x)^2
proof
assume
A1: sin.x<>0;
A2: sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
then
diff(cos/sin,x) = (diff(cos,x) * sin.x - diff(sin,x)*cos.x)/(sin.x)^2 by A1,
FDIFF_2:14
.=((-sin.x)*sin.x - diff(sin,x)*cos.x)/(sin.x)^2 by SIN_COS:63
.=(-(sin.x)*(sin.x)-(cos.x)*(cos.x))/(sin.x)^2 by SIN_COS:64
.=(-((cos.x)^2 + (sin.x)*(sin.x)))/(sin.x)^2
.=-((cos.x)^2 + (sin.x)^2)/(sin.x)^2by XCMPLX_1:187
.=-1/(sin.x)^2 by SIN_COS:28;
hence thesis by A2,A1,FDIFF_2:14;
end;
::f.x=(tan.x) ^ 2
theorem
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)
proof
assume that
A1: Z c= dom (( #Z 2)*(sin/cos)) and
A2: for x st x in Z holds cos.x<>0;
for y being object st y in Z holds y in dom (sin/cos) by A1,FUNCT_1:11;
then
A3: Z c= dom (sin/cos) by TARSKI:def 3;
A4: for x st x in Z holds ( #Z 2)*(sin/cos) is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A2;
then sin/cos is_differentiable_in x by Th46;
hence thesis by TAYLOR_1:3;
end;
then
A5: ( #Z 2)*(sin/cos) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z 2)*(sin/cos))`|Z).x =2*sin.x/((cos.x) #Z 3 )
proof
let x;
assume
A6: x in Z;
then
A7: (sin/cos).x = sin.x*(cos.x)" by A3,RFUNCT_1:def 1
.=sin.x*(1/cos.x) by XCMPLX_1:215
.=sin.x/cos.x by XCMPLX_1:99;
A8: cos.x<>0 by A2,A6;
then
A9: sin/cos is_differentiable_in x by Th46;
((( #Z 2)*(sin/cos))`|Z).x=diff(( #Z 2)*(sin/cos),x) by A5,A6,FDIFF_1:def 7
.=2*(((sin/cos).x) #Z (2-1)) * diff(sin/cos,x) by A9,TAYLOR_1:3
.=2*(((sin/cos).x) #Z (2-1)) *(1/(cos.x)^2) by A8,Th46
.=2*(((sin/cos).x) #Z 1) /(cos.x)^2 by XCMPLX_1:99
.=2*(sin.x/cos.x)/(cos.x)^2 by A7,PREPOWER:35
.=2*sin.x/cos.x/(cos.x)^2 by XCMPLX_1:74
.=2*sin.x/(cos.x*(cos.x)^2) by XCMPLX_1:78
.=2*sin.x/(cos.x*((cos.x) #Z 2)) by Th1
.=2*sin.x/(((cos.x) #Z 1) *((cos.x) #Z 2)) by PREPOWER:35
.=2*sin.x/((cos.x) #Z (1+2)) by A2,A6,PREPOWER:44
.=2*sin.x/((cos.x) #Z 3);
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=(cot.x) ^ 2
theorem
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)
proof
assume that
A1: Z c= dom (( #Z 2)*(cos/sin)) and
A2: for x st x in Z holds sin.x<>0;
for y being object st y in Z holds y in dom (cos/sin) by A1,FUNCT_1:11;
then
A3: Z c= dom (cos/sin) by TARSKI:def 3;
A4: for x st x in Z holds ( #Z 2)*(cos/sin) is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A2;
then cos/sin is_differentiable_in x by Th47;
hence thesis by TAYLOR_1:3;
end;
then
A5: ( #Z 2)*(cos/sin) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z 2)*(cos/sin))`|Z).x=-2*cos.x/((sin.x) #Z 3 )
proof
let x;
assume
A6: x in Z;
then
A7: (cos/sin).x = cos.x*(sin.x)" by A3,RFUNCT_1:def 1
.=cos.x*(1/sin.x) by XCMPLX_1:215
.=cos.x/sin.x by XCMPLX_1:99;
A8: sin.x<>0 by A2,A6;
then
A9: cos/sin is_differentiable_in x by Th47;
((( #Z 2)*(cos/sin))`|Z).x=diff(( #Z 2)*(cos/sin),x) by A5,A6,FDIFF_1:def 7
.=2*(((cos/sin).x) #Z (2-1)) * diff(cos/sin,x) by A9,TAYLOR_1:3
.=2*(((cos/sin).x) #Z (2-1)) *(-1/(sin.x)^2) by A8,Th47
.=-2*(((cos/sin).x) #Z (2-1)) *(1/(sin.x)^2)
.=-2*(((cos/sin).x) #Z 1) /(sin.x)^2 by XCMPLX_1:99
.=-2*(cos.x/sin.x)/(sin.x)^2 by A7,PREPOWER:35
.=-2*cos.x/sin.x/(sin.x)^2 by XCMPLX_1:74
.=-2*cos.x/(sin.x*(sin.x)^2) by XCMPLX_1:78
.=-2*cos.x/(sin.x*((sin.x) #Z 2)) by Th1
.=-2*cos.x/(((sin.x) #Z 1) *((sin.x) #Z 2)) by PREPOWER:35
.=-2*cos.x/((sin.x) #Z (1+2)) by A2,A6,PREPOWER:44
.=-2*cos.x/((sin.x) #Z 3);
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=tan.(x/2)
theorem
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)
proof
assume that
A1: Z c= dom ((sin/cos)*f) and
A2: for x st x in Z holds f.x=x/2 & cos.(f.x)<>0;
A3: for x st x in Z holds f.x=(1/2)*x+0
proof
let x;
assume x in Z;
then f.x=x/2 by A2;
hence thesis;
end;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom f by TARSKI:def 3;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds (sin/cos)*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then cos.(f.x)<>0 by A2;
then
A8: (sin/cos) is_differentiable_in f.x by Th46;
f is_differentiable_in x by A5,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: (sin/cos)*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (((sin/cos)*f)`|Z).x = 1/(1+cos.x)
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x by A5,FDIFF_1:9;
A12: cos.(f.x)<>0 by A2,A10;
then (sin/cos) is_differentiable_in f.x by Th46;
then diff((sin/cos)*f,x) = diff(sin/cos, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(1/(cos.(f.x))^2) * diff(f,x) by A12,Th46
.=diff(f,x)/(cos.(f.x))^2 by XCMPLX_1:99
.=diff(f,x)/(cos.(x/2))^2 by A2,A10
.=(f`|Z).x/(cos.(x/2))^2 by A5,A10,FDIFF_1:def 7
.=1/2/(cos.(x/2))^2 by A3,A4,A10,FDIFF_1:23
.=1/(2*(cos.(x/2))^2) by XCMPLX_1:78
.=1/(1+cos.x) by Lm1;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
::f.x=cot.(x/2)
theorem
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)
proof
assume that
A1: Z c= dom ((cos/sin)*f) and
A2: for x st x in Z holds f.x=x/2 & sin.(f.x)<>0;
A3: for x st x in Z holds f.x=(1/2)*x+0
proof
let x;
assume x in Z;
then f.x=x/2 by A2;
hence thesis;
end;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom f by TARSKI:def 3;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds (cos/sin)*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then sin.(f.x)<>0 by A2;
then
A8: cos/sin is_differentiable_in f.x by Th47;
f is_differentiable_in x by A5,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: (cos/sin)*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (((cos/sin)*f)`|Z).x = -1/(1-cos.x)
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x by A5,FDIFF_1:9;
A12: sin.(f.x)<>0 by A2,A10;
then cos/sin is_differentiable_in f.x by Th47;
then diff((cos/sin)*f,x) = diff(cos/sin, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(-1/(sin.(f.x))^2) * diff(f,x) by A12,Th47
.=-(1/(sin.(f.x))^2) * diff(f,x)
.=-diff(f,x)/(sin.(f.x))^2 by XCMPLX_1:99
.=-diff(f,x)/(sin.(x/2))^2 by A2,A10
.=-(f`|Z).x/(sin.(x/2))^2 by A5,A10,FDIFF_1:def 7
.=-1/2/(sin.(x/2))^2 by A3,A4,A10,FDIFF_1:23
.=-1/(2*(sin.(x/2))^2) by XCMPLX_1:78
.=-1/(1-cos.x) by Lm2;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;