:: Several Differentiation Formulas of Special Functions -- Part {VII}
:: by Fuguo Ge and Bing Xie
::
:: Received September 23, 2008
:: Copyright (c) 2008-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, SUBSET_1, RCOMP_1, PARTFUN1, TARSKI, RELAT_1,
SIN_COS9, SIN_COS, FUNCT_1, XXREAL_0, ARYTM_1, ARYTM_3, FDIFF_1,
SQUARE_1, CARD_1, XXREAL_1, SIN_COS4, VALUED_1, XBOOLE_0, ORDINAL4,
PREPOWER;
notations TARSKI, SUBSET_1, XXREAL_0, FUNCT_1, RELSET_1, PARTFUN1, ORDINAL1,
RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, XCMPLX_0,
XREAL_0, REAL_1, FDIFF_1, PARTFUN2, TAYLOR_1, PREPOWER, FDIFF_9,
SIN_COS9;
constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, SIN_COS, PARTFUN2,
TOPALG_2, TAYLOR_1, PREPOWER, LIMFUNC1, FDIFF_9, SIN_COS9, COMPLEX1;
registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
SIN_COS6, NUMBERS, INT_1, VALUED_0, SQUARE_1, PREPOWER;
requirements SUBSET, NUMERALS, ARITHM, REAL;
equalities XCMPLX_0, SIN_COS, SQUARE_1, FDIFF_9, SUBSET_1;
theorems FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, FUNCT_1, SQUARE_1,
XREAL_1, TARSKI, XBOOLE_1, FDIFF_7, RFUNCT_1, TAYLOR_1, PREPOWER,
VALUED_1, FDIFF_9, SIN_COS9, FDIFF_8, XXREAL_1;
begin
reserve x for Real,
n for Element of NAT,
y for set,
Z for open Subset of REAL,
g for PartFunc of REAL,REAL;
::f.x=arctan.(sin.x)
theorem
Z c= dom (arctan*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1)
implies arctan*sin is_differentiable_on Z & for x st x in Z holds ((arctan*sin)
`|Z).x = cos.x/(1+(sin.x)^2)
proof
assume that
A1: Z c= dom (arctan*sin) and
A2: for x st x in Z holds sin.x > -1 & sin.x < 1;
A3: for x st x in Z holds arctan*sin is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: sin.x > -1 & sin.x < 1 by A2;
sin is_differentiable_in x by SIN_COS:64;
hence thesis by A4,SIN_COS9:85;
end;
then
A5: arctan*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*sin)`|Z).x = cos.x/(1+(sin.x)^2)
proof
let x;
A6: sin is_differentiable_in x by SIN_COS:64;
assume
A7: x in Z;
then
A8: sin.x > -1 & sin.x < 1 by A2;
((arctan*sin)`|Z).x = diff(arctan*sin,x) by A5,A7,FDIFF_1:def 7
.= diff(sin,x)/(1+(sin.x)^2) by A6,A8,SIN_COS9:85
.= cos.x/(1+(sin.x)^2) by SIN_COS:64;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=arccot.(sin.x)
theorem
Z c= dom (arccot*sin) & (for x st x in Z holds sin.x > -1 & sin.x < 1)
implies arccot*sin is_differentiable_on Z & for x st x in Z holds ((arccot*sin)
`|Z).x = -cos.x/(1+(sin.x)^2)
proof
assume that
A1: Z c= dom (arccot*sin) and
A2: for x st x in Z holds sin.x > -1 & sin.x < 1;
A3: for x st x in Z holds arccot*sin is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: sin.x > -1 & sin.x < 1 by A2;
sin is_differentiable_in x by SIN_COS:64;
hence thesis by A4,SIN_COS9:86;
end;
then
A5: arccot*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*sin)`|Z).x = -cos.x/(1+(sin.x)^2)
proof
let x;
A6: sin is_differentiable_in x by SIN_COS:64;
assume
A7: x in Z;
then
A8: sin.x > -1 & sin.x < 1 by A2;
((arccot*sin)`|Z).x = diff(arccot*sin,x) by A5,A7,FDIFF_1:def 7
.= -diff(sin,x)/(1+(sin.x)^2) by A6,A8,SIN_COS9:86
.= -cos.x/(1+(sin.x)^2) by SIN_COS:64;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=arctan.(cos.x)
theorem
Z c= dom (arctan*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1)
implies arctan*cos is_differentiable_on Z & for x st x in Z holds ((arctan*cos)
`|Z).x = -sin.x/(1+(cos.x)^2)
proof
assume that
A1: Z c= dom (arctan*cos) and
A2: for x st x in Z holds cos.x > -1 & cos.x < 1;
A3: for x st x in Z holds arctan*cos is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: cos.x > -1 & cos.x < 1 by A2;
cos is_differentiable_in x by SIN_COS:63;
hence thesis by A4,SIN_COS9:85;
end;
then
A5: arctan*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*cos)`|Z).x = -sin.x/(1+(cos.x)^2)
proof
let x;
A6: cos is_differentiable_in x by SIN_COS:63;
assume
A7: x in Z;
then
A8: cos.x > -1 & cos.x < 1 by A2;
((arctan*cos)`|Z).x = diff(arctan*cos,x) by A5,A7,FDIFF_1:def 7
.= diff(cos,x)/(1+(cos.x)^2) by A6,A8,SIN_COS9:85
.= (-sin.x)/(1+(cos.x)^2) by SIN_COS:63
.= -sin.x/(1+(cos.x)^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=arccot.(cos.x)
theorem
Z c= dom (arccot*cos) & (for x st x in Z holds cos.x > -1 & cos.x < 1)
implies arccot*cos is_differentiable_on Z & for x st x in Z holds ((arccot*cos)
`|Z).x = sin.x/(1+(cos.x)^2)
proof
assume that
A1: Z c= dom (arccot*cos) and
A2: for x st x in Z holds cos.x > -1 & cos.x < 1;
A3: for x st x in Z holds arccot*cos is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: cos.x > -1 & cos.x < 1 by A2;
cos is_differentiable_in x by SIN_COS:63;
hence thesis by A4,SIN_COS9:86;
end;
then
A5: arccot*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*cos)`|Z).x = sin.x/(1+(cos.x)^2)
proof
let x;
A6: cos is_differentiable_in x by SIN_COS:63;
assume
A7: x in Z;
then
A8: cos.x > -1 & cos.x < 1 by A2;
((arccot*cos)`|Z).x = diff(arccot*cos,x) by A5,A7,FDIFF_1:def 7
.= -diff(cos,x)/(1+(cos.x)^2) by A6,A8,SIN_COS9:86
.= -(-sin.x)/(1+(cos.x)^2) by SIN_COS:63
.= sin.x/(1+(cos.x)^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=arctan.(tan.x)
theorem
Z c= dom (arctan*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1)
implies arctan*tan is_differentiable_on Z & for x st x in Z holds ((arctan*tan)
`|Z).x = 1
proof
assume that
A1: Z c= dom (arctan*tan) and
A2: for x st x in Z holds tan.x > -1 & tan.x < 1;
dom (arctan*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 arctan*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.x <> 0 by A3,FDIFF_8:1;
then
A6: tan is_differentiable_in x by FDIFF_7:46;
tan.x > -1 & tan.x < 1 by A2,A5;
hence thesis by A6,SIN_COS9:85;
end;
then
A7: arctan*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*tan)`|Z).x = 1
proof
let x;
assume
A8: x in Z;
then
A9: tan.x > -1 & tan.x < 1 by A2;
A10: tan.x = sin.x/cos.x by A3,A8,RFUNCT_1:def 1;
A11: cos.x <> 0 by A3,A8,FDIFF_8:1;
then
A12: tan is_differentiable_in x by FDIFF_7:46;
A13: (cos.x)^2 <> 0 by A11,SQUARE_1:12;
((arctan*tan)`|Z).x = diff(arctan*tan,x) by A7,A8,FDIFF_1:def 7
.= diff(tan,x)/(1+(tan.x)^2) by A12,A9,SIN_COS9:85
.= (1/(cos.x)^2)/(1+(tan.x)^2) by A11,FDIFF_7:46
.= 1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A10,XCMPLX_1:78
.= 1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:76
.= 1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
.= 1/((cos.x)^2+(sin.x)^2) by A13,XCMPLX_1:89
.= 1/1 by SIN_COS:28
.= 1;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arccot.(tan.x)
theorem
Z c= dom (arccot*tan) & (for x st x in Z holds tan.x > -1 & tan.x < 1)
implies arccot*tan is_differentiable_on Z & for x st x in Z holds ((arccot*tan)
`|Z).x = -1
proof
assume that
A1: Z c= dom (arccot*tan) and
A2: for x st x in Z holds tan.x > -1 & tan.x < 1;
dom (arccot*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 arccot*tan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.x <> 0 by A3,FDIFF_8:1;
then
A6: tan is_differentiable_in x by FDIFF_7:46;
tan.x > -1 & tan.x < 1 by A2,A5;
hence thesis by A6,SIN_COS9:86;
end;
then
A7: arccot*tan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*tan)`|Z).x = -1
proof
let x;
assume
A8: x in Z;
then
A9: tan.x > -1 & tan.x < 1 by A2;
A10: tan.x = sin.x/cos.x by A3,A8,RFUNCT_1:def 1;
A11: cos.x <> 0 by A3,A8,FDIFF_8:1;
then
A12: tan is_differentiable_in x by FDIFF_7:46;
A13: (cos.x)^2 <> 0 by A11,SQUARE_1:12;
((arccot*tan)`|Z).x = diff(arccot*tan,x) by A7,A8,FDIFF_1:def 7
.= -diff(tan,x)/(1+(tan.x)^2) by A12,A9,SIN_COS9:86
.= -(1/(cos.x)^2)/(1+(tan.x)^2) by A11,FDIFF_7:46
.= -1/((cos.x)^2*(1+(sin.x/cos.x)*(sin.x/cos.x))) by A10,XCMPLX_1:78
.= -1/((cos.x)^2*(1+(sin.x)^2/(cos.x)^2)) by XCMPLX_1:76
.= -1/((cos.x)^2+((cos.x)^2*(sin.x)^2)/(cos.x)^2)
.= -1/((cos.x)^2+(sin.x)^2) by A13,XCMPLX_1:89
.= -1/1 by SIN_COS:28
.= -1;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arctan.(cot.x)
theorem
Z c= dom (arctan*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1)
implies arctan*cot is_differentiable_on Z & for x st x in Z holds ((arctan*cot)
`|Z).x = -1
proof
assume that
A1: Z c= dom (arctan*cot) and
A2: for x st x in Z holds cot.x > -1 & cot.x < 1;
dom (arctan*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 arctan*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.x <> 0 by A3,FDIFF_8:2;
then
A6: cot is_differentiable_in x by FDIFF_7:47;
cot.x > -1 & cot.x < 1 by A2,A5;
hence thesis by A6,SIN_COS9:85;
end;
then
A7: arctan*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*cot)`|Z).x = -1
proof
let x;
assume
A8: x in Z;
then
A9: cot.x > -1 & cot.x < 1 by A2;
A10: cot.x = cos.x/sin.x by A3,A8,RFUNCT_1:def 1;
A11: sin.x <> 0 by A3,A8,FDIFF_8:2;
then
A12: cot is_differentiable_in x by FDIFF_7:47;
A13: (sin.x)^2 <> 0 by A11,SQUARE_1:12;
((arctan*cot)`|Z).x = diff(arctan*cot,x) by A7,A8,FDIFF_1:def 7
.= diff(cot,x)/(1+(cot.x)^2) by A12,A9,SIN_COS9:85
.= (-1/(sin.x)^2)/(1+(cot.x)^2) by A11,FDIFF_7:47
.= -1/(sin.x)^2/(1+(cot.x)^2)
.= -1/((sin.x)^2*(1+(cos.x/sin.x)*(cos.x/sin.x))) by A10,XCMPLX_1:78
.= -1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:76
.= -1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
.= -1/((sin.x)^2+(cos.x)^2) by A13,XCMPLX_1:89
.= -1/1 by SIN_COS:28
.= -1;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arccot.(cot.x)
theorem
Z c= dom (arccot*cot) & (for x st x in Z holds cot.x > -1 & cot.x < 1)
implies arccot*cot is_differentiable_on Z & for x st x in Z holds ((arccot*cot)
`|Z).x = 1
proof
assume that
A1: Z c= dom (arccot*cot) and
A2: for x st x in Z holds cot.x > -1 & cot.x < 1;
dom (arccot*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 arccot*cot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.x <> 0 by A3,FDIFF_8:2;
then
A6: cot is_differentiable_in x by FDIFF_7:47;
cot.x > -1 & cot.x < 1 by A2,A5;
hence thesis by A6,SIN_COS9:86;
end;
then
A7: arccot*cot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*cot)`|Z).x = 1
proof
let x;
assume
A8: x in Z;
then
A9: cot.x > -1 & cot.x < 1 by A2;
A10: cot.x = cos.x/sin.x by A3,A8,RFUNCT_1:def 1;
A11: sin.x <> 0 by A3,A8,FDIFF_8:2;
then
A12: cot is_differentiable_in x by FDIFF_7:47;
A13: (sin.x)^2 <> 0 by A11,SQUARE_1:12;
((arccot*cot)`|Z).x = diff(arccot*cot,x) by A7,A8,FDIFF_1:def 7
.= -diff(cot,x)/(1+(cot.x)^2) by A12,A9,SIN_COS9:86
.= -(-1/(sin.x)^2)/(1+(cot.x)^2) by A11,FDIFF_7:47
.= 1/(sin.x)^2/(1+(cot.x)^2)
.= 1/((sin.x)^2*(1+(cos.x/sin.x)*(cos.x/sin.x))) by A10,XCMPLX_1:78
.= 1/((sin.x)^2*(1+(cos.x)^2/(sin.x)^2)) by XCMPLX_1:76
.= 1/((sin.x)^2+((sin.x)^2*(cos.x)^2)/(sin.x)^2)
.= 1/((sin.x)^2+(cos.x)^2) by A13,XCMPLX_1:89
.= 1/1 by SIN_COS:28
.= 1;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arctan.(arctan.x)
theorem
Z c= dom (arctan*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds
arctan.x > -1 & arctan.x < 1) implies arctan*arctan is_differentiable_on Z &
for x st x in Z holds ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.x)^2))
proof
assume that
A1: Z c= dom (arctan*arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > -1 & arctan.x < 1;
A4: for x st x in Z holds arctan*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arctan.x > -1 & arctan.x < 1 by A3;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,SIN_COS9:85;
end;
then
A7: arctan*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*arctan)`|Z).x = 1/((1+x^2)*(1+(arctan.x) ^2))
proof
let x;
assume
A8: x in Z;
then
A9: arctan.x > -1 & arctan.x < 1 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
((arctan*arctan)`|Z).x = diff(arctan*arctan,x) by A7,A8,FDIFF_1:def 7
.= diff(arctan,x)/(1+(arctan.x)^2) by A11,A9,SIN_COS9:85
.= ((arctan)`|Z).x/(1+(arctan.x)^2) by A8,A10,FDIFF_1:def 7
.= (1/(1+x^2))/(1+(arctan.x)^2) by A2,A8,SIN_COS9:81
.= 1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arccot.(arctan.x)
theorem
Z c= dom (arccot*arctan) & Z c= ].-1,1.[ & (for x st x in Z holds
arctan.x > -1 & arctan.x < 1) implies arccot*arctan is_differentiable_on Z &
for x st x in Z holds ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.x)^2))
proof
assume that
A1: Z c= dom (arccot*arctan) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > -1 & arctan.x < 1;
A4: for x st x in Z holds arccot*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arctan.x > -1 & arctan.x < 1 by A3;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,SIN_COS9:86;
end;
then
A7: arccot*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*arctan)`|Z).x = -1/((1+x^2)*(1+(arctan.x )^2))
proof
let x;
assume
A8: x in Z;
then
A9: arctan.x > -1 & arctan.x < 1 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
((arccot*arctan)`|Z).x = diff(arccot*arctan,x) by A7,A8,FDIFF_1:def 7
.= -diff(arctan,x)/(1+(arctan.x)^2) by A11,A9,SIN_COS9:86
.= -((arctan)`|Z).x/(1+(arctan.x)^2) by A8,A10,FDIFF_1:def 7
.= -(1/(1+x^2))/(1+(arctan.x)^2) by A2,A8,SIN_COS9:81
.= -1/((1+x^2)*(1+(arctan.x)^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arctan.(arccot.x)
theorem
Z c= dom (arctan*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds
arccot.x > -1 & arccot.x < 1) implies arctan*arccot is_differentiable_on Z &
for x st x in Z holds ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.x)^2))
proof
assume that
A1: Z c= dom (arctan*arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arccot.x > -1 & arccot.x < 1;
A4: for x st x in Z holds arctan*arccot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arccot.x > -1 & arccot.x < 1 by A3;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,SIN_COS9:85;
end;
then
A7: arctan*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arctan*arccot)`|Z).x = -1/((1+x^2)*(1+(arccot.x )^2))
proof
let x;
assume
A8: x in Z;
then
A9: arccot.x > -1 & arccot.x < 1 by A3;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A11: arccot is_differentiable_in x by A8,FDIFF_1:9;
((arctan*arccot)`|Z).x = diff(arctan*arccot,x) by A7,A8,FDIFF_1:def 7
.= diff(arccot,x)/(1+(arccot.x)^2) by A11,A9,SIN_COS9:85
.= ((arccot)`|Z).x/(1+(arccot.x)^2) by A8,A10,FDIFF_1:def 7
.= (-1/(1+x^2))/(1+(arccot.x)^2) by A2,A8,SIN_COS9:82
.= -1/(1+x^2)/(1+(arccot.x)^2)
.= -1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=arccot.(arccot.x)
theorem
Z c= dom (arccot*arccot) & Z c= ].-1,1.[ & (for x st x in Z holds
arccot.x > -1 & arccot.x < 1) implies arccot*arccot is_differentiable_on Z &
for x st x in Z holds ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.x)^2))
proof
assume that
A1: Z c= dom (arccot*arccot) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arccot.x > -1 & arccot.x < 1;
A4: for x st x in Z holds arccot*arccot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arccot.x > -1 & arccot.x < 1 by A3;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,SIN_COS9:86;
end;
then
A7: arccot*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((arccot*arccot)`|Z).x = 1/((1+x^2)*(1+(arccot.x) ^2))
proof
let x;
assume
A8: x in Z;
then
A9: arccot.x > -1 & arccot.x < 1 by A3;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A11: arccot is_differentiable_in x by A8,FDIFF_1:9;
((arccot*arccot)`|Z).x = diff(arccot*arccot,x) by A7,A8,FDIFF_1:def 7
.= -diff(arccot,x)/(1+(arccot.x)^2) by A11,A9,SIN_COS9:86
.= -((arccot)`|Z).x/(1+(arccot.x)^2) by A8,A10,FDIFF_1:def 7
.= -(-1/(1+x^2))/(1+(arccot.x)^2) by A2,A8,SIN_COS9:82
.= 1/(1+x^2)/(1+(arccot.x)^2)
.= 1/((1+x^2)*(1+(arccot.x)^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=sin.(arctan.x)
theorem
Z c= dom (sin*arctan) & Z c= ].-1,1.[ implies sin*arctan
is_differentiable_on Z & for x st x in Z holds ((sin*arctan)`|Z).x = cos.(
arctan.x)/(1+x^2)
proof
assume that
A1: Z c= dom (sin*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin*arctan is_differentiable_in x
proof
let x;
assume
A4: x in Z;
A5: sin is_differentiable_in arctan.x by SIN_COS:64;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*arctan)`|Z).x = cos.(arctan.x)/(1+x^2)
proof
let x;
assume
A7: x in Z;
A8: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A9: arctan is_differentiable_in x by A7,FDIFF_1:9;
A10: sin is_differentiable_in arctan.x by SIN_COS:64;
((sin*arctan)`|Z).x = diff(sin*arctan,x) by A6,A7,FDIFF_1:def 7
.= diff(sin,arctan.x)*diff(arctan,x) by A9,A10,FDIFF_2:13
.= cos.(arctan.x)*diff(arctan,x) by SIN_COS:64
.= cos.(arctan.x)*((arctan)`|Z).x by A7,A8,FDIFF_1:def 7
.= cos.(arctan.x)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
.= cos.(arctan.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=sin.(arccot.x)
theorem
Z c= dom (sin*arccot) & Z c= ].-1,1.[ implies sin*arccot
is_differentiable_on Z & for x st x in Z holds ((sin*arccot)`|Z).x = -cos.(
arccot.x)/(1+x^2)
proof
assume that
A1: Z c= dom (sin*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin*arccot is_differentiable_in x
proof
let x;
assume
A4: x in Z;
A5: sin is_differentiable_in arccot.x by SIN_COS:64;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*arccot)`|Z).x = -cos.(arccot.x)/(1+x^2)
proof
let x;
assume
A7: x in Z;
A8: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A9: arccot is_differentiable_in x by A7,FDIFF_1:9;
A10: sin is_differentiable_in arccot.x by SIN_COS:64;
((sin*arccot)`|Z).x = diff(sin*arccot,x) by A6,A7,FDIFF_1:def 7
.= diff(sin,arccot.x)*diff(arccot,x) by A9,A10,FDIFF_2:13
.= cos.(arccot.x)*diff(arccot,x) by SIN_COS:64
.= cos.(arccot.x)*((arccot)`|Z).x by A7,A8,FDIFF_1:def 7
.= cos.(arccot.x)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
.= -cos.(arccot.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cos.(arctan.x)
theorem
Z c= dom (cos*arctan) & Z c= ].-1,1.[ implies cos*arctan
is_differentiable_on Z & for x st x in Z holds ((cos*arctan)`|Z).x = -sin.(
arctan.x)/(1+x^2)
proof
assume that
A1: Z c= dom (cos*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos*arctan is_differentiable_in x
proof
let x;
assume
A4: x in Z;
A5: cos is_differentiable_in arctan.x by SIN_COS:63;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*arctan)`|Z).x = -sin.(arctan.x)/(1+x^2)
proof
let x;
assume
A7: x in Z;
A8: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A9: arctan is_differentiable_in x by A7,FDIFF_1:9;
A10: cos is_differentiable_in arctan.x by SIN_COS:63;
((cos*arctan)`|Z).x = diff(cos*arctan,x) by A6,A7,FDIFF_1:def 7
.= diff(cos,arctan.x)*diff(arctan,x) by A9,A10,FDIFF_2:13
.= (-sin.(arctan.x))*diff(arctan,x) by SIN_COS:63
.= -sin.(arctan.x)*diff(arctan,x)
.= -sin.(arctan.x)*((arctan)`|Z).x by A7,A8,FDIFF_1:def 7
.= -sin.(arctan.x)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
.= -sin.(arctan.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cos.(arccot.x)
theorem
Z c= dom (cos*arccot) & Z c= ].-1,1.[ implies cos*arccot
is_differentiable_on Z & for x st x in Z holds ((cos*arccot)`|Z).x = sin.(
arccot.x)/(1+x^2)
proof
assume that
A1: Z c= dom (cos*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos*arccot is_differentiable_in x
proof
let x;
assume
A4: x in Z;
A5: cos is_differentiable_in arccot.x by SIN_COS:63;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*arccot)`|Z).x = sin.(arccot.x)/(1+x^2)
proof
let x;
assume
A7: x in Z;
A8: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A9: arccot is_differentiable_in x by A7,FDIFF_1:9;
A10: cos is_differentiable_in arccot.x by SIN_COS:63;
((cos*arccot)`|Z).x = diff(cos*arccot,x) by A6,A7,FDIFF_1:def 7
.= diff(cos,arccot.x)*diff(arccot,x) by A9,A10,FDIFF_2:13
.= (-sin.(arccot.x))*diff(arccot,x) by SIN_COS:63
.= -sin.(arccot.x)*diff(arccot,x)
.= -sin.(arccot.x)*((arccot)`|Z).x by A7,A8,FDIFF_1:def 7
.= -sin.(arccot.x)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
.= sin.(arccot.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=tan.(arctan.x)
theorem
Z c= dom (tan*arctan) & Z c= ].-1,1.[ implies tan*arctan
is_differentiable_on Z & for x st x in Z holds ((tan*arctan)`|Z).x = 1/((cos.(
arctan.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (tan*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds tan*arctan is_differentiable_in x
proof
let x;
assume
A4: x in Z;
then arctan.x in dom tan by A1,FUNCT_1:11;
then cos.(arctan.x) <> 0 by FDIFF_8:1;
then
A5: tan is_differentiable_in arctan.x by FDIFF_7:46;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: tan*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*arctan)`|Z).x = 1/((cos.(arctan.x))^2*(1+x ^2))
proof
let x;
assume
A7: x in Z;
then arctan.x in dom tan by A1,FUNCT_1:11;
then
A8: cos.(arctan.x) <> 0 by FDIFF_8:1;
then
A9: tan is_differentiable_in arctan.x by FDIFF_7:46;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A7,FDIFF_1:9;
((tan*arctan)`|Z).x = diff(tan*arctan,x) by A6,A7,FDIFF_1:def 7
.= diff(tan,arctan.x)*diff(arctan,x) by A11,A9,FDIFF_2:13
.= (1/(cos.(arctan.x))^2)*diff(arctan,x) by A8,FDIFF_7:46
.= (1/(cos.(arctan.x))^2)*((arctan)`|Z).x by A7,A10,FDIFF_1:def 7
.= (1/(cos.(arctan.x))^2)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
.= 1/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=tan.(arccot.x)
theorem
Z c= dom (tan*arccot) & Z c= ].-1,1.[ implies tan*arccot
is_differentiable_on Z & for x st x in Z holds ((tan*arccot)`|Z).x = -1/((cos.(
arccot.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (tan*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds tan*arccot is_differentiable_in x
proof
let x;
assume
A4: x in Z;
then arccot.x in dom tan by A1,FUNCT_1:11;
then cos.(arccot.x) <> 0 by FDIFF_8:1;
then
A5: tan is_differentiable_in arccot.x by FDIFF_7:46;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: tan*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((tan*arccot)`|Z).x = -1/((cos.(arccot.x))^2*(1+x ^2))
proof
let x;
assume
A7: x in Z;
then arccot.x in dom tan by A1,FUNCT_1:11;
then
A8: cos.(arccot.x) <> 0 by FDIFF_8:1;
then
A9: tan is_differentiable_in arccot.x by FDIFF_7:46;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A11: arccot is_differentiable_in x by A7,FDIFF_1:9;
((tan*arccot)`|Z).x = diff(tan*arccot,x) by A6,A7,FDIFF_1:def 7
.= diff(tan,arccot.x)*diff(arccot,x) by A11,A9,FDIFF_2:13
.= (1/(cos.(arccot.x))^2)*diff(arccot,x) by A8,FDIFF_7:46
.= (1/(cos.(arccot.x))^2)*((arccot)`|Z).x by A7,A10,FDIFF_1:def 7
.= (1/(cos.(arccot.x))^2)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
.= -(1/(cos.(arccot.x))^2)*(1/(1+x^2))
.= -1/((cos.(arccot.x))^2*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cot.(arctan.x)
theorem
Z c= dom (cot*arctan) & Z c= ].-1,1.[ implies cot*arctan
is_differentiable_on Z & for x st x in Z holds ((cot*arctan)`|Z).x = -1/((sin.(
arctan.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (cot*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cot*arctan is_differentiable_in x
proof
let x;
assume
A4: x in Z;
then arctan.x in dom cot by A1,FUNCT_1:11;
then sin.(arctan.x) <> 0 by FDIFF_8:2;
then
A5: cot is_differentiable_in arctan.x by FDIFF_7:47;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cot*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*arctan)`|Z).x = -1/((sin.(arctan.x))^2*(1+x ^2))
proof
let x;
assume
A7: x in Z;
then arctan.x in dom cot by A1,FUNCT_1:11;
then
A8: sin.(arctan.x) <> 0 by FDIFF_8:2;
then
A9: cot is_differentiable_in arctan.x by FDIFF_7:47;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A7,FDIFF_1:9;
((cot*arctan)`|Z).x = diff(cot*arctan,x) by A6,A7,FDIFF_1:def 7
.= diff(cot,arctan.x)*diff(arctan,x) by A11,A9,FDIFF_2:13
.= (-1/(sin.(arctan.x))^2)*diff(arctan,x) by A8,FDIFF_7:47
.= -(1/(sin.(arctan.x))^2)*diff(arctan,x)
.= -(1/(sin.(arctan.x))^2)*((arctan)`|Z).x by A7,A10,FDIFF_1:def 7
.= -(1/(sin.(arctan.x))^2)*(1/(1+x^2)) by A2,A7,SIN_COS9:81
.= -1/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=cot.(arccot.x)
theorem
Z c= dom (cot*arccot) & Z c= ].-1,1.[ implies cot*arccot
is_differentiable_on Z & for x st x in Z holds ((cot*arccot)`|Z).x = 1/((sin.(
arccot.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (cot*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cot*arccot is_differentiable_in x
proof
let x;
assume
A4: x in Z;
then arccot.x in dom cot by A1,FUNCT_1:11;
then sin.(arccot.x) <> 0 by FDIFF_8:2;
then
A5: cot is_differentiable_in arccot.x by FDIFF_7:47;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A4,FDIFF_1:9;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cot*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cot*arccot)`|Z).x = 1/((sin.(arccot.x))^2*(1+x ^2))
proof
let x;
assume
A7: x in Z;
then arccot.x in dom cot by A1,FUNCT_1:11;
then
A8: sin.(arccot.x) <> 0 by FDIFF_8:2;
then
A9: cot is_differentiable_in arccot.x by FDIFF_7:47;
A10: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A11: arccot is_differentiable_in x by A7,FDIFF_1:9;
((cot*arccot)`|Z).x = diff(cot*arccot,x) by A6,A7,FDIFF_1:def 7
.= diff(cot,arccot.x)*diff(arccot,x) by A11,A9,FDIFF_2:13
.= (-1/(sin.(arccot.x))^2)*diff(arccot,x) by A8,FDIFF_7:47
.= -(1/(sin.(arccot.x))^2)*diff(arccot,x)
.= -(1/(sin.(arccot.x))^2)*((arccot)`|Z).x by A7,A10,FDIFF_1:def 7
.= -(1/(sin.(arccot.x))^2)*(-1/(1+x^2)) by A2,A7,SIN_COS9:82
.= (1/(sin.(arccot.x))^2)*(1/(1+x^2))
.= 1/((sin.(arccot.x))^2*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
::f.x=sec.(arctan.x)
theorem
Z c= dom (sec*arctan) & Z c= ].-1,1.[ implies sec*arctan
is_differentiable_on Z & for x st x in Z holds ((sec*arctan)`|Z).x = sin.(
arctan.x)/((cos.(arctan.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (sec*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos.(arctan.x) <> 0
proof
let x;
assume x in Z;
then arctan.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A4: for x st x in Z holds sec*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.(arctan.x) <> 0 by A3;
then
A6: sec is_differentiable_in arctan.x by FDIFF_9:1;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sec*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*arctan)`|Z).x = sin.(arctan.x)/((cos.(
arctan.x))^2*(1+x^2))
proof
let x;
assume
A8: x in Z;
then
A9: cos.(arctan.x) <> 0 by A3;
cos.(arctan.x) <> 0 by A3,A8;
then
A10: sec is_differentiable_in arctan.x by FDIFF_9:1;
A11: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A12: arctan is_differentiable_in x by A8,FDIFF_1:9;
((sec*arctan)`|Z).x = diff(sec*arctan,x) by A7,A8,FDIFF_1:def 7
.= diff(sec,arctan.x)*diff(arctan,x) by A12,A10,FDIFF_2:13
.= (sin.(arctan.x)/(cos.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_9:1
.= (sin.(arctan.x)/(cos.(arctan.x))^2)*((arctan)`|Z).x by A8,A11,
FDIFF_1:def 7
.= (sin.(arctan.x)/(cos.(arctan.x))^2)*(1/(1+x^2)) by A2,A8,SIN_COS9:81
.= (sin.(arctan.x)*1)/((cos.(arctan.x))^2*(1+x^2)) by XCMPLX_1:76
.= sin.(arctan.x)/((cos.(arctan.x))^2*(1+x^2));
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=sec.(arccot.x)
theorem
Z c= dom (sec*arccot) & Z c= ].-1,1.[ implies sec*arccot
is_differentiable_on Z & for x st x in Z holds ((sec*arccot)`|Z).x = -sin.(
arccot.x)/((cos.(arccot.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (sec*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds cos.(arccot.x) <> 0
proof
let x;
assume x in Z;
then arccot.x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A4: for x st x in Z holds sec*arccot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then cos.(arccot.x) <> 0 by A3;
then
A6: sec is_differentiable_in arccot.x by FDIFF_9:1;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sec*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sec*arccot)`|Z).x = -sin.(arccot.x)/((cos.(
arccot.x))^2*(1+x^2))
proof
let x;
assume
A8: x in Z;
then
A9: cos.(arccot.x) <> 0 by A3;
cos.(arccot.x) <> 0 by A3,A8;
then
A10: sec is_differentiable_in arccot.x by FDIFF_9:1;
A11: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A12: arccot is_differentiable_in x by A8,FDIFF_1:9;
((sec*arccot)`|Z).x = diff(sec*arccot,x) by A7,A8,FDIFF_1:def 7
.= diff(sec,arccot.x)*diff(arccot,x) by A12,A10,FDIFF_2:13
.= (sin.(arccot.x)/(cos.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_9:1
.= (sin.(arccot.x)/(cos.(arccot.x))^2)*((arccot)`|Z).x by A8,A11,
FDIFF_1:def 7
.= (sin.(arccot.x)/(cos.(arccot.x))^2)*(-1/(1+x^2)) by A2,A8,SIN_COS9:82
.= -(sin.(arccot.x)/(cos.(arccot.x))^2)*(1/(1+x^2))
.= -(sin.(arccot.x)*1)/((cos.(arccot.x))^2*(1+x^2)) by XCMPLX_1:76
.= -sin.(arccot.x)/((cos.(arccot.x))^2*(1+x^2));
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cosec.(arctan.x)
theorem
Z c= dom (cosec*arctan) & Z c= ].-1,1.[ implies cosec*arctan
is_differentiable_on Z & for x st x in Z holds ((cosec*arctan)`|Z).x = -cos.(
arctan.x)/((sin.(arctan.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (cosec*arctan) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin.(arctan.x) <> 0
proof
let x;
assume x in Z;
then arctan.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A4: for x st x in Z holds cosec*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.(arctan.x) <> 0 by A3;
then
A6: cosec is_differentiable_in arctan.x by FDIFF_9:2;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cosec*arctan is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*arctan)`|Z).x = -cos.(arctan.x)/((sin.(
arctan.x))^2*(1+x^2))
proof
let x;
assume
A8: x in Z;
then
A9: sin.(arctan.x) <> 0 by A3;
sin.(arctan.x) <> 0 by A3,A8;
then
A10: cosec is_differentiable_in arctan.x by FDIFF_9:2;
A11: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A12: arctan is_differentiable_in x by A8,FDIFF_1:9;
((cosec*arctan)`|Z).x = diff(cosec*arctan,x) by A7,A8,FDIFF_1:def 7
.= diff(cosec,arctan.x)*diff(arctan,x) by A12,A10,FDIFF_2:13
.= (-cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x) by A9,FDIFF_9:2
.= -(cos.(arctan.x)/(sin.(arctan.x))^2)*diff(arctan,x)
.= -(cos.(arctan.x)/(sin.(arctan.x))^2)*((arctan)`|Z).x by A8,A11,
FDIFF_1:def 7
.= -(cos.(arctan.x)/(sin.(arctan.x))^2)*(1/(1+x^2)) by A2,A8,SIN_COS9:81
.= -(cos.(arctan.x)*1)/((sin.(arctan.x))^2*(1+x^2)) by XCMPLX_1:76
.= -cos.(arctan.x)/((sin.(arctan.x))^2*(1+x^2));
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cosec.(arccot.x)
theorem
Z c= dom (cosec*arccot) & Z c= ].-1,1.[ implies cosec*arccot
is_differentiable_on Z & for x st x in Z holds ((cosec*arccot)`|Z).x = cos.(
arccot.x)/((sin.(arccot.x))^2*(1+x^2))
proof
assume that
A1: Z c= dom (cosec*arccot) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds sin.(arccot.x) <> 0
proof
let x;
assume x in Z;
then arccot.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A4: for x st x in Z holds cosec*arccot is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then sin.(arccot.x) <> 0 by A3;
then
A6: cosec is_differentiable_in arccot.x by FDIFF_9:2;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cosec*arccot is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cosec*arccot)`|Z).x = cos.(arccot.x)/((sin.(
arccot.x))^2*(1+x^2))
proof
let x;
assume
A8: x in Z;
then
A9: sin.(arccot.x) <> 0 by A3;
sin.(arccot.x) <> 0 by A3,A8;
then
A10: cosec is_differentiable_in arccot.x by FDIFF_9:2;
A11: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A12: arccot is_differentiable_in x by A8,FDIFF_1:9;
((cosec*arccot)`|Z).x = diff(cosec*arccot,x) by A7,A8,FDIFF_1:def 7
.= diff(cosec,arccot.x)*diff(arccot,x) by A12,A10,FDIFF_2:13
.= (-cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x) by A9,FDIFF_9:2
.= -(cos.(arccot.x)/(sin.(arccot.x))^2)*diff(arccot,x)
.= -(cos.(arccot.x)/(sin.(arccot.x))^2)*((arccot)`|Z).x by A8,A11,
FDIFF_1:def 7
.= -(cos.(arccot.x)/(sin.(arccot.x))^2)*(-1/(1+x^2)) by A2,A8,SIN_COS9:82
.= (cos.(arccot.x)/(sin.(arccot.x))^2)*(1/(1+x^2))
.= (cos.(arccot.x)*1)/((sin.(arccot.x))^2*(1+x^2)) by XCMPLX_1:76
.= cos.(arccot.x)/((sin.(arccot.x))^2*(1+x^2));
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=sin.x*arctan.x
theorem
Z c= dom (sin(#)arctan) & Z c= ].-1,1.[ implies (sin(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((sin(#)arctan)`|Z).x = cos.x*
arctan.x+sin.x/(1+x^2)
proof
assume that
A1: Z c= dom (sin(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
Z c= dom sin /\ dom arctan by A1,VALUED_1:def 4;
then Z c= dom sin by XBOOLE_1:18;
then
A5: sin is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((sin(#)arctan)`|Z).x = cos.x*arctan.x+sin.x/(1+x ^2)
proof
let x;
assume
A6: x in Z;
then
((sin(#)arctan)`|Z).x = (arctan.x)*diff(sin,x)+(sin.x)*diff(arctan,x)
by A1,A5,A3,FDIFF_1:21
.= (arctan.x)*(cos.x)+(sin.x)*diff(arctan,x) by SIN_COS:64
.= cos.x*arctan.x+(sin.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
.= cos.x*arctan.x+(sin.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= cos.x*arctan.x+sin.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=sin.x*arccot.x
theorem
Z c= dom (sin(#)arccot) & Z c= ].-1,1.[ implies (sin(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((sin(#)arccot)`|Z).x = cos.x*
arccot.x-sin.x/(1+x^2)
proof
assume that
A1: Z c= dom (sin(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A4: for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
Z c= dom sin /\ dom arccot by A1,VALUED_1:def 4;
then Z c= dom sin by XBOOLE_1:18;
then
A5: sin is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((sin(#)arccot)`|Z).x = cos.x*arccot.x-sin.x/(1+x ^2)
proof
let x;
assume
A6: x in Z;
then
((sin(#)arccot)`|Z).x = (arccot.x)*diff(sin,x)+(sin.x)*diff(arccot,x)
by A1,A5,A3,FDIFF_1:21
.= (arccot.x)*(cos.x)+(sin.x)*diff(arccot,x) by SIN_COS:64
.= cos.x*arccot.x+(sin.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
.= cos.x*arccot.x+(sin.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
.= cos.x*arccot.x-sin.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cos.x*arctan.x
theorem
Z c= dom (cos(#)arctan) & Z c= ].-1,1.[ implies (cos(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cos(#)arctan)`|Z).x = -sin.x*
arctan.x+cos.x/(1+x^2)
proof
assume that
A1: Z c= dom (cos(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
Z c= dom cos /\ dom arctan by A1,VALUED_1:def 4;
then Z c= dom cos by XBOOLE_1:18;
then
A5: cos is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((cos(#)arctan)`|Z).x = -sin.x*arctan.x+cos.x/(1+x ^2)
proof
let x;
assume
A6: x in Z;
then
((cos(#)arctan)`|Z).x = (arctan.x)*diff(cos,x)+(cos.x)*diff(arctan,x)
by A1,A5,A3,FDIFF_1:21
.= (arctan.x)*(-sin.x)+(cos.x)*diff(arctan,x) by SIN_COS:63
.= -sin.x*arctan.x+(cos.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
.= -sin.x*arctan.x+(cos.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= -sin.x*arctan.x+cos.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cos.x*arccot.x
theorem
Z c= dom (cos(#)arccot) & Z c= ].-1,1.[ implies (cos(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cos(#)arccot)`|Z).x = -sin.x*
arccot.x-cos.x/(1+x^2)
proof
assume that
A1: Z c= dom (cos(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
A4: for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
Z c= dom cos /\ dom arccot by A1,VALUED_1:def 4;
then Z c= dom cos by XBOOLE_1:18;
then
A5: cos is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((cos(#)arccot)`|Z).x = -sin.x*arccot.x-cos.x/(1+x ^2)
proof
let x;
assume
A6: x in Z;
then
((cos(#)arccot)`|Z).x = (arccot.x)*diff(cos,x)+(cos.x)*diff(arccot,x)
by A1,A5,A3,FDIFF_1:21
.= (arccot.x)*(-sin.x)+(cos.x)*diff(arccot,x) by SIN_COS:63
.= -sin.x*arccot.x+(cos.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
.= -sin.x*arccot.x+(cos.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
.= -sin.x*arccot.x-cos.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=tan.x*arctan.x
theorem
Z c= dom (tan(#)arctan) & Z c= ].-1,1.[ implies (tan(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((tan(#)arctan)`|Z).x = arctan.x
/(cos.x)^2+tan.x/(1+x^2)
proof
assume that
A1: Z c= dom (tan(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
Z c= dom tan /\ dom arctan by A1,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;
for x st x in Z holds ((tan(#)arctan)`|Z).x = arctan.x/(cos.x)^2+tan.x/
(1+x^2)
proof
let x;
assume
A6: x in Z;
then
A7: cos.x <> 0 by A4,FDIFF_8:1;
((tan(#)arctan)`|Z).x = (arctan.x)*diff(tan,x)+(tan.x)*diff(arctan,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arctan.x)*(1/(cos.x)^2)+(tan.x)*diff(arctan,x) by A7,FDIFF_7:46
.= arctan.x/(cos.x)^2+(tan.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
.= arctan.x/(cos.x)^2+(tan.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= arctan.x/(cos.x)^2+tan.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=tan.x*arccot.x
theorem
Z c= dom (tan(#)arccot) & Z c= ].-1,1.[ implies (tan(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)arccot)`|Z).x = arccot.x
/(cos.x)^2-tan.x/(1+x^2)
proof
assume that
A1: Z c= dom (tan(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
Z c= dom tan /\ dom arccot by A1,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;
for x st x in Z holds ((tan(#)arccot)`|Z).x = arccot.x/(cos.x)^2-tan.x/
(1+x^2)
proof
let x;
assume
A6: x in Z;
then
A7: cos.x <> 0 by A4,FDIFF_8:1;
((tan(#)arccot)`|Z).x = (arccot.x)*diff(tan,x)+(tan.x)*diff(arccot,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arccot.x)*(1/(cos.x)^2)+(tan.x)*diff(arccot,x) by A7,FDIFF_7:46
.= arccot.x/(cos.x)^2+(tan.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
.= arccot.x/(cos.x)^2+(tan.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
.= arccot.x/(cos.x)^2-tan.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cot.x*arctan.x
theorem
Z c= dom (cot(#)arctan) & Z c= ].-1,1.[ implies (cot(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cot(#)arctan)`|Z).x = -arctan.
x/(sin.x)^2+cot.x/(1+x^2)
proof
assume that
A1: Z c= dom (cot(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
Z c= dom cot /\ dom arctan by A1,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;
for x st x in Z holds ((cot(#)arctan)`|Z).x = -arctan.x/(sin.x)^2+cot.x
/(1+x^2)
proof
let x;
assume
A6: x in Z;
then
A7: sin.x <> 0 by A4,FDIFF_8:2;
((cot(#)arctan)`|Z).x = (arctan.x)*diff(cot,x)+(cot.x)*diff(arctan,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arctan.x)*(-1/(sin.x)^2)+(cot.x)*diff(arctan,x) by A7,FDIFF_7:47
.= -arctan.x/(sin.x)^2+(cot.x)*((arctan)`|Z).x by A3,A6,FDIFF_1:def 7
.= -arctan.x/(sin.x)^2+(cot.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= -arctan.x/(sin.x)^2+cot.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cot.x*arccot.x
theorem
Z c= dom (cot(#)arccot) & Z c= ].-1,1.[ implies (cot(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)arccot)`|Z).x = -arccot.
x/(sin.x)^2-cot.x/(1+x^2)
proof
assume that
A1: Z c= dom (cot(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
Z c= dom cot /\ dom arccot by A1,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;
for x st x in Z holds ((cot(#)arccot)`|Z).x = -arccot.x/(sin.x)^2-cot.x
/(1+x^2)
proof
let x;
assume
A6: x in Z;
then
A7: sin.x <> 0 by A4,FDIFF_8:2;
((cot(#)arccot)`|Z).x = (arccot.x)*diff(cot,x)+(cot.x)*diff(arccot,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arccot.x)*(-1/(sin.x)^2)+(cot.x)*diff(arccot,x) by A7,FDIFF_7:47
.= -arccot.x/(sin.x)^2+(cot.x)*((arccot)`|Z).x by A3,A6,FDIFF_1:def 7
.= -arccot.x/(sin.x)^2+(cot.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
.= -arccot.x/(sin.x)^2-cot.x/(1+x^2);
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=sec.x*arctan.x
theorem
Z c= dom (sec(#)arctan) & Z c= ].-1,1.[ implies (sec(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((sec(#)arctan)`|Z).x = (sin.x*
arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2))
proof
assume that
A1: Z c= dom (sec(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
Z c= dom sec /\ dom arctan by A1,VALUED_1:def 4;
then
A4: Z c= dom sec by XBOOLE_1:18;
for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A4,RFUNCT_1:3;
hence thesis by FDIFF_9:1;
end;
then
A5: sec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((sec(#)arctan)`|Z).x = (sin.x*arctan.x)/(cos.x)
^2+1/(cos.x*(1+x^2))
proof
let x;
assume
A6: x in Z;
then
A7: cos.x <> 0 by A4,RFUNCT_1:3;
((sec(#)arctan)`|Z).x = (arctan.x)*diff(sec,x)+(sec.x)*diff(arctan,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arctan.x)*(sin.x/(cos.x)^2)+(sec.x)*diff(arctan,x) by A7,FDIFF_9:1
.= (sin.x*arctan.x)/(cos.x)^2+(sec.x)*((arctan)`|Z).x by A3,A6,
FDIFF_1:def 7
.= (sin.x*arctan.x)/(cos.x)^2+(sec.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= (sin.x*arctan.x)/(cos.x)^2+(1/cos.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
.= (sin.x*arctan.x)/(cos.x)^2+1/(cos.x*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=sec.x*arccot.x
theorem
Z c= dom (sec(#)arccot) & Z c= ].-1,1.[ implies (sec(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)arccot)`|Z).x = (sin.x*
arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2))
proof
assume that
A1: Z c= dom (sec(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
Z c= dom sec /\ dom arccot by A1,VALUED_1:def 4;
then
A4: Z c= dom sec by XBOOLE_1:18;
for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A4,RFUNCT_1:3;
hence thesis by FDIFF_9:1;
end;
then
A5: sec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((sec(#)arccot)`|Z).x = (sin.x*arccot.x)/(cos.x)
^2-1/(cos.x*(1+x^2))
proof
let x;
assume
A6: x in Z;
then
A7: cos.x <> 0 by A4,RFUNCT_1:3;
((sec(#)arccot)`|Z).x = (arccot.x)*diff(sec,x)+(sec.x)*diff(arccot,x)
by A1,A5,A3,A6,FDIFF_1:21
.= (arccot.x)*(sin.x/(cos.x)^2)+(sec.x)*diff(arccot,x) by A7,FDIFF_9:1
.= (sin.x*arccot.x)/(cos.x)^2+(sec.x)*((arccot)`|Z).x by A3,A6,
FDIFF_1:def 7
.= (sin.x*arccot.x)/(cos.x)^2+(sec.x)*(-1/(1+x^2)) by A2,A6,SIN_COS9:82
.= (sin.x*arccot.x)/(cos.x)^2-(sec.x)*(1/(1+x^2))
.= (sin.x*arccot.x)/(cos.x)^2-(1/cos.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
.= (sin.x*arccot.x)/(cos.x)^2-1/(cos.x*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cosec.x*arctan.x
theorem
Z c= dom (cosec(#)arctan) & Z c= ].-1,1.[ implies (cosec(#)arctan)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)arctan)`|Z).x = -(cos.
x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2))
proof
assume that
A1: Z c= dom (cosec(#)arctan) and
A2: Z c= ].-1,1.[;
A3: arctan is_differentiable_on Z by A2,SIN_COS9:81;
Z c= dom cosec /\ dom arctan by A1,VALUED_1:def 4;
then
A4: Z c= dom cosec by XBOOLE_1:18;
for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A4,RFUNCT_1:3;
hence thesis by FDIFF_9:2;
end;
then
A5: cosec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((cosec(#)arctan)`|Z).x = -(cos.x*arctan.x)/(sin.
x)^2+1/(sin.x*(1+x^2))
proof
let x;
assume
A6: x in Z;
then
A7: sin.x <> 0 by A4,RFUNCT_1:3;
((cosec(#)arctan)`|Z).x = (arctan.x)*diff(cosec,x)+(cosec.x)*diff(
arctan,x) by A1,A5,A3,A6,FDIFF_1:21
.= (arctan.x)*(-cos.x/(sin.x)^2)+(cosec.x)*diff(arctan,x) by A7,FDIFF_9:2
.= -(cos.x*arctan.x)/(sin.x)^2+(cosec.x)*((arctan)`|Z).x by A3,A6,
FDIFF_1:def 7
.= -(cos.x*arctan.x)/(sin.x)^2+(cosec.x)*(1/(1+x^2)) by A2,A6,SIN_COS9:81
.= -(cos.x*arctan.x)/(sin.x)^2+(1/sin.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
.= -(cos.x*arctan.x)/(sin.x)^2+1/(sin.x*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=cosec.x*arccot.x
theorem
Z c= dom (cosec(#)arccot) & Z c= ].-1,1.[ implies (cosec(#)arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)arccot)`|Z).x = -(cos.
x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2))
proof
assume that
A1: Z c= dom (cosec(#)arccot) and
A2: Z c= ].-1,1.[;
A3: arccot is_differentiable_on Z by A2,SIN_COS9:82;
Z c= dom cosec /\ dom arccot by A1,VALUED_1:def 4;
then
A4: Z c= dom cosec by XBOOLE_1:18;
for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A4,RFUNCT_1:3;
hence thesis by FDIFF_9:2;
end;
then
A5: cosec is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((cosec(#)arccot)`|Z).x = -(cos.x*arccot.x)/(sin.
x)^2-1/(sin.x*(1+x^2))
proof
let x;
assume
A6: x in Z;
then
A7: sin.x <> 0 by A4,RFUNCT_1:3;
((cosec(#)arccot)`|Z).x = (arccot.x)*diff(cosec,x)+(cosec.x)*diff(
arccot,x) by A1,A5,A3,A6,FDIFF_1:21
.= (arccot.x)*(-cos.x/(sin.x)^2)+(cosec.x)*diff(arccot,x) by A7,FDIFF_9:2
.= -(cos.x*arccot.x)/(sin.x)^2+(cosec.x)*((arccot)`|Z).x by A3,A6,
FDIFF_1:def 7
.= -(cos.x*arccot.x)/(sin.x)^2+(cosec.x)*(-1/(1+x^2)) by A2,A6,
SIN_COS9:82
.= -(cos.x*arccot.x)/(sin.x)^2-(cosec.x)*(1/(1+x^2))
.= -(cos.x*arccot.x)/(sin.x)^2-(1/sin.x)*(1/(1+x^2)) by A4,A6,
RFUNCT_1:def 2
.= -(cos.x*arccot.x)/(sin.x)^2-1/(sin.x*(1+x^2)) by XCMPLX_1:102;
hence thesis;
end;
hence thesis by A1,A5,A3,FDIFF_1:21;
end;
::f.x=arctan.x+arccot.x
theorem Th37:
Z c= ].-1,1.[ implies (arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((arctan+arccot)`|Z).x = 0
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
for x st x in Z holds ((arctan+arccot)`|Z).x = 0
proof
let x;
assume
A7: x in Z;
then ((arctan+arccot)`|Z).x = diff(arctan,x)+diff(arccot,x) by A6,A2,A5,
FDIFF_1:18
.= ((arctan)`|Z).x+diff(arccot,x) by A2,A7,FDIFF_1:def 7
.= 1/(1+x^2)+diff(arccot,x) by A1,A7,SIN_COS9:81
.= 1/(1+x^2)+((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
.= 1/(1+x^2)+(-1/(1+x^2)) by A1,A7,SIN_COS9:82
.= 0;
hence thesis;
end;
hence thesis by A6,A2,A5,FDIFF_1:18;
end;
::f.x=arctan.x-arccot.x
theorem Th38:
Z c= ].-1,1.[ implies (arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2)
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
for x st x in Z holds ((arctan-arccot)`|Z).x = 2/(1+x^2)
proof
let x;
assume
A7: x in Z;
then ((arctan-arccot)`|Z).x = diff(arctan,x)-diff(arccot,x) by A6,A2,A5,
FDIFF_1:19
.= ((arctan)`|Z).x-diff(arccot,x) by A2,A7,FDIFF_1:def 7
.= 1/(1+x^2)-diff(arccot,x) by A1,A7,SIN_COS9:81
.= 1/(1+x^2)-((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
.= 1/(1+x^2)-(-1/(1+x^2)) by A1,A7,SIN_COS9:82
.= 2/(1+x^2);
hence thesis;
end;
hence thesis by A6,A2,A5,FDIFF_1:19;
end;
::f.x=sin.x*(arctan.x+arccot.x)
theorem
Z c= ].-1,1.[ implies sin(#)(arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((sin(#)(arctan+arccot))`|Z).x = cos.x*(arctan.x+arccot.x
)
proof
for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
then
A1: sin is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
assume
A2: Z c= ].-1,1.[;
then
A3: arctan+arccot is_differentiable_on Z by Th37;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom sin /\ dom (arctan+arccot) by SIN_COS:24,XBOOLE_1:19;
then
A7: Z c= dom (sin(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (sin(#)(arctan+arccot)`|Z).x = cos.x*(arctan.x+
arccot.x)
proof
let x;
assume
A8: x in Z;
then
(sin(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(sin,x)+sin.x*
diff(arctan+arccot,x) by A7,A1,A3,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(sin,x)+sin.x*diff(arctan+arccot,x) by A6,A8,
VALUED_1:def 1
.= (arctan.x+arccot.x)*cos.x+sin.x*diff(arctan+arccot,x) by SIN_COS:64
.= (arctan.x+arccot.x)*cos.x+sin.x*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= (arctan.x+arccot.x)*cos.x+sin.x*0 by A2,A8,Th37
.= cos.x*(arctan.x+arccot.x);
hence thesis;
end;
hence thesis by A7,A1,A3,FDIFF_1:21;
end;
::f.x=sin.x*(arctan.x-arccot.x)
theorem
Z c= ].-1,1.[ implies sin(#)(arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((sin(#)(arctan-arccot))`|Z).x = cos.x*(arctan.x-arccot.x
)+2*sin.x/(1+x^2)
proof
for x st x in Z holds sin is_differentiable_in x by SIN_COS:64;
then
A1: sin is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
assume
A2: Z c= ].-1,1.[;
then
A3: arctan-arccot is_differentiable_on Z by Th38;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom sin /\ dom (arctan-arccot) by SIN_COS:24,XBOOLE_1:19;
then
A7: Z c= dom (sin(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds (sin(#)(arctan-arccot)`|Z).x = cos.x*(arctan.x-
arccot.x)+2*sin.x/(1+x^2)
proof
let x;
assume
A8: x in Z;
then
(sin(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(sin,x)+sin.x*
diff(arctan-arccot,x) by A7,A1,A3,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(sin,x)+sin.x*diff(arctan-arccot,x) by A6,A8,
VALUED_1:13
.= (arctan.x-arccot.x)*cos.x+sin.x*diff(arctan-arccot,x) by SIN_COS:64
.= (arctan.x-arccot.x)*cos.x+sin.x*((arctan-arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= (arctan.x-arccot.x)*cos.x+sin.x*(2/(1+x^2)) by A2,A8,Th38
.= cos.x*(arctan.x-arccot.x)+2*sin.x/(1+x^2);
hence thesis;
end;
hence thesis by A7,A1,A3,FDIFF_1:21;
end;
::f.x=cos.x*(arctan.x+arccot.x)
theorem
Z c= ].-1,1.[ implies cos(#)(arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((cos(#)(arctan+arccot))`|Z).x = -sin.x*(arctan.x+arccot.
x)
proof
for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
then
A1: cos is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
assume
A2: Z c= ].-1,1.[;
then
A3: arctan+arccot is_differentiable_on Z by Th37;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
then
A6: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom cos /\ dom (arctan+arccot) by SIN_COS:24,XBOOLE_1:19;
then
A7: Z c= dom (cos(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (cos(#)(arctan+arccot)`|Z).x = -sin.x*(arctan.x+
arccot.x)
proof
let x;
assume
A8: x in Z;
then
(cos(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cos,x)+cos.x*
diff(arctan+arccot,x) by A7,A1,A3,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(cos,x)+cos.x*diff(arctan+arccot,x) by A6,A8,
VALUED_1:def 1
.= (arctan.x+arccot.x)*(-sin.x)+cos.x*diff(arctan+arccot,x) by SIN_COS:63
.= (arctan.x+arccot.x)*(-sin.x)+cos.x*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= -(arctan.x+arccot.x)*sin.x+cos.x*0 by A2,A8,Th37
.= -sin.x*(arctan.x+arccot.x);
hence thesis;
end;
hence thesis by A7,A1,A3,FDIFF_1:21;
end;
::f.x=cos.x*(arctan.x-arccot.x)
theorem
Z c= ].-1,1.[ implies cos(#)(arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((cos(#)(arctan-arccot))`|Z).x = -sin.x*(arctan.x-arccot.
x)+2*cos.x/(1+x^2)
proof
for x st x in Z holds cos is_differentiable_in x by SIN_COS:63;
then
A1: cos is_differentiable_on Z by FDIFF_1:9,SIN_COS:24;
assume
A2: Z c= ].-1,1.[;
then
A3: arctan-arccot is_differentiable_on Z by Th38;
A4: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A5: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A4,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A5,XBOOLE_1:19;
then
A6: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom cos /\ dom (arctan-arccot) by SIN_COS:24,XBOOLE_1:19;
then
A7: Z c= dom (cos(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds (cos(#)(arctan-arccot)`|Z).x = -sin.x*(arctan.x-
arccot.x)+2*cos.x/(1+x^2)
proof
let x;
assume
A8: x in Z;
then
(cos(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cos,x)+cos.x*
diff(arctan-arccot,x) by A7,A1,A3,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(cos,x)+cos.x*diff(arctan-arccot,x) by A6,A8,
VALUED_1:13
.= (arctan.x-arccot.x)*(-sin.x)+cos.x*diff(arctan-arccot,x) by SIN_COS:63
.= (arctan.x-arccot.x)*(-sin.x)+cos.x*((arctan-arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= -(arctan.x-arccot.x)*sin.x+cos.x*(2/(1+x^2)) by A2,A8,Th38
.= -sin.x*(arctan.x-arccot.x)+2*cos.x/(1+x^2);
hence thesis;
end;
hence thesis by A7,A1,A3,FDIFF_1:21;
end;
::f.x=tan.x*(arctan.x+arccot.x)
theorem
Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan+arccot))`|Z).x =
(arctan.x+arccot.x)/(cos.x)^2
proof
assume that
A1: Z c= dom tan and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A1,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A4: tan is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom tan /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (tan(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (tan(#)(arctan+arccot)`|Z).x = (arctan.x+arccot.x
)/(cos.x)^2
proof
let x;
assume
A9: x in Z;
then
A10: cos.x <> 0 by A1,FDIFF_8:1;
(tan(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(tan,x)+tan.x*
diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(tan,x)+tan.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
.= (arctan.x+arccot.x)*(1/(cos.x)^2)+tan.x*diff(arctan+arccot,x) by A10,
FDIFF_7:46
.= (arctan.x+arccot.x)/(cos.x)^2+tan.x*((arctan+arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
.= (arctan.x+arccot.x)/(cos.x)^2+tan.x*0 by A2,A9,Th37
.= (arctan.x+arccot.x)/(cos.x)^2;
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=tan.x*(arctan.x-arccot.x)
theorem
Z c= dom tan & Z c= ].-1,1.[ implies tan(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((tan(#)(arctan-arccot))`|Z).x =
(arctan.x-arccot.x)/(cos.x)^2+2*tan.x/(1+x^2)
proof
assume that
A1: Z c= dom tan and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A1,FDIFF_8:1;
hence thesis by FDIFF_7:46;
end;
then
A4: tan is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom tan /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (tan(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds (tan(#)(arctan-arccot)`|Z).x = (arctan.x-arccot.x
)/(cos.x)^2+2*tan.x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then
A10: cos.x <> 0 by A1,FDIFF_8:1;
(tan(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(tan,x)+tan.x*
diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(tan,x)+tan.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
.= (arctan.x-arccot.x)*(1/(cos.x)^2)+tan.x*diff(arctan-arccot,x) by A10,
FDIFF_7:46
.= (arctan.x-arccot.x)/(cos.x)^2+tan.x*((arctan-arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
.= (arctan.x-arccot.x)/(cos.x)^2+tan.x*(2/(1+x^2)) by A2,A9,Th38
.= (arctan.x-arccot.x)/(cos.x)^2+2*tan.x/(1+x^2);
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=cot.x*(arctan.x+arccot.x)
theorem
Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan+arccot))`|Z).x =
-(arctan.x+arccot.x)/(sin.x)^2
proof
assume that
A1: Z c= dom cot and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A1,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A4: cot is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom cot /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (cot(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (cot(#)(arctan+arccot)`|Z).x = -(arctan.x+arccot.
x)/(sin.x)^2
proof
let x;
assume
A9: x in Z;
then
A10: sin.x <> 0 by A1,FDIFF_8:2;
(cot(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cot,x)+cot.x*
diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(cot,x)+cot.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
.= (arctan.x+arccot.x)*(-1/(sin.x)^2)+cot.x*diff(arctan+arccot,x) by A10,
FDIFF_7:47
.= -(arctan.x+arccot.x)/(sin.x)^2+cot.x*((arctan+arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
.= -(arctan.x+arccot.x)/(sin.x)^2+cot.x*0 by A2,A9,Th37
.= -(arctan.x+arccot.x)/(sin.x)^2;
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=cot.x*(arctan.x-arccot.x)
theorem
Z c= dom cot & Z c= ].-1,1.[ implies cot(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((cot(#)(arctan-arccot))`|Z).x =
-(arctan.x-arccot.x)/(sin.x)^2+2*cot.x/(1+x^2)
proof
assume that
A1: Z c= dom cot and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A1,FDIFF_8:2;
hence thesis by FDIFF_7:47;
end;
then
A4: cot is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom cot /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (cot(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds (cot(#)(arctan-arccot)`|Z).x = -(arctan.x-arccot.
x)/(sin.x)^2+2*cot.x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then
A10: sin.x <> 0 by A1,FDIFF_8:2;
(cot(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cot,x)+cot.x*
diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(cot,x)+cot.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
.= (arctan.x-arccot.x)*(-1/(sin.x)^2)+cot.x*diff(arctan-arccot,x) by A10,
FDIFF_7:47
.= -(arctan.x-arccot.x)/(sin.x)^2+cot.x*((arctan-arccot)`|Z).x by A3,A9,
FDIFF_1:def 7
.= -(arctan.x-arccot.x)/(sin.x)^2+cot.x*(2/(1+x^2)) by A2,A9,Th38
.= -(arctan.x-arccot.x)/(sin.x)^2+2*cot.x/(1+x^2);
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=sec.x*(arctan.x+arccot.x)
theorem
Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)(arctan+arccot))`|Z).x =
(arctan.x+arccot.x)*sin.x/(cos.x)^2
proof
assume that
A1: Z c= dom sec and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A1,RFUNCT_1:3;
hence thesis by FDIFF_9:1;
end;
then
A4: sec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom sec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (sec(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (sec(#)(arctan+arccot)`|Z).x = (arctan.x+arccot.x
)*sin.x/(cos.x)^2
proof
let x;
assume
A9: x in Z;
then
A10: cos.x <> 0 by A1,RFUNCT_1:3;
(sec(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(sec,x)+sec.x*
diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(sec,x)+sec.x*diff(arctan+arccot,x) by A7,A9,
VALUED_1:def 1
.= (arctan.x+arccot.x)*(sin.x/(cos.x)^2)+sec.x*diff(arctan+arccot,x)
by A10,FDIFF_9:1
.= (arctan.x+arccot.x)*sin.x/(cos.x)^2+sec.x*((arctan+arccot)`|Z).x by A3
,A9,FDIFF_1:def 7
.= (arctan.x+arccot.x)*sin.x/(cos.x)^2+sec.x*0 by A2,A9,Th37
.= (arctan.x+arccot.x)*sin.x/(cos.x)^2;
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=sec.x*(arctan.x-arccot.x)
theorem
Z c= dom sec & Z c= ].-1,1.[ implies sec(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((sec(#)(arctan-arccot))`|Z).x =
(arctan.x-arccot.x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2)
proof
assume that
A1: Z c= dom sec and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
for x st x in Z holds sec is_differentiable_in x
proof
let x;
assume x in Z;
then cos.x <> 0 by A1,RFUNCT_1:3;
hence thesis by FDIFF_9:1;
end;
then
A4: sec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom sec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (sec(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds ((sec(#)(arctan-arccot))`|Z).x = (arctan.x-arccot
.x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then
A10: cos.x <> 0 by A1,RFUNCT_1:3;
(sec(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(sec,x)+sec.x*
diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(sec,x)+sec.x*diff(arctan-arccot,x) by A7,A9,
VALUED_1:13
.= (arctan.x-arccot.x)*(sin.x/(cos.x)^2)+sec.x*diff(arctan-arccot,x)
by A10,FDIFF_9:1
.= (arctan.x-arccot.x)*sin.x/(cos.x)^2+sec.x*((arctan-arccot)`|Z).x by A3
,A9,FDIFF_1:def 7
.= (arctan.x-arccot.x)*sin.x/(cos.x)^2+sec.x*(2/(1+x^2)) by A2,A9,Th38
.= (arctan.x-arccot.x)*sin.x/(cos.x)^2+2*sec.x/(1+x^2);
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=cosec.x*(arctan.x+arccot.x)
theorem
Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan+arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)(arctan+arccot))`|Z).x
= -(arctan.x+arccot.x)*cos.x/(sin.x)^2
proof
assume that
A1: Z c= dom cosec and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A1,RFUNCT_1:3;
hence thesis by FDIFF_9:2;
end;
then
A4: cosec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom cosec /\ dom (arctan+arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (cosec(#)(arctan+arccot)) by VALUED_1:def 4;
for x st x in Z holds (cosec(#)(arctan+arccot)`|Z).x = -(arctan.x+
arccot.x)*cos.x/(sin.x)^2
proof
let x;
assume
A9: x in Z;
then
A10: sin.x <> 0 by A1,RFUNCT_1:3;
(cosec(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(cosec,x)+
cosec.x*diff(arctan+arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(cosec,x)+cosec.x*diff(arctan+arccot,x) by A7
,A9,VALUED_1:def 1
.= (arctan.x+arccot.x)*(-cos.x/(sin.x)^2) +cosec.x*diff(arctan+arccot,
x) by A10,FDIFF_9:2
.= -(arctan.x+arccot.x)*cos.x/(sin.x)^2+cosec.x*((arctan+arccot)`|Z).x
by A3,A9,FDIFF_1:def 7
.= -(arctan.x+arccot.x)*cos.x/(sin.x)^2+cosec.x*0 by A2,A9,Th37
.= -(arctan.x+arccot.x)*cos.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=cosec.x*(arctan.x-arccot.x)
theorem
Z c= dom cosec & Z c= ].-1,1.[ implies cosec(#)(arctan-arccot)
is_differentiable_on Z & for x st x in Z holds ((cosec(#)(arctan-arccot))`|Z).x
= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2)
proof
assume that
A1: Z c= dom cosec and
A2: Z c= ].-1,1.[;
A3: arctan-arccot is_differentiable_on Z by A2,Th38;
for x st x in Z holds cosec is_differentiable_in x
proof
let x;
assume x in Z;
then sin.x <> 0 by A1,RFUNCT_1:3;
hence thesis by FDIFF_9:2;
end;
then
A4: cosec is_differentiable_on Z by A1,FDIFF_1:9;
A5: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A6: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A5,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A6,XBOOLE_1:19;
then
A7: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom cosec /\ dom (arctan-arccot) by A1,XBOOLE_1:19;
then
A8: Z c= dom (cosec(#)(arctan-arccot)) by VALUED_1:def 4;
for x st x in Z holds (cosec(#)(arctan-arccot)`|Z).x = -(arctan.x-
arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2)
proof
let x;
assume
A9: x in Z;
then
A10: sin.x <> 0 by A1,RFUNCT_1:3;
(cosec(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(cosec,x)+
cosec.x*diff(arctan-arccot,x) by A8,A4,A3,A9,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(cosec,x)+cosec.x*diff(arctan-arccot,x) by A7
,A9,VALUED_1:13
.= (arctan.x-arccot.x)*(-cos.x/(sin.x)^2) +cosec.x*diff(arctan-arccot,
x) by A10,FDIFF_9:2
.= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+cosec.x*((arctan-arccot)`|Z).x
by A3,A9,FDIFF_1:def 7
.= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+cosec.x*(2/(1+x^2)) by A2,A9,Th38
.= -(arctan.x-arccot.x)*cos.x/(sin.x)^2+2*cosec.x/(1+x^2);
hence thesis;
end;
hence thesis by A8,A4,A3,FDIFF_1:21;
end;
::f.x=exp_R.x*(arctan.x+arccot.x)
theorem
Z c= ].-1,1.[ implies exp_R(#)(arctan+arccot) is_differentiable_on Z &
for x st x in Z holds ((exp_R(#)(arctan+arccot))`|Z).x = exp_R.x*(arctan.x+
arccot.x)
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan+arccot is_differentiable_on Z by Th37;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan+arccot) by VALUED_1:def 1;
then Z c= dom exp_R /\ dom (arctan+arccot) by TAYLOR_1:16,XBOOLE_1:19;
then
A6: Z c= dom (exp_R(#)(arctan+arccot)) by VALUED_1:def 4;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds (exp_R(#)(arctan+arccot)`|Z).x = exp_R.x*(arctan.
x+arccot.x)
proof
let x;
assume
A8: x in Z;
then (exp_R(#)(arctan+arccot)`|Z).x = ((arctan+arccot).x)*diff(exp_R,x)+
exp_R.x*diff(arctan+arccot,x) by A6,A7,A2,FDIFF_1:21
.= (arctan.x+arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan+arccot,x) by A5
,A8,VALUED_1:def 1
.= (arctan.x+arccot.x)*exp_R.x+exp_R.x*diff(arctan+arccot,x) by
TAYLOR_1:16
.= (arctan.x+arccot.x)*exp_R.x+exp_R.x*((arctan+arccot)`|Z).x by A2,A8,
FDIFF_1:def 7
.= (arctan.x+arccot.x)*exp_R.x+exp_R.x*0 by A1,A8,Th37
.= exp_R.x*(arctan.x+arccot.x);
hence thesis;
end;
hence thesis by A6,A7,A2,FDIFF_1:21;
end;
::f.x=exp_R.x*(arctan.x-arccot.x)
theorem
Z c= ].-1,1.[ implies exp_R(#)(arctan-arccot) is_differentiable_on Z &
for x st x in Z holds ((exp_R(#)(arctan-arccot))`|Z).x = exp_R.x*(arctan.x-
arccot.x)+2*exp_R.x/(1+x^2)
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan-arccot is_differentiable_on Z by Th38;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
then Z c= dom exp_R /\ dom (arctan-arccot) by TAYLOR_1:16,XBOOLE_1:19;
then
A6: Z c= dom (exp_R(#)(arctan-arccot)) by VALUED_1:def 4;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
for x st x in Z holds (exp_R(#)(arctan-arccot)`|Z).x = exp_R.x*(arctan.
x-arccot.x)+2*exp_R.x/(1+x^2)
proof
let x;
assume
A8: x in Z;
then (exp_R(#)(arctan-arccot)`|Z).x = ((arctan-arccot).x)*diff(exp_R,x)+
exp_R.x*diff(arctan-arccot,x) by A6,A7,A2,FDIFF_1:21
.= (arctan.x-arccot.x)*diff(exp_R,x)+exp_R.x*diff(arctan-arccot,x) by A5
,A8,VALUED_1:13
.= (arctan.x-arccot.x)*exp_R.x+exp_R.x*diff(arctan-arccot,x) by
TAYLOR_1:16
.= (arctan.x-arccot.x)*exp_R.x+exp_R.x*((arctan-arccot)`|Z).x by A2,A8,
FDIFF_1:def 7
.= (arctan.x-arccot.x)*exp_R.x+exp_R.x*(2/(1+x^2)) by A1,A8,Th38
.= exp_R.x*(arctan.x-arccot.x)+2*exp_R.x/(1+x^2);
hence thesis;
end;
hence thesis by A6,A7,A2,FDIFF_1:21;
end;
::f.x=(arctan.x+arccot.x)/exp_R.x
theorem
Z c= ].-1,1.[ implies (arctan+arccot)/exp_R is_differentiable_on Z &
for x st x in Z holds (((arctan+arccot)/exp_R)`|Z).x = -(arctan.x+arccot.x)/
exp_R.x
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan+arccot is_differentiable_on Z by Th37;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan+arccot) by VALUED_1:def 1;
A6: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
then
A7: (arctan+arccot)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
for x st x in Z holds (((arctan+arccot)/exp_R)`|Z).x = -(arctan.x+
arccot.x)/exp_R.x
proof
let x;
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: exp_R.x <>0 by SIN_COS:54;
assume
A10: x in Z;
then
A11: arctan+arccot is_differentiable_in x by A2,FDIFF_1:9;
(((arctan+arccot)/exp_R)`|Z).x = diff((arctan+arccot)/exp_R,x) by A7,A10,
FDIFF_1:def 7
.= (diff(arctan+arccot,x)*exp_R.x-diff(exp_R,x)*(arctan+arccot).x) /(
exp_R.x)^2 by A11,A8,A9,FDIFF_2:14
.= (((arctan+arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan+arccot).x) /(
exp_R.x)^2 by A2,A10,FDIFF_1:def 7
.= (0*exp_R.x-diff(exp_R,x)*(arctan+arccot).x)/(exp_R.x)^2 by A1,A10,Th37
.= -diff(exp_R,x)*(arctan+arccot).x/(exp_R.x)^2
.= -exp_R.x*(arctan+arccot).x/(exp_R.x)^2 by SIN_COS:65
.= -(arctan.x+arccot.x)*exp_R.x/(exp_R.x*exp_R.x) by A5,A10,
VALUED_1:def 1
.= -(arctan.x+arccot.x)*(exp_R.x/(exp_R.x*exp_R.x))
.= -(arctan.x+arccot.x)*(exp_R.x/exp_R.x/exp_R.x) by XCMPLX_1:78
.= -(arctan.x+arccot.x)*(1/exp_R.x) by A9,XCMPLX_1:60
.= -(arctan.x+arccot.x)/exp_R.x;
hence thesis;
end;
hence thesis by A2,A6,FDIFF_2:21;
end;
::f.x=(arctan.x-arccot.x)/exp_R.x
theorem
Z c= ].-1,1.[ implies (arctan-arccot)/exp_R is_differentiable_on Z &
for x st x in Z holds (((arctan-arccot)/exp_R)`|Z).x = ((2/(1+x^2))-arctan.x+
arccot.x)/exp_R.x
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan-arccot is_differentiable_on Z by Th38;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by
FDIFF_1:26,SIN_COS:54,TAYLOR_1:16;
then
A7: (arctan-arccot)/exp_R is_differentiable_on Z by A2,FDIFF_2:21;
for x st x in Z holds (((arctan-arccot)/exp_R)`|Z).x = ((2/(1+x^2))-
arctan.x+arccot.x)/exp_R.x
proof
let x;
A8: exp_R is_differentiable_in x by SIN_COS:65;
A9: exp_R.x <>0 by SIN_COS:54;
assume
A10: x in Z;
then
A11: arctan-arccot is_differentiable_in x by A2,FDIFF_1:9;
(((arctan-arccot)/exp_R)`|Z).x = diff((arctan-arccot)/exp_R,x) by A7,A10,
FDIFF_1:def 7
.= (diff(arctan-arccot,x)*exp_R.x-diff(exp_R,x)*(arctan-arccot).x) /(
exp_R.x)^2 by A11,A8,A9,FDIFF_2:14
.= (((arctan-arccot)`|Z).x*exp_R.x-diff(exp_R,x)*(arctan-arccot).x) /(
exp_R.x)^2 by A2,A10,FDIFF_1:def 7
.= ((2/(1+x^2))*exp_R.x-diff(exp_R,x)*(arctan-arccot).x)/(exp_R.x)^2
by A1,A10,Th38
.= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan-arccot).x)/(exp_R.x)^2 by
SIN_COS:65
.= ((2/(1+x^2))*exp_R.x-exp_R.x*(arctan.x-arccot.x))/(exp_R.x)^2 by A5
,A10,VALUED_1:13
.= ((2/(1+x^2))-(arctan.x-arccot.x))*(exp_R.x/(exp_R.x*exp_R.x))
.= ((2/(1+x^2))-(arctan.x-arccot.x))*(exp_R.x/exp_R.x/exp_R.x) by
XCMPLX_1:78
.= ((2/(1+x^2))-(arctan.x-arccot.x))*(1/exp_R.x) by A9,XCMPLX_1:60
.= ((2/(1+x^2))-arctan.x+arccot.x)/exp_R.x;
hence thesis;
end;
hence thesis by A2,A6,FDIFF_2:21;
end;
::f.x=exp_R.(arctan.x+arccot.x)
theorem
Z c= dom (exp_R*(arctan+arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan
+arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan+arccot)
`|Z).x = 0
proof
assume that
A1: Z c= dom (exp_R*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds exp_R*(arctan+arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:65;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: exp_R*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (exp_R*(arctan+arccot)`|Z).x = 0
proof
let x;
A7: exp_R is_differentiable_in (arctan+arccot).x by SIN_COS:65;
assume
A8: x in Z;
then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
(exp_R*(arctan+arccot)`|Z).x = diff(exp_R*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
.= diff(exp_R,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
.= exp_R.((arctan+arccot).x)*diff((arctan+arccot),x) by SIN_COS:65
.= exp_R.((arctan+arccot).x)*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= exp_R.((arctan+arccot).x)*0 by A2,A8,Th37
.= 0;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=exp_R.(arctan.x-arccot.x)
theorem
Z c= dom (exp_R*(arctan-arccot)) & Z c= ].-1,1.[ implies exp_R*(arctan
-arccot) is_differentiable_on Z & for x st x in Z holds (exp_R*(arctan-arccot)
`|Z).x = 2*exp_R.(arctan.x-arccot.x)/(1+x^2)
proof
assume that
A1: Z c= dom (exp_R*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds exp_R*(arctan-arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:65;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: exp_R*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (exp_R*(arctan-arccot)`|Z).x = 2*exp_R.(arctan.x-
arccot.x)/(1+x^2)
proof
let x;
A10: exp_R is_differentiable_in (arctan-arccot).x by SIN_COS:65;
assume
A11: x in Z;
then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
(exp_R*(arctan-arccot)`|Z).x = diff(exp_R*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
.= diff(exp_R,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
.= exp_R.((arctan-arccot).x)*diff((arctan-arccot),x) by SIN_COS:65
.= exp_R.((arctan-arccot).x)*((arctan-arccot)`|Z).x by A6,A11,
FDIFF_1:def 7
.= exp_R.((arctan-arccot).x)*(2/(1+x^2)) by A2,A11,Th38
.= exp_R.(arctan.x-arccot.x)*(2/(1+x^2)) by A5,A11,VALUED_1:13
.= 2*exp_R.(arctan.x-arccot.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
::f.x=sin.(arctan.x+arccot.x)
theorem
Z c= dom (sin*(arctan+arccot)) & Z c= ].-1,1.[ implies sin*(arctan+
arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan+arccot)`|Z)
.x = 0
proof
assume that
A1: Z c= dom (sin*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds sin*(arctan+arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
sin is_differentiable_in (arctan+arccot).x by SIN_COS:64;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin*(arctan+arccot)`|Z).x = 0
proof
let x;
A7: sin is_differentiable_in (arctan+arccot).x by SIN_COS:64;
assume
A8: x in Z;
then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
(sin*(arctan+arccot)`|Z).x = diff(sin*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
.= diff(sin,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
.= cos.((arctan+arccot).x)*diff((arctan+arccot),x) by SIN_COS:64
.= cos.((arctan+arccot).x)*((arctan+arccot)`|Z).x by A3,A8,FDIFF_1:def 7
.= cos.((arctan+arccot).x)*0 by A2,A8,Th37
.= 0;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=sin.(arctan.x-arccot.x)
theorem
Z c= dom (sin*(arctan-arccot)) & Z c= ].-1,1.[ implies sin*(arctan-
arccot) is_differentiable_on Z & for x st x in Z holds (sin*(arctan-arccot)`|Z)
.x = 2*cos.(arctan.x-arccot.x)/(1+x^2)
proof
assume that
A1: Z c= dom (sin*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds sin*(arctan-arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
sin is_differentiable_in (arctan-arccot).x by SIN_COS:64;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: sin*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (sin*(arctan-arccot)`|Z).x = 2*cos.(arctan.x-
arccot.x)/(1+x^2)
proof
let x;
A10: sin is_differentiable_in (arctan-arccot).x by SIN_COS:64;
assume
A11: x in Z;
then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
(sin*(arctan-arccot)`|Z).x = diff(sin*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
.= diff(sin,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
.= cos.((arctan-arccot).x)*diff((arctan-arccot),x) by SIN_COS:64
.= cos.((arctan-arccot).x)*((arctan-arccot)`|Z).x by A6,A11,FDIFF_1:def 7
.= cos.((arctan-arccot).x)*(2/(1+x^2)) by A2,A11,Th38
.= cos.(arctan.x-arccot.x)*(2/(1+x^2)) by A5,A11,VALUED_1:13
.= 2*cos.(arctan.x-arccot.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
::f.x=cos.(arctan.x+arccot.x)
theorem
Z c= dom (cos*(arctan+arccot)) & Z c= ].-1,1.[ implies cos*(arctan+
arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan+arccot)`|Z)
.x = 0
proof
assume that
A1: Z c= dom (cos*(arctan+arccot)) and
A2: Z c= ].-1,1.[;
A3: arctan+arccot is_differentiable_on Z by A2,Th37;
A4: for x st x in Z holds cos*(arctan+arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: (arctan+arccot) is_differentiable_in x by A3,FDIFF_1:9;
cos is_differentiable_in (arctan+arccot).x by SIN_COS:63;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*(arctan+arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos*(arctan+arccot)`|Z).x = 0
proof
let x;
A7: cos is_differentiable_in (arctan+arccot).x by SIN_COS:63;
assume
A8: x in Z;
then
A9: arctan+arccot is_differentiable_in x by A3,FDIFF_1:9;
(cos*(arctan+arccot)`|Z).x = diff(cos*(arctan+arccot),x) by A6,A8,
FDIFF_1:def 7
.= diff(cos,(arctan+arccot).x)*diff((arctan+arccot),x) by A9,A7,
FDIFF_2:13
.= (-sin.((arctan+arccot).x))*diff((arctan+arccot),x) by SIN_COS:63
.= (-sin.((arctan+arccot).x))*((arctan+arccot)`|Z).x by A3,A8,
FDIFF_1:def 7
.= (-sin.((arctan+arccot).x))*0 by A2,A8,Th37
.= 0;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
::f.x=cos.(arctan.x-arccot.x)
theorem
Z c= dom (cos*(arctan-arccot)) & Z c= ].-1,1.[ implies cos*(arctan-
arccot) is_differentiable_on Z & for x st x in Z holds (cos*(arctan-arccot)`|Z)
.x = -2*sin.(arctan.x-arccot.x)/(1+x^2)
proof
assume that
A1: Z c= dom (cos*(arctan-arccot)) and
A2: Z c= ].-1,1.[;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A2,XBOOLE_1:1;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A2,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A5: Z c= dom (arctan-arccot) by VALUED_1:12;
A6: arctan-arccot is_differentiable_on Z by A2,Th38;
A7: for x st x in Z holds cos*(arctan-arccot) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: (arctan-arccot) is_differentiable_in x by A6,FDIFF_1:9;
cos is_differentiable_in (arctan-arccot).x by SIN_COS:63;
hence thesis by A8,FDIFF_2:13;
end;
then
A9: cos*(arctan-arccot) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (cos*(arctan-arccot)`|Z).x = -2*sin.(arctan.x-
arccot.x)/(1+x^2)
proof
let x;
A10: cos is_differentiable_in (arctan-arccot).x by SIN_COS:63;
assume
A11: x in Z;
then
A12: arctan-arccot is_differentiable_in x by A6,FDIFF_1:9;
(cos*(arctan-arccot)`|Z).x = diff(cos*(arctan-arccot),x) by A9,A11,
FDIFF_1:def 7
.= diff(cos,(arctan-arccot).x)*diff((arctan-arccot),x) by A12,A10,
FDIFF_2:13
.= (-sin.((arctan-arccot).x))*diff((arctan-arccot),x) by SIN_COS:63
.= (-sin.((arctan-arccot).x))*((arctan-arccot)`|Z).x by A6,A11,
FDIFF_1:def 7
.= (-sin.((arctan-arccot).x))*(2/(1+x^2)) by A2,A11,Th38
.= (-sin.(arctan.x-arccot.x))*(2/(1+x^2)) by A5,A11,VALUED_1:13
.= -2*sin.(arctan.x-arccot.x)/(1+x^2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
::f.x=arctan.x*arccot.x
theorem
Z c= ].-1,1.[ implies arctan(#)arccot is_differentiable_on Z & for x
st x in Z holds ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1+x^2)
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arctan is_differentiable_on Z by SIN_COS9:81;
A3: ].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then ].-1,1.[ c= dom arccot by SIN_COS9:24,XBOOLE_1:1;
then
A4: Z c= dom arccot by A1,XBOOLE_1:1;
A5: arccot is_differentiable_on Z by A1,SIN_COS9:82;
].-1,1.[ c= dom arctan by A3,SIN_COS9:23,XBOOLE_1:1;
then Z c= dom arctan by A1,XBOOLE_1:1;
then Z c= dom arctan /\ dom arccot by A4,XBOOLE_1:19;
then
A6: Z c= dom(arctan(#)arccot) by VALUED_1:def 4;
for x st x in Z holds ((arctan(#)arccot)`|Z).x = (arccot.x-arctan.x)/(1 +x^2)
proof
let x;
assume
A7: x in Z;
then
((arctan(#)arccot)`|Z).x = (arccot.x)*diff(arctan,x)+(arctan.x)*diff(
arccot,x) by A6,A2,A5,FDIFF_1:21
.= arccot.x*((arctan)`|Z).x+arctan.x*diff(arccot,x) by A2,A7,
FDIFF_1:def 7
.= arccot.x*(1/(1+x^2))+arctan.x*diff(arccot,x) by A1,A7,SIN_COS9:81
.= arccot.x*(1/(1+x^2))+arctan.x*((arccot)`|Z).x by A5,A7,FDIFF_1:def 7
.= arccot.x*(1/(1+x^2))+arctan.x*(-1/(1+x^2)) by A1,A7,SIN_COS9:82
.= (arccot.x-arctan.x)/(1+x^2);
hence thesis;
end;
hence thesis by A6,A2,A5,FDIFF_1:21;
end;
::f.x=arctan.(1/x)*arccot.(1/x)
theorem
not 0 in Z & Z c= dom((arctan*((id Z)^))(#)(arccot*((id Z)^))) & (for
x st x in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (arctan*((id Z)^)
)(#)(arccot*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((arctan
*((id Z)^))(#)(arccot*((id Z)^)))`|Z).x = (arctan.(1/x)-arccot.(1/x))/(1+x^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom((arctan*(f^))(#)(arccot*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom(arctan*(f^)) /\ dom(arccot*(f^)) by A2,VALUED_1:def 4;
then
A5: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
then
A6: arctan*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:111;
A7: Z c= dom (arccot*(f^)) by A4,XBOOLE_1:18;
then
A8: arccot*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:112;
for y being object st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
then
A9: Z c= dom (f^) by TARSKI:def 3;
for x st x in Z holds (((arctan*(f^))(#)(arccot*(f^)))`|Z).x = (arctan.
(1/x)-arccot.(1/x))/(1+x^2)
proof
let x;
assume
A10: x in Z;
then (((arctan*(f^))(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff((
arctan*(f^)),x)+ ((arctan*(f^)).x)*diff(arccot*(f^),x) by A2,A6,A8,
FDIFF_1:21
.= ((arccot*(f^)).x)*((arctan*(f^))`|Z).x+ ((arctan*(f^)).x)*diff(
arccot*(f^),x) by A6,A10,FDIFF_1:def 7
.= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*diff(arccot*(f^),x
) by A1,A3,A5,A10,SIN_COS9:111
.= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*((arccot*(f^))`|Z)
.x by A8,A10,FDIFF_1:def 7
.= ((arccot*(f^)).x)*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A1,A3
,A7,A10,SIN_COS9:112
.= (arccot.((f^).x))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A7,A10
,FUNCT_1:12
.= (arccot.((f.x)"))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A9,A10
,RFUNCT_1:def 2
.= (arccot.(1/x))*(-1/(1+x^2))+((arctan*(f^)).x)*(1/(1+x^2)) by A10,
FUNCT_1:18
.= (arccot.(1/x))*(-1/(1+x^2))+(arctan.((f^).x))*(1/(1+x^2)) by A5,A10,
FUNCT_1:12
.= (arccot.(1/x))*(-1/(1+x^2))+(arctan.((f.x)"))*(1/(1+x^2)) by A9,A10,
RFUNCT_1:def 2
.= -(arccot.(1/x))*(1/(1+x^2))+(arctan.(1/x))*(1/(1+x^2)) by A10,
FUNCT_1:18
.= (arctan.(1/x)-arccot.(1/x))/(1+x^2);
hence thesis;
end;
hence thesis by A2,A6,A8,FDIFF_1:21;
end;
::f.x=x*arctan(1/x)
theorem
not 0 in Z & Z c= dom ((id Z)(#)(arctan*((id Z)^))) & (for x st x in Z
holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arctan*((id Z)^))
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arctan*((id Z)^)))`|
Z).x = arctan.(1/x)-x/(1+x^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom ((id Z)(#)(arctan*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom (id Z) /\ dom (arctan*(f^)) by A2,VALUED_1:def 4;
then
A5: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
then
A6: arctan*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:111;
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A8: Z c= dom id Z by A4,XBOOLE_1:18;
then
A9: id Z is_differentiable_on Z by A7,FDIFF_1:23;
for y being object st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
then
A10: Z c= dom (f^) by TARSKI:def 3;
for x st x in Z holds (((id Z)(#)(arctan*(f^)))`|Z).x = arctan.(1/x)-x/
(1+x^2)
proof
let x;
assume
A11: x in Z;
then
(((id Z)(#)(arctan*(f^)))`|Z).x = ((arctan*(f^)).x)*diff((id Z),x)+((
id Z).x)*diff(arctan*(f^),x) by A2,A6,A9,FDIFF_1:21
.= ((arctan*(f^)).x)*((id Z)`|Z).x+((id Z).x)*diff(arctan*(f^),x) by A9
,A11,FDIFF_1:def 7
.= ((arctan*(f^)).x)*1+((id Z).x)*diff(arctan*(f^),x) by A8,A7,A11,
FDIFF_1:23
.= ((arctan*(f^)).x)*1+x*diff(arctan*(f^),x) by A11,FUNCT_1:18
.= (arctan*(f^)).x+x*(((arctan*(f^))`|Z).x) by A6,A11,FDIFF_1:def 7
.= (arctan*(f^)).x+x*(-1/(1+x^2)) by A1,A3,A5,A11,SIN_COS9:111
.= arctan.((f^).x)-x/(1+x^2) by A5,A11,FUNCT_1:12
.= arctan.((f.x)")-x/(1+x^2) by A10,A11,RFUNCT_1:def 2
.= arctan.(1/x)-x/(1+x^2) by A11,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A6,A9,FDIFF_1:21;
end;
::f.x=x*arccot(1/x)
theorem
not 0 in Z & Z c= dom ((id Z)(#)(arccot*((id Z)^))) & (for x st x in Z
holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies (id Z)(#)(arccot*((id Z)^))
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(arccot*((id Z)^)))`|
Z).x = arccot.(1/x)+x/(1+x^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom ((id Z)(#)(arccot*(f^))) and
A3: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A4: Z c= dom (id Z) /\ dom (arccot*(f^)) by A2,VALUED_1:def 4;
then
A5: Z c= dom (arccot*(f^)) by XBOOLE_1:18;
then
A6: arccot*(f^) is_differentiable_on Z by A1,A3,SIN_COS9:112;
A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A8: Z c= dom id Z by A4,XBOOLE_1:18;
then
A9: id Z is_differentiable_on Z by A7,FDIFF_1:23;
for y being object st y in Z holds y in dom (f^) by A5,FUNCT_1:11;
then
A10: Z c= dom (f^) by TARSKI:def 3;
for x st x in Z holds (((id Z)(#)(arccot*(f^)))`|Z).x = arccot.(1/x)+x/
(1+x^2)
proof
let x;
assume
A11: x in Z;
then
(((id Z)(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff((id Z),x)+((
id Z).x)*diff(arccot*(f^),x) by A2,A6,A9,FDIFF_1:21
.= ((arccot*(f^)).x)*((id Z)`|Z).x+((id Z).x)*diff(arccot*(f^),x) by A9
,A11,FDIFF_1:def 7
.= ((arccot*(f^)).x)*1+((id Z).x)*diff(arccot*(f^),x) by A8,A7,A11,
FDIFF_1:23
.= ((arccot*(f^)).x)*1+x*diff(arccot*(f^),x) by A11,FUNCT_1:18
.= (arccot*(f^)).x+x*(((arccot*(f^))`|Z).x) by A6,A11,FDIFF_1:def 7
.= (arccot*(f^)).x+x*(1/(1+x^2)) by A1,A3,A5,A11,SIN_COS9:112
.= arccot.((f^).x)+x/(1+x^2) by A5,A11,FUNCT_1:12
.= arccot.((f.x)")+x/(1+x^2) by A10,A11,RFUNCT_1:def 2
.= arccot.(1/x)+x/(1+x^2) by A11,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A6,A9,FDIFF_1:21;
end;
::f.x=x^2*arctan(1/x)
theorem
not 0 in Z & Z c= dom (g(#)(arctan*((id Z)^))) & g=#Z 2 & (for x st x
in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arctan*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((g(#)(arctan*((id Z)^)))`|Z).x
= 2*x*arctan.(1/x)-x^2/(1+x^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(arctan*(f^))) and
A3: g=#Z 2 and
A4: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A5: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A6: Z c= dom g /\ dom (arctan*(f^)) by A2,VALUED_1:def 4;
then
A7: Z c= dom (arctan*(f^)) by XBOOLE_1:18;
then
A8: arctan*(f^) is_differentiable_on Z by A1,A4,SIN_COS9:111;
Z c= dom g by A6,XBOOLE_1:18;
then
A9: g is_differentiable_on Z by A5,FDIFF_1:9;
A10: for x st x in Z holds (g`|Z).x = 2*x
proof
let x;
assume x in Z;
then (g`|Z).x = diff(g,x) by A9,FDIFF_1:def 7
.= 2*(x #Z (2-1)) by A3,TAYLOR_1:2
.= 2*x by PREPOWER:35;
hence thesis;
end;
for y being object st y in Z holds y in dom (f^) by A7,FUNCT_1:11;
then
A11: Z c= dom (f^) by TARSKI:def 3;
for x st x in Z holds ((g(#)(arctan*(f^)))`|Z).x = 2*x*arctan.(1/x)-x^2
/(1+x^2)
proof
let x;
assume
A12: x in Z;
then ((g(#)(arctan*(f^)))`|Z).x = ((arctan*(f^)).x)*diff(g,x)+(g.x)*diff(
arctan*(f^),x) by A2,A8,A9,FDIFF_1:21
.= ((arctan*(f^)).x)*(g`|Z).x+(g.x)*diff(arctan*(f^),x) by A9,A12,
FDIFF_1:def 7
.= ((arctan*(f^)).x)*(2*x)+(g.x)*diff(arctan*(f^),x) by A10,A12
.= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*diff(arctan*(f^),x) by A3,
TAYLOR_1:def 1
.= ((arctan*(f^)).x)*(2*x)+(x #Z 2)*(((arctan*(f^))`|Z).x ) by A8,A12,
FDIFF_1:def 7
.= ((arctan*(f^)).x)*(2*x)+(x #Z (1+1))*(-1/(1+x^2)) by A1,A4,A7,A12,
SIN_COS9:111
.= ((arctan*(f^)).x)*(2*x)+((x #Z 1)*(x #Z 1))*(-1/(1+x^2)) by TAYLOR_1:1
.= ((arctan*(f^)).x)*(2*x)+(x*(x #Z 1))*(-1/(1+x^2)) by PREPOWER:35
.= ((arctan*(f^)).x)*(2*x)+x^2*(-1/(1+x^2)) by PREPOWER:35
.= arctan.((f^).x)*(2*x)-x^2/(1+x^2) by A7,A12,FUNCT_1:12
.= arctan.((f.x)")*(2*x)-x^2/(1+x^2) by A11,A12,RFUNCT_1:def 2
.= 2*x*arctan.(1/x)-x^2/(1+x^2) by A12,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A8,A9,FDIFF_1:21;
end;
::f.x=x^2*arccot(1/x)
theorem
not 0 in Z & Z c= dom (g(#)(arccot*((id Z)^))) & g=#Z 2 & (for x st x
in Z holds ((id Z)^).x > -1 & ((id Z)^).x < 1) implies g(#)(arccot*((id Z)^))
is_differentiable_on Z & for x st x in Z holds ((g(#)(arccot*((id Z)^)))`|Z).x
= 2*x*arccot.(1/x)+x^2/(1+x^2)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(arccot*(f^))) and
A3: g=#Z 2 and
A4: for x st x in Z holds (f^).x > -1 & (f^).x < 1;
A5: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A6: Z c= dom g /\ dom (arccot*(f^)) by A2,VALUED_1:def 4;
then
A7: Z c= dom (arccot*(f^)) by XBOOLE_1:18;
then
A8: arccot*(f^) is_differentiable_on Z by A1,A4,SIN_COS9:112;
Z c= dom g by A6,XBOOLE_1:18;
then
A9: g is_differentiable_on Z by A5,FDIFF_1:9;
A10: for x st x in Z holds (g`|Z).x = 2*x
proof
let x;
assume x in Z;
then (g`|Z).x = diff(g,x) by A9,FDIFF_1:def 7
.= 2*(x #Z (2-1)) by A3,TAYLOR_1:2
.= 2*x by PREPOWER:35;
hence thesis;
end;
for y being object st y in Z holds y in dom (f^) by A7,FUNCT_1:11;
then
A11: Z c= dom (f^) by TARSKI:def 3;
for x st x in Z holds ((g(#)(arccot*(f^)))`|Z).x = 2*x*arccot.(1/x)+x^2
/(1+x^2)
proof
let x;
assume
A12: x in Z;
then ((g(#)(arccot*(f^)))`|Z).x = ((arccot*(f^)).x)*diff(g,x)+(g.x)*diff(
arccot*(f^),x) by A2,A8,A9,FDIFF_1:21
.= ((arccot*(f^)).x)*(g`|Z).x+(g.x)*diff(arccot*(f^),x) by A9,A12,
FDIFF_1:def 7
.= ((arccot*(f^)).x)*(2*x)+(g.x)*diff(arccot*(f^),x) by A10,A12
.= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*diff(arccot*(f^),x) by A3,
TAYLOR_1:def 1
.= ((arccot*(f^)).x)*(2*x)+(x #Z 2)*(((arccot*(f^))`|Z).x ) by A8,A12,
FDIFF_1:def 7
.= ((arccot*(f^)).x)*(2*x)+(x #Z (1+1))*(1/(1+x^2)) by A1,A4,A7,A12,
SIN_COS9:112
.= ((arccot*(f^)).x)*(2*x)+((x #Z 1)*(x #Z 1))*(1/(1+x^2)) by TAYLOR_1:1
.= ((arccot*(f^)).x)*(2*x)+(x*(x #Z 1))*(1/(1+x^2)) by PREPOWER:35
.= ((arccot*(f^)).x)*(2*x)+x^2/(1+x^2) by PREPOWER:35
.= arccot.((f^).x)*(2*x)+x^2/(1+x^2) by A7,A12,FUNCT_1:12
.= arccot.((f.x)")*(2*x)+x^2/(1+x^2) by A11,A12,RFUNCT_1:def 2
.= 2*x*arccot.(1/x)+x^2/(1+x^2) by A12,FUNCT_1:18;
hence thesis;
end;
hence thesis by A2,A8,A9,FDIFF_1:21;
end;
::f.x=1/arctan.x
theorem Th67:
Z c= ].-1,1.[ & (for x st x in Z holds arctan.x<>0) implies
arctan^ is_differentiable_on Z & for x st x in Z holds ((arctan^)`|Z).x = -1/((
arctan.x)^2*(1+x^2))
proof
assume that
A1: Z c= ].-1,1.[ and
A2: for x st x in Z holds arctan.x<>0;
A3: arctan is_differentiable_on Z by A1,SIN_COS9:81;
then
A4: arctan^ is_differentiable_on Z by A2,FDIFF_2:22;
for x st x in Z holds ((arctan^)`|Z).x = -1/((arctan.x)^2*(1+x^2))
proof
let x;
assume
A5: x in Z;
then
A6: arctan.x<>0 & arctan is_differentiable_in x by A2,A3,FDIFF_1:9;
((arctan^)`|Z).x = diff(arctan^,x) by A4,A5,FDIFF_1:def 7
.= -diff(arctan,x)/(arctan.x)^2 by A6,FDIFF_2:15
.= -((arctan)`|Z).x/(arctan.x)^2 by A3,A5,FDIFF_1:def 7
.= -(1/(1+x^2))/(arctan.x)^2 by A1,A5,SIN_COS9:81
.= -1/((arctan.x)^2*(1+x^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A2,A3,FDIFF_2:22;
end;
::f.x=1/arccot.x
theorem Th68:
Z c= ].-1,1.[ implies arccot^ is_differentiable_on Z & for x st
x in Z holds ((arccot^)`|Z).x= 1/((arccot.x)^2*(1+x^2))
proof
assume
A1: Z c= ].-1,1.[;
then
A2: arccot is_differentiable_on Z by SIN_COS9:82;
A3: for x st x in Z holds arccot.x<>0
proof
PI in ].0,4.[ by SIN_COS:def 28;
then PI > 0 by XXREAL_1:4;
then
A4: PI/4 > 0/4 by XREAL_1:74;
let x;
assume
A5: x in Z;
assume
A6: arccot.x=0;
].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then Z c= [.-1,1.] by A1,XBOOLE_1:1;
then x in [.-1,1.] by A5;
then 0 in arccot.:[.-1,1.] by A6,FUNCT_1:def 6,SIN_COS9:24;
then 0 in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
hence contradiction by A4,XXREAL_1:1;
end;
then
A7: arccot^ is_differentiable_on Z by A2,FDIFF_2:22;
for x st x in Z holds ((arccot^)`|Z).x = 1/((arccot.x)^2*(1+x^2))
proof
let x;
assume
A8: x in Z;
then
A9: arccot.x<>0 & arccot is_differentiable_in x by A3,A2,FDIFF_1:9;
((arccot^)`|Z).x = diff(arccot^,x) by A7,A8,FDIFF_1:def 7
.= -diff(arccot,x)/(arccot.x)^2 by A9,FDIFF_2:15
.= -((arccot)`|Z).x/(arccot.x)^2 by A2,A8,FDIFF_1:def 7
.= -(-1/(1+x^2))/(arccot.x)^2 by A1,A8,SIN_COS9:82
.= (1/(1+x^2))/(arccot.x)^2
.= 1/((arccot.x)^2*(1+x^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A3,A2,FDIFF_2:22;
end;
::f.x=1/(n*(arctan.x)|^n)
theorem
Z c= dom ((1/n)(#)(( #Z n)*(arctan^))) & Z c= ].-1,1.[ & n>0 & (for x
st x in Z holds arctan.x<>0) implies (1/n)(#)(( #Z n)*(arctan^))
is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*(arctan^)))`|
Z).x = -1/(((arctan.x) #Z (n+1))*(1+x^2))
proof
assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*(arctan^))) and
A2: Z c= ].-1,1.[ and
A3: n>0 and
A4: for x st x in Z holds arctan.x<>0;
A5: Z c= dom (( #Z n)*(arctan^)) by A1,VALUED_1:def 5;
A6: arctan^ is_differentiable_on Z by A2,A4,Th67;
for x st x in Z holds ( #Z n)*(arctan^) is_differentiable_in x
proof
let x;
assume x in Z;
then arctan^ is_differentiable_in x by A6,FDIFF_1:9;
hence thesis by TAYLOR_1:3;
end;
then
A7: ( #Z n)*(arctan^) is_differentiable_on Z by A5,FDIFF_1:9;
for y being object st y in Z holds y in dom (arctan^) by A5,FUNCT_1:11;
then
A8: Z c= dom (arctan^) by TARSKI:def 3;
for x st x in Z holds (((1/n)(#)(( #Z n)*(arctan^)))`|Z).x = -1/(((
arctan.x) #Z (n+1))*(1+x^2))
proof
let x;
assume
A9: x in Z;
then
A10: arctan^ is_differentiable_in x by A6,FDIFF_1:9;
A11: (arctan^).x = 1/arctan.x by A8,A9,RFUNCT_1:def 2;
(((1/n)(#)(( #Z n)*(arctan^)))`|Z).x = (1/n)*diff((( #Z n)*(arctan^))
,x) by A1,A7,A9,FDIFF_1:20
.= (1/n)*(n*(((arctan^).x) #Z (n-1))*diff(arctan^,x)) by A10,TAYLOR_1:3
.= (1/n)*(n*(((arctan^).x) #Z (n-1))*((arctan^)`|Z).x) by A6,A9,
FDIFF_1:def 7
.= (1/n)*(n*(((arctan^).x) #Z (n-1))*(-1/((arctan.x)^2*(1+x^2)))) by A2
,A4,A9,Th67
.= -((1/n)*n)*(((arctan^).x) #Z (n-1))*(1/((arctan.x)^2*(1+x^2)))
.= -1*(((arctan^).x) #Z (n-1))*(1/((arctan.x)^2*(1+x^2))) by A3,
XCMPLX_1:106
.= -((1/arctan.x) #Z (n-1))*(1/(((arctan.x) #Z 2)*(1+x^2))) by A11,
FDIFF_7:1
.= -(1/((arctan.x) #Z (n-1)))/(((arctan.x) #Z 2)*(1+x^2)) by PREPOWER:42
.= -1/(((arctan.x) #Z (n-1))*(((arctan.x) #Z 2)*(1+x^2))) by XCMPLX_1:78
.= -1/(((arctan.x) #Z (n-1))*((arctan.x) #Z 2)*(1+x^2))
.= -1/(((arctan.x) #Z ((n-1)+2))*(1+x^2)) by A4,A9,PREPOWER:44
.= -1/(((arctan.x) #Z (n+1))*(1+x^2));
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
::f.x=1/(n*(arccot.x)|^n)
theorem
Z c= dom ((1/n)(#)(( #Z n)*(arccot^))) & Z c= ].-1,1.[ & n>0 implies (
1/n)(#)(( #Z n)*(arccot^)) is_differentiable_on Z & for x st x in Z holds (((1/
n)(#)(( #Z n)*(arccot^)))`|Z).x = 1/(((arccot.x) #Z (n+1))*(1+x^2))
proof
assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*(arccot^))) and
A2: Z c= ].-1,1.[ and
A3: n>0;
A4: Z c= dom (( #Z n)*(arccot^)) by A1,VALUED_1:def 5;
A5: for x st x in Z holds arccot.x<>0
proof
PI in ].0,4.[ by SIN_COS:def 28;
then PI > 0 by XXREAL_1:4;
then
A6: PI/4 > 0/4 by XREAL_1:74;
let x;
assume
A7: x in Z;
assume
A8: arccot.x=0;
].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then Z c= [.-1,1.] by A2,XBOOLE_1:1;
then x in [.-1,1.] by A7;
then 0 in arccot.:[.-1,1.] by A8,FUNCT_1:def 6,SIN_COS9:24;
then 0 in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
hence contradiction by A6,XXREAL_1:1;
end;
A9: arccot^ is_differentiable_on Z by A2,Th68;
for x st x in Z holds ( #Z n)*(arccot^) is_differentiable_in x
proof
let x;
assume x in Z;
then arccot^ is_differentiable_in x by A9,FDIFF_1:9;
hence thesis by TAYLOR_1:3;
end;
then
A10: ( #Z n)*(arccot^) is_differentiable_on Z by A4,FDIFF_1:9;
for y being object st y in Z holds y in dom (arccot^) by A4,FUNCT_1:11;
then
A11: Z c= dom (arccot^) by TARSKI:def 3;
for x st x in Z holds (((1/n)(#)(( #Z n)*(arccot^)))`|Z).x = 1/(((
arccot.x) #Z (n+1))*(1+x^2))
proof
let x;
assume
A12: x in Z;
then
A13: arccot^ is_differentiable_in x by A9,FDIFF_1:9;
A14: (arccot^).x = 1/arccot.x by A11,A12,RFUNCT_1:def 2;
(((1/n)(#)(( #Z n)*(arccot^)))`|Z).x = (1/n)*diff((( #Z n)*(arccot^))
,x) by A1,A10,A12,FDIFF_1:20
.= (1/n)*(n*(((arccot^).x) #Z (n-1))*diff(arccot^,x)) by A13,TAYLOR_1:3
.= (1/n)*(n*(((arccot^).x) #Z (n-1))*((arccot^)`|Z).x) by A9,A12,
FDIFF_1:def 7
.= (1/n)*(n*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2)))) by A2
,A12,Th68
.= ((1/n)*n)*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2)))
.= 1*(((arccot^).x) #Z (n-1))*(1/((arccot.x)^2*(1+x^2))) by A3,
XCMPLX_1:106
.= ((1/arccot.x) #Z (n-1))*(1/(((arccot.x) #Z 2)*(1+x^2))) by A14,
FDIFF_7:1
.= (1/((arccot.x) #Z (n-1)))/(((arccot.x) #Z 2)*(1+x^2)) by PREPOWER:42
.= 1/(((arccot.x) #Z (n-1))*(((arccot.x) #Z 2)*(1+x^2))) by XCMPLX_1:78
.= 1/(((arccot.x) #Z (n-1))*((arccot.x) #Z 2)*(1+x^2))
.= 1/(((arccot.x) #Z ((n-1)+2))*(1+x^2)) by A5,A12,PREPOWER:44
.= 1/(((arccot.x) #Z (n+1))*(1+x^2));
hence thesis;
end;
hence thesis by A1,A10,FDIFF_1:20;
end;
::f.x=2*(arctan #R (1/2))
theorem
Z c= dom ((2(#)(( #R (1/2))*arctan))) & Z c= ].-1,1.[ & (for x st x in
Z holds arctan.x > 0) implies 2(#)(( #R (1/2))*arctan) is_differentiable_on Z &
for x st x in Z holds ((2(#)(( #R (1/2))*arctan))`|Z).x = (arctan.x) #R (-1/2)/
(1+x^2)
proof
assume that
A1: Z c= dom ((2(#)(( #R (1/2))*arctan))) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > 0;
A4: for x st x in Z holds ( #R (1/2))*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arctan.x > 0 by A3;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,TAYLOR_1:22;
end;
Z c= dom (( #R (1/2))*arctan) by A1,VALUED_1:def 5;
then
A7: ( #R (1/2))*arctan is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((2(#)(( #R (1/2))*arctan))`|Z).x = ((arctan.x)
#R (-1/2))/(1+x^2)
proof
let x;
assume
A8: x in Z;
then
A9: arctan.x > 0 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
((2(#)(( #R (1/2))*arctan))`|Z).x = 2*diff((( #R (1/2))*arctan),x) by A1,A7
,A8,FDIFF_1:20
.= 2*((1/2)*((arctan.x) #R (1/2-1))*diff(arctan,x)) by A11,A9,TAYLOR_1:22
.= 2*((1/2)*((arctan.x) #R (1/2-1))*((arctan)`|Z).x) by A8,A10,
FDIFF_1:def 7
.= 2*((1/2)*((arctan.x) #R (1/2-1))*(1/(1+x^2))) by A2,A8,SIN_COS9:81
.= ((arctan.x) #R (-1/2))/(1+x^2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
::f.x=2*(arccot #R (1/2))
theorem
Z c= dom ((2(#)(( #R (1/2))*arccot))) & Z c= ].-1,1.[ implies 2(#)((
#R (1/2))*arccot) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1
/2))*arccot))`|Z).x = -(arccot.x) #R (-1/2)/(1+x^2)
proof
assume that
A1: Z c= dom ((2(#)(( #R (1/2))*arccot))) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds arccot.x > 0
proof
let x;
].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then
A4: Z c= [.-1,1.] by A2,XBOOLE_1:1;
assume x in Z;
then x in [.-1,1.] by A4;
then arccot.x in arccot.:[.-1,1.] by FUNCT_1:def 6,SIN_COS9:24;
then arccot.x in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
then arccot.x >= PI/4 by XXREAL_1:1;
then
A5: arccot.x + 0 > PI/4 + (-PI/4) by XREAL_1:8;
assume arccot.x <= 0;
hence contradiction by A5;
end;
A6: for x st x in Z holds ( #R (1/2))*arccot is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then
A8: arccot.x > 0 by A3;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A7,FDIFF_1:9;
hence thesis by A8,TAYLOR_1:22;
end;
Z c= dom (( #R (1/2))*arccot) by A1,VALUED_1:def 5;
then
A9: ( #R (1/2))*arccot is_differentiable_on Z by A6,FDIFF_1:9;
for x st x in Z holds ((2(#)(( #R (1/2))*arccot))`|Z).x = -(arccot.x)
#R (-1/2)/(1+x^2)
proof
let x;
assume
A10: x in Z;
then
A11: arccot.x > 0 by A3;
A12: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A13: arccot is_differentiable_in x by A10,FDIFF_1:9;
((2(#)(( #R (1/2))*arccot))`|Z).x = 2*diff((( #R (1/2))*arccot),x) by A1,A9
,A10,FDIFF_1:20
.= 2*((1/2)*((arccot.x) #R (1/2-1))*diff(arccot,x)) by A13,A11,
TAYLOR_1:22
.= 2*((1/2)*((arccot.x) #R (1/2-1))*((arccot)`|Z).x) by A10,A12,
FDIFF_1:def 7
.= 2*((1/2)*((arccot.x) #R (1/2-1))*(-1/(1+x^2))) by A2,A10,SIN_COS9:82
.= -((arccot.x) #R (-1/2))/(1+x^2);
hence thesis;
end;
hence thesis by A1,A9,FDIFF_1:20;
end;
::f.x=(2/3)*(arctan #R (3/2))
theorem
Z c= dom (((2/3)(#)(( #R (3/2))*arctan))) & Z c= ].-1,1.[ & (for x st
x in Z holds arctan.x > 0) implies (2/3)(#)(( #R (3/2))*arctan)
is_differentiable_on Z & for x st x in Z holds (((2/3)(#)(( #R (3/2))*arctan))
`|Z).x = (arctan.x) #R (1/2)/(1+x^2)
proof
assume that
A1: Z c= dom (((2/3)(#)(( #R (3/2))*arctan))) and
A2: Z c= ].-1,1.[ and
A3: for x st x in Z holds arctan.x > 0;
A4: for x st x in Z holds ( #R (3/2))*arctan is_differentiable_in x
proof
let x;
assume
A5: x in Z;
then
A6: arctan.x > 0 by A3;
arctan is_differentiable_on Z by A2,SIN_COS9:81;
then arctan is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by A6,TAYLOR_1:22;
end;
Z c= dom (( #R (3/2))*arctan) by A1,VALUED_1:def 5;
then
A7: ( #R (3/2))*arctan is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds (((2/3)(#)(( #R (3/2))*arctan))`|Z).x = ((arctan.
x) #R (1/2))/(1+x^2)
proof
let x;
assume
A8: x in Z;
then
A9: arctan.x > 0 by A3;
A10: arctan is_differentiable_on Z by A2,SIN_COS9:81;
then
A11: arctan is_differentiable_in x by A8,FDIFF_1:9;
(((2/3)(#)(( #R (3/2))*arctan))`|Z).x = (2/3)*diff((( #R (3/2))*
arctan),x) by A1,A7,A8,FDIFF_1:20
.= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*diff(arctan,x)) by A11,A9,
TAYLOR_1:22
.= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*((arctan)`|Z).x) by A8,A10,
FDIFF_1:def 7
.= (2/3)*((3/2)*((arctan.x) #R (3/2-1))*(1/(1+x^2))) by A2,A8,SIN_COS9:81
.= ((arctan.x) #R (1/2))/(1+x^2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
::f.x=(2/3)*(arccot #R (3/2))
theorem
Z c= dom (((2/3)(#)(( #R (3/2))*arccot))) & Z c= ].-1,1.[ implies (2/3
)(#)(( #R (3/2))*arccot) is_differentiable_on Z & for x st x in Z holds (((2/3)
(#)(( #R (3/2))*arccot))`|Z).x = -(arccot.x) #R (1/2)/(1+x^2)
proof
assume that
A1: Z c= dom (((2/3)(#)(( #R (3/2))*arccot))) and
A2: Z c= ].-1,1.[;
A3: for x st x in Z holds arccot.x > 0
proof
let x;
].-1,1.[ c= [.-1,1.] by XXREAL_1:25;
then
A4: Z c= [.-1,1.] by A2,XBOOLE_1:1;
assume x in Z;
then x in [.-1,1.] by A4;
then arccot.x in arccot.:[.-1,1.] by FUNCT_1:def 6,SIN_COS9:24;
then arccot.x in [.PI/4,3/4*PI.] by RELAT_1:115,SIN_COS9:56;
then arccot.x >= PI/4 by XXREAL_1:1;
then
A5: arccot.x + 0 > PI/4 + (-PI/4) by XREAL_1:8;
assume arccot.x <= 0;
hence contradiction by A5;
end;
A6: for x st x in Z holds ( #R (3/2))*arccot is_differentiable_in x
proof
let x;
assume
A7: x in Z;
then
A8: arccot.x > 0 by A3;
arccot is_differentiable_on Z by A2,SIN_COS9:82;
then arccot is_differentiable_in x by A7,FDIFF_1:9;
hence thesis by A8,TAYLOR_1:22;
end;
Z c= dom (( #R (3/2))*arccot) by A1,VALUED_1:def 5;
then
A9: ( #R (3/2))*arccot is_differentiable_on Z by A6,FDIFF_1:9;
for x st x in Z holds (((2/3)(#)(( #R (3/2))*arccot))`|Z).x = -(arccot.
x) #R (1/2)/(1+x^2)
proof
let x;
assume
A10: x in Z;
then
A11: arccot.x > 0 by A3;
A12: arccot is_differentiable_on Z by A2,SIN_COS9:82;
then
A13: arccot is_differentiable_in x by A10,FDIFF_1:9;
(((2/3)(#)(( #R (3/2))*arccot))`|Z).x = (2/3)*diff((( #R (3/2))*
arccot),x) by A1,A9,A10,FDIFF_1:20
.= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*diff(arccot,x)) by A13,A11,
TAYLOR_1:22
.= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*((arccot)`|Z).x) by A10,A12,
FDIFF_1:def 7
.= (2/3)*((3/2)*((arccot.x) #R (3/2-1))*(-1/(1+x^2))) by A2,A10,
SIN_COS9:82
.= -((arccot.x) #R (1/2))/(1+x^2);
hence thesis;
end;
hence thesis by A1,A9,FDIFF_1:20;
end;