:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Peng Wang and Bo Li
::
:: Received July 9, 2007
:: Copyright (c) 2007-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 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;
equalities SQUARE_1, LIMFUNC1, XCMPLX_0, SIN_COS, VALUED_1;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, NAT_1, FDIFF_1, SQUARE_1,
FDIFF_7, FDIFF_4, RFUNCT_1, PREPOWER, FDIFF_5, FUNCT_1, NEWTON, SIN_COS,
RELAT_1, FDIFF_8, VALUED_1, XXREAL_1;
begin
definition
func sec -> PartFunc of REAL,REAL equals
cos^;
coherence;
func cosec -> PartFunc of REAL,REAL equals
sin^;
coherence;
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 Th1:
cos.x<>0 implies sec is_differentiable_in x & diff(sec, x) = sin. x/(cos.x)^2
proof
A1: cos is_differentiable_in x by SIN_COS:63;
assume
A2: cos.x<>0;
then diff(cos^,x)= - diff(cos,x)/(cos.x)^2 by A1,FDIFF_2:15
.=- (-sin.x)/(cos.x)^2 by SIN_COS:63
.=sin.x/(cos.x)^2;
hence thesis by A2,A1,FDIFF_2:15;
end;
theorem Th2:
sin.x<>0 implies cosec is_differentiable_in x & diff(cosec, x) =
-cos.x/(sin.x)^2
proof
A1: sin is_differentiable_in x by SIN_COS:64;
assume
A2: sin.x<>0;
then diff(sin^,x)= - diff(sin,x)/(sin.x)^2 by A1,FDIFF_2:15
.=-cos.x/(sin.x)^2 by SIN_COS:64;
hence thesis by A2,A1,FDIFF_2:15;
end;
theorem Th3:
(1/x) #Z n = 1/(x #Z n)
proof
(1/x) #Z n = (1/x) |^ n by PREPOWER:36
.=1/x |^ n by PREPOWER:7;
hence thesis by PREPOWER:36;
end;
:: f.x=sec.x
theorem
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
proof
assume Z c= dom sec;
then for x st x in Z holds cos.x<>0 by RFUNCT_1:3;
hence thesis by FDIFF_4:39;
end;
:: f.x=cosec.x
theorem
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
proof
assume Z c= dom cosec;
then for x st x in Z holds sin.x<>0 by RFUNCT_1:3;
hence thesis by FDIFF_4:40;
end;
:: f.x=sec.(a*x+b)
theorem Th6:
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
proof
assume that
A1: Z c= dom (sec*f) and
A2: for x st x in Z holds f.x = a*x+b;
dom(sec*f) c= dom f by RELAT_1:25;
then
A3: Z c= dom f by A1,XBOOLE_1:1;
then
A4: f is_differentiable_on Z by A2,FDIFF_1:23;
A5: for x st x in Z holds cos.(f.x)<>0
proof
let x;
assume x in Z;
then f.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds sec*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then cos.(f.x)<>0 by A5;
then
A8: sec is_differentiable_in f.x by Th1;
f is_differentiable_in x by A4,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: sec*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*f)`|Z).x = a*sin.(a*x+b)/(cos.(a*x+b))^2
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x by A4,FDIFF_1:9;
A12: cos.(f.x)<>0 by A5,A10;
then sec is_differentiable_in f.x by Th1;
then diff(sec*f,x) = diff(sec, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(sin.(f.x)/(cos.(f.x))^2) * diff(f,x) by A12,Th1
.=diff(f,x)*(sin.(f.x)/(cos.(a*x+b))^2) by A2,A10
.=(f`|Z).x*(sin.(f.x)/(cos.(a*x+b))^2) by A4,A10,FDIFF_1:def 7
.=a*(sin.(f.x)/(cos.(a*x+b))^2) by A2,A3,A10,FDIFF_1:23
.=a*(sin.(a*x+b)/(cos.(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=cosec.(a*x+b)
theorem Th7:
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
proof
assume that
A1: Z c= dom (cosec*f) and
A2: for x st x in Z holds f.x = a*x+b;
dom(cosec*f) c= dom f by RELAT_1:25;
then
A3: Z c= dom f by A1,XBOOLE_1:1;
then
A4: f is_differentiable_on Z by A2,FDIFF_1:23;
A5: for x st x in Z holds sin.(f.x)<>0
proof
let x;
assume x in Z;
then f.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds cosec*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then sin.(f.x)<>0 by A5;
then
A8: cosec is_differentiable_in f.x by Th2;
f is_differentiable_in x by A4,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cosec*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*f)`|Z).x = -a*cos.(a*x+b)/(sin.(a*x+b))^2
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x by A4,FDIFF_1:9;
A12: sin.(f.x)<>0 by A5,A10;
then cosec is_differentiable_in f.x by Th2;
then diff(cosec*f,x) = diff(cosec, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(-cos.(f.x)/(sin.(f.x))^2) * diff(f,x) by A12,Th2
.=diff(f,x)*(-cos.(f.x)/(sin.(a*x+b))^2) by A2,A10
.=(f`|Z).x*(-cos.(f.x)/(sin.(a*x+b))^2) by A4,A10,FDIFF_1:def 7
.=a*(-cos.(f.x)/(sin.(a*x+b))^2) by A2,A3,A10,FDIFF_1:23
.=a*(-cos.(a*x+b)/(sin.(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 = sec.(1/x)
theorem
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)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (sec*(f^));
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
dom (sec*(f^)) c= dom (f^) by RELAT_1:25;
then
A4: Z c= dom (f^) by A2,XBOOLE_1:1;
A5: for x st x in Z holds (cos.((f^).x))<>0
proof
let x;
assume x in Z;
then f^.x in dom sec by A2,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds sec*(f^) is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then (cos.((f^).x))<>0 by A5;
then
A8: sec is_differentiable_in (f^).x by Th1;
f^ is_differentiable_in x by A3,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: sec*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((sec*(f^))`|Z).x = -sin.(1/x)/(x^2*(cos.(1/x))^2 )
proof
let x;
assume
A10: x in Z;
then
A11: f^ is_differentiable_in x by A3,FDIFF_1:9;
A12: cos.((f^).x)<>0 by A5,A10;
then sec is_differentiable_in (f^).x by Th1;
then diff(sec*(f^),x) = diff(sec,(f^).x)*diff((f^),x) by A11,FDIFF_2:13
.=sin.((f^).x)/(cos.((f^).x))^2 * diff((f^),x) by A12,Th1
.=diff((f^),x)*(sin.((f^).x)/(cos.((f.x)"))^2) by A4,A10,RFUNCT_1:def 2
.=diff((f^),x)*(sin.((f.x)")/(cos.((f.x)"))^2) by A4,A10,RFUNCT_1:def 2
.=diff((f^),x)*(sin.((f.x)")/(cos.(1*x"))^2) by A10,FUNCT_1:18
.=diff((f^),x)*(sin.(1*x")/(cos.(1*x"))^2) by A10,FUNCT_1:18
.=((f^)`|Z).x*(sin.(1*x")/(cos.(1*x"))^2) by A3,A10,FDIFF_1:def 7
.=(-1/x^2)*(sin.(1*x")/(cos.(1*x"))^2) by A1,A10,FDIFF_5:4
.=(-1)/x^2*(sin.(1/x)/(cos.(1/x))^2)
.=(-1)*sin.(1/x)/(x^2*(cos.(1/x))^2) by XCMPLX_1:76
.=-sin.(1/x)/(x^2*(cos.(1/x))^2);
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A2,A6,FDIFF_1:9;
end;
:: f.x = cosec.(1/x)
theorem
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)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (cosec*(f^));
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
dom (cosec*(f^)) c= dom (f^) by RELAT_1:25;
then
A4: Z c= dom (f^) by A2,XBOOLE_1:1;
A5: for x st x in Z holds (sin.((f^).x))<>0
proof
let x;
assume x in Z;
then f^.x in dom cosec by A2,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds cosec*(f^) is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then (sin.((f^).x))<>0 by A5;
then
A8: cosec is_differentiable_in (f^).x by Th2;
f^ is_differentiable_in x by A3,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cosec*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((cosec*(f^))`|Z).x = cos.(1/x)/(x^2*(sin.(1/x)) ^2)
proof
let x;
assume
A10: x in Z;
then
A11: f^ is_differentiable_in x by A3,FDIFF_1:9;
A12: sin.((f^).x)<>0 by A5,A10;
then cosec is_differentiable_in (f^).x by Th2;
then diff(cosec*(f^),x) = diff(cosec,(f^).x)*diff((f^),x) by A11,FDIFF_2:13
.=(-cos.((f^).x)/(sin.((f^).x))^2) * diff((f^),x) by A12,Th2
.=diff((f^),x)*(-cos.((f^).x)/(sin.((f.x)"))^2) by A4,A10,RFUNCT_1:def 2
.=diff((f^),x)*(-cos.((f.x)")/(sin.((f.x)"))^2) by A4,A10,RFUNCT_1:def 2
.=diff((f^),x)*(-cos.((f.x)")/(sin.(1*x"))^2) by A10,FUNCT_1:18
.=diff((f^),x)*(-cos.(1*x")/(sin.(1*x"))^2) by A10,FUNCT_1:18
.=((f^)`|Z).x*(-cos.(1*x")/(sin.(1*x"))^2) by A3,A10,FDIFF_1:def 7
.=(-1/x^2)*(-cos.(1*x")/(sin.(1*x"))^2) by A1,A10,FDIFF_5:4
.=(-1)/x^2*((-cos.(1/x))/(sin.(1/x))^2)
.=(-1)*(-cos.(1/x))/(x^2*(sin.(1/x))^2) by XCMPLX_1:76
.=cos.(1/x)/(x^2*(sin.(1/x))^2);
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A2,A6,FDIFF_1:9;
end;
:: f.x = sec.(a+b*x+c*x^2)
theorem
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
proof
assume that
A1: Z c= dom (sec*(f1+c(#)f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x = a+b*x;
dom (sec*(f1+c(#)f2)) c= dom (f1+c(#)f2) by RELAT_1:25;
then
A4: Z c= dom (f1+c(#)f2) by A1,XBOOLE_1:1;
then
A5: (f1+c(#)f2) is_differentiable_on Z by A2,A3,FDIFF_4:12;
Z c= dom f1 /\ dom (c(#)f2) by A4,VALUED_1:def 1;
then
A6: Z c= dom (c(#)f2) by XBOOLE_1:18;
A7: for x st x in Z holds cos.((f1+c(#)f2).x)<>0
proof
let x;
assume x in Z;
then (f1+c(#)f2).x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A8: for x st x in Z holds sec*(f1+c(#)f2) is_differentiable_in x
proof
let x;
assume
A9: x in Z;
then cos.((f1+c(#)f2).x)<>0 by A7;
then
A10: sec is_differentiable_in (f1+c(#)f2).x by Th1;
(f1+c(#)f2) is_differentiable_in x by A5,A9,FDIFF_1:9;
hence thesis by A10,FDIFF_2:13;
end;
then
A11: sec*(f1+c(#)f2) is_differentiable_on Z by A1,FDIFF_1:9;
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
proof
let x;
assume
A12: x in Z;
then
A13: ( f1+c(#)f2).x=f1.x+(c(#)f2).x by A4,VALUED_1:def 1
.=f1.x +c*f2.x by A6,A12,VALUED_1:def 5
.=a+b*x +c*(f2.x) by A3,A12
.=a+b*x +c*(x #Z 2) by A2,TAYLOR_1:def 1
.=a+b*x +c*(x |^2) by PREPOWER:36
.=a+b*x+c*x^2 by NEWTON:81;
A14: (f1+c(#)f2) is_differentiable_in x by A5,A12,FDIFF_1:9;
A15: cos.((f1+c(#)f2).x)<>0 by A7,A12;
then sec is_differentiable_in (f1+c(#)f2).x by Th1;
then
diff(sec*(f1+c(#)f2),x) = diff(sec, (f1+c(#)f2).x)*diff((f1+c(#)f2),x
) by A14,FDIFF_2:13
.=(sin.((f1+c(#)f2).x)/(cos.((f1+c(#)f2).x))^2)*diff((f1+c(#)f2),x) by
A15,Th1
.=((f1+c(#)f2)`|Z).x*(sin.(a+b*x+c*x^2)/(cos.(a+b*x+c*x^2))^2) by A5,A12
,A13,FDIFF_1:def 7
.=(b+2*c*x)*(sin.(a+b*x+c*x^2)/(cos.(a+b*x+c*x^2))^2) by A2,A3,A4,A12,
FDIFF_4:12;
hence thesis by A11,A12,FDIFF_1:def 7;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
:: f.x = cosec.(a+b*x+c*x^2)
theorem
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
proof
assume that
A1: Z c= dom (cosec*(f1+c(#)f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x = a+b*x;
dom (cosec*(f1+c(#)f2)) c= dom (f1+c(#)f2) by RELAT_1:25;
then
A4: Z c= dom (f1+c(#)f2) by A1,XBOOLE_1:1;
then
A5: (f1+c(#)f2) is_differentiable_on Z by A2,A3,FDIFF_4:12;
Z c= dom f1 /\ dom (c(#)f2) by A4,VALUED_1:def 1;
then
A6: Z c= dom (c(#)f2) by XBOOLE_1:18;
A7: for x st x in Z holds sin.((f1+c(#)f2).x)<>0
proof
let x;
assume x in Z;
then (f1+c(#)f2).x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A8: for x st x in Z holds cosec*(f1+c(#)f2) is_differentiable_in x
proof
let x;
assume
A9: x in Z;
then sin.((f1+c(#)f2).x)<>0 by A7;
then
A10: cosec is_differentiable_in (f1+c(#)f2).x by Th2;
(f1+c(#)f2) is_differentiable_in x by A5,A9,FDIFF_1:9;
hence thesis by A10,FDIFF_2:13;
end;
then
A11: cosec*(f1+c(#)f2) is_differentiable_on Z by A1,FDIFF_1:9;
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
proof
let x;
assume
A12: x in Z;
then
A13: ( f1+c(#)f2).x=f1.x+(c(#)f2).x by A4,VALUED_1:def 1
.=f1.x +c*f2.x by A6,A12,VALUED_1:def 5
.=a+b*x +c*(f2.x) by A3,A12
.=a+b*x +c*(x #Z 2) by A2,TAYLOR_1:def 1
.=a+b*x +c*(x |^2) by PREPOWER:36
.=a+b*x+c*x^2 by NEWTON:81;
A14: (f1+c(#)f2) is_differentiable_in x by A5,A12,FDIFF_1:9;
A15: sin.((f1+c(#)f2).x)<>0 by A7,A12;
then cosec is_differentiable_in (f1+c(#)f2).x by Th2;
then diff(cosec*(f1+c(#)f2),x) = diff(cosec, (f1+c(#)f2).x)*diff((f1+c(#)
f2),x) by A14,FDIFF_2:13
.=(-cos.((f1+c(#)f2).x)/(sin.((f1+c(#)f2).x))^2)*diff((f1+c(#)f2),x)
by A15,Th2
.=((f1+c(#)f2)`|Z).x*(-cos.(a+b*x+c*x^2)/(sin.(a+b*x+c*x^2))^2) by A5,A12
,A13,FDIFF_1:def 7
.=(b+2*c*x)*(-cos.(a+b*x+c*x^2)/(sin.(a+b*x+c*x^2))^2) by A2,A3,A4,A12,
FDIFF_4:12;
hence thesis by A11,A12,FDIFF_1:def 7;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
:: f.x = sec.(exp_R.x)
theorem
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
proof
assume
A1: Z c= dom (sec*exp_R);
A2: for x st x in Z holds cos.(exp_R.x)<>0
proof
let x;
assume x in Z;
then exp_R.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds sec*exp_R is_differentiable_in x
proof
let x;
assume x in Z;
then cos.(exp_R.x)<>0 by A2;
then exp_R is_differentiable_in x & sec is_differentiable_in exp_R.x by Th1
,SIN_COS:65;
hence thesis by FDIFF_2:13;
end;
then
A4: sec*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*exp_R)`|Z).x = exp_R.x*sin.(exp_R.x)/(cos.(
exp_R.x))^2
proof
let x;
assume
A5: x in Z;
then
A6: cos.(exp_R.x)<>0 by A2;
then exp_R is_differentiable_in x & sec is_differentiable_in exp_R.x by Th1
,SIN_COS:65;
then diff(sec*exp_R,x) = diff(sec, exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=(sin.(exp_R.x)/(cos.(exp_R.x))^2) * diff(exp_R,x) by A6,Th1
.=exp_R.x*(sin.(exp_R.x)/(cos.(exp_R.x))^2) by SIN_COS:65;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = cosec.(exp_R.x)
theorem
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
proof
assume
A1: Z c= dom (cosec*exp_R);
A2: for x st x in Z holds sin.(exp_R.x)<>0
proof
let x;
assume x in Z;
then exp_R.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds cosec*exp_R is_differentiable_in x
proof
let x;
assume x in Z;
then sin.(exp_R.x)<>0 by A2;
then exp_R is_differentiable_in x & cosec is_differentiable_in exp_R.x by
Th2,SIN_COS:65;
hence thesis by FDIFF_2:13;
end;
then
A4: cosec*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*exp_R)`|Z).x = -exp_R.x*cos.(exp_R.x)/(
sin.(exp_R.x))^2
proof
let x;
assume
A5: x in Z;
then
A6: sin.(exp_R.x)<>0 by A2;
then exp_R is_differentiable_in x & cosec is_differentiable_in exp_R.x by
Th2,SIN_COS:65;
then diff(cosec*exp_R,x) = diff(cosec, exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=(-cos.(exp_R.x)/(sin.(exp_R.x))^2) * diff(exp_R,x) by A6,Th2
.=exp_R.x*(-cos.(exp_R.x)/(sin.(exp_R.x))^2) by SIN_COS:65;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
Lm1: right_open_halfline 0 = {g where g is Real: 0<g}
by XXREAL_1:230;
:: f.x = sec.(ln.x)
theorem
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)
proof
assume
A1: Z c= dom (sec*ln);
dom (sec*ln) c= dom ln by RELAT_1:25;
then
A2: Z c= dom ln by A1,XBOOLE_1:1;
A3: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A2,TAYLOR_1:18;
then ex g being Real st x=g & 0<g by Lm1;
hence thesis;
end;
A4: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A3;
then x in right_open_halfline(0) by Lm1;
hence thesis by TAYLOR_1:18;
end;
A5: for x st x in Z holds cos.(ln.x)<>0
proof
let x;
assume x in Z;
then ln.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds sec*ln is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then cos.(ln.x)<>0 by A5;
then
A8: sec is_differentiable_in ln.x by Th1;
ln is_differentiable_in x by A3,A7,TAYLOR_1:18;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: sec*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*ln)`|Z).x = sin.(ln.x)/(x*(cos.(ln.x))^2)
proof
let x;
assume
A10: x in Z;
then
A11: ln is_differentiable_in x by A3,TAYLOR_1:18;
A12: cos.(ln.x)<>0 by A5,A10;
then sec is_differentiable_in ln.x by Th1;
then diff(sec*ln,x) = diff(sec,ln.x)*diff(ln,x) by A11,FDIFF_2:13
.=(sin.(ln.x)/(cos.(ln.x))^2) * diff(ln,x) by A12,Th1
.=(1/x)*(sin.(ln.x)/(cos.(ln.x))^2) by A4,A10
.=(1*sin.(ln.x))/(x*(cos.(ln.x))^2) by XCMPLX_1:76;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = cosec.(ln.x)
theorem
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)
proof
assume
A1: Z c= dom (cosec*ln);
dom (cosec*ln) c= dom ln by RELAT_1:25;
then
A2: Z c= dom ln by A1,XBOOLE_1:1;
A3: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A2,TAYLOR_1:18;
then ex g being Real st x=g & 0<g by Lm1;
hence thesis;
end;
A4: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A3;
then x in right_open_halfline(0) by Lm1;
hence thesis by TAYLOR_1:18;
end;
A5: for x st x in Z holds sin.(ln.x)<>0
proof
let x;
assume x in Z;
then ln.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6: for x st x in Z holds cosec*ln is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then sin.(ln.x)<>0 by A5;
then
A8: cosec is_differentiable_in ln.x by Th2;
ln is_differentiable_in x by A3,A7,TAYLOR_1:18;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cosec*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*ln)`|Z).x = -cos.(ln.x)/(x*(sin.(ln.x))^2 )
proof
let x;
assume
A10: x in Z;
then
A11: ln is_differentiable_in x by A3,TAYLOR_1:18;
A12: sin.(ln.x)<>0 by A5,A10;
then cosec is_differentiable_in ln.x by Th2;
then diff(cosec*ln,x) = diff(cosec,ln.x)*diff(ln,x) by A11,FDIFF_2:13
.=(-cos.(ln.x)/(sin.(ln.x))^2) * diff(ln,x) by A12,Th2
.=(1/x)*((-cos.(ln.x))/(sin.(ln.x))^2) by A4,A10
.=(1*(-cos.(ln.x)))/(x*(sin.(ln.x))^2) by XCMPLX_1:76;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = exp_R.(sec.x)
theorem
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
proof
assume
A1: Z c= dom (exp_R*sec);
A2: for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds exp_R*sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A2;
then
A4: sec is_differentiable_in x by Th1;
exp_R is_differentiable_in sec.x by SIN_COS:65;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: exp_R*sec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*sec)`|Z).x = exp_R.(sec.x)*sin.x/(cos.x) ^2
proof
let x;
A6: exp_R is_differentiable_in sec.x by SIN_COS:65;
assume
A7: x in Z;
then
A8: cos.x<>0 by A2;
then sec is_differentiable_in x by Th1;
then diff(exp_R*sec,x) = diff(exp_R,sec.x)*diff(sec,x) by A6,FDIFF_2:13
.=diff(exp_R,sec.x)*(sin.x/(cos.x)^2) by A8,Th1
.=exp_R.(sec.x)*(sin.x/(cos.x)^2) by SIN_COS:65;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = exp_R.(cosec.x)
theorem
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
proof
assume
A1: Z c= dom (exp_R*cosec);
A2: for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds exp_R*cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A2;
then
A4: cosec is_differentiable_in x by Th2;
exp_R is_differentiable_in cosec.x by SIN_COS:65;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: exp_R*cosec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*cosec)`|Z).x = -exp_R.(cosec.x)*cos.x/(
sin.x)^2
proof
let x;
A6: exp_R is_differentiable_in cosec.x by SIN_COS:65;
assume
A7: x in Z;
then
A8: sin.x<>0 by A2;
then cosec is_differentiable_in x by Th2;
then diff(exp_R*cosec,x) = diff(exp_R,cosec.x)*diff(cosec,x) by A6,
FDIFF_2:13
.=diff(exp_R,cosec.x)*(-cos.x/(sin.x)^2) by A8,Th2
.=exp_R.(cosec.x)*(-cos.x/(sin.x)^2) by SIN_COS:65;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = ln.(sec.x)
theorem
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
proof
assume
A1: Z c= dom (ln*sec);
A2: for x st x in Z holds sec.x>0
proof
let x;
assume x in Z;
then sec.x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
then ex g being Real st sec.x=g & 0<g by Lm1;
hence thesis;
end;
dom (ln*sec) c= dom sec by RELAT_1:25;
then
A3: Z c= dom sec by A1,XBOOLE_1:1;
A4: for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A5: for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4;
hence thesis by Th1;
end;
A6: for x st x in Z holds ln*sec is_differentiable_in x
proof
let x;
assume x in Z;
then sec is_differentiable_in x & sec.x>0 by A2,A5;
hence thesis by TAYLOR_1:20;
end;
then
A7: ln*sec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*sec)`|Z).x = sin.x/cos.x
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A4;
sec is_differentiable_in x & sec.x>0 by A2,A5,A8;
then diff(ln*sec,x) =diff(sec,x)/(sec.x) by TAYLOR_1:20
.=(sin.x/(cos.x)^2)/(sec.x) by A9,Th1
.=(sin.x/(cos.x)^2)/(cos.x)" by A3,A8,RFUNCT_1:def 2
.=(sin.x*cos.x)/(cos.x*cos.x)
.=sin.x/cos.x by A4,A8,XCMPLX_1:91;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = ln.(cosec.x)
theorem
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
proof
assume
A1: Z c= dom (ln*cosec);
A2: for x st x in Z holds cosec.x>0
proof
let x;
assume x in Z;
then cosec.x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
then ex g being Real st cosec.x=g & 0<g by Lm1;
hence thesis;
end;
dom (ln*cosec) c= dom cosec by RELAT_1:25;
then
A3: Z c= dom cosec by A1,XBOOLE_1:1;
A4: for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A5: for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4;
hence thesis by Th2;
end;
A6: for x st x in Z holds ln*cosec is_differentiable_in x
proof
let x;
assume x in Z;
then cosec is_differentiable_in x & cosec.x>0 by A2,A5;
hence thesis by TAYLOR_1:20;
end;
then
A7: ln*cosec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*cosec)`|Z).x = -cos.x/sin.x
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A4;
cosec is_differentiable_in x & cosec.x>0 by A2,A5,A8;
then diff(ln*cosec,x) =diff(cosec,x)/(cosec.x) by TAYLOR_1:20
.=(-cos.x/(sin.x)^2)/(cosec.x) by A9,Th2
.=(-cos.x/(sin.x)^2)/(sin.x)" by A3,A8,RFUNCT_1:def 2
.=((-cos.x)*sin.x)/(sin.x*sin.x)
.=(-cos.x)/sin.x by A4,A8,XCMPLX_1:91;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x=(sec.x) #Z n
theorem
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)
proof
assume that
A1: Z c= dom (( #Z n)*sec) and
A2: 1<=n;
dom (( #Z n)*sec) c= dom sec by RELAT_1:25;
then
A3: Z c= dom sec by A1,XBOOLE_1:1;
A4: for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A5: for x st x in Z holds ( #Z n)*sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4;
then sec is_differentiable_in x by Th1;
hence thesis by TAYLOR_1:3;
end;
then
A6: ( #Z n)*sec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*sec)`|Z).x = n*sin.x/(cos.x) #Z (n+1)
proof
set m = n-1;
let x;
A7: ex m being Nat st n = m + 1 by A2,NAT_1:6;
assume
A8: x in Z;
then
A9: cos.x<>0 by A4;
then
A10: sec is_differentiable_in x by Th1;
((( #Z n)*sec)`|Z).x=diff(( #Z n)*sec,x) by A6,A8,FDIFF_1:def 7
.=n*(sec.x) #Z (n-1) * diff(sec,x) by A10,TAYLOR_1:3
.=n*(sec.x) #Z (n-1) *(sin.x/(cos.x)^2) by A9,Th1
.=n*(1/cos.x) #Z (n-1) *(sin.x/(cos.x)^2) by A3,A8,RFUNCT_1:def 2
.=n*(1/(cos.x) #Z m) *(sin.x/(cos.x)^2) by A7,Th3
.=(n/(cos.x) #Z (n-1))*(sin.x/(cos.x)^2)
.=(n*(sin.x))/((cos.x) #Z (n-1)*(cos.x)^2) by XCMPLX_1:76
.=(n*(sin.x))/((cos.x) #Z (n-1)*(cos.x) #Z 2) by FDIFF_7:1
.=(n*(sin.x))/((cos.x) #Z (n-1+2)) by A4,A8,PREPOWER:44
.=n*(sin.x)/(cos.x) #Z (n+1);
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: f.x=(cosec.x) #Z n
theorem
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)
proof
assume that
A1: Z c= dom (( #Z n)*cosec) and
A2: 1<=n;
dom (( #Z n)*cosec) c= dom cosec by RELAT_1:25;
then
A3: Z c= dom cosec by A1,XBOOLE_1:1;
A4: for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A5: for x st x in Z holds ( #Z n)*cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4;
then cosec is_differentiable_in x by Th2;
hence thesis by TAYLOR_1:3;
end;
then
A6: ( #Z n)*cosec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*cosec)`|Z).x = -n*cos.x/(sin.x) #Z (n+1 )
proof
set m = n-1;
let x;
A7: ex m being Nat st n = m + 1 by A2,NAT_1:6;
assume
A8: x in Z;
then
A9: sin.x<>0 by A4;
then
A10: cosec is_differentiable_in x by Th2;
((( #Z n)*cosec)`|Z).x=diff(( #Z n)*cosec,x) by A6,A8,FDIFF_1:def 7
.=n*(cosec.x) #Z (n-1) * diff(cosec,x) by A10,TAYLOR_1:3
.=n*(cosec.x) #Z (n-1) *(-cos.x/(sin.x)^2) by A9,Th2
.=n*(1/sin.x) #Z (n-1) *(-cos.x/(sin.x)^2) by A3,A8,RFUNCT_1:def 2
.=n*(1/(sin.x) #Z m) *(-cos.x/(sin.x)^2) by A7,Th3
.=(n/(sin.x) #Z (n-1))*((-cos.x)/(sin.x)^2)
.=(n*(-cos.x))/((sin.x) #Z (n-1)*(sin.x)^2) by XCMPLX_1:76
.=(n*(-cos.x))/((sin.x) #Z (n-1)*(sin.x) #Z 2) by FDIFF_7:1
.=(n*(-cos.x))/((sin.x) #Z (n-1+2)) by A4,A8,PREPOWER:44
.=n*(-cos.x)/(sin.x) #Z (n+1);
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: f.x = sec.x-x
theorem
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
proof
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom (sec-id Z);
then
A3: Z c= dom sec /\ dom (id Z) by VALUED_1:12;
then
A4: Z c= dom sec by XBOOLE_1:18;
A5: Z c= dom (id Z) by A3,XBOOLE_1:18;
then
A6: id Z is_differentiable_on Z by A1,FDIFF_1:23;
for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4,RFUNCT_1:3;
hence thesis by Th1;
end;
then
A7: sec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((sec-id Z)`|Z).x=(sin.x-(cos.x)^2)/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A4,RFUNCT_1:3;
then
A10: (cos.x)^2 >0 by SQUARE_1:12;
((sec-id Z)`|Z).x= diff(sec,x) - diff(id Z,x) by A2,A6,A7,A8,FDIFF_1:19
.=sin.x/(cos.x)^2-diff(id Z,x) by A9,Th1
.=sin.x/(cos.x)^2-((id Z)`|Z).x by A6,A8,FDIFF_1:def 7
.=sin.x/(cos.x)^2-1 by A5,A1,A8,FDIFF_1:23
.=sin.x/(cos.x)^2-(cos.x)^2/(cos.x)^2 by A10,XCMPLX_1:60
.=(sin.x-(cos.x)^2)/(cos.x)^2;
hence thesis;
end;
hence thesis by A2,A6,A7,FDIFF_1:19;
end;
:: f.x = -cosec.x-x
theorem
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
proof
set f = -cosec;
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom (-cosec-id Z);
then
A3: Z c= dom (-cosec) /\ dom (id Z) by VALUED_1:12;
then
A4: Z c= dom (-cosec) by XBOOLE_1:18;
then
A5: Z c= dom cosec by VALUED_1:8;
for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th2;
end;
then
A6: cosec is_differentiable_on Z by A5,FDIFF_1:9;
then
A7: (-1)(#)cosec is_differentiable_on Z by A4,FDIFF_1:20;
A8: Z c= dom (id Z) by A3,XBOOLE_1:18;
then
A9: id Z is_differentiable_on Z by A1,FDIFF_1:23;
for x st x in Z holds ((-cosec-id Z)`|Z).x=(cos.x-(sin.x)^2)/(sin.x)^2
proof
let x;
assume
A10: x in Z;
then
A11: sin.x<>0 by A5,RFUNCT_1:3;
then
A12: (sin.x)^2 >0 by SQUARE_1:12;
((f-id Z)`|Z).x=diff(f,x) - diff(id Z,x) by A2,A9,A7,A10,FDIFF_1:19
.=(((-1)(#)cosec)`|Z).x-diff(id Z,x) by A7,A10,FDIFF_1:def 7
.=(-1)*diff(cosec,x)-diff(id Z,x) by A4,A6,A10,FDIFF_1:20
.=(-1)*(-cos.x/(sin.x)^2)-diff(id Z,x) by A11,Th2
.=cos.x/(sin.x)^2-((id Z)`|Z).x by A9,A10,FDIFF_1:def 7
.=cos.x/(sin.x)^2-1 by A8,A1,A10,FDIFF_1:23
.=cos.x/(sin.x)^2-(sin.x)^2/(sin.x)^2 by A12,XCMPLX_1:60
.=(cos.x-(sin.x)^2)/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A9,A7,FDIFF_1:19;
end;
:: f.x = exp_R.x*sec.x
theorem
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
proof
A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS:65;
assume
A2: Z c= dom (exp_R(#)sec);
then
A3: Z c= dom (exp_R) /\ dom sec by VALUED_1:def 4;
then
A4: Z c= dom sec by XBOOLE_1:18;
Z c= dom (exp_R) by A3,XBOOLE_1:18;
then
A5: exp_R is_differentiable_on Z by A1,FDIFF_1:9;
A6: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A7: sec is_differentiable_on Z by A4,FDIFF_1:9;
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
proof
let x;
assume
A8: x in Z;
then
((exp_R(#)sec)`|Z).x = (sec.x)*diff(exp_R,x)+(exp_R.x)*diff(sec,x) by A2,A5
,A7,FDIFF_1:21
.=(sec.x)*exp_R.x+(exp_R.x)*diff(sec,x) by SIN_COS:65
.=(sec.x)*exp_R.x+(exp_R.x)*(sin.x/(cos.x)^2) by A6,A8
.=exp_R.x/cos.x+exp_R.x*sin.x/(cos.x)^2 by A4,A8,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A2,A5,A7,FDIFF_1:21;
end;
:: f.x = exp_R.x*cosec.x
theorem
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
proof
A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS:65;
assume
A2: Z c= dom (exp_R(#)cosec);
then
A3: Z c= dom (exp_R) /\ dom cosec by VALUED_1:def 4;
then
A4: Z c= dom cosec by XBOOLE_1:18;
Z c= dom (exp_R) by A3,XBOOLE_1:18;
then
A5: exp_R is_differentiable_on Z by A1,FDIFF_1:9;
A6: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-cos
.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A7: cosec is_differentiable_on Z by A4,FDIFF_1:9;
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
proof
let x;
assume
A8: x in Z;
then ((exp_R(#)cosec)`|Z).x = (cosec.x)*diff(exp_R,x)+(exp_R.x)*diff(
cosec,x) by A2,A5,A7,FDIFF_1:21
.=(cosec.x)*exp_R.x+(exp_R.x)*diff(cosec,x) by SIN_COS:65
.=(cosec.x)*exp_R.x+(exp_R.x)*(-cos.x/(sin.x)^2) by A6,A8
.=exp_R.x/sin.x+(exp_R.x*(-cos.x))/(sin.x)^2 by A4,A8,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A2,A5,A7,FDIFF_1:21;
end;
:: f.x = (1/a)*sec.(a*x)-x
theorem
(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
proof
assume that
A1: Z c= dom ((1/a)(#)(sec*f)-id Z) and
A2: for x st x in Z holds f.x=a*x & a<>0;
A3: Z c= dom ((1/a)(#)(sec*f)) /\ dom (id Z) by A1,VALUED_1:12;
then
A4: Z c= dom ((1/a)(#)(sec*f)) by XBOOLE_1:18;
then
A5: Z c= dom (sec*f) by VALUED_1:def 5;
A6: for x st x in Z holds f.x=a*x+0 by A2;
then
A7: sec*f is_differentiable_on Z by A5,Th6;
then
A8: (1/a)(#)(sec*f) is_differentiable_on Z by A4,FDIFF_1:20;
set g = (1/a)(#)(sec*f);
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom (id Z) by A3,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds cos.(f.x)<>0
proof
let x;
assume x in Z;
then f.x in dom sec by A5,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
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
proof
let x;
assume
A13: x in Z;
then
A14: f.x=a*x+0 by A2;
cos.(f.x)<>0 by A12,A13;
then
A15: (cos.(a*x))^2>0 by A14,SQUARE_1:12;
((g-id Z)`|Z).x=diff(g,x)-diff(id Z,x) by A1,A8,A11,A13,FDIFF_1:19
.=(g`|Z).x-diff(id Z,x) by A8,A13,FDIFF_1:def 7
.=(1/a)*diff(sec*f,x)-diff(id Z,x) by A4,A7,A13,FDIFF_1:20
.=(1/a)*((sec*f)`|Z).x-diff(id Z,x) by A7,A13,FDIFF_1:def 7
.=(1/a)*((sec*f)`|Z).x-((id Z)`|Z).x by A11,A13,FDIFF_1:def 7
.=(1/a)*(a*sin.(a*x)/(cos.(a*x))^2)-((id Z)`|Z).x by A5,A6,A13,A14,Th6
.=(1/a)*((a*sin.(a*x))/(cos.(a*x))^2) -1 by A10,A9,A13,FDIFF_1:23
.=(1*(a*sin.(a*x)))/(a*(cos.(a*x))^2) -1 by XCMPLX_1:76
.=sin.(a*x)/(cos.(a*x))^2 -1 by A2,A13,XCMPLX_1:91
.=sin.(a*x)/(cos.(a*x))^2-(cos.(a*x))^2/(cos.(a*x))^2 by A15,XCMPLX_1:60
.=(sin.(a*x)-(cos.(a*x))^2)/(cos.(a*x))^2;
hence thesis;
end;
hence thesis by A1,A8,A11,FDIFF_1:19;
end;
:: f.x = (-1/a)*cosec.(a*x)-x
theorem
(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
proof
assume that
A1: Z c= dom ((-1/a)(#)(cosec*f)-id Z) and
A2: for x st x in Z holds f.x=a*x & a<>0;
A3: Z c= dom ((-1/a)(#)(cosec*f)) /\ dom (id Z) by A1,VALUED_1:12;
then
A4: Z c= dom ((-1/a)(#)(cosec*f)) by XBOOLE_1:18;
then
A5: Z c= dom (cosec*f) by VALUED_1:def 5;
A6: for x st x in Z holds f.x=a*x+0 by A2;
then
A7: cosec*f is_differentiable_on Z by A5,Th7;
then
A8: (-1/a)(#)(cosec*f) is_differentiable_on Z by A4,FDIFF_1:20;
set g = (-1/a)(#)(cosec*f);
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom (id Z) by A3,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds sin.(f.x)<>0
proof
let x;
assume x in Z;
then f.x in dom cosec by A5,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
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
proof
let x;
assume
A13: x in Z;
then
A14: f.x=a*x+0 by A2;
sin.(f.x)<>0 by A12,A13;
then
A15: (sin.(a*x))^2>0 by A14,SQUARE_1:12;
((g-id Z)`|Z).x=diff(g,x)-diff(id Z,x) by A1,A8,A11,A13,FDIFF_1:19
.=(g`|Z).x-diff(id Z,x) by A8,A13,FDIFF_1:def 7
.=(-1/a)*diff(cosec*f,x)-diff(id Z,x) by A4,A7,A13,FDIFF_1:20
.=(-1/a)*((cosec*f)`|Z).x-diff(id Z,x) by A7,A13,FDIFF_1:def 7
.=(-1/a)*((cosec*f)`|Z).x-((id Z)`|Z).x by A11,A13,FDIFF_1:def 7
.=(-1/a)*(-a*cos.(a*x)/(sin.(a*x))^2)-((id Z)`|Z).x by A5,A6,A13,A14,Th7
.=((-1)/a)*((a*(-cos.(a*x)))/(sin.(a*x))^2) -1 by A10,A9,A13,FDIFF_1:23
.=((-1)*(a*(-cos.(a*x))))/(a*(sin.(a*x))^2) -1 by XCMPLX_1:76
.=(cos.(a*x)*a)/((sin.(a*x))^2*a) -1
.=cos.(a*x)/(sin.(a*x))^2 -1 by A2,A13,XCMPLX_1:91
.=cos.(a*x)/(sin.(a*x))^2-(sin.(a*x))^2/(sin.(a*x))^2 by A15,XCMPLX_1:60
.=(cos.(a*x)-(sin.(a*x))^2)/(sin.(a*x))^2;
hence thesis;
end;
hence thesis by A1,A8,A11,FDIFF_1:19;
end;
:: f.x = (a*x+b)*sec.x
theorem
(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
proof
assume that
A1: Z c= dom (f(#)sec) and
A2: for x st x in Z holds f.x=a*x+b;
A3: Z c= dom f /\ dom sec by A1,VALUED_1:def 4;
then
A4: Z c= dom sec by XBOOLE_1:18;
A5: Z c= dom f by A3,XBOOLE_1:18;
then
A6: f is_differentiable_on Z by A2,FDIFF_1:23;
A7: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A8: sec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((f(#)sec)`|Z).x = a/cos.x+(a*x+b)*sin.x/(cos.x) ^2
proof
let x;
assume
A9: x in Z;
then ((f(#)sec)`|Z).x= (sec.x)*diff(f,x)+(f.x)*diff(sec,x) by A1,A6,A8,
FDIFF_1:21
.=(sec.x)*((f`|Z).x)+(f.x)*diff(sec,x) by A6,A9,FDIFF_1:def 7
.=(sec.x)*a+(f.x)*diff(sec,x) by A2,A5,A9,FDIFF_1:23
.=(sec.x)*a+(a*x+b)*diff(sec,x) by A2,A9
.=(sec.x)*a+(a*x+b)*(sin.x/(cos.x)^2) by A7,A9
.=a/cos.x+(a*x+b)*sin.x/(cos.x)^2 by A4,A9,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A6,A8,FDIFF_1:21;
end;
:: f.x = (a*x+b)*cosec.x
theorem
(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
proof
assume that
A1: Z c= dom (f(#)cosec) and
A2: for x st x in Z holds f.x=a*x+b;
A3: Z c= dom f /\ dom cosec by A1,VALUED_1:def 4;
then
A4: Z c= dom cosec by XBOOLE_1:18;
A5: Z c= dom f by A3,XBOOLE_1:18;
then
A6: f is_differentiable_on Z by A2,FDIFF_1:23;
A7: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-cos
.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A8: cosec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((f(#)cosec)`|Z).x = a/sin.x-(a*x+b)*cos.x/(sin.x )^2
proof
let x;
assume
A9: x in Z;
then
((f(#)cosec)`|Z).x= (cosec.x)*diff(f,x)+(f.x)*diff(cosec,x) by A1,A6,A8,
FDIFF_1:21
.=(cosec.x)*((f`|Z).x)+(f.x)*diff(cosec,x) by A6,A9,FDIFF_1:def 7
.=(cosec.x)*a+(f.x)*diff(cosec,x) by A2,A5,A9,FDIFF_1:23
.=(cosec.x)*a+(a*x+b)*diff(cosec,x) by A2,A9
.=(cosec.x)*a+(a*x+b)*(-cos.x/(sin.x)^2) by A7,A9
.=a/sin.x-(a*x+b)*cos.x/(sin.x)^2 by A4,A9,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A6,A8,FDIFF_1:21;
end;
:: f.x = ln.x*sec.x
theorem
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
proof
assume
A1: Z c= dom (ln(#)sec);
then
A2: Z c= dom ln /\ dom sec by VALUED_1:def 4;
then
A3: Z c= dom sec by XBOOLE_1:18;
A4: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A3,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A5: sec is_differentiable_on Z by A3,FDIFF_1:9;
A6: Z c= dom ln by A2,XBOOLE_1:18;
A7: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A6,TAYLOR_1:18;
then ex g being Real st x=g & 0<g by Lm1;
hence thesis;
end;
then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
then
A8: ln is_differentiable_on Z by A6,FDIFF_1:9;
A9: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A7;
then x in right_open_halfline(0) by Lm1;
hence thesis by TAYLOR_1:18;
end;
for x st x in Z holds ((ln(#)sec)`|Z).x = 1/cos.x/x+ln.x*sin.x/(cos.x) ^2
proof
let x;
assume
A10: x in Z;
then ((ln(#)sec)`|Z).x= (sec.x)*diff(ln,x)+(ln.x)*diff(sec,x) by A1,A8,A5,
FDIFF_1:21
.=(sec.x)*(1/x)+(ln.x)*diff(sec,x) by A9,A10
.=(sec.x)*(1/x)+(ln.x)*(sin.x/(cos.x)^2) by A4,A10
.=1/cos.x/x+ln.x*sin.x/(cos.x)^2 by A3,A10,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A8,A5,FDIFF_1:21;
end;
:: f.x = ln.x*cosec.x
theorem
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
proof
assume
A1: Z c= dom (ln(#)cosec);
then
A2: Z c= dom ln /\ dom cosec by VALUED_1:def 4;
then
A3: Z c= dom cosec by XBOOLE_1:18;
A4: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-
cos.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A3,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A5: cosec is_differentiable_on Z by A3,FDIFF_1:9;
A6: Z c= dom ln by A2,XBOOLE_1:18;
A7: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A6,TAYLOR_1:18;
then ex g being Real st x=g & 0<g by Lm1;
hence thesis;
end;
then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
then
A8: ln is_differentiable_on Z by A6,FDIFF_1:9;
A9: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A7;
then x in right_open_halfline(0) by Lm1;
hence thesis by TAYLOR_1:18;
end;
for x st x in Z holds ((ln(#)cosec)`|Z).x = 1/sin.x/x-ln.x*cos.x/(sin.x )^2
proof
let x;
assume
A10: x in Z;
then
((ln(#)cosec)`|Z).x= (cosec.x)*diff(ln,x)+(ln.x)*diff(cosec,x) by A1,A8,A5,
FDIFF_1:21
.=(cosec.x)*(1/x)+(ln.x)*diff(cosec,x) by A9,A10
.=(cosec.x)*(1/x)+(ln.x)*(-cos.x/(sin.x)^2) by A4,A10
.=1/sin.x/x-ln.x*cos.x/(sin.x)^2 by A3,A10,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A8,A5,FDIFF_1:21;
end;
:: f.x = 1/x*sec.x
theorem
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
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)sec);
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A4: Z c= dom (f^) /\ dom sec by A2,VALUED_1:def 4;
then
A5: Z c= dom sec by XBOOLE_1:18;
A6: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A7: sec is_differentiable_on Z by A5,FDIFF_1:9;
A8: Z c= dom (f^) by A4,XBOOLE_1:18;
for x st x in Z holds ((f^(#)sec)`|Z).x =-1/cos.x/x^2+sin.x/x/(cos.x)^2
proof
let x;
assume
A9: x in Z;
then ((f^(#)sec)`|Z).x= (sec.x)*diff(f^,x)+((f^).x)*diff(sec,x) by A2,A3,A7
,FDIFF_1:21
.=(sec.x)*((f^)`|Z).x+((f^).x)*diff(sec,x) by A3,A9,FDIFF_1:def 7
.=(sec.x)*(-1/x^2)+((f^).x)*diff(sec,x) by A1,A9,FDIFF_5:4
.=-(sec.x)*(1/x^2)+((f^).x)*(sin.x/(cos.x)^2) by A6,A9
.=-(cos.x)"*(1/x^2)+((f^).x)*(sin.x/(cos.x)^2) by A5,A9,RFUNCT_1:def 2
.=-1/cos.x/x^2+(f.x)"*(sin.x/(cos.x)^2) by A8,A9,RFUNCT_1:def 2
.=-1/cos.x/x^2+(1/x)*(sin.x/(cos.x)^2) by A9,FUNCT_1:18
.=-1/cos.x/x^2+sin.x/x/(cos.x)^2;
hence thesis;
end;
hence thesis by A2,A3,A7,FDIFF_1:21;
end;
:: f.x = 1/x*cosec.x
theorem
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
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)cosec);
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A4: Z c= dom (f^) /\ dom cosec by A2,VALUED_1:def 4;
then
A5: Z c= dom cosec by XBOOLE_1:18;
A6: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-cos
.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A7: cosec is_differentiable_on Z by A5,FDIFF_1:9;
A8: Z c= dom (f^) by A4,XBOOLE_1:18;
for x st x in Z holds ((f^(#)cosec)`|Z).x = -1/sin.x/x^2-cos.x/x/(sin.x )^2
proof
let x;
assume
A9: x in Z;
then ((f^(#)cosec)`|Z).x= (cosec.x)*diff(f^,x)+((f^).x)*diff(cosec,x) by A2
,A3,A7,FDIFF_1:21
.=(cosec.x)*((f^)`|Z).x+((f^).x)*diff(cosec,x) by A3,A9,FDIFF_1:def 7
.=(cosec.x)*(-1/x^2)+((f^).x)*diff(cosec,x) by A1,A9,FDIFF_5:4
.=-(cosec.x)*(1/x^2)+((f^).x)*(-cos.x/(sin.x)^2) by A6,A9
.=-(sin.x)"*(1/x^2)+((f^).x)*((-cos.x)/(sin.x)^2) by A5,A9,RFUNCT_1:def 2
.=-1/sin.x/x^2+(f.x)"*((-cos.x)/(sin.x)^2) by A8,A9,RFUNCT_1:def 2
.=-1/sin.x/x^2+(1/x)*((-cos.x)/(sin.x)^2) by A9,FUNCT_1:18
.=-1/sin.x/x^2+(-cos.x)/x/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A3,A7,FDIFF_1:21;
end;
:: f.x = sec.(sin.x)
theorem
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
proof
assume
A1: Z c= dom (sec*sin);
A2: for x st x in Z holds cos.(sin.x)<>0
proof
let x;
assume x in Z;
then sin.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds sec*sin is_differentiable_in x
proof
let x;
assume x in Z;
then cos.(sin.x)<>0 by A2;
then sin is_differentiable_in x & sec is_differentiable_in sin.x by Th1,
SIN_COS:64;
hence thesis by FDIFF_2:13;
end;
then
A4: sec*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*sin)`|Z).x = cos.x*sin.(sin.x)/(cos.(sin.x) )^2
proof
let x;
assume
A5: x in Z;
then
A6: cos.(sin.x)<>0 by A2;
then sin is_differentiable_in x & sec is_differentiable_in sin.x by Th1,
SIN_COS:64;
then diff(sec*sin,x) = diff(sec, sin.x)*diff(sin,x) by FDIFF_2:13
.=(sin.(sin.x)/(cos.(sin.x))^2) * diff(sin,x) by A6,Th1
.=cos.x*(sin.(sin.x)/(cos.(sin.x))^2) by SIN_COS:64;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = sec.(cos.x)
theorem
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
proof
assume
A1: Z c= dom (sec*cos);
A2: for x st x in Z holds cos.(cos.x)<>0
proof
let x;
assume x in Z;
then cos.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds sec*cos is_differentiable_in x
proof
let x;
assume x in Z;
then cos.(cos.x)<>0 by A2;
then cos is_differentiable_in x & sec is_differentiable_in cos.x by Th1,
SIN_COS:63;
hence thesis by FDIFF_2:13;
end;
then
A4: sec*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*cos)`|Z).x = -sin.x*sin.(cos.x)/(cos.(cos.x ))^2
proof
let x;
assume
A5: x in Z;
then
A6: cos.(cos.x)<>0 by A2;
then cos is_differentiable_in x & sec is_differentiable_in cos.x by Th1,
SIN_COS:63;
then diff(sec*cos,x) = diff(sec, cos.x)*diff(cos,x) by FDIFF_2:13
.=(sin.(cos.x)/(cos.(cos.x))^2) * diff(cos,x) by A6,Th1
.=(-sin.x)*(sin.(cos.x)/(cos.(cos.x))^2) by SIN_COS:63;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = cosec.(sin.x)
theorem
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
proof
assume
A1: Z c= dom (cosec*sin);
A2: for x st x in Z holds sin.(sin.x)<>0
proof
let x;
assume x in Z;
then sin.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds cosec*sin is_differentiable_in x
proof
let x;
assume x in Z;
then sin.(sin.x)<>0 by A2;
then sin is_differentiable_in x & cosec is_differentiable_in sin.x by Th2,
SIN_COS:64;
hence thesis by FDIFF_2:13;
end;
then
A4: cosec*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*sin)`|Z).x = -cos.x*cos.(sin.x)/(sin.(sin
.x))^2
proof
let x;
assume
A5: x in Z;
then
A6: sin.(sin.x)<>0 by A2;
then sin is_differentiable_in x & cosec is_differentiable_in sin.x by Th2,
SIN_COS:64;
then diff(cosec*sin,x) = diff(cosec, sin.x)*diff(sin,x) by FDIFF_2:13
.=(-cos.(sin.x)/(sin.(sin.x))^2) * diff(sin,x) by A6,Th2
.=cos.x*(-cos.(sin.x)/(sin.(sin.x))^2) by SIN_COS:64;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = cosec.(cos.x)
theorem
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
proof
assume
A1: Z c= dom (cosec*cos);
A2: for x st x in Z holds sin.(cos.x)<>0
proof
let x;
assume x in Z;
then cos.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A3: for x st x in Z holds cosec*cos is_differentiable_in x
proof
let x;
assume x in Z;
then sin.(cos.x)<>0 by A2;
then cos is_differentiable_in x & cosec is_differentiable_in cos.x by Th2,
SIN_COS:63;
hence thesis by FDIFF_2:13;
end;
then
A4: cosec*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*cos)`|Z).x = sin.x*cos.(cos.x)/(sin.(cos. x))^2
proof
let x;
assume
A5: x in Z;
then
A6: sin.(cos.x)<>0 by A2;
then cos is_differentiable_in x & cosec is_differentiable_in cos.x by Th2,
SIN_COS:63;
then diff(cosec*cos,x) = diff(cosec, cos.x)*diff(cos,x) by FDIFF_2:13
.=(-cos.(cos.x)/(sin.(cos.x))^2) * diff(cos,x) by A6,Th2
.=(-sin.x)*(-cos.(cos.x)/(sin.(cos.x))^2) by SIN_COS:63;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = sec.(tan.x)
theorem
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
proof
assume
A1: Z c= dom (sec*tan);
A2: for x st x in Z holds cos.(tan.x)<>0
proof
let x;
assume x in Z;
then tan.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
dom (sec*tan) c= dom tan by RELAT_1:25;
then
A3: Z c= dom tan by A1,XBOOLE_1:1;
A4: for x st x in Z holds sec*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
then
A6: tan is_differentiable_in x by FDIFF_7:46;
cos.(tan.x)<>0 by A2,A5;
then sec is_differentiable_in tan.x by Th1;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sec*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*tan)`|Z).x = sin.(tan.x)/(cos.x)^2/(cos.(
tan.x))^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A3,FDIFF_8:1;
then
A10: tan is_differentiable_in x by FDIFF_7:46;
A11: cos.(tan.x)<>0 by A2,A8;
then sec is_differentiable_in tan.x by Th1;
then diff(sec*tan,x) = diff(sec, tan.x)*diff(tan,x) by A10,FDIFF_2:13
.=(sin.(tan.x)/(cos.(tan.x))^2) * diff(tan,x) by A11,Th1
.=(1/(cos.x)^2)*(sin.(tan.x)/(cos.(tan.x))^2) by A9,FDIFF_7:46
.=sin.(tan.x)/(cos.x)^2/(cos.(tan.x))^2;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: f.x = sec.(cot.x)
theorem
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
proof
assume
A1: Z c= dom (sec*cot);
A2: for x st x in Z holds cos.(cot.x)<>0
proof
let x;
assume x in Z;
then cot.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
dom (sec*cot) c= dom cot by RELAT_1:25;
then
A3: Z c= dom cot by A1,XBOOLE_1:1;
A4: for x st x in Z holds sec*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.x<>0 by A3,FDIFF_8:2;
then
A6: cot is_differentiable_in x by FDIFF_7:47;
cos.(cot.x)<>0 by A2,A5;
then sec is_differentiable_in cot.x by Th1;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sec*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*cot)`|Z).x = -sin.(cot.x)/(sin.x)^2/(cos.(
cot.x))^2
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A3,FDIFF_8:2;
then
A10: cot is_differentiable_in x by FDIFF_7:47;
A11: cos.(cot.x)<>0 by A2,A8;
then sec is_differentiable_in cot.x by Th1;
then diff(sec*cot,x) = diff(sec, cot.x)*diff(cot,x) by A10,FDIFF_2:13
.=(sin.(cot.x)/(cos.(cot.x))^2) * diff(cot,x) by A11,Th1
.=(-1/(sin.x)^2)*(sin.(cot.x)/(cos.(cot.x))^2) by A9,FDIFF_7:47
.=-sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: f.x = cosec.(tan.x)
theorem
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
proof
assume
A1: Z c= dom (cosec*tan);
A2: for x st x in Z holds sin.(tan.x)<>0
proof
let x;
assume x in Z;
then tan.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
dom (cosec*tan) c= dom tan by RELAT_1:25;
then
A3: Z c= dom tan by A1,XBOOLE_1:1;
A4: for x st x in Z holds cosec*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
then
A6: tan is_differentiable_in x by FDIFF_7:46;
sin.(tan.x)<>0 by A2,A5;
then cosec is_differentiable_in tan.x by Th2;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cosec*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*tan)`|Z).x = -cos.(tan.x)/(cos.x)^2/(sin.
(tan.x))^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A3,FDIFF_8:1;
then
A10: tan is_differentiable_in x by FDIFF_7:46;
A11: sin.(tan.x)<>0 by A2,A8;
then cosec is_differentiable_in tan.x by Th2;
then diff(cosec*tan,x) = diff(cosec, tan.x)*diff(tan,x) by A10,FDIFF_2:13
.=(-cos.(tan.x)/(sin.(tan.x))^2) * diff(tan,x) by A11,Th2
.=(1/(cos.x)^2)*(-cos.(tan.x)/(sin.(tan.x))^2) by A9,FDIFF_7:46
.=-cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: f.x = cosec.(cot.x)
theorem
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
proof
assume
A1: Z c= dom (cosec*cot);
A2: for x st x in Z holds sin.(cot.x)<>0
proof
let x;
assume x in Z;
then cot.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
dom (cosec*cot) c= dom cot by RELAT_1:25;
then
A3: Z c= dom cot by A1,XBOOLE_1:1;
A4: for x st x in Z holds cosec*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.x<>0 by A3,FDIFF_8:2;
then
A6: cot is_differentiable_in x by FDIFF_7:47;
sin.(cot.x)<>0 by A2,A5;
then cosec is_differentiable_in cot.x by Th2;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cosec*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*cot)`|Z).x = cos.(cot.x)/(sin.x)^2/(sin.(
cot.x))^2
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A3,FDIFF_8:2;
then
A10: cot is_differentiable_in x by FDIFF_7:47;
A11: sin.(cot.x)<>0 by A2,A8;
then cosec is_differentiable_in cot.x by Th2;
then diff(cosec*cot,x) = diff(cosec, cot.x)*diff(cot,x) by A10,FDIFF_2:13
.=(-cos.(cot.x)/(sin.(cot.x))^2) * diff(cot,x) by A11,Th2
.=(-1/(sin.x)^2)*(-cos.(cot.x)/(sin.(cot.x))^2) by A9,FDIFF_7:47
.=cos.(cot.x)/(sin.x)^2/(sin.(cot.x))^2;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: f.x = tan.x*sec.x
theorem
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
proof
assume
A1: Z c= dom (tan(#)sec);
then
A2: Z c= dom (tan) /\ dom sec by VALUED_1:def 4;
then
A3: Z c= dom (tan) by XBOOLE_1:18;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A4: tan is_differentiable_on Z by A3,FDIFF_1:9;
A5: Z c= dom sec by A2,XBOOLE_1:18;
A6: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A7: sec is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((tan(#)sec)`|Z).x = 1/(cos.x)^2/cos.x+tan.x*sin.
x/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A3,FDIFF_8:1;
((tan(#)sec)`|Z).x = (sec.x)*diff(tan,x)+(tan.x)*diff(sec,x) by A1,A4,A7,A8
,FDIFF_1:21
.=(sec.x)*(1/(cos.x)^2)+(tan.x)*diff(sec,x) by A9,FDIFF_7:46
.=(sec.x)*(1/(cos.x)^2)+(tan.x)*(sin.x/(cos.x)^2) by A6,A8
.=(1/(cos.x)^2)/cos.x+tan.x*sin.x/(cos.x)^2 by A5,A8,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A4,A7,FDIFF_1:21;
end;
:: f.x = cot.x*sec.x
theorem
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
proof
assume
A1: Z c= dom (cot(#)sec);
then
A2: Z c= dom (cot) /\ dom sec by VALUED_1:def 4;
then
A3: Z c= dom (cot) by XBOOLE_1:18;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A3,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A4: cot is_differentiable_on Z by A3,FDIFF_1:9;
A5: Z c= dom sec by A2,XBOOLE_1:18;
A6: for x st x in Z holds sec is_differentiable_in x & diff(sec, x)=sin.x/(
cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th1;
end;
then for x st x in Z holds sec is_differentiable_in x;
then
A7: sec is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((cot(#)sec)`|Z).x = -1/(sin.x)^2/cos.x+cot.x*sin
.x/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A3,FDIFF_8:2;
((cot(#)sec)`|Z).x = (sec.x)*diff(cot,x)+(cot.x)*diff(sec,x) by A1,A4,A7,A8
,FDIFF_1:21
.=(sec.x)*(-1/(sin.x)^2)+(cot.x)*diff(sec,x) by A9,FDIFF_7:47
.=(sec.x)*(-1/(sin.x)^2)+(cot.x)*(sin.x/(cos.x)^2) by A6,A8
.=(-1/(sin.x)^2)/cos.x+cot.x*sin.x/(cos.x)^2 by A5,A8,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A4,A7,FDIFF_1:21;
end;
:: f.x = tan.x*cosec.x
theorem
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
proof
assume
A1: Z c= dom (tan(#)cosec);
then
A2: Z c= dom (tan) /\ dom cosec by VALUED_1:def 4;
then
A3: Z c= dom (tan) by XBOOLE_1:18;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A3,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A4: tan is_differentiable_on Z by A3,FDIFF_1:9;
A5: Z c= dom cosec by A2,XBOOLE_1:18;
A6: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-cos
.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A7: cosec is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((tan(#)cosec)`|Z).x = 1/(cos.x)^2/sin.x-tan.x*
cos.x/(sin.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A3,FDIFF_8:1;
((tan(#)cosec)`|Z).x = (cosec.x)*diff(tan,x)+(tan.x)*diff(cosec,x) by A1,A4
,A7,A8,FDIFF_1:21
.=(cosec.x)*(1/(cos.x)^2)+(tan.x)*diff(cosec,x) by A9,FDIFF_7:46
.=(cosec.x)*(1/(cos.x)^2)+(tan.x)*(-cos.x/(sin.x)^2) by A6,A8
.=(1/(cos.x)^2)/sin.x+(tan.x)*(-cos.x/(sin.x)^2) by A5,A8,RFUNCT_1:def 2;
hence thesis;
end;
hence thesis by A1,A4,A7,FDIFF_1:21;
end;
:: f.x = cot.x*cosec.x
theorem
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
proof
assume
A1: Z c= dom (cot(#)cosec);
then
A2: Z c= dom (cot) /\ dom cosec by VALUED_1:def 4;
then
A3: Z c= dom (cot) by XBOOLE_1:18;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A3,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A4: cot is_differentiable_on Z by A3,FDIFF_1:9;
A5: Z c= dom cosec by A2,XBOOLE_1:18;
A6: for x st x in Z holds cosec is_differentiable_in x & diff(cosec, x)=-cos
.x/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A5,RFUNCT_1:3;
hence thesis by Th2;
end;
then for x st x in Z holds cosec is_differentiable_in x;
then
A7: cosec is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((cot(#)cosec)`|Z).x = -1/(sin.x)^2/sin.x-cot.x*
cos.x/(sin.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A3,FDIFF_8:2;
((cot(#)cosec)`|Z).x = (cosec.x)*diff(cot,x)+(cot.x)*diff(cosec,x) by A1,A4
,A7,A8,FDIFF_1:21
.=(cosec.x)*(-1/(sin.x)^2)+(cot.x)*diff(cosec,x) by A9,FDIFF_7:47
.=(cosec.x)*(-1/(sin.x)^2)+(cot.x)*(-cos.x/(sin.x)^2) by A6,A8
.=(-1/(sin.x)^2)/sin.x+(cot.x)*(-cos.x/(sin.x)^2) by A5,A8,RFUNCT_1:def 2
;
hence thesis;
end;
hence thesis by A1,A4,A7,FDIFF_1:21;
end;