:: Several Differentiation Formulas of Special Functions -- Part {IV}
:: by Bo Li and Peng Wang
::
:: Received September 29, 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 NUMBERS, REAL_1, RCOMP_1, SUBSET_1, PARTFUN1, RELAT_1, SIN_COS,
FUNCT_1, CARD_1, XBOOLE_0, ORDINAL4, TARSKI, ARYTM_3, PREPOWER, NEWTON,
ARYTM_1, FDIFF_1, SQUARE_1, LIMFUNC1, TAYLOR_1, XXREAL_0, VALUED_1,
NAT_1;
notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1,
PARTFUN2, XCMPLX_0, XREAL_0, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1,
SQUARE_1, NUMBERS, REAL_1, NAT_1, NEWTON, VALUED_1, FDIFF_1, PREPOWER,
LIMFUNC1;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1,
LIMFUNC1, FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1,
NEWTON;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, INT_1, MEMBERED, RCOMP_1,
VALUED_0, XREAL_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, XBOOLE_0, VALUED_1, XXREAL_1;
begin
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:
x in dom tan implies cos.x<>0
proof
assume x in dom tan;
then x in dom sin /\ (dom cos \ cos"{0}) by RFUNCT_1:def 1;
then x in dom cos \ cos"{0} by XBOOLE_0:def 4;
then x in dom (cos^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
theorem Th2:
x in dom cot implies sin.x<>0
proof
assume x in dom cot;
then x in dom cos /\ (dom sin \ sin"{0}) by RFUNCT_1:def 1;
then x in dom sin \ sin"{0} by XBOOLE_0:def 4;
then x in dom (sin^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
:: ((f1/f2).x) ^ n = (f1.x) ^ n/(f2.x) ^ n
theorem Th3:
Z c= dom (f1/f2) implies for x st x in Z holds ((f1/f2).x) #Z n =
(f1.x) #Z n/(f2.x) #Z n
proof
assume
A1: Z c= dom (f1/f2);
let x;
assume x in Z;
then ((f1/f2).x) #Z n = (f1.x/f2.x) #Z n by A1,RFUNCT_1:def 1
.=(f1.x/f2.x) |^ n by PREPOWER:36
.=(f1.x) |^ n/(f2.x) |^ n by PREPOWER:8
.=(f1.x) #Z n/(f2.x) |^ n by PREPOWER:36
.=(f1.x) #Z n/(f2.x) #Z n by PREPOWER:36;
hence thesis;
end;
:: f.x=(x+a)/(x-b)
theorem
Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x+a & f2.x=x-b) implies
(f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z).x = (-a-b)/
(x-b)^2
proof
assume that
A1: Z c= dom (f1/f2) and
A2: for x st x in Z holds f1.x=x+a & f2.x=x-b;
Z c= dom f1 /\ (dom f2 \ f2"{0}) by A1,RFUNCT_1:def 1;
then
A3: Z c= dom f2 \ f2"{0} by XBOOLE_1:18;
for x st x in Z holds f2.x<>0
proof
let x;
assume x in Z;
then x in dom f2 \ f2"{0} by A3;
then x in dom (f2^) by RFUNCT_1:def 2;
hence thesis by RFUNCT_1:3;
end;
then for x st x in Z holds f1.x=x-(-a) & f2.x=x-b & f2.x<>0 by A2;
hence thesis by A1,FDIFF_5:3;
end;
Lm1: right_open_halfline 0 = {g where g is Real: 0<g} by XXREAL_1:230;
:: f.x=ln(1/x)
theorem
not 0 in Z & Z c= dom (ln*((id Z)^)) implies (ln*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((ln*((id Z)^))`|Z).x = -1/x
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (ln*((id Z)^));
dom (ln*(f^)) c= dom(f^) by RELAT_1:25;
then
A3: Z c= dom (f^) by A2,XBOOLE_1:1;
A4: for x st x in Z holds f^.x>0
proof
let x;
assume
A5: x in Z;
then
A6: f^.x=(f.x)" by A3,RFUNCT_1:def 2
.=1/x by A5,FUNCT_1:18;
f^.x in right_open_halfline(0) by A2,A5,FUNCT_1:11,TAYLOR_1:18;
then ex g being Real st (1/x)=g & 0<g by A6,Lm1;
hence thesis by A6;
end;
A7: for x st x in Z holds f.x>0
proof
let x;
assume
A8: x in Z;
then f^.x>0 by A4;
then (f.x)">0 by A3,A8,RFUNCT_1:def 2;
hence thesis;
end;
A9: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A10: for x st x in Z holds (ln *(f^)) is_differentiable_in x & diff((ln *(f^
)),x) = diff(f^,x)/(f^.x)
proof
let x;
assume x in Z;
then f^ is_differentiable_in x & f^.x>0 by A4,A9,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A11: for x st x in Z holds (ln *(f^)) is_differentiable_in x;
then
A12: (ln *(f^)) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((ln*(f^))`|Z).x = -1/x
proof
let x;
assume
A13: x in Z;
then f.x<>0 by A7;
then
A14: x<>0 by A13,FUNCT_1:18;
diff((ln *(f^)),x) = diff(f^,x)/(f^.x) by A10,A13
.= (((f^)`|Z).x)/(f^.x) by A9,A13,FDIFF_1:def 7
.= (((f^)`|Z).x)/((f.x)") by A3,A13,RFUNCT_1:def 2
.= (((f^)`|Z).x)/(1*x") by A13,FUNCT_1:18
.= (-1/x^2)/(1*x") by A1,A13,FDIFF_5:4
.= -(x/x^2)
.= -(x/x/x) by XCMPLX_1:78
.= -1/x by A14,XCMPLX_1:60;
hence thesis by A12,A13,FDIFF_1:def 7;
end;
hence thesis by A2,A11,FDIFF_1:9;
end;
:: f.x = tan.(a*x+b)
theorem Th6:
Z c= dom (tan*f) & (for x st x in Z holds f.x = a*x+b) implies
tan*f is_differentiable_on Z & for x st x in Z holds ((tan*f)`|Z).x = a/(cos.(a
*x+b))^2
proof
assume that
A1: Z c= dom (tan*f) and
A2: for x st x in Z holds f.x = a*x+b;
dom(tan*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 (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A6: for x st x in Z holds tan*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then cos.(f.x)<>0 by A5;
then
A8: tan is_differentiable_in f.x by FDIFF_7:46;
f is_differentiable_in x by A4,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: tan*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*f)`|Z).x = a/(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 tan is_differentiable_in f.x by FDIFF_7:46;
then diff(tan*f,x) = diff(tan, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(1/(cos.(f.x))^2) * diff(f,x) by A12,FDIFF_7:46
.=diff(f,x)/(cos.(a*x+b))^2 by A2,A10
.=(f`|Z).x/(cos.(a*x+b))^2 by A4,A10,FDIFF_1:def 7
.=a/(cos.(a*x+b))^2 by A2,A3,A10,FDIFF_1:23;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = cot.(a*x+b)
theorem Th7:
Z c= dom (cot*f) & (for x st x in Z holds f.x = a*x+b) implies
cot*f is_differentiable_on Z & for x st x in Z holds ((cot*f)`|Z).x = -a/(sin.(
a*x+b))^2
proof
assume that
A1: Z c= dom (cot*f) and
A2: for x st x in Z holds f.x = a*x+b;
dom(cot*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 (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A6: for x st x in Z holds cot*f is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then sin.(f.x)<>0 by A5;
then
A8: cot is_differentiable_in f.x by FDIFF_7:47;
f is_differentiable_in x by A4,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cot*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*f)`|Z).x = -a/(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 cot is_differentiable_in f.x by FDIFF_7:47;
then diff(cot*f,x) = diff(cot, f.x)*diff(f,x) by A11,FDIFF_2:13
.=(-1/(sin.(f.x))^2) * diff(f,x) by A12,FDIFF_7:47
.=-diff(f,x)/(sin.(f.x))^2
.=-diff(f,x)/(sin.(a*x+b))^2 by A2,A10
.=-(f`|Z).x/(sin.(a*x+b))^2 by A4,A10,FDIFF_1:def 7
.=-a/(sin.(a*x+b))^2 by A2,A3,A10,FDIFF_1:23;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = tan.(1/x)
theorem
not 0 in Z & Z c= dom (tan*((id Z)^)) implies (tan*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((tan*((id Z)^))`|Z).x = -1/(x^2
*(cos.(1/x))^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (tan*((id Z)^));
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
dom (tan*(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 (sin/cos) by A2,FUNCT_1:11;
hence thesis by Th1;
end;
A6: for x st x in Z holds tan*(f^) is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then (cos.((f^).x))<>0 by A5;
then
A8: tan is_differentiable_in (f^).x by FDIFF_7:46;
f^ is_differentiable_in x by A3,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: tan*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((tan*(f^))`|Z).x = -1/(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 tan is_differentiable_in (f^).x by FDIFF_7:46;
then diff(tan*(f^),x) = diff(tan,(f^).x)*diff((f^),x) by A11,FDIFF_2:13
.=(1/(cos.((f^).x))^2) * diff((f^),x) by A12,FDIFF_7:46
.=diff((f^),x)/(cos.((f.x)"))^2 by A4,A10,RFUNCT_1:def 2
.=diff((f^),x)/(cos.(1*x"))^2 by A10,FUNCT_1:18
.=((f^)`|Z).x/(cos.(1*x"))^2 by A3,A10,FDIFF_1:def 7
.=(-1/x^2)/(cos.(1*x"))^2 by A1,A10,FDIFF_5:4
.=(-1)/x^2/(cos.(1/x))^2
.=(-1)/(x^2*(cos.(1/x))^2) by XCMPLX_1:78
.=-1/(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 = cot.(1/x)
theorem
not 0 in Z & Z c= dom (cot*((id Z)^)) implies (cot*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((cot*((id Z)^))`|Z).x = 1/(x^2*
(sin.(1/x))^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (cot*(f^));
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
dom (cot*(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 (cos/sin) by A2,FUNCT_1:11;
hence thesis by Th2;
end;
A6: for x st x in Z holds cot*(f^) is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then (sin.((f^).x))<>0 by A5;
then
A8: cot is_differentiable_in (f^).x by FDIFF_7:47;
f^ is_differentiable_in x by A3,A7,FDIFF_1:9;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cot*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((cot*(f^))`|Z).x = 1/(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 cot is_differentiable_in (f^).x by FDIFF_7:47;
then diff(cot*(f^),x) = diff(cot,(f^).x)*diff((f^),x) by A11,FDIFF_2:13
.=(-1/(sin.((f^).x))^2) * diff((f^),x) by A12,FDIFF_7:47
.=-diff((f^),x)/(sin.((f^).x))^2
.=-diff((f^),x)/(sin.((f.x)"))^2 by A4,A10,RFUNCT_1:def 2
.=-diff((f^),x)/(sin.(1*x"))^2 by A10,FUNCT_1:18
.=-((f^)`|Z).x/(sin.(1*x"))^2 by A3,A10,FDIFF_1:def 7
.=-(-1/x^2)/(sin.(1*x"))^2 by A1,A10,FDIFF_5:4
.=-(-1)/x^2/(sin.(1/x))^2
.=-(-1)/(x^2*(sin.(1/x))^2) by XCMPLX_1:78
.=1/(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 = tan.(a+b*x+c*x^2)
theorem
Z c= dom (tan*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x = a
+b*x) implies tan*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds ((
tan*(f1+c(#)f2))`|Z).x = (b+2*c*x)/(cos.(a+b*x+c*x^2))^2
proof
assume that
A1: Z c= dom (tan*(f1+c(#)f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x = a+b*x;
dom (tan*(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 (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A8: for x st x in Z holds tan*(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: tan is_differentiable_in (f1+c(#)f2).x by FDIFF_7:46;
(f1+c(#)f2) is_differentiable_in x by A5,A9,FDIFF_1:9;
hence thesis by A10,FDIFF_2:13;
end;
then
A11: tan*(f1+c(#)f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*(f1+c(#)f2))`|Z).x = (b+2*c*x)/(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 tan is_differentiable_in (f1+c(#)f2).x by FDIFF_7:46;
then
diff(tan*(f1+c(#)f2),x) = diff(tan, (f1+c(#)f2).x)*diff((f1+c(#)f2),x
) by A14,FDIFF_2:13
.=(1/(cos.((f1+c(#)f2).x))^2)*diff((f1+c(#)f2),x) by A15,FDIFF_7:46
.=((f1+c(#)f2)`|Z).x/(cos.(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))^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 = cot.(a+b*x+c*x^2)
theorem
Z c= dom (cot*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.x = a
+b*x) implies cot*(f1+c(#)f2) is_differentiable_on Z & for x st x in Z holds ((
cot*(f1+c(#)f2))`|Z).x = -(b+2*c*x)/(sin.(a+b*x+c*x^2))^2
proof
assume that
A1: Z c= dom (cot*(f1+c(#)f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x = a+b*x;
dom (cot*(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 (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A8: for x st x in Z holds cot*(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: cot is_differentiable_in (f1+c(#)f2).x by FDIFF_7:47;
(f1+c(#)f2) is_differentiable_in x by A5,A9,FDIFF_1:9;
hence thesis by A10,FDIFF_2:13;
end;
then
A11: cot*(f1+c(#)f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*(f1+c(#)f2))`|Z).x = -(b+2*c*x)/(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 cot is_differentiable_in (f1+c(#)f2).x by FDIFF_7:47;
then
diff(cot*(f1+c(#)f2),x) = diff(cot, (f1+c(#)f2).x)*diff((f1+c(#)f2),x
) by A14,FDIFF_2:13
.=(-1/(sin.((f1+c(#)f2).x))^2)*diff((f1+c(#)f2),x) by A15,FDIFF_7:47
.=-diff((f1+c(#)f2),x)/(sin.(a+b*x+c*x^2))^2 by A13
.=-((f1+c(#)f2)`|Z).x/(sin.(a+b*x+c*x^2))^2 by A5,A12,FDIFF_1:def 7
.=-(b+2*c*x)/(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 = tan.(exp_R.x)
theorem
Z c= dom (tan*exp_R) implies tan*exp_R is_differentiable_on Z & for x
st x in Z holds ((tan*exp_R)`|Z).x = exp_R.x/(cos.(exp_R.x))^2
proof
assume
A1: Z c= dom (tan*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 (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A3: for x st x in Z holds tan*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 & tan is_differentiable_in exp_R.x by
FDIFF_7:46,SIN_COS:65;
hence thesis by FDIFF_2:13;
end;
then
A4: tan*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*exp_R)`|Z).x = 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 & tan is_differentiable_in exp_R.x by
FDIFF_7:46,SIN_COS:65;
then diff(tan*exp_R,x) = diff(tan, exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=(1/(cos.(exp_R.x))^2) * diff(exp_R,x) by A6,FDIFF_7:46
.=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 = cot.(exp_R.x)
theorem
Z c= dom (cot*exp_R) implies cot*exp_R is_differentiable_on Z & for x
st x in Z holds ((cot*exp_R)`|Z).x = -exp_R.x/(sin.(exp_R.x))^2
proof
assume
A1: Z c= dom (cot*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 (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A3: for x st x in Z holds cot*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 & cot is_differentiable_in exp_R.x by
FDIFF_7:47,SIN_COS:65;
hence thesis by FDIFF_2:13;
end;
then
A4: cot*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*exp_R)`|Z).x = -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 & cot is_differentiable_in exp_R.x by
FDIFF_7:47,SIN_COS:65;
then diff(cot*exp_R,x) = diff(cot, exp_R.x)*diff(exp_R,x) by FDIFF_2:13
.=(-1/(sin.(exp_R.x))^2) * diff(exp_R,x) by A6,FDIFF_7:47
.=-diff(exp_R,x)/(sin.(exp_R.x))^2
.=-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;
:: f.x = tan.(ln.x)
theorem
Z c= dom (tan*ln) implies tan*ln is_differentiable_on Z & for x st x
in Z holds ((tan*ln)`|Z).x = 1/(x*(cos.(ln.x))^2)
proof
assume
A1: Z c= dom (tan*ln);
dom (tan*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 (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A6: for x st x in Z holds tan*ln is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then cos.(ln.x)<>0 by A5;
then
A8: tan is_differentiable_in ln.x by FDIFF_7:46;
ln is_differentiable_in x by A3,A7,TAYLOR_1:18;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: tan*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*ln)`|Z).x = 1/(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 tan is_differentiable_in ln.x by FDIFF_7:46;
then diff(tan*ln,x) = diff(tan,ln.x)*diff(ln,x) by A11,FDIFF_2:13
.=(1/(cos.(ln.x))^2) * diff(ln,x) by A12,FDIFF_7:46
.=(1/x)/(cos.(ln.x))^2 by A4,A10
.=1/(x*(cos.(ln.x))^2) by XCMPLX_1:78;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = cot.(ln.x)
theorem
Z c= dom (cot*ln) implies cot*ln is_differentiable_on Z & for x st x
in Z holds ((cot*ln)`|Z).x = -1/(x*(sin.(ln.x))^2)
proof
assume
A1: Z c= dom (cot*ln);
dom (cot*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 (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A6: for x st x in Z holds cot*ln is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then sin.(ln.x)<>0 by A5;
then
A8: cot is_differentiable_in ln.x by FDIFF_7:47;
ln is_differentiable_in x by A3,A7,TAYLOR_1:18;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cot*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*ln)`|Z).x = -1/(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 cot is_differentiable_in ln.x by FDIFF_7:47;
then diff(cot*ln,x) = diff(cot,ln.x)*diff(ln,x) by A11,FDIFF_2:13
.=(-1/(sin.(ln.x))^2) * diff(ln,x) by A12,FDIFF_7:47
.=-diff(ln,x)/(sin.(ln.x))^2
.=-(1/x)/(sin.(ln.x))^2 by A4,A10
.=-1/(x*(sin.(ln.x))^2) by XCMPLX_1:78;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = exp_R.(tan.x)
theorem
Z c= dom (exp_R*tan) implies exp_R*tan is_differentiable_on Z & for x
st x in Z holds ((exp_R*tan)`|Z).x = exp_R.(tan.x)/(cos.x)^2
proof
assume
A1: Z c= dom (exp_R*tan);
A2: for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A3: for x st x in Z holds exp_R*tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A2;
then
A4: tan is_differentiable_in x by FDIFF_7:46;
exp_R is_differentiable_in tan.x by SIN_COS:65;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: exp_R*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*tan)`|Z).x = exp_R.(tan.x)/(cos.x)^2
proof
let x;
A6: exp_R is_differentiable_in tan.x by SIN_COS:65;
assume
A7: x in Z;
then
A8: cos.x<>0 by A2;
then tan is_differentiable_in x by FDIFF_7:46;
then diff(exp_R*tan,x) = diff(exp_R,tan.x)*diff(tan,x) by A6,FDIFF_2:13
.=diff(exp_R,tan.x)*(1/(cos.x)^2) by A8,FDIFF_7:46
.=exp_R.(tan.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.(cot.x)
theorem
Z c= dom (exp_R*cot) implies exp_R*cot is_differentiable_on Z & for x
st x in Z holds ((exp_R*cot)`|Z).x = -exp_R.(cot.x)/(sin.x)^2
proof
assume
A1: Z c= dom (exp_R*cot);
A2: for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A3: for x st x in Z holds exp_R*cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A2;
then
A4: cot is_differentiable_in x by FDIFF_7:47;
exp_R is_differentiable_in cot.x by SIN_COS:65;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: exp_R*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*cot)`|Z).x = -exp_R.(cot.x)/(sin.x)^2
proof
let x;
A6: exp_R is_differentiable_in cot.x by SIN_COS:65;
assume
A7: x in Z;
then
A8: sin.x<>0 by A2;
then cot is_differentiable_in x by FDIFF_7:47;
then diff(exp_R*cot,x) = diff(exp_R,cot.x)*diff(cot,x) by A6,FDIFF_2:13
.=diff(exp_R,cot.x)*(-1/(sin.x)^2) by A8,FDIFF_7:47
.=exp_R.(cot.x) * (-1/(sin.x)^2) by SIN_COS:65
.=-exp_R.(cot.x)/(sin.x)^2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = ln.(tan.x)
theorem
Z c= dom (ln*tan) implies ln*tan is_differentiable_on Z & for x st x
in Z holds ((ln*tan)`|Z).x = 1/(cos.x*sin.x)
proof
assume
A1: Z c= dom (ln*tan);
A2: for x st x in Z holds tan.x>0
proof
let x;
assume x in Z;
then tan.x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
then ex g being Real st tan.x=g & 0<g by Lm1;
hence thesis;
end;
dom (ln*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 cos.x<>0
proof
let x;
assume x in Z;
then x in dom (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A5: for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4;
hence thesis by FDIFF_7:46;
end;
A6: for x st x in Z holds ln*tan is_differentiable_in x
proof
let x;
assume x in Z;
then tan is_differentiable_in x & tan.x>0 by A2,A5;
hence thesis by TAYLOR_1:20;
end;
then
A7: ln*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*tan)`|Z).x =1/(cos.x*sin.x)
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A4;
tan is_differentiable_in x & tan.x>0 by A2,A5,A8;
then diff(ln*tan,x) =diff(tan,x)/(tan.x) by TAYLOR_1:20
.=(1/(cos.x)^2)/(tan.x) by A9,FDIFF_7:46
.=1/((cos.x)^2*tan.x) by XCMPLX_1:78
.=1/((cos.x)^2*(sin.x/cos.x)) by A3,A8,RFUNCT_1:def 1
.=1/(((cos.x)^2*sin.x)/cos.x)
.=cos.x/((cos.x)^2*sin.x) by XCMPLX_1:57
.=cos.x/(cos.x)^2/sin.x by XCMPLX_1:78
.=cos.x/cos.x/cos.x/sin.x by XCMPLX_1:78
.=1/cos.x/sin.x by A4,A8,XCMPLX_1:60
.=1/(cos.x*sin.x) by XCMPLX_1:78;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x = ln.(cot.x)
theorem
Z c= dom (ln*cot) implies ln*cot is_differentiable_on Z & for x st x
in Z holds ((ln*cot)`|Z).x = -1/(sin.x*cos.x)
proof
assume
A1: Z c= dom (ln*cot);
A2: for x st x in Z holds cot.x>0
proof
let x;
assume x in Z;
then cot.x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
then ex g being Real st cot.x=g & 0<g by Lm1;
hence thesis;
end;
dom (ln*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 sin.x<>0
proof
let x;
assume x in Z;
then x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A5: for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4;
hence thesis by FDIFF_7:47;
end;
A6: for x st x in Z holds ln*cot is_differentiable_in x
proof
let x;
assume x in Z;
then cot is_differentiable_in x & cot.x>0 by A2,A5;
hence thesis by TAYLOR_1:20;
end;
then
A7: ln*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*cot)`|Z).x =-1/(sin.x*cos.x)
proof
let x;
assume
A8: x in Z;
then
A9: sin.x<>0 by A4;
cot is_differentiable_in x & cot.x>0 by A2,A5,A8;
then diff(ln*cot,x) =diff(cot,x)/(cot.x) by TAYLOR_1:20
.=(-1/(sin.x)^2)/(cot.x) by A9,FDIFF_7:47
.=-1/(sin.x)^2/cot.x
.=-1/((sin.x)^2*cot.x) by XCMPLX_1:78
.=-1/((sin.x)^2*(cos.x/sin.x)) by A3,A8,RFUNCT_1:def 1
.=-1/(((sin.x)^2*cos.x)/sin.x)
.=-sin.x/((sin.x)^2*cos.x) by XCMPLX_1:57
.=-sin.x/(sin.x)^2/cos.x by XCMPLX_1:78
.=-sin.x/sin.x/sin.x/cos.x by XCMPLX_1:78
.=-1/sin.x/cos.x by A4,A8,XCMPLX_1:60
.=-1/(sin.x*cos.x) by XCMPLX_1:78;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: f.x=(tan.x) ^ n
theorem
Z c= dom (( #Z n)*tan) & 1<=n implies ( #Z n)*tan is_differentiable_on
Z & for x st x in Z holds ((( #Z n)*tan)`|Z).x =n*(sin.x) #Z (n-1)/(cos.x) #Z (
n+1)
proof
assume that
A1: Z c= dom (( #Z n)*tan) and
A2: 1<=n;
A3: dom (( #Z n)*tan) c= dom tan by RELAT_1:25;
A4: for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom (sin/cos) by A1,FUNCT_1:11;
hence thesis by Th1;
end;
A5: for x st x in Z holds ( #Z n)*tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4;
then tan is_differentiable_in x by FDIFF_7:46;
hence thesis by TAYLOR_1:3;
end;
then
A6: ( #Z n)*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*tan)`|Z).x =n*((sin.x) #Z (n-1))/(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: tan is_differentiable_in x by FDIFF_7:46;
((( #Z n)*tan)`|Z).x=diff(( #Z n)*tan,x) by A6,A8,FDIFF_1:def 7
.=n*(tan.x) #Z (n-1) * diff(tan,x) by A10,TAYLOR_1:3
.=n*(tan.x) #Z (n-1) *(1/(cos.x)^2) by A9,FDIFF_7:46
.=n*((sin.x) #Z m /(cos.x) #Z m)/(cos.x)^2 by A1,A3,A8,A7,Th3,XBOOLE_1:1
.=n*(sin.x) #Z (n-1)/(cos.x) #Z (n-1)/(cos.x)^2
.=n*(sin.x) #Z (n-1)/((cos.x) #Z (n-1)*(cos.x)^2) by XCMPLX_1:78
.=n*((sin.x) #Z (n-1))/((cos.x) #Z (n-1)*(cos.x) #Z 2) by FDIFF_7:1
.=n*((sin.x) #Z (n-1))/((cos.x) #Z (n-1+2)) by A4,A8,PREPOWER:44
.=n*((sin.x) #Z (n-1))/(cos.x) #Z (n+1);
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: f.x=(cot.x) ^ n
theorem
Z c= dom (( #Z n)*cot) & 1<=n implies ( #Z n)*cot is_differentiable_on
Z & for x st x in Z holds ((( #Z n)*cot)`|Z).x =-n*(cos.x) #Z (n-1)/(sin.x) #Z
(n+1)
proof
assume that
A1: Z c= dom (( #Z n)*cot) and
A2: 1<=n;
A3: dom (( #Z n)*cot) c= dom cot by RELAT_1:25;
A4: for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom (cos/sin) by A1,FUNCT_1:11;
hence thesis by Th2;
end;
A5: for x st x in Z holds ( #Z n)*cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A4;
then cot is_differentiable_in x by FDIFF_7:47;
hence thesis by TAYLOR_1:3;
end;
then
A6: ( #Z n)*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z n)*cot)`|Z).x =-n*((cos.x) #Z (n-1))/(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: cot is_differentiable_in x by FDIFF_7:47;
((( #Z n)*cot)`|Z).x=diff(( #Z n)*cot,x) by A6,A8,FDIFF_1:def 7
.=n*(cot.x) #Z (n-1) * diff(cot,x) by A10,TAYLOR_1:3
.=n*(cot.x) #Z (n-1) *(-1/(sin.x)^2) by A9,FDIFF_7:47
.=-(n*(cot.x) #Z (n-1))/(sin.x)^2
.=-n*((cos.x) #Z m/(sin.x) #Z m)/(sin.x)^2 by A1,A3,A8,A7,Th3,XBOOLE_1:1
.=-n*(cos.x) #Z (n-1)/(sin.x) #Z (n-1)/(sin.x)^2
.=-n*(cos.x) #Z (n-1)/((sin.x) #Z (n-1)*(sin.x)^2) by XCMPLX_1:78
.=-n*((cos.x) #Z (n-1))/((sin.x) #Z (n-1)*(sin.x) #Z 2) by FDIFF_7:1
.=-n*((cos.x) #Z (n-1))/((sin.x) #Z (n-1+2)) by A4,A8,PREPOWER:44
.=-n*((cos.x) #Z (n-1))/(sin.x) #Z (n+1);
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: f.x = tan.x+1/cos.x
theorem
(Z c= dom (tan+cos^) & for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)
<>0) implies tan+cos^ is_differentiable_on Z & for x st x in Z holds ((tan+cos^
)`|Z).x = 1/(1-sin.x)
proof
assume that
A1: Z c= dom (tan+cos^) and
A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0;
Z c= dom tan /\ dom (cos^) by A1,VALUED_1:def 1;
then
A3: Z c= dom tan by XBOOLE_1:18;
then
A4: for x st x in Z holds cos.x<>0 by Th1;
then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
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,Th1;
hence thesis by FDIFF_7:46;
end;
then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((tan+cos^)`|Z).x = 1/(1-sin.x)
proof
let x;
assume
A7: x in Z;
then
A8: 1+sin.x<>0 by A2;
A9: cos.x<>0 by A3,A7,Th1;
((tan+cos^)`|Z).x = diff(tan,x) + diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:18
.=1/(cos.x)^2 + diff(cos^,x) by A9,FDIFF_7:46
.=1/(cos.x)^2 + ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
.=1/(cos.x)^2 + sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
.=(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
.=(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=(1+sin.x)/((1+sin.x)*(1-sin.x))
.=(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78
.=1/(1-sin.x) by A8,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:18;
end;
:: f.x = tan.x-1/cos.x
theorem
(Z c= dom (tan-cos^) & for x st x in Z holds (1-sin.x)<>0 & (1+sin.x)
<>0) implies tan-cos^ is_differentiable_on Z & for x st x in Z holds ((tan-cos^
)`|Z).x = 1/(1+sin.x)
proof
assume that
A1: Z c= dom (tan-cos^) and
A2: for x st x in Z holds (1-sin.x)<>0 & (1+sin.x)<>0;
Z c= dom tan /\ dom (cos^) by A1,VALUED_1:12;
then
A3: Z c= dom tan by XBOOLE_1:18;
then
A4: for x st x in Z holds cos.x<>0 by Th1;
then
A5: cos^ is_differentiable_on Z by FDIFF_4:39;
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,Th1;
hence thesis by FDIFF_7:46;
end;
then
A6: tan is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((tan-cos^)`|Z).x = 1/(1+sin.x)
proof
let x;
assume
A7: x in Z;
then
A8: (1-sin.x)<>0 by A2;
A9: cos.x<>0 by A3,A7,Th1;
((tan-cos^)`|Z).x = diff(tan,x) - diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:19
.=1/(cos.x)^2 - diff(cos^,x) by A9,FDIFF_7:46
.=1/(cos.x)^2 - ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7
.=1/(cos.x)^2 - sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39
.=(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2)
.=(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28
.=(1-sin.x)/((1-sin.x)*(1+sin.x))
.=(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78
.=1/(1+sin.x) by A8,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A1,A5,A6,FDIFF_1:19;
end;
:: f.x = tan.x-x
theorem
Z c= dom (tan-id Z) implies tan-id Z is_differentiable_on Z & for x st
x in Z holds ((tan-id Z)`|Z).x=(sin.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 (tan-id Z);
then
A3: Z c= dom tan /\ dom (id Z) by VALUED_1:12;
then
A4: Z c= dom tan 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 tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A4,Th1;
hence thesis by FDIFF_7:46;
end;
then
A7: tan is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((tan-id Z)`|Z).x=(sin.x)^2/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then
A9: cos.x<>0 by A4,Th1;
then
A10: (cos.x)^2 >0 by SQUARE_1:12;
((tan-id Z)`|Z).x= diff(tan,x) - diff(id Z,x) by A2,A6,A7,A8,FDIFF_1:19
.=1/(cos.x)^2-diff(id Z,x) by A9,FDIFF_7:46
.=1/(cos.x)^2-((id Z)`|Z).x by A6,A8,FDIFF_1:def 7
.=1/(cos.x)^2-1 by A5,A1,A8,FDIFF_1:23
.=1/(cos.x)^2-(cos.x)^2/(cos.x)^2 by A10,XCMPLX_1:60
.=(1-(cos.x)^2)/(cos.x)^2
.=((sin.x)^2+(cos.x)^2-(cos.x)^2)/(cos.x)^2 by SIN_COS:28
.=(sin.x)^2/(cos.x)^2;
hence thesis;
end;
hence thesis by A2,A6,A7,FDIFF_1:19;
end;
:: f.x = -cot.x-x
theorem
Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z & for x
st x in Z holds ((-cot-id Z)`|Z).x=(cos.x)^2/(sin.x)^2
proof
set f = -cot;
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom (-cot-id Z);
then
A3: Z c= dom (-cot) /\ dom (id Z) by VALUED_1:12;
then
A4: Z c= dom (-cot) by XBOOLE_1:18;
then
A5: Z c= dom cot by VALUED_1:8;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A5,Th2;
hence thesis by FDIFF_7:47;
end;
then
A6: cot is_differentiable_on Z by A5,FDIFF_1:9;
then
A7: (-1)(#)cot 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 ((-cot-id Z)`|Z).x=(cos.x)^2/(sin.x)^2
proof
let x;
assume
A10: x in Z;
then
A11: sin.x<>0 by A5,Th2;
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)(#)cot)`|Z).x-diff(id Z,x) by A7,A10,FDIFF_1:def 7
.=(-1)*diff(cot,x)-diff(id Z,x) by A4,A6,A10,FDIFF_1:20
.=(-1)*(-1/(sin.x)^2)-diff(id Z,x) by A11,FDIFF_7:47
.=1/(sin.x)^2-((id Z)`|Z).x by A9,A10,FDIFF_1:def 7
.=1/(sin.x)^2-1 by A8,A1,A10,FDIFF_1:23
.=1/(sin.x)^2-(sin.x)^2/(sin.x)^2 by A12,XCMPLX_1:60
.=(1-(sin.x)^2)/(sin.x)^2
.=((cos.x)^2+(sin.x)^2-(sin.x)^2)/(sin.x)^2 by SIN_COS:28
.=(cos.x)^2/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A9,A7,FDIFF_1:19;
end;
:: f.x = (1/a)*tan.(a*x)-x
theorem
(Z c= dom ((1/a)(#)(tan*f)-id Z) & for x st x in Z holds f.x=a*x & a<>
0) implies (1/a)(#)(tan*f)-id Z is_differentiable_on Z & for x st x in Z holds
(((1/a)(#)(tan*f)-id Z)`|Z).x=(sin.(a*x))^2/(cos.(a*x))^2
proof
assume that
A1: Z c= dom ((1/a)(#)(tan*f)-id Z) and
A2: for x st x in Z holds f.x=a*x & a<>0;
A3: Z c= dom ((1/a)(#)(tan*f)) /\ dom (id Z) by A1,VALUED_1:12;
then
A4: Z c= dom ((1/a)(#)(tan*f)) by XBOOLE_1:18;
then
A5: Z c= dom (tan*f) by VALUED_1:def 5;
A6: for x st x in Z holds f.x=a*x+0 by A2;
then
A7: tan*f is_differentiable_on Z by A5,Th6;
then
A8: (1/a)(#)(tan*f) is_differentiable_on Z by A4,FDIFF_1:20;
set g = (1/a)(#)(tan*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 (sin/cos) by A5,FUNCT_1:11;
hence thesis by Th1;
end;
for x st x in Z holds (((1/a)(#)(tan*f)-id Z)`|Z).x=(sin.(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(tan*f,x)-diff(id Z,x) by A4,A7,A13,FDIFF_1:20
.=(1/a)*((tan*f)`|Z).x-diff(id Z,x) by A7,A13,FDIFF_1:def 7
.=(1/a)*((tan*f)`|Z).x-((id Z)`|Z).x by A11,A13,FDIFF_1:def 7
.=(1/a)*(a/(cos.(a*x))^2)-((id Z)`|Z).x by A5,A6,A13,A14,Th6
.=1/(cos.(a*x))^2*(a/a) -1 by A10,A9,A13,FDIFF_1:23
.=1/(cos.(a*x))^2*1 -1 by A2,A13,XCMPLX_1:60
.=1/(cos.(a*x))^2-(cos.(a*x))^2/(cos.(a*x))^2 by A15,XCMPLX_1:60
.=(1-(cos.(a*x))^2)/(cos.(a*x))^2
.=((sin.(a*x))^2+(cos.(a*x))^2-(cos.(a*x))^2)/(cos.(a*x))^2 by SIN_COS:28
.=(sin.(a*x))^2/(cos.(a*x))^2;
hence thesis;
end;
hence thesis by A1,A8,A11,FDIFF_1:19;
end;
:: f.x = (-1/a)*cot.(a*x)-x
theorem
(Z c= dom ((-1/a)(#)(cot*f)-id Z) & for x st x in Z holds f.x=a*x & a
<>0) implies (-1/a)(#)(cot*f)-id Z is_differentiable_on Z & for x st x in Z
holds (((-1/a)(#)(cot*f)-id Z)`|Z).x=(cos.(a*x))^2/(sin.(a*x))^2
proof
assume that
A1: Z c= dom ((-1/a)(#)(cot*f)-id Z) and
A2: for x st x in Z holds f.x=a*x & a<>0;
A3: Z c= dom ((-1/a)(#)(cot*f)) /\ dom (id Z) by A1,VALUED_1:12;
then
A4: Z c= dom ((-1/a)(#)(cot*f)) by XBOOLE_1:18;
then
A5: Z c= dom (cot*f) by VALUED_1:def 5;
A6: for x st x in Z holds f.x=a*x+0 by A2;
then
A7: cot*f is_differentiable_on Z by A5,Th7;
then
A8: (-1/a)(#)(cot*f) is_differentiable_on Z by A4,FDIFF_1:20;
set g = (-1/a)(#)(cot*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 (cos/sin) by A5,FUNCT_1:11;
hence thesis by Th2;
end;
for x st x in Z holds (((-1/a)(#)(cot*f)-id Z)`|Z).x=(cos.(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(cot*f,x)-diff(id Z,x) by A4,A7,A13,FDIFF_1:20
.=(-1/a)*((cot*f)`|Z).x-diff(id Z,x) by A7,A13,FDIFF_1:def 7
.=(-1/a)*((cot*f)`|Z).x-((id Z)`|Z).x by A11,A13,FDIFF_1:def 7
.=(-1/a)*(-a/(sin.(a*x))^2)-((id Z)`|Z).x by A5,A6,A13,A14,Th7
.=1/(sin.(a*x))^2*(a/a) -1 by A10,A9,A13,FDIFF_1:23
.=1/(sin.(a*x))^2*1 -1 by A2,A13,XCMPLX_1:60
.=1/(sin.(a*x))^2-(sin.(a*x))^2/(sin.(a*x))^2 by A15,XCMPLX_1:60
.=(1-(sin.(a*x))^2)/(sin.(a*x))^2
.=((cos.(a*x))^2+(sin.(a*x))^2-(sin.(a*x))^2)/(sin.(a*x))^2 by SIN_COS:28
.=(cos.(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)*tan.x
theorem
(Z c= dom (f(#)tan) & for x st x in Z holds f.x=a*x+b) implies (f(#)
tan) is_differentiable_on Z & for x st x in Z holds ((f(#)tan)`|Z).x = a*sin.x/
cos.x+(a*x+b)/(cos.x)^2
proof
assume that
A1: Z c= dom (f(#)tan) and
A2: for x st x in Z holds f.x=a*x+b;
A3: Z c= dom f /\ dom tan by A1,VALUED_1:def 4;
then
A4: Z c= dom tan 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 tan is_differentiable_in x & diff(tan, x)=1/(cos.x
)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,Th1;
hence thesis by FDIFF_7:46;
end;
then for x st x in Z holds tan is_differentiable_in x;
then
A8: tan is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((f(#)tan)`|Z).x = a*sin.x/cos.x+(a*x+b)/(cos.x) ^2
proof
let x;
assume
A9: x in Z;
then ((f(#)tan)`|Z).x= (tan.x)*diff(f,x)+(f.x)*diff(tan,x) by A1,A6,A8,
FDIFF_1:21
.=(tan.x)*((f`|Z).x)+(f.x)*diff(tan,x) by A6,A9,FDIFF_1:def 7
.=(tan.x)*a+(f.x)*diff(tan,x) by A2,A5,A9,FDIFF_1:23
.=(tan.x)*a+(a*x+b)*diff(tan,x) by A2,A9
.=(tan.x)*a+(a*x+b)*(1/(cos.x)^2) by A7,A9
.=(sin.x/cos.x)*(a/1)+(a*x+b)/(cos.x)^2 by A4,A9,RFUNCT_1:def 1
.=a*sin.x/cos.x+(a*x+b)/(cos.x)^2;
hence thesis;
end;
hence thesis by A1,A6,A8,FDIFF_1:21;
end;
:: f.x = (a*x+b)*cot.x
theorem
(Z c= dom (f(#)cot) & for x st x in Z holds f.x=a*x+b) implies (f(#)
cot) is_differentiable_on Z & for x st x in Z holds ((f(#)cot)`|Z).x = a*cos.x/
sin.x-(a*x+b)/(sin.x)^2
proof
assume that
A1: Z c= dom (f(#)cot) and
A2: for x st x in Z holds f.x=a*x+b;
A3: Z c= dom f /\ dom cot by A1,VALUED_1:def 4;
then
A4: Z c= dom cot 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 cot is_differentiable_in x & diff(cot, x)=-1/(sin.
x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,Th2;
hence thesis by FDIFF_7:47;
end;
then for x st x in Z holds cot is_differentiable_in x;
then
A8: cot is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((f(#)cot)`|Z).x = a*cos.x/sin.x-(a*x+b)/(sin.x) ^2
proof
let x;
assume
A9: x in Z;
then ((f(#)cot)`|Z).x= (cot.x)*diff(f,x)+(f.x)*diff(cot,x) by A1,A6,A8,
FDIFF_1:21
.=(cot.x)*((f`|Z).x)+(f.x)*diff(cot,x) by A6,A9,FDIFF_1:def 7
.=(cot.x)*a+(f.x)*diff(cot,x) by A2,A5,A9,FDIFF_1:23
.=(cot.x)*a+(a*x+b)*diff(cot,x) by A2,A9
.=(cot.x)*a+(a*x+b)*(-1/(sin.x)^2) by A7,A9
.=(cos.x/sin.x)*(a/1)-(a*x+b)/(sin.x)^2 by A4,A9,RFUNCT_1:def 1
.=a*cos.x/sin.x-(a*x+b)/(sin.x)^2;
hence thesis;
end;
hence thesis by A1,A6,A8,FDIFF_1:21;
end;
:: f.x = exp_R.x*tan.x
theorem
Z c= dom (exp_R(#)tan) implies (exp_R(#)tan) is_differentiable_on Z &
for x st x in Z holds ((exp_R(#)tan)`|Z).x = exp_R.x*sin.x/cos.x+exp_R.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(#)tan);
then
A3: Z c= dom (exp_R) /\ dom tan by VALUED_1:def 4;
then
A4: Z c= dom tan 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 tan is_differentiable_in x & diff(tan, x)=1/(cos.x
)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,Th1;
hence thesis by FDIFF_7:46;
end;
then for x st x in Z holds tan is_differentiable_in x;
then
A7: tan is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((exp_R(#)tan)`|Z).x = exp_R.x*sin.x/cos.x+exp_R.
x/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then
((exp_R(#)tan)`|Z).x = (tan.x)*diff(exp_R,x)+(exp_R.x)*diff(tan,x) by A2,A5
,A7,FDIFF_1:21
.=(tan.x)*exp_R.x+(exp_R.x)*diff(tan,x) by SIN_COS:65
.=(tan.x)*exp_R.x+(exp_R.x)*(1/(cos.x)^2) by A6,A8
.=(sin.x/cos.x)*(exp_R.x/1)+(exp_R.x)/(cos.x)^2 by A4,A8,RFUNCT_1:def 1
.=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2;
hence thesis;
end;
hence thesis by A2,A5,A7,FDIFF_1:21;
end;
:: f.x = exp_R.x*cot.x
theorem
Z c= dom (exp_R(#)cot) implies (exp_R(#)cot) is_differentiable_on Z &
for x st x in Z holds ((exp_R(#)cot)`|Z).x = exp_R.x*cos.x/sin.x-exp_R.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(#)cot);
then
A3: Z c= dom (exp_R) /\ dom cot by VALUED_1:def 4;
then
A4: Z c= dom cot 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 cot is_differentiable_in x & diff(cot, x)=-1/(sin.
x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,Th2;
hence thesis by FDIFF_7:47;
end;
then for x st x in Z holds cot is_differentiable_in x;
then
A7: cot is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((exp_R(#)cot)`|Z).x = exp_R.x*cos.x/sin.x-exp_R.
x/(sin.x)^2
proof
let x;
assume
A8: x in Z;
then ((exp_R(#)cot)`|Z).x= (cot.x)*diff(exp_R,x)+(exp_R.x)*diff(cot,x) by
A2,A5,A7,FDIFF_1:21
.=(cot.x)*exp_R.x+(exp_R.x)*diff(cot,x) by SIN_COS:65
.=(cot.x)*exp_R.x+(exp_R.x)*(-1/(sin.x)^2) by A6,A8
.=(cos.x/sin.x)*(exp_R.x/1)-(exp_R.x)/(sin.x)^2 by A4,A8,RFUNCT_1:def 1
.=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A5,A7,FDIFF_1:21;
end;
:: f.x = ln.x*tan.x
theorem
Z c= dom (ln(#)tan) implies (ln(#)tan) is_differentiable_on Z & for x
st x in Z holds ((ln(#)tan)`|Z).x = sin.x/cos.x/x+ln.x/(cos.x)^2
proof
assume
A1: Z c= dom (ln(#)tan);
then
A2: Z c= dom ln /\ dom tan by VALUED_1:def 4;
then
A3: Z c= dom tan by XBOOLE_1:18;
A4: for x st x in Z holds tan is_differentiable_in x & diff(tan, x)=1/(cos.
x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A3,Th1;
hence thesis by FDIFF_7:46;
end;
then for x st x in Z holds tan is_differentiable_in x;
then
A5: tan 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(#)tan)`|Z).x = sin.x/cos.x/x+ln.x/(cos.x)^2
proof
let x;
assume
A10: x in Z;
then ((ln(#)tan)`|Z).x= (tan.x)*diff(ln,x)+(ln.x)*diff(tan,x) by A1,A8,A5,
FDIFF_1:21
.=(tan.x)*(1/x)+(ln.x)*diff(tan,x) by A9,A10
.=(tan.x)*(1/x)+(ln.x)*(1/(cos.x)^2) by A4,A10
.=sin.x/cos.x/x+ln.x/(cos.x)^2 by A3,A10,RFUNCT_1:def 1;
hence thesis;
end;
hence thesis by A1,A8,A5,FDIFF_1:21;
end;
:: f.x = ln.x*cot.x
theorem
Z c= dom (ln(#)cot) implies ln(#)cot is_differentiable_on Z & for x st
x in Z holds ((ln(#)cot)`|Z).x = cos.x/sin.x/x-ln.x/(sin.x)^2
proof
assume
A1: Z c= dom (ln(#)cot);
then
A2: Z c= dom ln /\ dom cot by VALUED_1:def 4;
then
A3: Z c= dom cot by XBOOLE_1:18;
A4: for x st x in Z holds cot is_differentiable_in x & diff(cot, x)=-1/(sin
.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A3,Th2;
hence thesis by FDIFF_7:47;
end;
then for x st x in Z holds cot is_differentiable_in x;
then
A5: cot 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(#)cot)`|Z).x = cos.x/sin.x/x-ln.x/(sin.x)^2
proof
let x;
assume
A10: x in Z;
then ((ln(#)cot)`|Z).x = (cot.x)*diff(ln,x)+(ln.x)*diff(cot,x) by A1,A8,A5,
FDIFF_1:21
.=(cot.x)*(1/x)+(ln.x)*diff(cot,x) by A9,A10
.=(cot.x)*(1/x)+(ln.x)*(-1/(sin.x)^2) by A4,A10
.=cos.x/sin.x/x-ln.x/(sin.x)^2 by A3,A10,RFUNCT_1:def 1;
hence thesis;
end;
hence thesis by A1,A8,A5,FDIFF_1:21;
end;
:: f.x = 1/x*tan.x
theorem
not 0 in Z & Z c= dom ((id Z)^(#)tan) implies ((id Z)^(#)tan)
is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)tan)`|Z).x = -sin.x/
cos.x/x^2+1/x/(cos.x)^2
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)tan);
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A4: Z c= dom (f^) /\ dom tan by A2,VALUED_1:def 4;
then
A5: Z c= dom tan by XBOOLE_1:18;
A6: for x st x in Z holds tan is_differentiable_in x & diff(tan, x)=1/(cos.x
)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A5,Th1;
hence thesis by FDIFF_7:46;
end;
then for x st x in Z holds tan is_differentiable_in x;
then
A7: tan 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^(#)tan)`|Z).x =-sin.x/cos.x/x^2+1/x/(cos.x)^2
proof
let x;
assume
A9: x in Z;
then ((f^(#)tan)`|Z).x= (tan.x)*diff(f^,x)+((f^).x)*diff(tan,x) by A2,A3,A7
,FDIFF_1:21
.=(tan.x)*((f^)`|Z).x+((f^).x)*diff(tan,x) by A3,A9,FDIFF_1:def 7
.=(tan.x)*(-1/x^2)+((f^).x)*diff(tan,x) by A1,A9,FDIFF_5:4
.=-(tan.x)*(1/x^2)+((f^).x)*(1/(cos.x)^2) by A6,A9
.=-(sin.x/cos.x)*(1/x^2)+((f^).x)/(cos.x)^2 by A5,A9,RFUNCT_1:def 1
.=-sin.x/cos.x/x^2+(f.x)"/(cos.x)^2 by A8,A9,RFUNCT_1:def 2
.=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by A9,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A3,A7,FDIFF_1:21;
end;
:: f.x = 1/x*cot.x
theorem
not 0 in Z & Z c= dom ((id Z)^(#)cot) implies ((id Z)^(#)cot)
is_differentiable_on Z & for x st x in Z holds (((id Z)^(#)cot)`|Z).x = -cos.x/
sin.x/x^2-1/x/(sin.x)^2
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (f^(#)cot);
A3: f^ is_differentiable_on Z by A1,FDIFF_5:4;
A4: Z c= dom (f^) /\ dom cot by A2,VALUED_1:def 4;
then
A5: Z c= dom cot by XBOOLE_1:18;
A6: for x st x in Z holds cot is_differentiable_in x & diff(cot, x)=-1/(sin.
x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A5,Th2;
hence thesis by FDIFF_7:47;
end;
then for x st x in Z holds cot is_differentiable_in x;
then
A7: cot 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^(#)cot)`|Z).x =-cos.x/sin.x/x^2-1/x/(sin.x)^2
proof
let x;
assume
A9: x in Z;
then ((f^(#)cot)`|Z).x= (cot.x)*diff(f^,x)+((f^).x)*diff(cot,x) by A2,A3,A7
,FDIFF_1:21
.=(cot.x)*((f^)`|Z).x+((f^).x)*diff(cot,x) by A3,A9,FDIFF_1:def 7
.=(cot.x)*(-1/x^2)+((f^).x)*diff(cot,x) by A1,A9,FDIFF_5:4
.=-(cot.x)*(1/x^2)+((f^).x)*(-1/(sin.x)^2) by A6,A9
.=-(cos.x/sin.x)*(1/x^2)-((f^).x)/(sin.x)^2 by A5,A9,RFUNCT_1:def 1
.=-cos.x/sin.x/x^2-(f.x)"/(sin.x)^2 by A8,A9,RFUNCT_1:def 2
.=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by A9,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A3,A7,FDIFF_1:21;
end;