:: Several Differentiation Formulas of Special Functions -- Part {V}
:: by Bo Li and Pan Wang
::
:: Received September 19, 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 REAL_1, RCOMP_1, SUBSET_1, NUMBERS, TARSKI, RELAT_1, SIN_COS,
FDIFF_1, FUNCT_1, ARYTM_3, SQUARE_1, ARYTM_1, CARD_1, XBOOLE_0, VALUED_1,
TAYLOR_1, XXREAL_0, LIMFUNC1, XXREAL_1, SIN_COS4;
notations TARSKI, SUBSET_1, ORDINAL1, FUNCT_1, XXREAL_0, XCMPLX_0, XREAL_0,
RELSET_1, PARTFUN1, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1,
NUMBERS, REAL_1, VALUED_1, FDIFF_1, LIMFUNC1, FDIFF_9;
constructors REAL_1, PARTFUN1, PARTFUN2, LIMFUNC1, RCOMP_1, TAYLOR_1, SIN_COS,
FDIFF_1, RFUNCT_1, SQUARE_1, ARYTM_0, COMSEQ_3, FDIFF_9, VALUED_1,
RELSET_1, XREAL_0;
registrations RELSET_1, MEMBERED, RCOMP_1, XXREAL_0, VALUED_0, NUMBERS,
XREAL_0, SQUARE_1, SIN_COS;
requirements SUBSET, NUMERALS, ARITHM;
equalities SQUARE_1, LIMFUNC1, XCMPLX_0, SIN_COS, FDIFF_9;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FDIFF_7, RFUNCT_1,
FUNCT_1, SIN_COS, RELAT_1, FDIFF_8, FDIFF_9, VALUED_1, XXREAL_1, XREAL_0;
begin
reserve x for Real,
Z for open Subset of REAL;
::f.x=tan.(cot.x)
theorem
Z c= dom (tan*cot) implies tan*cot is_differentiable_on Z & for x st x
in Z holds((tan*cot)`|Z).x = 1/(cos.(cot.x))^2 *(-1/(sin.x)^2)
proof
assume
A1: Z c= dom (tan*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 (tan) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:1;
end;
A3: 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 FDIFF_8:2;
end;
A4: for x st x in Z holds tan*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.(cot.x)<>0 by A2;
then
A6: tan is_differentiable_in cot.x by FDIFF_7:46;
sin.x <> 0 by A3,A5;
then cot is_differentiable_in x by FDIFF_7:47;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: tan*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*cot)`|Z).x = 1/(cos.(cot.x))^2 *(-1/(sin.x) ^2)
proof
let x;
assume
A8: x in Z;
then
A9: cos.(cot.x)<>0 by A2;
then
A10: tan is_differentiable_in cot.x by FDIFF_7:46;
A11: sin.x<>0 by A3,A8;
then cot is_differentiable_in x by FDIFF_7:47;
then diff(tan*cot,x) = diff(tan, cot.x)*diff(cot,x) by A10,FDIFF_2:13
.=1/(cos.(cot.x))^2 * diff(cot,x) by A9,FDIFF_7:46
.=1/(cos.(cot.x))^2 *(-1/(sin.x)^2) by A11,FDIFF_7:47;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=tan.(tan.x)
theorem
Z c= dom (tan*tan) implies tan*tan is_differentiable_on Z & for x st x
in Z holds((tan*tan)`|Z).x = 1/(cos.(tan.x))^2 *(1/(cos.x)^2)
proof
assume
A1: Z c= dom (tan*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 (tan) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:1;
end;
A3: 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 FDIFF_8:1;
end;
A4: for x st x in Z holds tan*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.(tan.x)<>0 by A2;
then
A6: tan is_differentiable_in tan.x by FDIFF_7:46;
cos.x <> 0 by A3,A5;
then tan is_differentiable_in x by FDIFF_7:46;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: tan*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*tan)`|Z).x = 1/(cos.(tan.x))^2 *(1/(cos.x) ^2)
proof
let x;
assume
A8: x in Z;
then
A9: cos.(tan.x)<>0 by A2;
then
A10: tan is_differentiable_in tan.x by FDIFF_7:46;
A11: cos.x<>0 by A3,A8;
then tan is_differentiable_in x by FDIFF_7:46;
then diff(tan*tan,x) = diff(tan, tan.x)*diff(tan,x) by A10,FDIFF_2:13
.=1/(cos.(tan.x))^2 * diff(tan,x) by A9,FDIFF_7:46
.=1/(cos.(tan.x))^2 *(1/(cos.x)^2) by A11,FDIFF_7:46;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cot.(cot.x)
theorem
Z c= dom (cot*cot) implies cot*cot is_differentiable_on Z & for x st x
in Z holds((cot*cot)`|Z).x = (1/(sin.(cot.x))^2) *(1/(sin.x)^2)
proof
assume
A1: Z c= dom (cot*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 cot by A1,FUNCT_1:11;
hence thesis by FDIFF_8:2;
end;
A3: 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 FDIFF_8:2;
end;
A4: for x st x in Z holds cot*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.(cot.x)<>0 by A2;
then
A6: cot is_differentiable_in cot.x by FDIFF_7:47;
sin.x <> 0 by A3,A5;
then cot is_differentiable_in x by FDIFF_7:47;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cot*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*cot)`|Z).x=(1/(sin.(cot.x))^2)*(1/(sin.x)^2 )
proof
let x;
assume
A8: x in Z;
then
A9: sin.(cot.x)<>0 by A2;
then
A10: cot is_differentiable_in cot.x by FDIFF_7:47;
A11: sin.x<>0 by A3,A8;
then cot is_differentiable_in x by FDIFF_7:47;
then diff(cot*cot,x) = diff(cot, cot.x)*diff(cot,x) by A10,FDIFF_2:13
.=(-1/(sin.(cot.x))^2)* diff(cot,x) by A9,FDIFF_7:47
.=(-1/(sin.(cot.x))^2) *(-1/(sin.x)^2) by A11,FDIFF_7:47;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cot.(tan.x)
theorem
Z c= dom (cot*tan) implies cot*tan is_differentiable_on Z & for x st x
in Z holds((cot*tan)`|Z).x = (-1/(sin.(tan.x))^2)*(1/(cos.x)^2)
proof
assume
A1: Z c= dom (cot*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 (cot) by A1,FUNCT_1:11;
hence thesis by FDIFF_8:2;
end;
A3: 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 FDIFF_8:1;
end;
A4: for x st x in Z holds cot*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.(tan.x)<>0 by A2;
then
A6: cot is_differentiable_in tan.x by FDIFF_7:47;
cos.x <> 0 by A3,A5;
then tan is_differentiable_in x by FDIFF_7:46;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cot*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*tan)`|Z).x=(-1/(sin.(tan.x))^2)*(1/(cos.x) ^2)
proof
let x;
assume
A8: x in Z;
then
A9: sin.(tan.x)<>0 by A2;
then
A10: cot is_differentiable_in tan.x by FDIFF_7:47;
A11: cos.x<>0 by A3,A8;
then tan is_differentiable_in x by FDIFF_7:46;
then diff(cot*tan,x) = diff(cot, tan.x)*diff(tan,x) by A10,FDIFF_2:13
.=(-1/(sin.(tan.x))^2)* diff(tan,x) by A9,FDIFF_7:47
.=(-1/(sin.(tan.x))^2)*(1/(cos.x)^2) by A11,FDIFF_7:46;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x= tan.x - cot.x
theorem Th5:
Z c= dom(tan-cot) implies (tan - cot) is_differentiable_on Z &
for x st x in Z holds((tan - cot)`|Z).x = 1/(cos.x)^2+1/(sin.x)^2
proof
assume
A1: Z c= dom (tan-cot);
then
A2: Z c= dom tan /\ dom cot by VALUED_1:12;
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 cot by A2,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 A5,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A6: cot is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((tan-cot)`|Z).x =1/(cos.x)^2+1/(sin.x)^2
proof
let x;
assume
A7: x in Z;
then
A8: sin.x<> 0 by A5,FDIFF_8:2;
A9: cos.x<> 0 by A3,A7,FDIFF_8:1;
((tan-cot)`|Z).x = diff(tan,x)-diff(cot,x)by A1,A6,A4,A7,FDIFF_1:19
.=1/(cos.x)^2-diff(cot,x) by A9,FDIFF_7:46
.=1/(cos.x)^2-(-1/(sin.x)^2) by A8,FDIFF_7:47
.=1/(cos.x)^2+1/(sin.x)^2;
hence thesis;
end;
hence thesis by A1,A6,A4,FDIFF_1:19;
end;
::f.x= tan.x + cot.x
theorem Th6:
Z c= dom(tan+cot) implies (tan + cot) is_differentiable_on Z &
for x st x in Z holds((tan + cot)`|Z).x = 1/(cos.x)^2-1/(sin.x)^2
proof
assume
A1: Z c= dom (tan+cot);
then
A2: Z c= dom tan /\ dom cot by VALUED_1:def 1;
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 cot by A2,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 A5,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A6: cot is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds ((tan+cot)`|Z).x =1/(cos.x)^2-1/(sin.x)^2
proof
let x;
assume
A7: x in Z;
then
A8: sin.x<> 0 by A5,FDIFF_8:2;
A9: cos.x<> 0 by A3,A7,FDIFF_8:1;
((tan+cot)`|Z).x = diff(tan,x)+diff(cot,x)by A1,A6,A4,A7,FDIFF_1:18
.=1/(cos.x)^2+diff(cot,x) by A9,FDIFF_7:46
.=1/(cos.x)^2-1/(sin.x)^2 by A8,FDIFF_7:47;
hence thesis;
end;
hence thesis by A1,A6,A4,FDIFF_1:18;
end;
::f.x=sin.(sin.x)
theorem
sin*sin is_differentiable_on Z & for x st x in Z holds((sin*sin)`|Z).x
= cos.(sin.x)*cos.x
proof
A1: for x st x in Z holds sin*sin is_differentiable_in x
proof
let x;
assume x in Z;
A2: sin is_differentiable_in sin.x by SIN_COS:64;
sin is_differentiable_in x by SIN_COS:64;
hence thesis by A2,FDIFF_2:13;
end;
rng sin c= REAL;
then
A3: dom (sin*sin) = REAL by RELAT_1:27,SIN_COS:24;
then
A4: sin*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds((sin*sin)`|Z).x = cos.(sin.x)*cos.x
proof
let x;
assume
A5: x in Z;
A6: sin is_differentiable_in sin.x by SIN_COS:64;
sin is_differentiable_in x by SIN_COS:64;
then diff(sin*sin,x) = diff(sin,sin.x)*diff(sin,x) by A6,FDIFF_2:13
.=cos.(sin.x)*diff(sin,x) by SIN_COS:64
.=cos.(sin.x)*cos.x by SIN_COS:64;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A3,A1,FDIFF_1:9;
end;
::f.x=sin.(cos.x)
theorem
sin*cos is_differentiable_on Z & for x st x in Z holds((sin*cos)`|Z).x
= -cos.(cos.x)*sin.x
proof
A1: for x st x in Z holds sin*cos is_differentiable_in x
proof
let x;
assume x in Z;
A2: sin is_differentiable_in cos.x by SIN_COS:64;
cos is_differentiable_in x by SIN_COS:63;
hence thesis by A2,FDIFF_2:13;
end;
rng cos c= dom cos by SIN_COS:24;
then
A3: dom (sin*cos) = REAL by RELAT_1:27,SIN_COS:24;
then
A4: sin*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds((sin*cos)`|Z).x = -cos.(cos.x)*sin.x
proof
let x;
assume
A5: x in Z;
A6: sin is_differentiable_in cos.x by SIN_COS:64;
cos is_differentiable_in x by SIN_COS:63;
then diff(sin*cos,x) =diff(sin,cos.x)*diff(cos,x) by A6,FDIFF_2:13
.=cos.(cos.x)*diff(cos,x) by SIN_COS:64
.=cos.(cos.x)*(-sin.x) by SIN_COS:63;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A3,A1,FDIFF_1:9;
end;
::f.x=cos.(sin.x)
theorem
cos*sin is_differentiable_on Z & for x st x in Z holds((cos*sin)`|Z).x
= -sin.(sin.x)*cos.x
proof
A1: for x st x in Z holds cos*sin is_differentiable_in x
proof
let x;
assume x in Z;
A2: cos is_differentiable_in sin.x by SIN_COS:63;
sin is_differentiable_in x by SIN_COS:64;
hence thesis by A2,FDIFF_2:13;
end;
rng sin c= dom sin by SIN_COS:24;
then
A3: dom (cos*sin) = REAL by RELAT_1:27,SIN_COS:24;
then
A4: cos*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds((cos*sin)`|Z).x = -sin.(sin.x)*cos.x
proof
let x;
assume
A5: x in Z;
A6: cos is_differentiable_in sin.x by SIN_COS:63;
sin is_differentiable_in x by SIN_COS:64;
then diff(cos*sin,x) =diff(cos,sin.x)*diff(sin,x) by A6,FDIFF_2:13
.=(-sin.(sin.x))*diff(sin,x) by SIN_COS:63
.=(-sin.(sin.x))*cos.x by SIN_COS:64;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A3,A1,FDIFF_1:9;
end;
::f.x=cos.(cos.x)
theorem
cos*cos is_differentiable_on Z & for x st x in Z holds((cos*cos)`|Z).x
= sin.(cos.x)*sin.x
proof
A1: for x st x in Z holds cos*cos is_differentiable_in x
proof
let x;
assume x in Z;
A2: cos is_differentiable_in cos.x by SIN_COS:63;
cos is_differentiable_in x by SIN_COS:63;
hence thesis by A2,FDIFF_2:13;
end;
rng cos c= REAL;
then
A3: dom (cos*cos) = REAL by RELAT_1:27,SIN_COS:24;
then
A4: cos*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds((cos*cos)`|Z).x = sin.(cos.x)*sin.x
proof
let x;
assume
A5: x in Z;
A6: cos is_differentiable_in cos.x by SIN_COS:63;
cos is_differentiable_in x by SIN_COS:63;
then diff(cos*cos,x) =diff(cos,cos.x)*diff(cos,x) by A6,FDIFF_2:13
.=(-sin.(cos.x))*diff(cos,x) by SIN_COS:63
.=(-sin.(cos.x))*(-sin.x) by SIN_COS:63;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A3,A1,FDIFF_1:9;
end;
:: f.x=cos.x * cot.x
theorem
Z c= dom (cos (#) cot) implies (cos (#) cot) is_differentiable_on Z &
for x st x in Z holds((cos (#) cot)`|Z).x = -cos.x-cos.x/(sin.x)^2
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos (#) cot);
then
A3: Z c= dom cos /\ dom cot by VALUED_1:def 4;
then
A4: 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 A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
A7: for x st x in Z holds diff(cot, x)=-1/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
for x st x in Z holds((cos (#) cot)`|Z).x =-cos.x-cos.x/(sin.x)^2
proof
let x;
assume
A8: x in Z;
then ((cos (#) cot)`|Z).x= diff(cos,x)*cot.x+cos.x*diff(cot,x) by A2,A5,A6,
FDIFF_1:21
.=cot.x*(-sin.x)+cos.x*diff(cot,x) by SIN_COS:63
.=cot.x*(-sin.x)+cos.x*(-1/(sin.x)^2) by A7,A8
.=(cos.x/sin.x)*(-sin.x/1)-cos.x/(sin.x)^2 by A4,A8,RFUNCT_1:def 1
.=-cos.x*(sin.x/sin.x)-cos.x/(sin.x)^2
.=-cos.x*1-cos.x/(sin.x)^2 by A4,A8,FDIFF_8:2,XCMPLX_1:60
.=-cos.x-cos.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=sin.x * tan.x
theorem
Z c= dom (sin (#) tan) implies (sin (#)tan) is_differentiable_on Z &
for x st x in Z holds((sin (#) tan)`|Z).x = sin.x + sin.x/(cos.x)^2
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin (#) tan);
then
A3: Z c= dom sin /\ dom tan by VALUED_1:def 4;
then
A4: 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 A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A5: tan is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
A7: for x st x in Z holds diff(tan, x)=1/(cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
for x st x in Z holds((sin (#) tan)`|Z).x = sin.x + sin.x/(cos.x)^2
proof
let x;
assume
A8: x in Z;
then ((sin (#) tan)`|Z).x = diff(sin,x)*tan.x+sin.x*diff(tan,x) by A2,A5,A6
,FDIFF_1:21
.=cos.x*tan.x+sin.x*diff(tan,x) by SIN_COS:64
.=cos.x*tan.x+sin.x*(1/(cos.x)^2) by A7,A8
.=(sin.x/cos.x)*(cos.x/1)+sin.x/(cos.x)^2 by A4,A8,RFUNCT_1:def 1
.=sin.x*(cos.x/cos.x) + sin.x/(cos.x)^2
.=sin.x* 1 + sin.x/(cos.x)^2 by A4,A8,FDIFF_8:1,XCMPLX_1:60
.= sin.x +sin.x/(cos.x)^2;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=sin.x * cot.x
theorem
Z c= dom (sin (#) cot) implies (sin (#) cot) is_differentiable_on Z &
for x st x in Z holds((sin (#) cot)`|Z).x = cos.x*cot.x - 1/sin.x
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin (#) cot);
then
A3: Z c= dom sin /\ dom cot by VALUED_1:def 4;
then
A4: 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 A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A5: cot is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
A7: for x st x in Z holds diff(cot, x)=-1/(sin.x)^2
proof
let x;
assume x in Z;
then sin.x<>0 by A4,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
for x st x in Z holds((sin (#) cot)`|Z).x = cos.x*cot.x- 1/sin.x
proof
let x;
assume
A8: x in Z;
then ((sin (#) cot)`|Z).x = diff(sin,x)*cot.x+sin.x*diff(cot,x) by A2,A5,A6
,FDIFF_1:21
.=cos.x*cot.x+sin.x*diff(cot,x) by SIN_COS:64
.=cos.x*cot.x+sin.x*(-1/(sin.x)^2) by A7,A8
.=cos.x*cot.x-sin.x/(sin.x)^2
.=cos.x*cot.x-sin.x/sin.x/sin.x by XCMPLX_1:78
.=cos.x*cot.x-1/sin.x by A4,A8,FDIFF_8:2,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=cos.x * tan.x
theorem
Z c= dom (cos (#) tan) implies (cos (#) tan) is_differentiable_on Z &
for x st x in Z holds((cos (#) tan)`|Z).x = -(sin.x)^2/cos.x+1/cos.x
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos (#) tan);
then
A3: Z c= dom cos /\ dom tan by VALUED_1:def 4;
then
A4: 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 A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A5: tan is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
A7: for x st x in Z holds diff(tan, x)=1/(cos.x)^2
proof
let x;
assume x in Z;
then cos.x<>0 by A4,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
for x st x in Z holds((cos (#) tan)`|Z).x = -(sin.x)^2/cos.x+1/cos.x
proof
let x;
assume
A8: x in Z;
then ((cos (#) tan)`|Z).x= diff(cos,x)*tan.x+cos.x*diff(tan,x) by A2,A5,A6,
FDIFF_1:21
.=tan.x*(-sin.x)+cos.x*diff(tan,x) by SIN_COS:63
.=tan.x*(-sin.x)+cos.x*(1/(cos.x)^2) by A7,A8
.=(sin.x/cos.x)*(-sin.x/1)+cos.x/(cos.x)^2 by A4,A8,RFUNCT_1:def 1
.=-(sin.x)^2/cos.x+cos.x/cos.x/cos.x by XCMPLX_1:78
.=-(sin.x)^2/cos.x+1/cos.x by A4,A8,FDIFF_8:1,XCMPLX_1:60;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=sin.x * cos.x
theorem
Z c= dom (sin (#) cos) implies (sin (#) cos) is_differentiable_on Z &
for x st x in Z holds((sin (#) cos)`|Z).x =(cos.x)^2-(sin.x)^2
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
A2: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A3: Z c= dom (sin (#) cos);
then
A4: Z c= dom sin /\ dom cos by VALUED_1:def 4;
then Z c= dom cos by XBOOLE_1:18;
then
A5: cos is_differentiable_on Z by A2,FDIFF_1:9;
Z c= dom sin by A4,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin (#) cos)`|Z).x =(cos.x)^2-(sin.x)^2
proof
let x;
assume x in Z;
then
((sin (#) cos)`|Z).x = diff(sin,x)*cos.x + sin.x*diff(cos,x) by A3,A6,A5,
FDIFF_1:21
.=cos.x*cos.x +sin.x*diff(cos,x) by SIN_COS:64
.=cos.x*cos.x +sin.x*(-sin.x) by SIN_COS:63
.=(cos.x)^2-(sin.x)^2;
hence thesis;
end;
hence thesis by A3,A6,A5,FDIFF_1:21;
end;
:: f.x=ln.x * sin.x
theorem
Z c= dom (ln(#)sin) implies ln(#)sin is_differentiable_on Z & for x st
x in Z holds ((ln(#)sin)`|Z).x = sin.x/x+ln.x*cos.x
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (ln(#)sin);
then
A3: Z c= dom ln /\ dom sin by VALUED_1:def 4;
then Z c= dom sin by XBOOLE_1:18;
then
A4: sin is_differentiable_on Z by A1,FDIFF_1:9;
A5: Z c= dom ln by A3,XBOOLE_1:18;
A6: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A5,TAYLOR_1:18;
then x in {g where g is Real: 0<g} by XXREAL_1:230;
then ex g being Real st x=g & 0<g;
hence thesis;
end;
then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
then
A7: ln is_differentiable_on Z by A5,FDIFF_1:9;
A8: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A6;
then x in {g where g is Real : 0<g};
then x in right_open_halfline(0) by XXREAL_1:230;
hence thesis by TAYLOR_1:18;
end;
for x st x in Z holds ((ln(#)sin)`|Z).x = sin.x/x+ln.x*cos.x
proof
let x;
assume
A9: x in Z;
then ((ln(#)sin)`|Z).x =(sin.x)*diff(ln,x)+(ln.x)*diff(sin,x) by A2,A7,A4,
FDIFF_1:21
.=sin.x*(1/x)+ln.x*diff(sin,x) by A8,A9
.=sin.x/x+ln.x*cos.x by SIN_COS:64;
hence thesis;
end;
hence thesis by A2,A7,A4,FDIFF_1:21;
end;
:: f.x=ln.x * cos.x
theorem
Z c= dom (ln(#)cos) implies ln(#)cos is_differentiable_on Z & for x st
x in Z holds ((ln(#)cos)`|Z).x = cos.x/x - ln.x*sin.x
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (ln(#)cos);
then
A3: Z c= dom ln /\ dom cos by VALUED_1:def 4;
then Z c= dom cos by XBOOLE_1:18;
then
A4: cos is_differentiable_on Z by A1,FDIFF_1:9;
A5: Z c= dom ln by A3,XBOOLE_1:18;
A6: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A5,TAYLOR_1:18;
then x in {g where g is Real: 0<g} by XXREAL_1:230;
then ex g being Real st x=g & 0<g;
hence thesis;
end;
then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
then
A7: ln is_differentiable_on Z by A5,FDIFF_1:9;
A8: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A6;
then x in {g where g is Real: 0<g};
then x in right_open_halfline(0) by XXREAL_1:230;
hence thesis by TAYLOR_1:18;
end;
for x st x in Z holds ((ln(#)cos)`|Z).x = cos.x/x - ln.x*sin.x
proof
let x;
assume
A9: x in Z;
then
((ln(#)cos)`|Z).x =(cos.x)*diff(ln,x)+ln.x*diff(cos,x) by A2,A7,A4,
FDIFF_1:21
.=cos.x*(1/x)+ln.x*diff(cos,x) by A8,A9
.=cos.x/x+ln.x*(-sin.x) by SIN_COS:63;
hence thesis;
end;
hence thesis by A2,A7,A4,FDIFF_1:21;
end;
:: f.x=ln.x * exp_R.x
theorem
Z c= dom (ln(#)exp_R) implies ln(#)exp_R is_differentiable_on Z & for
x st x in Z holds ((ln(#)exp_R)`|Z).x = exp_R.x/x + ln.x*exp_R.x
proof
A1: for x st x in Z holds exp_R is_differentiable_in x by SIN_COS:65;
assume
A2: Z c= dom (ln(#)exp_R);
then
A3: Z c= dom ln /\ dom exp_Rby VALUED_1:def 4;
then Z c= dom exp_R by XBOOLE_1:18;
then
A4: exp_R is_differentiable_on Z by A1,FDIFF_1:9;
A5: Z c= dom ln by A3,XBOOLE_1:18;
A6: for x st x in Z holds x>0
proof
let x;
assume x in Z;
then x in right_open_halfline(0) by A5,TAYLOR_1:18;
then x in {g where g is Real: 0<g} by XXREAL_1:230;
then ex g being Real st x=g & 0<g;
hence thesis;
end;
then for x st x in Z holds ln is_differentiable_in x by TAYLOR_1:18;
then
A7: ln is_differentiable_on Z by A5,FDIFF_1:9;
A8: for x st x in Z holds diff(ln,x) = 1/x
proof
let x;
assume x in Z;
then x>0 by A6;
then x in {g where g is Real: 0<g};
then x in right_open_halfline(0) by XXREAL_1:230;
hence thesis by TAYLOR_1:18;
end;
for x st x in Z holds ((ln(#)exp_R)`|Z).x = exp_R.x/x + ln.x*exp_R.x
proof
let x;
assume
A9: x in Z;
then
((ln(#)exp_R)`|Z).x = exp_R.x*diff(ln,x)+ln.x*diff(exp_R,x) by A2,A7,A4,
FDIFF_1:21
.=exp_R.x*(1/x) + ln.x*diff(exp_R,x) by A8,A9
.=exp_R.x*(1/x) + ln.x*exp_R.x by SIN_COS:65;
hence thesis;
end;
hence thesis by A2,A7,A4,FDIFF_1:21;
end;
::f.x=ln.(ln.x)
theorem
Z c= dom (ln*ln) & (for x st x in Z holds x>0) implies ln*ln
is_differentiable_on Z & for x st x in Z holds ((ln*ln)`|Z).x = 1/(ln.x*x)
proof
assume that
A1: Z c= dom (ln*ln) and
A2: for x st x in Z holds x>0;
A3: for x st x in Z holds ln.x>0
proof
let x;
assume x in Z;
then
A4: ln.x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
]. 0,+infty.[ = {g where g is Real: 0<g} by XXREAL_1:230;
then ex g being Real st ln.x=g & 0<g by A4;
hence thesis;
end;
A5: for x st x in Z holds ln*ln is_differentiable_in x
proof
let x;
assume
A6: x in Z;
then
A7: ln.x > 0 by A3;
ln is_differentiable_in x by A2,A6,TAYLOR_1:18;
hence thesis by A7,TAYLOR_1:20;
end;
then
A8: ln*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*ln)`|Z).x = 1/(ln.x*x)
proof
let x;
A9: ]. 0,+infty.[ = {g where g is Real: 0<g} by XXREAL_1:230;
assume
A10: x in Z;
then
A11: ln.x >0 by A3;
x > 0 by A2,A10;
then
A12: x in right_open_halfline(0) by A9;
ln is_differentiable_in x by A2,A10,TAYLOR_1:18;
then diff(ln*ln,x) =diff(ln,x)/ln.x by A11,TAYLOR_1:20
.=(1/ln.x) * (1/x) by A12,TAYLOR_1:18
.=1/(ln.x*x) by XCMPLX_1:102;
hence thesis by A8,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
::f.x=exp_R.(exp_R.x)
theorem
Z c= dom (exp_R*exp_R) implies exp_R*exp_R is_differentiable_on Z &
for x st x in Z holds ((exp_R*exp_R)`|Z).x = exp_R.(exp_R.x)*exp_R.x
proof
A1: for x st x in Z holds exp_R*exp_R is_differentiable_in x
proof
let x;
assume x in Z;
A2: exp_R is_differentiable_in exp_R.x by SIN_COS:65;
exp_R is_differentiable_in x by SIN_COS:65;
hence thesis by A2,FDIFF_2:13;
end;
assume
A3: Z c= dom (exp_R*exp_R);
then
A4: exp_R*exp_R is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*exp_R)`|Z).x = exp_R.(exp_R.x)*exp_R.x
proof
let x;
assume
A5: x in Z;
A6: exp_R is_differentiable_in exp_R.x by SIN_COS:65;
exp_R is_differentiable_in x by SIN_COS:65;
then diff(exp_R*exp_R,x) = diff(exp_R,exp_R.x)*diff(exp_R,x) by A6,
FDIFF_2:13
.=exp_R.(exp_R.x)*diff(exp_R,x) by SIN_COS:65
.=exp_R.(exp_R.x)*exp_R.x by SIN_COS:65;
hence thesis by A4,A5,FDIFF_1:def 7;
end;
hence thesis by A3,A1,FDIFF_1:9;
end;
::f.x=sin.(tan.x)
theorem
Z c= dom (sin*tan) implies sin*tan is_differentiable_on Z & for x st x
in Z holds ((sin*tan)`|Z).x = cos(tan.x)/(cos.x)^2
proof
assume
A1: Z c= dom (sin*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 FDIFF_8:1;
end;
A3: for x st x in Z holds sin*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;
sin is_differentiable_in tan.x by SIN_COS:64;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: sin*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*tan)`|Z).x = cos(tan.x)/(cos.x)^2
proof
let x;
A6: sin is_differentiable_in tan.x by SIN_COS:64;
assume
A7: x in Z;
then
A8: cos.x<>0 by A2;
then tan is_differentiable_in x by FDIFF_7:46;
then diff(sin*tan,x) = diff(sin,tan.x)*diff(tan,x) by A6,FDIFF_2:13
.=cos(tan.x) * diff(tan,x) by SIN_COS:64
.=cos(tan.x) * (1/(cos.x)^2) by A8,FDIFF_7:46
.=cos(tan.x)/(cos.x)^2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=sin.(cot.x)
theorem
Z c= dom (sin*cot) implies sin*cot is_differentiable_on Z & for x st x
in Z holds ((sin*cot)`|Z).x =-cos(cot.x)/(sin.x)^2
proof
assume
A1: Z c= dom (sin*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 FDIFF_8:2;
end;
A3: for x st x in Z holds sin*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;
sin is_differentiable_in cot.x by SIN_COS:64;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: sin*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*cot)`|Z).x = -cos(cot.x)/(sin.x)^2
proof
let x;
A6: sin is_differentiable_in cot.x by SIN_COS:64;
assume
A7: x in Z;
then
A8: sin.x<>0 by A2;
then cot is_differentiable_in x by FDIFF_7:47;
then diff(sin*cot,x) = diff(sin,cot.x)*diff(cot,x) by A6,FDIFF_2:13
.=cos(cot.x) *diff(cot,x) by SIN_COS:64
.=cos(cot.x) * (-1/(sin.x)^2) by A8,FDIFF_7:47
.=-cos(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=cos.(tan.x)
theorem
Z c= dom (cos*tan) implies cos*tan is_differentiable_on Z & for x st x
in Z holds ((cos*tan)`|Z).x =-sin(tan.x)/(cos.x)^2
proof
assume
A1: Z c= dom (cos*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 FDIFF_8:1;
end;
A3: for x st x in Z holds cos*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;
cos is_differentiable_in tan.x by SIN_COS:63;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: cos*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*tan)`|Z).x = -sin(tan.x)/(cos.x)^2
proof
let x;
A6: cos is_differentiable_in tan.x by SIN_COS:63;
assume
A7: x in Z;
then
A8: cos.x<>0 by A2;
then tan is_differentiable_in x by FDIFF_7:46;
then diff(cos*tan,x) = diff(cos,tan.x)*diff(tan,x) by A6,FDIFF_2:13
.=(-sin(tan.x))*diff(tan,x) by SIN_COS:63
.=(-sin(tan.x)) * (1/(cos.x)^2) by A8,FDIFF_7:46
.=-sin(tan.x)/(cos.x)^2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cos.(cot.x)
theorem
Z c= dom (cos*cot) implies cos*cot is_differentiable_on Z & for x st x
in Z holds ((cos*cot)`|Z).x =sin(cot.x)/(sin.x)^2
proof
assume
A1: Z c= dom (cos*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 FDIFF_8:2;
end;
A3: for x st x in Z holds cos*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;
cos is_differentiable_in cot.x by SIN_COS:63;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: cos*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*cot)`|Z).x =sin(cot.x)/(sin.x)^2
proof
let x;
A6: cos is_differentiable_in cot.x by SIN_COS:63;
assume
A7: x in Z;
then
A8: sin.x<>0 by A2;
then cot is_differentiable_in x by FDIFF_7:47;
then diff(cos*cot,x) = diff(cos,cot.x)*diff(cot,x) by A6,FDIFF_2:13
.=(-sin(cot.x))*diff(cot,x) by SIN_COS:63
.=(-sin(cot.x)) * (-1/(sin.x)^2) by A8,FDIFF_7:47
.=sin(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=sin.x*(tan.x+cot.x)
theorem
Z c= dom (sin(#)(tan+cot)) implies sin(#)(tan+cot)
is_differentiable_on Z & for x st x in Z holds ((sin(#)(tan+cot))`|Z).x =cos.x*
(tan.x+cot.x)+sin.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin(#)(tan+cot));
then
A3: Z c= dom (tan+cot) /\ dom sin by VALUED_1:def 4;
then
A4: Z c= dom (tan+cot) by XBOOLE_1:18;
then
A5: tan+cot is_differentiable_on Z by Th6;
Z c=dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin(#)(tan+cot)`|Z).x =cos.x*(tan.x+cot.x)+sin.x*
(1/(cos.x)^2-1/(sin.x)^2)
proof
let x;
assume
A7: x in Z;
then
(sin(#)(tan+cot)`|Z).x = ((tan+cot).x)*diff(sin,x)+sin.x*diff(tan+cot
,x) by A2,A5,A6,FDIFF_1:21
.= (tan.x+cot.x)*diff(sin,x)+sin.x*diff(tan+cot,x) by A4,A7,
VALUED_1:def 1
.= (tan.x+cot.x) * cos.x +sin.x * diff(tan+cot,x) by SIN_COS:64
.=(tan.x+cot.x) * cos.x +sin.x * ((tan+cot)`|Z).x by A5,A7,FDIFF_1:def 7
.=(tan.x+cot.x) * cos.x +sin.x * (1/(cos.x)^2-1/(sin.x)^2) by A4,A7,Th6;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
::f.x=cos.x*(tan.x+cot.x)
theorem
Z c= dom (cos(#)(tan+cot)) implies cos(#)(tan+cot)
is_differentiable_on Z & for x st x in Z holds ((cos(#)(tan+cot))`|Z).x =-sin.x
*(tan.x+cot.x)+cos.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos(#)(tan+cot));
then
A3: Z c= dom (tan+cot) /\ dom cos by VALUED_1:def 4;
then
A4: Z c= dom (tan+cot) by XBOOLE_1:18;
then
A5: tan+cot is_differentiable_on Z by Th6;
Z c=dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos(#)(tan+cot)`|Z).x =-sin.x*(tan.x+cot.x)+cos.x
*(1/(cos.x)^2-1/(sin.x)^2)
proof
let x;
assume
A7: x in Z;
then (cos(#)(tan+cot)`|Z).x = ((tan+cot).x)*diff(cos,x) + cos.x*diff(tan+
cot,x) by A2,A5,A6,FDIFF_1:21
.= (tan.x+cot.x)*diff(cos,x) + cos.x*diff(tan+cot,x) by A4,A7,
VALUED_1:def 1
.= (tan.x+cot.x) * (-sin.x) + cos.x * diff(tan+cot,x) by SIN_COS:63
.=(tan.x+cot.x) * (-sin.x) + cos.x * ((tan+cot)`|Z).x by A5,A7,
FDIFF_1:def 7
.=(tan.x+cot.x) * (-sin.x) +cos.x * (1/(cos.x)^2-1/(sin.x)^2) by A4,A7
,Th6;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=sin.x*(tan.x-cot.x)
theorem
Z c= dom (sin(#)(tan-cot)) implies sin(#)(tan-cot)
is_differentiable_on Z & for x st x in Z holds ((sin(#)(tan-cot))`|Z).x =cos.x*
(tan.x-cot.x)+sin.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin(#)(tan-cot));
then
A3: Z c= dom (tan-cot) /\ dom sin by VALUED_1:def 4;
then
A4: Z c= dom (tan-cot) by XBOOLE_1:18;
then
A5: tan-cot is_differentiable_on Z by Th5;
Z c= dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin(#)(tan-cot)`|Z).x =cos.x*(tan.x-cot.x)+sin.x*
(1/(cos.x)^2+1/(sin.x)^2)
proof
let x;
assume
A7: x in Z;
then
(sin(#)(tan-cot)`|Z).x = ((tan-cot).x)*diff(sin,x)+sin.x*diff(tan-cot
,x) by A2,A5,A6,FDIFF_1:21
.= (tan.x-cot.x)*diff(sin,x)+sin.x*diff(tan-cot,x) by A4,A7,VALUED_1:13
.= (tan.x-cot.x) * cos.x +sin.x * diff(tan-cot,x) by SIN_COS:64
.=(tan.x-cot.x) * cos.x +sin.x * ((tan-cot)`|Z).x by A5,A7,FDIFF_1:def 7
.=(tan.x-cot.x) * cos.x +sin.x * (1/(cos.x)^2+1/(sin.x)^2) by A4,A7,Th5;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=cos.x*(tan.x-cot.x)
theorem
Z c= dom (cos(#)(tan-cot)) implies cos(#)(tan-cot)
is_differentiable_on Z & for x st x in Z holds ((cos(#)(tan-cot))`|Z).x =-sin.x
*(tan.x-cot.x)+cos.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos(#)(tan-cot));
then
A3: Z c= dom (tan-cot) /\ dom cos by VALUED_1:def 4;
then
A4: Z c= dom (tan-cot) by XBOOLE_1:18;
then
A5: tan-cot is_differentiable_on Z by Th5;
Z c=dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos(#)(tan-cot)`|Z).x =-sin.x*(tan.x-cot.x)+cos.x
*(1/(cos.x)^2+1/(sin.x)^2)
proof
let x;
assume
A7: x in Z;
then
(cos(#)(tan-cot)`|Z).x = ((tan-cot).x)*diff(cos,x)+cos.x*diff(tan-cot
,x) by A2,A5,A6,FDIFF_1:21
.= (tan.x-cot.x)*diff(cos,x)+cos.x*diff(tan-cot,x) by A4,A7,VALUED_1:13
.= (tan.x-cot.x) *(-sin.x)+cos.x * diff(tan-cot,x) by SIN_COS:63
.=(tan.x-cot.x) * (-sin.x)+cos.x * ((tan-cot)`|Z).x by A5,A7,
FDIFF_1:def 7
.=(tan.x-cot.x) * (-sin.x)+cos.x * (1/(cos.x)^2+1/(sin.x)^2) by A4,A7,Th5
;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
::f.x=exp_R.x*(tan.x + cot.x)
theorem
Z c= dom (exp_R(#)(tan+cot)) implies exp_R(#)(tan+cot)
is_differentiable_on Z & for x st x in Z holds ((exp_R(#)(tan+cot))`|Z).x =
exp_R.x*(tan.x+cot.x)+exp_R.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
assume
A1: Z c= dom (exp_R(#)(tan+cot));
then Z c= dom (tan+cot) /\ dom exp_R by VALUED_1:def 4;
then
A2: Z c= dom (tan+cot) by XBOOLE_1:18;
then
A3: tan+cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds (exp_R(#)(tan+cot)`|Z).x =exp_R.x*(tan.x+cot.x)+
exp_R.x*(1/(cos.x)^2-1/(sin.x)^2)
proof
let x;
assume
A5: x in Z;
then (exp_R(#)(tan+cot)`|Z).x = ((tan+cot).x)*diff(exp_R,x)+exp_R.x*diff(
tan+cot,x) by A1,A3,A4,FDIFF_1:21
.= (tan.x+cot.x)*diff(exp_R,x)+exp_R.x*diff(tan+cot,x) by A2,A5,
VALUED_1:def 1
.=exp_R.x*(tan.x+cot.x)+exp_R.x*diff(tan+cot,x) by TAYLOR_1:16
.=exp_R.x*(tan.x+cot.x)+exp_R.x*((tan+cot)`|Z).x by A3,A5,FDIFF_1:def 7
.=exp_R.x*(tan.x+cot.x)+exp_R.x*(1/(cos.x)^2-1/(sin.x)^2) by A2,A5,Th6;
hence thesis;
end;
hence thesis by A1,A3,A4,FDIFF_1:21;
end;
::f.x=exp_R.x*(tan.x - cot.x)
theorem
Z c= dom (exp_R(#)(tan-cot)) implies exp_R(#)(tan-cot)
is_differentiable_on Z & for x st x in Z holds ((exp_R(#)(tan-cot))`|Z).x =
exp_R.x*(tan.x-cot.x)+exp_R.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
assume
A1: Z c= dom (exp_R(#)(tan-cot));
then Z c= dom (tan-cot) /\ dom exp_R by VALUED_1:def 4;
then
A2: Z c= dom (tan-cot) by XBOOLE_1:18;
then
A3: tan-cot is_differentiable_on Z by Th5;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds (exp_R(#)(tan-cot)`|Z).x =exp_R.x*(tan.x-cot.x)+
exp_R.x*(1/(cos.x)^2+1/(sin.x)^2)
proof
let x;
assume
A5: x in Z;
then (exp_R(#)(tan-cot)`|Z).x = ((tan-cot).x)*diff(exp_R,x)+exp_R.x*diff(
tan-cot,x) by A1,A3,A4,FDIFF_1:21
.=(tan.x-cot.x)*diff(exp_R,x)+exp_R.x*diff(tan-cot,x) by A2,A5,
VALUED_1:13
.=exp_R.x*(tan.x-cot.x)+exp_R.x*diff(tan-cot,x) by TAYLOR_1:16
.=exp_R.x*(tan.x-cot.x)+exp_R.x*((tan-cot)`|Z).x by A3,A5,FDIFF_1:def 7
.=exp_R.x*(tan.x-cot.x)+exp_R.x*(1/(cos.x)^2+1/(sin.x)^2) by A2,A5,Th5;
hence thesis;
end;
hence thesis by A1,A3,A4,FDIFF_1:21;
end;
::f.x=sin.x*(sin.x+cos.x)
theorem
Z c= dom (sin(#)(sin+cos)) implies sin(#)(sin+cos)
is_differentiable_on Z & for x st x in Z holds ((sin(#)(sin+cos))`|Z).x =(cos.x
)^2+2*sin.x*cos.x-(sin.x)^2
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin(#)(sin+cos));
then
A3: Z c= dom (sin+cos) /\ dom sin by VALUED_1:def 4;
then
A4: Z c= dom (sin+cos) by XBOOLE_1:18;
then
A5: sin+cos is_differentiable_on Z by FDIFF_7:38;
Z c= dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin(#)(sin+cos))`|Z).x =(cos.x)^2+2*sin.x*cos.x-
(sin.x)^2
proof
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
assume
A7: x in Z;
then ((sin(#)(sin+cos))`|Z).x =((sin+cos).x)*diff(sin,x) + (sin.x)*diff((
sin+cos),x) by A2,A5,A6,FDIFF_1:21
.=(sin.xx+cos.xx)*diff(sin,x) + (sin.x)*diff((sin+cos),x)
by VALUED_1:1
.=(sin.x+cos.x)*cos.x + (sin.x)*diff((sin+cos),x) by SIN_COS:64
.=(sin.x+cos.x)*cos.x + (sin.x)*((sin+cos)`|Z).x by A5,A7,FDIFF_1:def 7
.=(sin.x+cos.x)*cos.x + (sin.x)*(cos.x-sin.x) by A4,A7,FDIFF_7:38;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
::f.x=sin.x*(sin.x-cos.x)
theorem
Z c= dom (sin(#)(sin-cos)) implies sin(#)(sin-cos)
is_differentiable_on Z & for x st x in Z holds ((sin(#)(sin-cos))`|Z).x =(sin.x
)^2+2*sin.x*cos.x-(cos.x)^2
proof
A1: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
assume
A2: Z c= dom (sin(#)(sin-cos));
then
A3: Z c= dom (sin-cos) /\ dom sin by VALUED_1:def 4;
then
A4: Z c= dom (sin-cos) by XBOOLE_1:18;
then
A5: sin-cos is_differentiable_on Z by FDIFF_7:39;
Z c= dom sin by A3,XBOOLE_1:18;
then
A6: sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin(#)(sin-cos))`|Z).x =(sin.x)^2+2*sin.x*cos.x-
(cos.x)^2
proof
let x;
assume
A7: x in Z;
then ((sin(#)(sin-cos))`|Z).x =((sin-cos).x)*diff(sin,x) + (sin.x)*diff((
sin-cos),x) by A2,A5,A6,FDIFF_1:21
.=(sin.x-cos.x)*diff(sin,x) + (sin.x)*diff((sin-cos),x) by A4,A7,
VALUED_1:13
.=(sin.x-cos.x)*cos.x + (sin.x)*diff((sin-cos),x) by SIN_COS:64
.=(sin.x-cos.x)*cos.x + (sin.x)*((sin-cos)`|Z).x by A5,A7,FDIFF_1:def 7
.=(sin.x-cos.x)*cos.x + (sin.x)*(cos.x+sin.x) by A4,A7,FDIFF_7:39;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=cos.x*(sin.x-cos.x)
theorem
Z c= dom (cos(#)(sin-cos)) implies cos(#)(sin-cos)
is_differentiable_on Z & for x st x in Z holds ((cos(#)(sin-cos))`|Z).x =(cos.x
)^2+2*sin.x*cos.x-(sin.x)^2
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos(#)(sin-cos));
then
A3: Z c= dom (sin-cos) /\ dom cos by VALUED_1:def 4;
then
A4: Z c= dom (sin-cos) by XBOOLE_1:18;
then
A5: sin-cos is_differentiable_on Z by FDIFF_7:39;
Z c= dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos(#)(sin-cos))`|Z).x =(cos.x)^2+2*sin.x*cos.x-
(sin.x)^2
proof
let x;
assume
A7: x in Z;
then ((cos(#)(sin-cos))`|Z).x =((sin-cos).x)*diff(cos,x) + (cos.x)*diff((
sin-cos),x) by A2,A5,A6,FDIFF_1:21
.=(sin.x-cos.x)*diff(cos,x) + (cos.x)*diff((sin-cos),x) by A4,A7,
VALUED_1:13
.=(sin.x-cos.x)*(-sin.x) + (cos.x)*diff((sin-cos),x) by SIN_COS:63
.=(sin.x-cos.x)*(-sin.x) + (cos.x)*((sin-cos)`|Z).x by A5,A7,
FDIFF_1:def 7
.=(sin.x-cos.x)*(-sin.x) + (cos.x)*(cos.x+sin.x) by A4,A7,FDIFF_7:39;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
:: f.x=cos.x*(sin.x+cos.x)
theorem
Z c= dom (cos(#)(sin+cos)) implies cos(#)(sin+cos)
is_differentiable_on Z & for x st x in Z holds ((cos(#)(sin+cos))`|Z).x =(cos.x
)^2-2*sin.x*cos.x-(sin.x)^2
proof
A1: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
assume
A2: Z c= dom (cos(#)(sin+cos));
then
A3: Z c= dom (sin+cos) /\ dom cos by VALUED_1:def 4;
then
A4: Z c= dom (sin+cos) by XBOOLE_1:18;
then
A5: sin+cos is_differentiable_on Z by FDIFF_7:38;
Z c= dom cos by A3,XBOOLE_1:18;
then
A6: cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos(#)(sin+cos))`|Z).x =(cos.x)^2-2*sin.x*cos.x-
(sin.x)^2
proof
let x;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
assume
A7: x in Z;
then ((cos(#)(sin+cos))`|Z).x =((sin+cos).x)*diff(cos,x) + (cos.x)*diff((
sin+cos),x) by A2,A5,A6,FDIFF_1:21
.=(sin.xx+cos.xx)*diff(cos,x) + (cos.x)*diff((sin+cos),x) by VALUED_1:1
.=(sin.x+cos.x)*(-sin.x) + (cos.x)*diff((sin+cos),x) by SIN_COS:63
.=(sin.x+cos.x)*(-sin.x) +(cos.x)*((sin+cos)`|Z).x by A5,A7,FDIFF_1:def 7
.=(sin.x+cos.x)*(-sin.x) + (cos.x)*(cos.x-sin.x) by A4,A7,FDIFF_7:38;
hence thesis;
end;
hence thesis by A2,A5,A6,FDIFF_1:21;
end;
::f.x=sin.(tan.x+cot.x)
theorem
Z c= dom (sin*(tan+cot)) implies sin*(tan+cot) is_differentiable_on Z
& for x st x in Z holds (sin*(tan+cot)`|Z).x = cos.(tan.x+cot.x)*(1/(cos.x)^2-1
/(sin.x)^2)
proof
assume that
A1: Z c= dom (sin*(tan+cot));
dom (sin*(tan+cot)) c= dom (tan+cot) by RELAT_1:25;
then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds sin*(tan + cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:9;
sin is_differentiable_in (tan+cot).x by SIN_COS:64;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin*(tan+cot)`|Z).x = cos.(tan.x+cot.x)*(1/(cos.
x)^2-1/(sin.x)^2)
proof
let x;
A7: sin is_differentiable_in (tan+cot).x by SIN_COS:64;
assume
A8: x in Z;
then tan + cot is_differentiable_in x by A3,FDIFF_1:9;
then
diff(sin*(tan + cot),x) = diff(sin, (tan+cot).x)*diff((tan+cot),x) by A7,
FDIFF_2:13
.=cos.((tan+cot).x)*diff((tan+cot),x) by SIN_COS:64
.=cos.((tan+cot).x)*((tan+cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=cos.((tan+cot).x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,Th6
.=cos.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,VALUED_1:def 1;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=sin.(tan.x-cot.x)
theorem
Z c= dom (sin*(tan-cot)) implies sin*(tan-cot) is_differentiable_on Z
& for x st x in Z holds (sin*(tan-cot)`|Z).x = cos.(tan.x-cot.x)*(1/(cos.x)^2+1
/(sin.x)^2)
proof
assume that
A1: Z c= dom (sin*(tan-cot));
dom (sin*(tan-cot)) c= dom (tan-cot) by RELAT_1:25;
then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds sin*(tan - cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:9;
sin is_differentiable_in (tan-cot).x by SIN_COS:64;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin*(tan-cot)`|Z).x = cos.(tan.x-cot.x)*(1/(cos.
x)^2+1/(sin.x)^2)
proof
let x;
A7: sin is_differentiable_in (tan-cot).x by SIN_COS:64;
assume
A8: x in Z;
then tan - cot is_differentiable_in x by A3,FDIFF_1:9;
then diff(sin*(tan -cot),x) = diff(sin, (tan-cot).x)*diff((tan-cot),x) by
A7,FDIFF_2:13
.=cos.((tan-cot).x)*diff((tan-cot),x) by SIN_COS:64
.=cos.((tan-cot).x)*((tan-cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=cos.((tan-cot).x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,Th5
.=cos.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,VALUED_1:13;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cos.(tan.x-cot.x)
theorem
Z c= dom (cos*(tan-cot)) implies cos*(tan-cot) is_differentiable_on Z
& for x st x in Z holds (cos*(tan-cot)`|Z).x = -sin.(tan.x-cot.x)*(1/(cos.x)^2+
1/(sin.x)^2)
proof
assume that
A1: Z c= dom (cos*(tan-cot));
dom (cos*(tan-cot)) c= dom (tan-cot) by RELAT_1:25;
then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds cos*(tan - cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:9;
cos is_differentiable_in (tan-cot).x by SIN_COS:63;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos*(tan-cot)`|Z).x = -sin.(tan.x-cot.x)*(1/(cos
.x)^2+1/(sin.x)^2)
proof
let x;
A7: cos is_differentiable_in (tan-cot).x by SIN_COS:63;
assume
A8: x in Z;
then tan - cot is_differentiable_in x by A3,FDIFF_1:9;
then diff(cos*(tan -cot),x) = diff(cos, (tan-cot).x)*diff((tan-cot),x) by
A7,FDIFF_2:13
.=(-sin.((tan-cot).x))*diff((tan-cot),x) by SIN_COS:63
.=(-sin.((tan-cot).x))*((tan-cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=(-sin.((tan-cot).x))*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,Th5
.=(-sin.(tan.x-cot.x))*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,VALUED_1:13;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cos.(tan.x+cot.x)
theorem
Z c= dom (cos*(tan+cot)) implies cos*(tan+cot) is_differentiable_on Z
& for x st x in Z holds (cos*(tan+cot)`|Z).x = -sin.(tan.x+cot.x)*(1/(cos.x)^2-
1/(sin.x)^2)
proof
assume that
A1: Z c= dom (cos*(tan+cot));
dom (cos*(tan+cot)) c= dom (tan+cot) by RELAT_1:25;
then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds cos*(tan + cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:9;
cos is_differentiable_in (tan+cot).x by SIN_COS:63;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos*(tan+cot)`|Z).x = -sin.(tan.x+cot.x)*(1/(cos
.x)^2-1/(sin.x)^2)
proof
let x;
A7: cos is_differentiable_in (tan+cot).x by SIN_COS:63;
assume
A8: x in Z;
then tan + cot is_differentiable_in x by A3,FDIFF_1:9;
then diff(cos*(tan +cot),x) = diff(cos, (tan+cot).x)*diff((tan+cot),x) by
A7,FDIFF_2:13
.=(-sin.((tan+cot).x))*diff((tan+cot),x) by SIN_COS:63
.=(-sin.((tan+cot).x))*((tan+cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=(-sin.((tan+cot).x))*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,Th6
.=(-sin.(tan.x+cot.x))*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,VALUED_1:def 1;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=exp_R.(tan.x + cot.x)
theorem
Z c= dom (exp_R*(tan+cot)) implies exp_R*(tan+cot)
is_differentiable_on Z & for x st x in Z holds (exp_R*(tan+cot)`|Z).x = exp_R.(
tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2)
proof
assume that
A1: Z c= dom (exp_R*(tan+cot));
dom (exp_R*(tan+cot)) c= dom (tan+cot) by RELAT_1:25;
then
A2: Z c=dom(tan+cot) by A1,XBOOLE_1:1;
then
A3: tan + cot is_differentiable_on Z by Th6;
A4: for x st x in Z holds exp_R*(tan + cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan + cot) is_differentiable_in x by A3,FDIFF_1:9;
exp_R is_differentiable_in (tan+cot).x by SIN_COS:65;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: exp_R*(tan + cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (exp_R*(tan+cot)`|Z).x = exp_R.(tan.x+cot.x)*(1/(
cos.x)^2-1/(sin.x)^2)
proof
let x;
A7: exp_R is_differentiable_in (tan+cot).x by SIN_COS:65;
assume
A8: x in Z;
then tan + cot is_differentiable_in x by A3,FDIFF_1:9;
then
diff(exp_R*(tan +cot),x) = diff(exp_R, (tan+cot).x)*diff((tan+cot),x)
by A7,FDIFF_2:13
.=exp_R.((tan+cot).x)*diff((tan+cot),x) by SIN_COS:65
.=exp_R.((tan+cot).x)*((tan+cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=exp_R.((tan+cot).x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,Th6
.=exp_R.(tan.x+cot.x)*(1/(cos.x)^2-1/(sin.x)^2) by A2,A8,VALUED_1:def 1;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=exp_R.(tan.x - cot.x)
theorem
Z c= dom (exp_R*(tan-cot)) implies exp_R*(tan-cot)
is_differentiable_on Z & for x st x in Z holds (exp_R*(tan-cot)`|Z).x = exp_R.(
tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2)
proof
assume that
A1: Z c= dom (exp_R*(tan-cot));
dom (exp_R*(tan-cot)) c= dom (tan-cot) by RELAT_1:25;
then
A2: Z c=dom(tan-cot) by A1,XBOOLE_1:1;
then
A3: tan - cot is_differentiable_on Z by Th5;
A4: for x st x in Z holds exp_R*(tan - cot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (tan - cot) is_differentiable_in x by A3,FDIFF_1:9;
exp_R is_differentiable_in (tan-cot).x by SIN_COS:65;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: exp_R*(tan - cot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (exp_R*(tan-cot)`|Z).x = exp_R.(tan.x-cot.x)*(1/(
cos.x)^2+1/(sin.x)^2)
proof
let x;
A7: exp_R is_differentiable_in (tan-cot).x by SIN_COS:65;
assume
A8: x in Z;
then tan - cot is_differentiable_in x by A3,FDIFF_1:9;
then
diff(exp_R*(tan -cot),x) = diff(exp_R, (tan-cot).x)*diff((tan-cot),x)
by A7,FDIFF_2:13
.=exp_R.((tan-cot).x)*diff((tan-cot),x) by SIN_COS:65
.=exp_R.((tan-cot).x)*((tan-cot)`|Z).x by A3,A8,FDIFF_1:def 7
.=exp_R.((tan-cot).x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,Th5
.=exp_R.(tan.x-cot.x)*(1/(cos.x)^2+1/(sin.x)^2) by A2,A8,VALUED_1:13;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=(tan.x-cot.x)/exp_.x
theorem
Z c= dom ((tan-cot)/exp_R) implies (tan-cot)/exp_R
is_differentiable_on Z & for x st x in Z holds (((tan-cot)/exp_R)`|Z).x = (1/(
cos.x)^2+1/(sin.x)^2-tan.x+cot.x)/exp_R.x
proof
A1: for x st x in Z holds exp_R.x<>0 by SIN_COS:54;
assume Z c= dom ((tan-cot)/exp_R);
then Z c= dom (tan-cot) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A2: Z c= dom (tan-cot) by XBOOLE_1:18;
then
A3: tan-cot is_differentiable_on Z by Th5;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A5: (tan-cot)/exp_R is_differentiable_on Z by A3,A1,FDIFF_2:21;
for x st x in Z holds (((tan-cot)/exp_R)`|Z).x =(1/(cos.x)^2+1/(sin.x)^2
-tan.x+cot.x)/exp_R.x
proof
let x;
A6: exp_R is_differentiable_in x by SIN_COS:65;
A7: exp_R.x <>0 by SIN_COS:54;
assume
A8: x in Z;
then
A9: (tan-cot).x=tan.x-cot.x by A2,VALUED_1:13;
tan-cot is_differentiable_in x by A3,A8,FDIFF_1:9;
then diff((tan-cot)/exp_R,x) =(diff(tan-cot,x) *exp_R.x -diff(exp_R,x) *(
tan-cot).x)/(exp_R.x)^2 by A6,A7,FDIFF_2:14
.=(((tan-cot)`|Z).x *exp_R.x-diff(exp_R,x) *(tan-cot).x)/(exp_R.x)^2
by A3,A8,FDIFF_1:def 7
.=((1/(cos.x)^2+1/(sin.x)^2)*exp_R.x-diff(exp_R,x)*(tan-cot).x) /(
exp_R.x)^2 by A2,A8,Th5
.=((1/(cos.x)^2+1/(sin.x)^2)*exp_R.x-exp_R.x*(tan.x-cot.x)) /(exp_R.x*
exp_R.x) by A9,SIN_COS:65
.=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))* (exp_R.x/((exp_R.x)*(exp_R.
x)))
.=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))* ((exp_R.x)/(exp_R.x)/(exp_R
.x)) by XCMPLX_1:78
.=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))*(1/exp_R.x) by A7,XCMPLX_1:60
.=(1/(cos.x)^2+1/(sin.x)^2-(tan.x-cot.x))/exp_R.x;
hence thesis by A5,A8,FDIFF_1:def 7;
end;
hence thesis by A3,A4,A1,FDIFF_2:21;
end;
::f.x=(tan.x+cot.x)/exp_.x
theorem
Z c= dom ((tan+cot)/exp_R) implies (tan+cot)/exp_R
is_differentiable_on Z & for x st x in Z holds (((tan+cot)/exp_R)`|Z).x = (1/(
cos.x)^2-1/(sin.x)^2-tan.x-cot.x)/exp_R.x
proof
A1: for x st x in Z holds exp_R.x<>0 by SIN_COS:54;
assume Z c= dom ((tan+cot)/exp_R);
then Z c= dom (tan+cot) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A2: Z c= dom (tan+cot) by XBOOLE_1:18;
then
A3: tan+cot is_differentiable_on Z by Th6;
A4: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A5: (tan+cot)/exp_R is_differentiable_on Z by A3,A1,FDIFF_2:21;
for x st x in Z holds (((tan+cot)/exp_R)`|Z).x =(1/(cos.x)^2-1/(sin.x)^2
-tan.x-cot.x)/exp_R.x
proof
let x;
A6: exp_R is_differentiable_in x by SIN_COS:65;
A7: exp_R.x <>0 by SIN_COS:54;
assume
A8: x in Z;
then
A9: (tan+cot).x=tan.x+cot.x by A2,VALUED_1:def 1;
tan+cot is_differentiable_in x by A3,A8,FDIFF_1:9;
then diff((tan+cot)/exp_R,x) =(diff(tan+cot,x) *exp_R.x -diff(exp_R,x) *(
tan+cot).x)/(exp_R.x)^2 by A6,A7,FDIFF_2:14
.=(((tan+cot)`|Z).x *exp_R.x-diff(exp_R,x) *(tan+cot).x)/(exp_R.x)^2
by A3,A8,FDIFF_1:def 7
.=((1/(cos.x)^2-1/(sin.x)^2)*exp_R.x-diff(exp_R,x)*(tan+cot).x) /(
exp_R.x)^2 by A2,A8,Th6
.=((1/(cos.x)^2-1/(sin.x)^2)*exp_R.x-exp_R.x*(tan.x+cot.x)) /(exp_R.x*
exp_R.x) by A9,SIN_COS:65
.=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))* (exp_R.x/((exp_R.x)*(exp_R.
x)))
.=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))* ((exp_R.x)/(exp_R.x)/(exp_R
.x)) by XCMPLX_1:78
.=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))*(1/exp_R.x) by A7,XCMPLX_1:60
.=(1/(cos.x)^2-1/(sin.x)^2-(tan.x+cot.x))/exp_R.x;
hence thesis by A5,A8,FDIFF_1:def 7;
end;
hence thesis by A3,A4,A1,FDIFF_2:21;
end;
:: f.x = sin.(sec.x)
theorem
Z c= dom (sin*sec) implies sin*sec is_differentiable_on Z & for x st x
in Z holds ((sin*sec)`|Z).x = cos.(sec.x)* sin.x/(cos.x)^2
proof
assume
A1: Z c= dom (sin*sec);
dom (sin*sec) c= dom sec by RELAT_1:25;
then
A2: Z c= dom sec by A1,XBOOLE_1:1;
A3: for x st x in Z holds sin*sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A2,RFUNCT_1:3;
then
A4: sec is_differentiable_in x by FDIFF_9:1;
sin is_differentiable_in sec.x by SIN_COS:64;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: sin*sec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*sec)`|Z).x = cos.(sec.x)* sin.x/(cos.x)^2
proof
let x;
A6: sin is_differentiable_in sec.x by SIN_COS:64;
assume
A7: x in Z;
then
A8: cos.x <>0 by A2,RFUNCT_1:3;
then sec is_differentiable_in x by FDIFF_9:1;
then diff(sin*sec,x) = diff(sin,sec.x)*diff(sec,x) by A6,FDIFF_2:13
.= cos(sec.x)*diff(sec,x) by SIN_COS:64
.= cos(sec.x)* (sin.x/(cos.x)^2) by A8,FDIFF_9:1
.=cos.(sec.x)* sin.x/(cos.x)^2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = cos.(sec.x)
theorem
Z c= dom (cos*sec) implies cos*sec is_differentiable_on Z & for x st x
in Z holds ((cos*sec)`|Z).x = -sin.(sec.x)* sin.x/(cos.x)^2
proof
assume
A1: Z c= dom (cos*sec);
dom (cos*sec) c= dom sec by RELAT_1:25;
then
A2: Z c= dom sec by A1,XBOOLE_1:1;
A3: for x st x in Z holds cos*sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x<>0 by A2,RFUNCT_1:3;
then
A4: sec is_differentiable_in x by FDIFF_9:1;
cos is_differentiable_in sec.x by SIN_COS:63;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: cos*sec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*sec)`|Z).x = -sin.(sec.x)* sin.x/(cos.x)^2
proof
let x;
A6: cos is_differentiable_in sec.x by SIN_COS:63;
assume
A7: x in Z;
then
A8: cos.x <>0 by A2,RFUNCT_1:3;
then sec is_differentiable_in x by FDIFF_9:1;
then diff(cos*sec,x) = diff(cos,sec.x)*diff(sec,x) by A6,FDIFF_2:13
.= (-sin(sec.x))*diff(sec,x) by SIN_COS:63
.= (-sin(sec.x))* (sin.x/(cos.x)^2) by A8,FDIFF_9:1
.=-sin.(sec.x)* sin.x/(cos.x)^2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: f.x = sin.(cosec.x)
theorem
Z c= dom (sin*cosec) implies sin*cosec is_differentiable_on Z & for x
st x in Z holds ((sin*cosec)`|Z).x = -cos.(cosec.x)*cos.x/(sin.x)^2
proof
assume
A1: Z c= dom (sin*cosec);
dom (sin*cosec) c= dom cosec by RELAT_1:25;
then
A2: Z c= dom cosec by A1,XBOOLE_1:1;
A3: for x st x in Z holds sin*cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A2,RFUNCT_1:3;
then
A4: cosec is_differentiable_in x by FDIFF_9:2;
sin is_differentiable_in cosec.x by SIN_COS:64;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: sin*cosec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*cosec)`|Z).x = -cos.(cosec.x)*cos.x/(sin.x) ^2
proof
let x;
A6: sin is_differentiable_in cosec.x by SIN_COS:64;
assume
A7: x in Z;
then
A8: sin.x <>0 by A2,RFUNCT_1:3;
then cosec is_differentiable_in x by FDIFF_9:2;
then diff(sin*cosec,x) = diff(sin,cosec.x)*diff(cosec,x) by A6,FDIFF_2:13
.= cos(cosec.x)*diff(cosec,x) by SIN_COS:64
.= cos(cosec.x)* (-cos.x/(sin.x)^2) by A8,FDIFF_9:2
.=-cos.(cosec.x)*cos.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 = cos.(cose.x)
theorem
Z c= dom (cos*cosec) implies cos*cosec is_differentiable_on Z & for x
st x in Z holds ((cos*cosec)`|Z).x = sin.(cosec.x)*cos.x/(sin.x)^2
proof
assume
A1: Z c= dom (cos*cosec);
dom (cos*cosec) c= dom cosec by RELAT_1:25;
then
A2: Z c= dom cosec by A1,XBOOLE_1:1;
A3: for x st x in Z holds cos*cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x<>0 by A2,RFUNCT_1:3;
then
A4: cosec is_differentiable_in x by FDIFF_9:2;
cos is_differentiable_in cosec.x by SIN_COS:63;
hence thesis by A4,FDIFF_2:13;
end;
then
A5: cos*cosec is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*cosec)`|Z).x = sin.(cosec.x)*cos.x/(sin.x) ^2
proof
let x;
A6: cos is_differentiable_in cosec.x by SIN_COS:63;
assume
A7: x in Z;
then
A8: sin.x <>0 by A2,RFUNCT_1:3;
then cosec is_differentiable_in x by FDIFF_9:2;
then diff(cos*cosec,x) = diff(cos,cosec.x)*diff(cosec,x) by A6,FDIFF_2:13
.= (-sin(cosec.x))*diff(cosec,x) by SIN_COS:63
.= (-sin(cosec.x))* (-cos.x/(sin.x)^2) by A8,FDIFF_9:2;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;