:: Some Differentiable Formulas of Special Functions
:: by Jianbing Cao , Fahui Zhai and Xiquan Liang
::
:: Received November 7, 2005
:: Copyright (c) 2005-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies REAL_1, SUBSET_1, NUMBERS, RCOMP_1, PARTFUN1, TARSKI, RELAT_1,
ARYTM_3, FUNCT_1, PREPOWER, FDIFF_1, XBOOLE_0, CARD_1, ARYTM_1, NEWTON,
LIMFUNC1, XXREAL_0, SQUARE_1, ORDINAL4, SIN_COS, VALUED_1, TAYLOR_1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, PARTFUN2,
ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, RCOMP_1, REAL_1,
VALUED_1, FDIFF_1, NEWTON, PREPOWER, TAYLOR_1, LIMFUNC1, SIN_COS,
RFUNCT_1, SQUARE_1;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1,
FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, LIMFUNC1, XXREAL_2,
RELSET_1, NEWTON;
registrations RELSET_1, NUMBERS, INT_1, MEMBERED, RCOMP_1, VALUED_0, XXREAL_0,
XREAL_0, PREPOWER, NEWTON, SQUARE_1;
requirements SUBSET, NUMERALS, ARITHM, BOOLE;
definitions TARSKI;
equalities SQUARE_1, LIMFUNC1;
expansions TARSKI;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, NAT_1, FDIFF_1, FUNCT_1,
TARSKI, PREPOWER, RFUNCT_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS, VALUED_1,
XXREAL_1, RELAT_1;
begin
reserve y for set,
x,a,b for Real,
n for Element of NAT,
Z for open Subset of REAL,
f,f1,f2,g for PartFunc of REAL,REAL;
Lm1: Z c= dom (f1+f2) & (for x st x in Z holds f1.x=a) & f2=#Z 2 implies f1+f2
is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x = 2*x
proof
assume that
A1: Z c= dom (f1+f2) and
A2: for x st x in Z holds f1.x=a and
A3: f2=#Z 2;
A4: for x st x in Z holds f2 is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom f1 /\ dom f2 by A1,VALUED_1:def 1;
then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x = 0*x+a by A2;
then
A8: f1 is_differentiable_on Z by A6,FDIFF_1:23;
Z c= dom f2 by A5,XBOOLE_1:18;
then
A9: f2 is_differentiable_on Z by A4,FDIFF_1:9;
A10: for x st x in Z holds (f2`|Z).x = 2 * x #Z (2-1)
proof
let x;
assume
A11: x in Z;
diff(f2,x) = 2 * x #Z (2-1) by A3,TAYLOR_1:2;
hence thesis by A9,A11,FDIFF_1:def 7;
end;
for x st x in Z holds ((f1+f2)`|Z).x = 2*x
proof
let x;
assume
A12: x in Z;
then ((f1+f2)`|Z).x=diff(f1,x)+diff(f2,x) by A1,A8,A9,FDIFF_1:18;
hence ((f1+f2)`|Z).x=(f1`|Z).x +diff(f2,x) by A8,A12,FDIFF_1:def 7
.=(f1`|Z).x +(f2`|Z).x by A9,A12,FDIFF_1:def 7
.=0+(f2`|Z).x by A6,A7,A12,FDIFF_1:23
.=2 * x #Z (2-1) by A10,A12
.=2*x|^1 by PREPOWER:36
.=2*x;
end;
hence thesis by A1,A8,A9,FDIFF_1:18;
end;
Lm2: Z c= dom (f1-f2) & (for x st x in Z holds f1.x=a) & f2=#Z 2 implies f1-f2
is_differentiable_on Z & for x st x in Z holds ((f1-f2)`|Z).x = -2*x
proof
assume that
A1: Z c= dom (f1-f2) and
A2: for x st x in Z holds f1.x=a and
A3: f2=#Z 2;
A4: for x st x in Z holds f2 is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom f1 /\ dom f2 by A1,VALUED_1:12;
then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x = 0*x+a by A2;
then
A8: f1 is_differentiable_on Z by A6,FDIFF_1:23;
Z c= dom f2 by A5,XBOOLE_1:18;
then
A9: f2 is_differentiable_on Z by A4,FDIFF_1:9;
A10: for x st x in Z holds (f2`|Z).x = 2 * x #Z (2-1)
proof
let x;
assume
A11: x in Z;
diff(f2,x) = 2 * x #Z (2-1) by A3,TAYLOR_1:2;
hence thesis by A9,A11,FDIFF_1:def 7;
end;
for x st x in Z holds ((f1-f2)`|Z).x = -2*x
proof
let x;
assume
A12: x in Z;
then ((f1-f2)`|Z).x=diff(f1,x)-diff(f2,x) by A1,A8,A9,FDIFF_1:19;
hence ((f1-f2)`|Z).x=(f1`|Z).x -diff(f2,x) by A8,A12,FDIFF_1:def 7
.=(f1`|Z).x -(f2`|Z).x by A9,A12,FDIFF_1:def 7
.=0-((f2`|Z).x) by A6,A7,A12,FDIFF_1:23
.=0-(2 * x #Z (2-1)) by A10,A12
.=0-(2*x|^1) by PREPOWER:36
.=-(2*x|^1)
.=-2*x;
end;
hence thesis by A1,A8,A9,FDIFF_1:19;
end;
Lm3: Z c= dom (( #R (1/2))) implies ( #R (1/2)) is_differentiable_on Z & for x
st x in Z holds ( ( #R (1/2)) `|Z).x =(1/2)*x #R (-1/2)
proof
assume
A1: Z c= dom (( #R (1/2)));
A2: for x st x in Z holds ( #R (1/2)) is_differentiable_in x
proof
let x;
assume x in Z;
then x in dom (( #R (1/2))) by A1;
then x in right_open_halfline 0 by TAYLOR_1:def 4;
then x >0 by XXREAL_1:4;
hence thesis by TAYLOR_1:21;
end;
then
A3: ( #R (1/2)) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ( ( #R (1/2)) `|Z).x =(1/2)*x #R (-1/2)
proof
let x;
assume
A4: x in Z;
then x in dom (( #R (1/2))) by A1;
then x in right_open_halfline 0 by TAYLOR_1:def 4;
then x >0 by XXREAL_1:4;
then diff(( #R (1/2)),x) = (1/2)*(x #R (1/2-1)) by TAYLOR_1:21
.= (1/2)*x #R (-1/2);
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A1,A2,FDIFF_1:9;
end;
:: 1 f.x=(a+x)/(a-x)
theorem
Z c= dom (f1/f2) & (for x st x in Z holds f1.x=a+x & f2.x=a-x & f2.x<>
0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z).
x = (2*a)/(a-x)^2
proof
assume that
A1: Z c= dom (f1/f2) and
A2: for x st x in Z holds f1.x=a+x & f2.x=a-x & f2.x<>0;
A3: Z c= dom f1 /\ (dom f2 \ f2"{0}) by A1,RFUNCT_1:def 1;
then
A4: Z c= dom f1 by XBOOLE_1:18;
A5: for x st x in Z holds f1.x=1*x+a by A2;
then
A6: f1 is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds f2.x =(-1)*x+a
proof
let x;
assume x in Z;
then f2.x =a-x by A2;
hence thesis;
end;
A8: Z c= dom f2 by A3,XBOOLE_1:1;
then
A9: f2 is_differentiable_on Z by A7,FDIFF_1:23;
A10: for x st x in Z holds f2.x <> 0 by A2;
then
A11: f1/f2 is_differentiable_on Z by A6,A9,FDIFF_2:21;
for x st x in Z holds ((f1/f2)`|Z).x = (2*a)/(a-x)^2
proof
let x;
assume
A12: x in Z;
then
A13: f2.x <>0 by A2;
A14: f1.x=a+x & f2.x=a-x by A2,A12;
f1 is_differentiable_in x & f2 is_differentiable_in x by A6,A9,A12,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A13
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A6,A12,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A9,A12,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A4,A5,A12,FDIFF_1:23
.=(1* f2.x-(-1)* f1.x)/(f2.x)^2 by A8,A7,A12,FDIFF_1:23
.=(2*a)/(a-x)^2 by A14;
hence thesis by A11,A12,FDIFF_1:def 7;
end;
hence thesis by A6,A9,A10,FDIFF_2:21;
end;
:: 2 f.x=(x-a)/(x+a)
theorem
Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x-a & f2.x=x+a & f2.x<>
0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z).
x = (2*a)/(x+a)^2
proof
assume that
A1: Z c= dom (f1/f2) and
A2: for x st x in Z holds f1.x=x-a & f2.x=x+a & f2.x<>0;
A3: for x st x in Z holds f2.x = 1*x+a by A2;
A4: Z c= dom f1 /\ (dom f2 \ f2"{0}) by A1,RFUNCT_1:def 1;
then
A5: Z c= dom f1 by XBOOLE_1:18;
A6: Z c= dom f2 by A4,XBOOLE_1:1;
then
A7: f2 is_differentiable_on Z by A3,FDIFF_1:23;
A8: for x st x in Z holds f1.x = 1*x+-a
proof
let x;
A9: 1*x+-a=1*x-a;
assume x in Z;
hence thesis by A2,A9;
end;
then
A10: f1 is_differentiable_on Z by A5,FDIFF_1:23;
A11: for x st x in Z holds f2.x <> 0 by A2;
then
A12: f1/f2 is_differentiable_on Z by A10,A7,FDIFF_2:21;
for x st x in Z holds ((f1/f2)`|Z).x = (2*a)/(x+a)^2
proof
let x;
assume
A13: x in Z;
then
A14: f2.x <>0 by A2;
A15: f1.x=x-a & f2.x=x+a by A2,A13;
f1 is_differentiable_in x & f2 is_differentiable_in x by A10,A7,A13,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A14
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A10,A13,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A7,A13,FDIFF_1:def 7
.=(1*f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A5,A8,A13,FDIFF_1:23
.=(1*f2.x-1* f1.x)/(f2.x)^2 by A6,A3,A13,FDIFF_1:23
.=(2*a)/(x+a)^2 by A15;
hence thesis by A12,A13,FDIFF_1:def 7;
end;
hence thesis by A10,A7,A11,FDIFF_2:21;
end;
:: 3 f.x=(x-a)/(x-b)
theorem
Z c= dom (f1/f2) & (for x st x in Z holds f1.x=x-a & f2.x=x-b & f2.x<>
0) implies (f1/f2) is_differentiable_on Z & for x st x in Z holds ((f1/f2)`|Z).
x = (a-b)/(x-b)^2
proof
assume that
A1: Z c= dom (f1/f2) and
A2: for x st x in Z holds f1.x=x-a & f2.x=x-b & f2.x<>0;
A3: for x st x in Z holds f1.x = 1*x+-a & f2.x = 1*x+-b
proof
let x;
A4: 1*x+-a=1*x-a & 1*x+-b=1*x-b;
assume x in Z;
hence thesis by A2,A4;
end;
then
A5: for x st x in Z holds f1.x = 1*x+-a;
A6: Z c= dom f1 /\ (dom f2 \ f2"{0}) by A1,RFUNCT_1:def 1;
then
A7: Z c= dom f1 by XBOOLE_1:18;
then
A8: f1 is_differentiable_on Z by A5,FDIFF_1:23;
A9: for x st x in Z holds f2.x = 1*x+-b by A3;
A10: Z c= dom f2 by A6,XBOOLE_1:1;
then
A11: f2 is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds f2.x <> 0 by A2;
then
A13: f1/f2 is_differentiable_on Z by A8,A11,FDIFF_2:21;
for x st x in Z holds ((f1/f2)`|Z).x = (a-b)/(x-b)^2
proof
let x;
assume
A14: x in Z;
then
A15: f2.x <>0 by A2;
A16: f1.x=x-a & f2.x=x-b by A2,A14;
f1 is_differentiable_in x & f2 is_differentiable_in x by A8,A11,A14,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A15
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A8,A14,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A11,A14,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A7,A5,A14,FDIFF_1:23
.=(1* f2.x-1* f1.x)/(f2.x)^2 by A10,A9,A14,FDIFF_1:23
.=(a-b)/(x-b)^2 by A16;
hence thesis by A13,A14,FDIFF_1:def 7;
end;
hence thesis by A8,A11,A12,FDIFF_2:21;
end;
:: 4 f.x=1/x
theorem Th4:
not 0 in Z implies (id Z)^ is_differentiable_on Z & for x st x in
Z holds (((id Z)^)`|Z).x= -1/x^2
proof
set f = id Z;
A1: Z c= dom f & for x st x in Z holds f.x = 1*x+0 by FUNCT_1:17;
then
A2: f is_differentiable_on Z by FDIFF_1:23;
assume
A3: not 0 in Z;
then
A4: for x st x in Z holds f.x<>0 by FUNCT_1:18;
then
A5: f^ is_differentiable_on Z by A2,FDIFF_2:22;
now
let x;
assume
A6: x in Z;
then
A7: f.x<>0 & f is_differentiable_in x by A3,A2,FDIFF_1:9,FUNCT_1:18;
((f^)`|Z).x= diff(f^,x) by A5,A6,FDIFF_1:def 7
.= - diff(f,x)/(f.x)^2 by A7,FDIFF_2:15
.=- (f`|Z).x/(f.x)^2 by A2,A6,FDIFF_1:def 7
.=-1/(f.x)^2 by A1,A6,FDIFF_1:23
.=-1/x^2 by A6,FUNCT_1:18;
hence ((f^)`|Z).x=-1/x^2;
end;
hence thesis by A2,A4,FDIFF_2:22;
end;
:: 5 f.x=sin(1/x)
Lm4: not 0 in Z implies dom (sin*((id Z)^)) = Z
proof
A1: rng ((id Z)^) c= REAL by RELAT_1:def 19;
assume
A2: not 0 in Z;
(id Z)"{0} c= {}
proof
let x be object;
assume
A3: x in (id Z)"{0};
then x in dom id Z by FUNCT_1:def 7;
then
A4: x in Z by FUNCT_1:17;
(id Z).x in {0} by A3,FUNCT_1:def 7;
then x in {0} by A4,FUNCT_1:18;
hence thesis by A2,A4,TARSKI:def 1;
end;
then
A5: (id Z)"{0} = {} by XBOOLE_1:3;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= Z by A5,FUNCT_1:17;
hence thesis by A1,RELAT_1:27,SIN_COS:24;
end;
theorem Th5:
not 0 in Z implies sin*((id Z)^) is_differentiable_on Z & for x
st x in Z holds ((sin*((id Z)^))`|Z).x = -(1/x^2)*cos.(1/x)
proof
set f = id Z;
assume
A1: not 0 in Z;
then
A2: Z c= dom (sin*(f^)) by Lm4;
then for y being object st y in Z holds y in dom (f^) by FUNCT_1:11;
then
A3: Z c= dom (f^);
A4: f^ is_differentiable_on Z by A1,Th4;
A5: for x st x in Z holds sin*(f^) is_differentiable_in x
proof
let x;
assume x in Z;
then
A6: f^ is_differentiable_in x by A4,FDIFF_1:9;
sin is_differentiable_in (f^).x by SIN_COS:64;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sin*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((sin*(f^))`|Z).x = -(1/x^2)*cos.(1/x)
proof
let x;
A8: sin is_differentiable_in (f^).x by SIN_COS:64;
assume
A9: x in Z;
then f^ is_differentiable_in x by A4,FDIFF_1:9;
then diff(sin*(f^),x) = diff(sin, (f^).x)*diff(f^,x) by A8,FDIFF_2:13
.=cos.((f^).x)*diff(f^,x) by SIN_COS:64
.=cos.((f.x)")*diff(f^,x) by A3,A9,RFUNCT_1:def 2
.=cos.((f.x)")*((f^)`|Z).x by A4,A9,FDIFF_1:def 7
.=cos.((f.x)")*(-1/x^2) by A1,A9,Th4
.=cos.(1*x")*(-1/x^2) by A9,FUNCT_1:18
.=cos.(1/x)*(-1/x^2) by XCMPLX_0:def 9;
hence thesis by A7,A9,FDIFF_1:def 7;
end;
hence thesis by A2,A5,FDIFF_1:9;
end;
:: 6 f.x=cos(1/x)
theorem Th6:
not 0 in Z & Z c= dom (cos*((id Z)^)) implies cos*((id Z)^)
is_differentiable_on Z & for x st x in Z holds ((cos*((id Z)^))`|Z).x = 1/x^2*
sin.(1/x)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (cos*(f^));
for y being object st y in Z holds y in dom (f^) by A2,FUNCT_1:11;
then
A3: Z c= dom (f^);
A4: f^ is_differentiable_on Z by A1,Th4;
A5: for x st x in Z holds cos*(f^) is_differentiable_in x
proof
let x;
assume x in Z;
then
A6: f^ is_differentiable_in x by A4,FDIFF_1:9;
cos is_differentiable_in (f^).x by SIN_COS:63;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cos*(f^) is_differentiable_on Z by A2,FDIFF_1:9;
for x st x in Z holds ((cos*(f^))`|Z).x = 1/x^2*sin.(1/x)
proof
let x;
A8: diff(cos,(f^).x)=-sin.((f^).x) by SIN_COS:63;
A9: cos is_differentiable_in (f^).x by SIN_COS:63;
assume
A10: x in Z;
then f^ is_differentiable_in x by A4,FDIFF_1:9;
then diff(cos*(f^),x) = diff(cos, (f^).x)*diff(f^,x) by A9,FDIFF_2:13
.=-sin.((f^).x)*diff(f^,x) by A8
.=-sin.((f.x)")*diff(f^,x) by A3,A10,RFUNCT_1:def 2
.=-sin.((f.x)")*((f^)`|Z).x by A4,A10,FDIFF_1:def 7
.=-sin.((f.x)")*(-1/x^2) by A1,A10,Th4
.=-sin.(1*x")*(-1/x^2) by A10,FUNCT_1:18
.=-sin.(1/x)*(-1/x^2) by XCMPLX_0:def 9
.=sin.(1/x)*(1/x^2);
hence thesis by A7,A10,FDIFF_1:def 7;
end;
hence thesis by A2,A5,FDIFF_1:9;
end;
:: 7 f.x=x*sin(1/x)
theorem
Z c= dom ((id Z)(#)(sin*((id Z)^))) & not 0 in Z implies (id Z)(#)(sin
*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(sin*((id
Z)^)))`|Z).x = sin.(1/x)-(1/x)*cos.(1/x)
proof
set f = id Z;
assume that
A1: Z c= dom ((id Z)(#)(sin*(f^))) and
A2: not 0 in Z;
A3: sin*(f^) is_differentiable_on Z by A2,Th5;
A4: Z c= dom (id Z) /\ dom (sin*(f^)) by A1,VALUED_1:def 4;
then
A5: Z c= dom id Z by XBOOLE_1:18;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
then
A7: id Z is_differentiable_on Z by A5,FDIFF_1:23;
A8: Z c= dom (sin*(f^)) by A4,XBOOLE_1:18;
then for y being object st y in Z holds y in dom (f^) by FUNCT_1:11;
then
A9: Z c= dom (f^);
now
let x;
assume
A10: x in Z;
then
(((id Z)(#)(sin*(f^)))`|Z).x = ((sin*(f^)).x)*diff((id Z),x) + ((id Z
).x)*diff(sin*(f^),x) by A1,A3,A7,FDIFF_1:21
.=((sin*(f^)).x)*((id Z)`|Z).x+ ((id Z).x)*diff(sin*(f^),x) by A7,A10,
FDIFF_1:def 7
.=((sin*(f^)).x)*1+ ((id Z).x)*diff(sin*(f^),x) by A5,A6,A10,FDIFF_1:23
.=((sin*(f^)).x)+ x*diff(sin*(f^),x) by A10,FUNCT_1:18
.=((sin*(f^)).x)+ x*(((sin*(f^))`|Z).x) by A3,A10,FDIFF_1:def 7
.=((sin*(f^)).x)+ x*(-(1/x^2)*cos.(1/x)) by A2,A10,Th5
.=((sin*(f^)).x) -(x*(1/(x*x))*cos.(1/x))
.=((sin*(f^)).x) -x*((1/x)*(1/x))*cos.(1/x) by XCMPLX_1:102
.=((sin*(f^)).x)-(x*(1/x))*(1/x)*cos.(1/x)
.=((sin*(f^)).x)-(1)*(1/x)*cos.(1/x) by A2,A10,XCMPLX_1:106
.=(sin.((f^).x))-(1/x)*cos.(1/x) by A8,A10,FUNCT_1:12
.=(sin.((f.x)"))-(1/x)*cos.(1/x) by A9,A10,RFUNCT_1:def 2
.=sin.(1*x")-(1/x)*cos.(1/x) by A10,FUNCT_1:18
.=sin.(1/x)-(1/x)*cos.(1/x) by XCMPLX_0:def 9;
hence (((id Z)(#)(sin*(f^)))`|Z).x = sin.(1/x)-(1/x)*cos.(1/x);
end;
hence thesis by A1,A3,A7,FDIFF_1:21;
end;
:: 8 f.x=x*cos(1/x)
theorem
Z c= dom ((id Z)(#)(cos*((id Z)^))) & not 0 in Z implies (id Z)(#)(cos
*((id Z)^)) is_differentiable_on Z & for x st x in Z holds (((id Z)(#)(cos*((id
Z)^)))`|Z).x = cos.(1/x)+(1/x)*sin.(1/x)
proof
set f = id Z;
assume that
A1: Z c= dom ((id Z)(#)(cos*(f^))) and
A2: not 0 in Z;
A3: Z c= dom (id Z) /\ dom (cos*(f^)) by A1,VALUED_1:def 4;
then
A4: Z c= dom (cos*(f^)) by XBOOLE_1:18;
then
A5: cos*(f^) is_differentiable_on Z by A2,Th6;
A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A7: Z c= dom id Z by A3,XBOOLE_1:18;
then
A8: id Z is_differentiable_on Z by A6,FDIFF_1:23;
for y being object st y in Z holds y in dom (f^) by A4,FUNCT_1:11;
then
A9: Z c= dom (f^);
now
let x;
assume
A10: x in Z;
then
(((id Z)(#)(cos*(f^)))`|Z).x = ((cos*(f^)).x)*diff((id Z),x) + ((id Z
).x)*diff(cos*(f^),x) by A1,A5,A8,FDIFF_1:21
.=((cos*(f^)).x)*((id Z)`|Z).x+ ((id Z).x)*diff(cos*(f^),x) by A8,A10,
FDIFF_1:def 7
.=((cos*(f^)).x)*1+ ((id Z).x)*diff(cos*(f^),x) by A7,A6,A10,FDIFF_1:23
.=((cos*(f^)).x)+ x*diff(cos*(f^),x) by A10,FUNCT_1:18
.=((cos*(f^)).x)+ x*(((cos*(f^))`|Z).x) by A5,A10,FDIFF_1:def 7
.=((cos*(f^)).x)+ x*((1/x^2)*sin.(1/x)) by A2,A4,A10,Th6
.=((cos*(f^)).x) +(x*(1/(x*x))*sin.(1/x))
.=((cos*(f^)).x) +x*((1/x)*(1/x))*sin.(1/x) by XCMPLX_1:102
.=((cos*(f^)).x)+(x*(1/x))*(1/x)*sin.(1/x)
.=((cos*(f^)).x)+(1)*(1/x)*sin.(1/x) by A2,A10,XCMPLX_1:106
.=(cos.((f^).x))+(1/x)*sin.(1/x) by A4,A10,FUNCT_1:12
.=(cos.((f.x)"))+(1/x)*sin.(1/x) by A9,A10,RFUNCT_1:def 2
.=cos.(1*x")+(1/x)*sin.(1/x) by A10,FUNCT_1:18
.=cos.(1/x)+(1/x)*sin.(1/x) by XCMPLX_0:def 9;
hence (((id Z)(#)(cos*(f^)))`|Z).x = cos.(1/x)+(1/x)*sin.(1/x);
end;
hence thesis by A1,A5,A8,FDIFF_1:21;
end;
:: 9 f.x=sin(1/x)*cos(1/x)
theorem
Z c= dom ((sin*((id Z)^))(#)(cos*((id Z)^))) & not 0 in Z implies (sin
*((id Z)^))(#)(cos*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((
(sin*((id Z)^))(#)(cos*((id Z)^)))`|Z).x = (1/x^2)*((sin.(1/x))^2-(cos.(1/x))^2
)
proof
set f = id Z;
assume that
A1: Z c= dom ((sin*(f^))(#)(cos*(f^))) and
A2: not 0 in Z;
A3: sin*(f^) is_differentiable_on Z by A2,Th5;
A4: Z c= dom (sin*(f^)) /\ dom (cos*(f^)) by A1,VALUED_1:def 4;
then
A5: Z c= dom (cos*(f^)) by XBOOLE_1:18;
then
A6: cos*(f^) is_differentiable_on Z by A2,Th6;
A7: Z c= dom (sin*(f^)) by A4,XBOOLE_1:18;
then for y being object st y in Z holds y in dom (f^) by FUNCT_1:11;
then
A8: Z c= dom (f^);
now
let x;
assume
A9: x in Z;
then (((sin*(f^))(#)(cos*(f^)))`|Z).x = ((cos*(f^)).x)*diff((sin*(f^)),x)
+ ((sin*(f^)).x)*diff(cos*(f^),x) by A1,A6,A3,FDIFF_1:21
.=((cos*(f^)).x)*((sin*(f^))`|Z).x+ ((sin*(f^)).x)*diff(cos*(f^),x) by A3
,A9,FDIFF_1:def 7
.=((cos*(f^)).x)*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*diff(cos*(f^),x)
by A2,A9,Th5
.=((cos*(f^)).x)*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*(((cos*(f^))`|Z).
x) by A6,A9,FDIFF_1:def 7
.=((cos*(f^)).x)*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*((1/x^2)*sin.(1/x
)) by A2,A5,A9,Th6
.=(cos.((f^).x))*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*((1/x^2)*sin.(1/x
)) by A5,A9,FUNCT_1:12
.=(cos.((f.x)"))*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*((1/x^2)*sin.(1/x
)) by A8,A9,RFUNCT_1:def 2
.=(cos.(1*x"))*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*((1/x^2)*sin.(1/x))
by A9,FUNCT_1:18
.=cos.(1/x)*(-(1/x^2)*cos.(1/x))+((sin*(f^)).x)*((1/x^2)*sin.(1/x)) by
XCMPLX_0:def 9
.=cos.(1/x)*(-(1/x^2)*cos.(1/x))+(sin.((f^).x))*((1/x^2)*sin.(1/x)) by A7
,A9,FUNCT_1:12
.=cos.(1/x)*(-(1/x^2)*cos.(1/x))+(sin.((f.x)"))*((1/x^2)*sin.(1/x)) by A8
,A9,RFUNCT_1:def 2
.=cos.(1/x)*(-(1/x^2)*cos.(1/x))+(sin.(1*x"))*((1/x^2)*sin.(1/x)) by A9,
FUNCT_1:18
.=-cos.(1/x)*(1/x^2)*cos.(1/x)+sin.(1/x)*((1/x^2)*sin.(1/x)) by
XCMPLX_0:def 9
.=(1/x^2)*((sin.(1/x))^2-(cos.(1/x))^2);
hence
(((sin*(f^))(#)(cos*(f^)))`|Z).x = (1/x^2)*((sin.(1/x))^2-(cos.(1/x)) ^2);
end;
hence thesis by A1,A6,A3,FDIFF_1:21;
end;
:: 10 f.x=sin(n*x)*(sin x ^ n)
theorem
Z c= dom ((sin*f)(#)(( #Z n)*sin)) & n>=1 & (for x st x in Z holds f.x
=n*x) implies (sin*f)(#)(( #Z n)*sin) is_differentiable_on Z & for x st x in Z
holds (((sin*f)(#)(( #Z n)*sin))`|Z).x =n*(sin.x) #Z (n-1)*sin.((n+1)*x)
proof
assume that
A1: Z c= dom ((sin*f)(#)(( #Z n)*sin)) and
A2: n>=1 and
A3: for x st x in Z holds f.x=n*x;
A4: for x st x in Z holds f.x=n*x+0 by A3;
A5: Z c= dom (sin*f) /\ dom (( #Z n)*sin) by A1,VALUED_1:def 4;
then
A6: Z c= dom (sin*f) by XBOOLE_1:18;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A7: Z c= dom f;
then
A8: f is_differentiable_on Z by A4,FDIFF_1:23;
for x st x in Z holds sin*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A9: f is_differentiable_in x by A8,FDIFF_1:9;
sin is_differentiable_in f.x by SIN_COS:64;
hence thesis by A9,FDIFF_2:13;
end;
then
A10: sin*f is_differentiable_on Z by A6,FDIFF_1:9;
A11: for x st x in Z holds ((sin*f)`|Z).x = n*cos.(n*x)
proof
let x;
A12: sin is_differentiable_in f.x by SIN_COS:64;
assume
A13: x in Z;
then f is_differentiable_in x by A8,FDIFF_1:9;
then diff(sin*f,x) = diff(sin, f.x)*diff(f,x) by A12,FDIFF_2:13
.=cos.( f.x)*diff(f,x) by SIN_COS:64
.=cos.(n*x)*diff(f,x) by A3,A13
.=cos.(n*x)*(f`|Z).x by A8,A13,FDIFF_1:def 7
.=n* cos.(n*x) by A7,A4,A13,FDIFF_1:23;
hence thesis by A10,A13,FDIFF_1:def 7;
end;
A14: Z c= dom (( #Z n)*sin) by A5,XBOOLE_1:18;
now
let x;
assume x in Z;
sin is_differentiable_in x by SIN_COS:64;
hence ( #Z n)*sin is_differentiable_in x by TAYLOR_1:3;
end;
then
A15: ( #Z n)*sin is_differentiable_on Z by A14,FDIFF_1:9;
A16: for x st x in Z holds ((( #Z n)*sin)`|Z).x =n*((sin.x) #Z (n-1))*cos.x
proof
let x;
sin is_differentiable_in x by SIN_COS:64;
then
A17: diff((( #Z n)*sin),x) =(n*((sin.x) #Z (n-1)) * diff(sin,x)) by TAYLOR_1:3
.=n*((sin.x) #Z (n-1)) *cos.x by SIN_COS:64;
assume x in Z;
hence thesis by A15,A17,FDIFF_1:def 7;
end;
now
let x;
A18: n-1 is Element of NAT by A2,NAT_1:21;
assume
A19: x in Z;
then
(((sin*f)(#)(( #Z n)*sin))`|Z).x =(( #Z n)*sin).x*diff(sin*f,x)+(sin*
f).x*diff((( #Z n)*sin),x) by A1,A10,A15,FDIFF_1:21
.=(( #Z n).(sin.x))*diff(sin*f,x)+(sin*f).x*diff((( #Z n)*sin),x) by A14
,A19,FUNCT_1:12
.=((sin.x) #Z n)*diff(sin*f,x)+(sin*f).x*diff((( #Z n)*sin),x) by
TAYLOR_1:def 1
.=((sin.x) #Z n)*((sin*f)`|Z).x+(sin*f).x*diff((( #Z n)*sin),x) by A10
,A19,FDIFF_1:def 7
.=((sin.x) #Z n)*(n* cos.(n*x))+(sin*f).x*diff((( #Z n)*sin),x) by A11
,A19
.=((sin.x) #Z n)*(n* cos.(n*x))+(sin.(f.x))*diff((( #Z n)*sin),x) by A6
,A19,FUNCT_1:12
.=((sin.x) #Z n)*(n* cos.(n*x))+(sin.(n*x))*diff((( #Z n)*sin),x) by A3
,A19
.=((sin.x) #Z n)*(n* cos.(n*x))+(sin.(n*x))*((( #Z n)*sin)`|Z).x by A15
,A19,FDIFF_1:def 7
.=((sin.x) #Z n)*(n* cos.(n*x))+(sin.(n*x))*(n*((sin.x) #Z (n-1))*cos.
x) by A16,A19
.=((sin.x) #Z ((n-1)+1))*(n* cos.(n*x))+ sin.(n*x)*n*((sin.x) #Z (n-1)
) *cos.x
.=(((sin.x) #Z (n-1))*((sin.x) #Z 1))*(n* cos.(n*x))+ (sin.(n*x)*n*((
sin.x) #Z (n-1)) *cos.x) by A18,TAYLOR_1:1
.=(((sin.x) #Z (n-1))*(sin.x))*(n* cos.(n*x))+ (sin.(n*x)*n*((sin.x)
#Z (n-1)) *cos.x) by PREPOWER:35
.= n*((sin.x) #Z (n-1))*(sin.x*cos.(n*x)+cos.x*sin.(n*x))
.= n*((sin.x) #Z (n-1))*(sin.(x+n*x)) by SIN_COS:74
.= n*((sin.x) #Z (n-1))*sin.((n+1)*x);
hence (((sin*f)(#)(( #Z n)*sin))`|Z).x =n*(sin.x) #Z (n-1) *sin.((n+1)*x);
end;
hence thesis by A1,A10,A15,FDIFF_1:21;
end;
:: 11 f.x=cos(n*x)*(sin x ^ n)
theorem
Z c= dom ((cos*f)(#)(( #Z n)*sin)) & n>=1 & (for x st x in Z holds f.x
=n*x) implies (cos*f)(#)(( #Z n)*sin) is_differentiable_on Z & for x st x in Z
holds (((cos*f)(#)(( #Z n)*sin))`|Z).x =n*(sin.x) #Z (n-1) * cos.((n+1)*x)
proof
assume that
A1: Z c= dom ((cos*f)(#)(( #Z n)*sin)) and
A2: n>=1 and
A3: for x st x in Z holds f.x=n*x;
A4: for x st x in Z holds f.x=n*x+0 by A3;
A5: Z c= dom (cos*f) /\ dom (( #Z n)*sin) by A1,VALUED_1:def 4;
then
A6: Z c= dom (cos*f) by XBOOLE_1:18;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A7: Z c= dom f;
then
A8: f is_differentiable_on Z by A4,FDIFF_1:23;
for x st x in Z holds cos*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A9: f is_differentiable_in x by A8,FDIFF_1:9;
cos is_differentiable_in f.x by SIN_COS:63;
hence thesis by A9,FDIFF_2:13;
end;
then
A10: cos*f is_differentiable_on Z by A6,FDIFF_1:9;
A11: for x st x in Z holds ((cos*f)`|Z).x = -n* sin.(n*x)
proof
let x;
A12: cos is_differentiable_in f.x by SIN_COS:63;
assume
A13: x in Z;
then f is_differentiable_in x by A8,FDIFF_1:9;
then diff(cos*f,x) = diff(cos, f.x)*diff(f,x) by A12,FDIFF_2:13
.=(-sin.( f.x))*diff(f,x) by SIN_COS:63
.=(-sin.(n*x))*diff(f,x) by A3,A13
.=(-sin.(n*x))*(f`|Z).x by A8,A13,FDIFF_1:def 7
.=(-sin.(n*x))*n by A7,A4,A13,FDIFF_1:23
.=-n* sin.(n*x);
hence thesis by A10,A13,FDIFF_1:def 7;
end;
A14: Z c= dom (( #Z n)*sin) by A5,XBOOLE_1:18;
now
let x;
assume x in Z;
sin is_differentiable_in x by SIN_COS:64;
hence ( #Z n)*sin is_differentiable_in x by TAYLOR_1:3;
end;
then
A15: ( #Z n)*sin is_differentiable_on Z by A14,FDIFF_1:9;
A16: for x st x in Z holds ((( #Z n)*sin)`|Z).x =n*((sin.x) #Z (n-1)) *cos.x
proof
let x;
sin is_differentiable_in x by SIN_COS:64;
then
A17: diff((( #Z n)*sin),x) =(n*((sin.x) #Z (n-1)) * diff(sin,x)) by TAYLOR_1:3
.=n*((sin.x) #Z (n-1)) *cos.x by SIN_COS:64;
assume x in Z;
hence thesis by A15,A17,FDIFF_1:def 7;
end;
now
let x;
A18: n-1 is Element of NAT by A2,NAT_1:21;
assume
A19: x in Z;
then
(((cos*f)(#)(( #Z n)*sin))`|Z).x =(( #Z n)*sin).x*diff(cos*f,x)+(cos*
f).x*diff((( #Z n)*sin),x) by A1,A10,A15,FDIFF_1:21
.=(( #Z n).(sin.x))*diff(cos*f,x)+(cos*f).x*diff((( #Z n)*sin),x) by A14
,A19,FUNCT_1:12
.=((sin.x) #Z n)*diff(cos*f,x)+(cos*f).x*diff((( #Z n)*sin),x) by
TAYLOR_1:def 1
.=((sin.x) #Z n)*((cos*f)`|Z).x+(cos*f).x*diff((( #Z n)*sin),x) by A10
,A19,FDIFF_1:def 7
.=((sin.x) #Z n)*(-n* sin.(n*x))+(cos*f).x*diff((( #Z n)*sin),x) by A11
,A19
.=((sin.x) #Z n)*(-n* sin.(n*x))+(cos.(f.x))*diff((( #Z n)*sin),x) by A6
,A19,FUNCT_1:12
.=((sin.x) #Z n)*(-n* sin.(n*x))+(cos.(n*x))*diff((( #Z n)*sin),x) by A3
,A19
.=((sin.x) #Z n)*(-n* sin.(n*x))+(cos.(n*x))*((( #Z n)*sin)`|Z).x by A15
,A19,FDIFF_1:def 7
.=((sin.x) #Z n)*(-n* sin.(n*x))+ (cos.(n*x))*(n*((sin.x) #Z (n-1)) *
cos.x) by A16,A19
.=((sin.x) #Z ((n-1)+1))*(-n* sin.(n*x))+ cos.(n*x)*n*((sin.x) #Z (n-1
)) *cos.x
.=(((sin.x) #Z (n-1))*((sin.x) #Z 1))*(-n* sin.(n*x))+ (cos.(n*x)*n*((
sin.x) #Z (n-1)) *cos.x) by A18,TAYLOR_1:1
.=(((sin.x) #Z (n-1))*(sin.x))*(-n* sin.(n*x))+ (cos.(n*x)*n*((sin.x)
#Z (n-1)) *cos.x) by PREPOWER:35
.= n*((sin.x) #Z (n-1))*(cos.(n*x)*cos.x-sin.x*sin.(n*x))
.= n*((sin.x) #Z (n-1))*(cos.(x+n*x)) by SIN_COS:74
.= n*((sin.x) #Z (n-1))*cos.((n+1)*x);
hence (((cos*f)(#)(( #Z n)*sin))`|Z).x = n*(sin.x) #Z (n-1) *cos.((n+1)*x);
end;
hence thesis by A1,A10,A15,FDIFF_1:21;
end;
:: 12 f.x=cos(n*x)*(cos x ^ n)
theorem
Z c= dom ((cos*f)(#)(( #Z n)*cos)) & n>=1 & (for x st x in Z holds f.x
=n*x) implies (cos*f)(#)(( #Z n)*cos) is_differentiable_on Z & for x st x in Z
holds (((cos*f)(#)(( #Z n)*cos))`|Z).x =-n*(cos.x) #Z (n-1) *sin.((n+1)*x)
proof
assume that
A1: Z c= dom ((cos*f)(#)(( #Z n)*cos)) and
A2: n>=1 and
A3: for x st x in Z holds f.x=n*x;
A4: for x st x in Z holds f.x=n*x+0 by A3;
A5: Z c= dom (cos*f) /\ dom (( #Z n)*cos) by A1,VALUED_1:def 4;
then
A6: Z c= dom (cos*f) by XBOOLE_1:18;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A7: Z c= dom f;
then
A8: f is_differentiable_on Z by A4,FDIFF_1:23;
for x st x in Z holds cos*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A9: f is_differentiable_in x by A8,FDIFF_1:9;
cos is_differentiable_in f.x by SIN_COS:63;
hence thesis by A9,FDIFF_2:13;
end;
then
A10: cos*f is_differentiable_on Z by A6,FDIFF_1:9;
A11: for x st x in Z holds ((cos*f)`|Z).x = -n* sin.(n*x)
proof
let x;
A12: cos is_differentiable_in f.x by SIN_COS:63;
assume
A13: x in Z;
then f is_differentiable_in x by A8,FDIFF_1:9;
then diff(cos*f,x) = diff(cos, f.x)*diff(f,x) by A12,FDIFF_2:13
.=(-sin.( f.x))*diff(f,x) by SIN_COS:63
.=-sin.( f.x)*diff(f,x)
.=-sin.(n*x)*diff(f,x) by A3,A13
.=-sin.(n*x)*(f`|Z).x by A8,A13,FDIFF_1:def 7
.=-n* sin.(n*x) by A7,A4,A13,FDIFF_1:23;
hence thesis by A10,A13,FDIFF_1:def 7;
end;
A14: Z c= dom (( #Z n)*cos) by A5,XBOOLE_1:18;
now
let x;
assume x in Z;
cos is_differentiable_in x by SIN_COS:63;
hence ( #Z n)*cos is_differentiable_in x by TAYLOR_1:3;
end;
then
A15: ( #Z n)*cos is_differentiable_on Z by A14,FDIFF_1:9;
A16: for x st x in Z holds ((( #Z n)*cos)`|Z).x =-n*((cos.x) #Z (n-1)) *sin. x
proof
let x;
cos is_differentiable_in x by SIN_COS:63;
then
A17: diff((( #Z n)*cos),x) =(n*((cos.x) #Z (n-1)) * diff(cos,x)) by TAYLOR_1:3
.=n*((cos.x) #Z (n-1))*(-sin.x) by SIN_COS:63
.=-n*((cos.x) #Z (n-1))*sin.x;
assume x in Z;
hence thesis by A15,A17,FDIFF_1:def 7;
end;
now
let x;
A18: n-1 is Element of NAT by A2,NAT_1:21;
assume
A19: x in Z;
then
(((cos*f)(#)(( #Z n)*cos))`|Z).x =(( #Z n)*cos).x*diff(cos*f,x)+(cos*
f).x*diff((( #Z n)*cos),x) by A1,A10,A15,FDIFF_1:21
.=(( #Z n).(cos.x))*diff(cos*f,x)+(cos*f).x*diff((( #Z n)*cos),x) by A14
,A19,FUNCT_1:12
.=((cos.x) #Z n)*diff(cos*f,x)+(cos*f).x*diff((( #Z n)*cos),x) by
TAYLOR_1:def 1
.=((cos.x) #Z n)*((cos*f)`|Z).x+(cos*f).x*diff((( #Z n)*cos),x) by A10
,A19,FDIFF_1:def 7
.=((cos.x) #Z n)*(-n* sin.(n*x))+(cos*f).x*diff((( #Z n)*cos),x) by A11
,A19
.=((cos.x) #Z n)*(-n* sin.(n*x))+(cos.(f.x))*diff((( #Z n)*cos),x) by A6
,A19,FUNCT_1:12
.=((cos.x) #Z n)*(-n* sin.(n*x))+(cos.(n*x))*diff((( #Z n)*cos),x) by A3
,A19
.=((cos.x) #Z n)*(-n* sin.(n*x))+(cos.(n*x))*((( #Z n)*cos)`|Z).x by A15
,A19,FDIFF_1:def 7
.=((cos.x) #Z ((n-1)+1))*(-n* sin.(n*x))+ (cos.(n*x))*(-n*((cos.x) #Z
(n-1)) *sin.x) by A16,A19
.=(((cos.x) #Z (n-1))*((cos.x) #Z 1))*(-n* sin.(n*x))+ (cos.(n*x))*(-n
*((cos.x) #Z (n-1)) *sin.x) by A18,TAYLOR_1:1
.=(((cos.x) #Z (n-1))*(cos.x))*(-n* sin.(n*x))+ (cos.(n*x))*(-n*((cos.
x) #Z (n-1)) *sin.x) by PREPOWER:35
.= -n*((cos.x) #Z (n-1))*(sin.(n*x)*cos.x+cos.(n*x)*sin.x)
.= -n*((cos.x) #Z (n-1))*(sin.(x+n*x)) by SIN_COS:74
.= -n*((cos.x) #Z (n-1))*sin.((n+1)*x);
hence
(((cos*f)(#)(( #Z n)*cos))`|Z).x = -n*(cos.x) #Z (n-1) *sin.((n+1)*x);
end;
hence thesis by A1,A10,A15,FDIFF_1:21;
end;
:: 13 f.x=sin(n*x)*(cos x ^ n)
theorem
Z c= dom ((sin*f)(#)(( #Z n)*cos)) & n>=1 & (for x st x in Z holds f.x
=n*x) implies (sin*f)(#)(( #Z n)*cos) is_differentiable_on Z & for x st x in Z
holds (((sin*f)(#)(( #Z n)*cos))`|Z).x =n*(cos.x) #Z (n-1) *cos.((n+1)*x)
proof
assume that
A1: Z c= dom ((sin*f)(#)(( #Z n)*cos)) and
A2: n>=1 and
A3: for x st x in Z holds f.x=n*x;
A4: for x st x in Z holds f.x=n*x+0 by A3;
A5: Z c= dom (sin*f) /\ dom (( #Z n)*cos) by A1,VALUED_1:def 4;
then
A6: Z c= dom (sin*f) by XBOOLE_1:18;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A7: Z c= dom f;
then
A8: f is_differentiable_on Z by A4,FDIFF_1:23;
for x st x in Z holds sin*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A9: f is_differentiable_in x by A8,FDIFF_1:9;
sin is_differentiable_in f.x by SIN_COS:64;
hence thesis by A9,FDIFF_2:13;
end;
then
A10: sin*f is_differentiable_on Z by A6,FDIFF_1:9;
A11: for x st x in Z holds ((sin*f)`|Z).x = n* cos.(n*x)
proof
let x;
A12: sin is_differentiable_in f.x by SIN_COS:64;
assume
A13: x in Z;
then f is_differentiable_in x by A8,FDIFF_1:9;
then diff(sin*f,x) = diff(sin, f.x)*diff(f,x) by A12,FDIFF_2:13
.=cos.(f.x)*diff(f,x) by SIN_COS:64
.=cos.(n*x)*diff(f,x) by A3,A13
.=cos.(n*x)*(f`|Z).x by A8,A13,FDIFF_1:def 7
.=n* cos.(n*x) by A7,A4,A13,FDIFF_1:23;
hence thesis by A10,A13,FDIFF_1:def 7;
end;
A14: Z c= dom (( #Z n)*cos) by A5,XBOOLE_1:18;
now
let x;
assume x in Z;
cos is_differentiable_in x by SIN_COS:63;
hence ( #Z n)*cos is_differentiable_in x by TAYLOR_1:3;
end;
then
A15: ( #Z n)*cos is_differentiable_on Z by A14,FDIFF_1:9;
A16: for x st x in Z holds ((( #Z n)*cos)`|Z).x =-n*((cos.x) #Z (n-1)) *sin. x
proof
let x;
cos is_differentiable_in x by SIN_COS:63;
then
A17: diff((( #Z n)*cos),x) =(n*((cos.x) #Z (n-1)) * diff(cos,x)) by TAYLOR_1:3
.=(n*((cos.x) #Z (n-1))) *(-sin.x) by SIN_COS:63
.=-n*((cos.x) #Z (n-1)) *sin.x;
assume x in Z;
hence thesis by A15,A17,FDIFF_1:def 7;
end;
now
let x;
A18: n-1 is Element of NAT by A2,NAT_1:21;
assume
A19: x in Z;
then
(((sin*f)(#)(( #Z n)*cos))`|Z).x =(( #Z n)*cos).x*diff(sin*f,x)+(sin*
f).x*diff((( #Z n)*cos),x) by A1,A10,A15,FDIFF_1:21
.=(( #Z n).(cos.x))*diff(sin*f,x)+(sin*f).x*diff((( #Z n)*cos),x) by A14
,A19,FUNCT_1:12
.=((cos.x) #Z n)*diff(sin*f,x)+(sin*f).x*diff((( #Z n)*cos),x) by
TAYLOR_1:def 1
.=((cos.x) #Z n)*((sin*f)`|Z).x+(sin*f).x*diff((( #Z n)*cos),x) by A10
,A19,FDIFF_1:def 7
.=((cos.x) #Z n)*(n* cos.(n*x))+(sin*f).x*diff((( #Z n)*cos),x) by A11
,A19
.=((cos.x) #Z n)*(n* cos.(n*x))+(sin.(f.x))*diff((( #Z n)*cos),x) by A6
,A19,FUNCT_1:12
.=((cos.x) #Z n)*(n* cos.(n*x))+(sin.(n*x))*diff((( #Z n)*cos),x) by A3
,A19
.=((cos.x) #Z n)*(n* cos.(n*x))+(sin.(n*x))*((( #Z n)*cos)`|Z).x by A15
,A19,FDIFF_1:def 7
.=((cos.x) #Z ((n-1)+1))*(n*cos.(n*x))+ sin.(n*x)*(-n*((cos.x) #Z (n-1
)) *sin.x) by A16,A19
.=(((cos.x) #Z (n-1))*((cos.x) #Z 1))*(n* cos.(n*x))+ sin.(n*x)*(-n*((
cos.x) #Z (n-1)) *sin.x) by A18,TAYLOR_1:1
.=(((cos.x) #Z (n-1))*((cos.x) #Z 1))*(n* cos.(n*x))- sin.(n*x)*n*((
cos.x) #Z (n-1)) *sin.x
.=(((cos.x) #Z (n-1))*(cos.x))*(n* cos.(n*x))- (sin.(n*x)*n*((cos.x)
#Z (n-1)) *sin.x) by PREPOWER:35
.= n*((cos.x) #Z (n-1))*(cos.(n*x)*cos.x-sin.x*sin.(n*x))
.= n*((cos.x) #Z (n-1))*(cos.(x+n*x)) by SIN_COS:74
.= n*((cos.x) #Z (n-1))*cos.((n+1)*x);
hence (((sin*f)(#)(( #Z n)*cos))`|Z).x = n*(cos.x) #Z (n-1) *cos.((n+1)*x);
end;
hence thesis by A1,A10,A15,FDIFF_1:21;
end;
:: 14 f.x=(1/x)*sin x
theorem
not 0 in Z & Z c= dom (((id Z)^)(#)sin) implies ((id Z)^)(#)sin
is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)sin)`|Z).x =(1/x)*
cos.x-(1/x^2)*sin.x
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom ((f^)(#)sin);
A3: f^ is_differentiable_on Z by A1,Th4;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
Z c= dom (f^) /\ dom (sin) by A2,VALUED_1:def 4;
then
A5: Z c= dom (f^) by XBOOLE_1:18;
now
let x;
assume
A6: x in Z;
hence
(((f^)(#)sin)`|Z).x = (sin.x)*diff((f^),x)+((f^).x)*diff(sin,x) by A2,A3,A4
,FDIFF_1:21
.=(sin.x)*((f^)`|Z).x+ ((f^).x)*diff(sin,x) by A3,A6,FDIFF_1:def 7
.=(sin.x)*(-1/x^2)+ ((f^).x)*diff(sin,x) by A1,A6,Th4
.=(sin.x)*(-1/x^2)+((f^).x)*(cos.x) by SIN_COS:64
.=(sin.x)*(-1/x^2)+((f.x)")*(cos.x) by A5,A6,RFUNCT_1:def 2
.=(sin.x)*(-1/x^2)+(1*x")*(cos.x) by A6,FUNCT_1:18
.=-(1/x^2)*(sin.x)+(1/x)*(cos.x) by XCMPLX_0:def 9
.=(1/x)*cos.x-(1/x^2)*sin.x;
end;
hence thesis by A2,A3,A4,FDIFF_1:21;
end;
:: 15 f.x=(1/x)*cos x
theorem
not 0 in Z & Z c= dom (((id Z)^)(#)cos) implies ((id Z)^)(#)cos
is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)cos)`|Z).x =-(1/x)
*sin.x-(1/x^2)*cos.x
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (((id Z)^)(#)cos);
A3: f^ is_differentiable_on Z by A1,Th4;
A4: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
Z c= dom (f^) /\ dom (cos) by A2,VALUED_1:def 4;
then
A5: Z c= dom (f^) by XBOOLE_1:18;
now
let x;
assume
A6: x in Z;
hence
(((f^)(#)cos)`|Z).x = (cos.x)*diff((f^),x)+((f^).x)*diff(cos,x) by A2,A3,A4
,FDIFF_1:21
.=(cos.x)*((f^)`|Z).x+ ((f^).x)*diff(cos,x) by A3,A6,FDIFF_1:def 7
.=(cos.x)*(-1/x^2)+ ((f^).x)*diff(cos,x) by A1,A6,Th4
.=(cos.x)*(-1/x^2)+((f^).x)*(-sin.x) by SIN_COS:63
.=(cos.x)*(-1/x^2)+((f.x)")*(-sin.x) by A5,A6,RFUNCT_1:def 2
.=(cos.x)*(-1/x^2)+(1*x")*(-sin.x) by A6,FUNCT_1:18
.=-(1/x^2)*(cos.x)+(1/x)*(-sin.x) by XCMPLX_0:def 9
.=-(1/x)*sin.x-(1/x^2)*cos.x;
end;
hence thesis by A2,A3,A4,FDIFF_1:21;
end;
:: 16 f.x=sin.x+x^(1/2)
theorem
Z c= dom (sin+( #R (1/2))) implies sin+( #R (1/2))
is_differentiable_on Z & for x st x in Z holds ((sin+( #R (1/2)))`|Z).x =cos.x+
(1/2)* x #R (-1/2)
proof
assume
A1: Z c= dom (sin+( #R (1/2)));
then Z c= dom (( #R (1/2))) /\ dom sin by VALUED_1:def 1;
then
A2: Z c= dom (( #R (1/2))) by XBOOLE_1:18;
then
A3: ( #R (1/2)) is_differentiable_on Z by Lm3;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A5: x in Z;
then
((sin+( #R (1/2)))`|Z).x = diff(sin,x) + diff(( #R (1/2)),x) by A1,A3,A4,
FDIFF_1:18
.=cos.x + diff(( #R (1/2)),x) by SIN_COS:64
.=cos.x + ((( #R (1/2)))`|Z).x by A3,A5,FDIFF_1:def 7
.=cos.x +(1/2)*x #R (-1/2) by A2,A5,Lm3;
hence ((sin+( #R (1/2)))`|Z).x =cos.x+(1/2)*x #R (-1/2);
end;
hence thesis by A1,A3,A4,FDIFF_1:18;
end;
:: 17 f.x=x^2*sin(1/x)
theorem
not 0 in Z & Z c= dom (g(#)(sin*((id Z)^))) & g=#Z 2 implies g(#)(sin*
((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(sin*((id Z)^))
)`|Z).x = 2*x*sin.(1/x)-cos.(1/x)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(sin*(f^))) and
A3: g=#Z 2;
A4: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom g /\ dom (sin*(f^)) by A2,VALUED_1:def 4;
then Z c= dom g by XBOOLE_1:18;
then
A6: g is_differentiable_on Z by A4,FDIFF_1:9;
A7: for x st x in Z holds (g`|Z).x = 2*x
proof
let x;
assume
A8: x in Z;
diff(g,x) = 2 * (x #Z (2-1)) by A3,TAYLOR_1:2
.=2*x by PREPOWER:35;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
A9: sin*(f^) is_differentiable_on Z by A1,Th5;
A10: Z c= dom (sin*(f^)) by A5,XBOOLE_1:18;
then for y being object st y in Z holds y in dom (f^) by FUNCT_1:11;
then
A11: Z c= dom (f^);
now
let x;
assume
A12: x in Z;
then
((g(#)(sin*(f^)))`|Z).x = ((sin*(f^)).x)*diff(g,x) + (g.x)*diff(sin*(
f^),x) by A2,A9,A6,FDIFF_1:21
.=((sin*(f^)).x)*(g`|Z).x+ (g.x)*diff(sin*(f^),x) by A6,A12,FDIFF_1:def 7
.=((sin*(f^)).x)*(2*x)+(g.x)*diff(sin*(f^),x) by A7,A12
.=((sin*(f^)).x)*(2*x)+(x #Z 2)*diff(sin*(f^),x) by A3,TAYLOR_1:def 1
.=((sin*(f^)).x)*(2*x)+(x #Z 2)*(((sin*(f^))`|Z).x ) by A9,A12,
FDIFF_1:def 7
.=((sin*(f^)).x)*(2*x)+(x #Z 2)*(-(1/x^2)*cos.(1/x)) by A1,A12,Th5
.=((sin*(f^)).x)*(2*x)-(x #Z (1+1))*((1/x^2)*cos.(1/x))
.=((sin*(f^)).x)*(2*x) -((x #Z 1)*(x #Z 1))*((1/x^2)*cos.(1/x)) by
TAYLOR_1:1
.=((sin*(f^)).x)*(2*x) -(x*(x #Z 1))*((1/x^2)*cos.(1/x)) by PREPOWER:35
.=((sin*(f^)).x)*(2*x) -(x*x)*(((1*1)/(x*x))*cos.(1/x)) by PREPOWER:35
.=((sin*(f^)).x)*(2*x) -(x*x)*(((1/x)*(1/x))*cos.(1/x)) by XCMPLX_1:102
.=((sin*(f^)).x)*(2*x) -(x*(1/x))*(x*(1/x))*cos.(1/x)
.=((sin*(f^)).x)*(2*x) -(x*(1/x))*(1)*cos.(1/x) by A1,A12,XCMPLX_1:106
.=((sin*(f^)).x)*(2*x) -(1)*(1)*cos.(1/x) by A1,A12,XCMPLX_1:106
.=(sin.((f^).x))*(2*x) -cos.(1/x) by A10,A12,FUNCT_1:12
.=(sin.((f.x)"))*(2*x) -cos.(1/x) by A11,A12,RFUNCT_1:def 2
.=(sin.(1*x"))*(2*x) -cos.(1/x) by A12,FUNCT_1:18
.=2*x*sin.(1/x)-cos.(1/x) by XCMPLX_0:def 9;
hence ((g(#)(sin*(f^)))`|Z).x = 2*x*sin.(1/x)-cos.(1/x);
end;
hence thesis by A2,A9,A6,FDIFF_1:21;
end;
:: 18 f.x=x^2*cos(1/x)
theorem
not 0 in Z & Z c= dom (g(#)(cos*((id Z)^))) & g=#Z 2 implies g(#)(cos*
((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((g(#)(cos*((id Z)^))
)`|Z).x = 2*x*cos.(1/x)+sin.(1/x)
proof
set f = id Z;
assume that
A1: not 0 in Z and
A2: Z c= dom (g(#)(cos*(f^))) and
A3: g=#Z 2;
A4: for x st x in Z holds g is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom g /\ dom (cos*(f^)) by A2,VALUED_1:def 4;
then
A6: Z c= dom (cos*(f^)) by XBOOLE_1:18;
then
A7: cos*(f^) is_differentiable_on Z by A1,Th6;
Z c= dom g by A5,XBOOLE_1:18;
then
A8: g is_differentiable_on Z by A4,FDIFF_1:9;
A9: for x st x in Z holds (g`|Z).x = 2*x
proof
let x;
assume
A10: x in Z;
diff(g,x) = 2 * (x #Z (2-1)) by A3,TAYLOR_1:2
.=2*x by PREPOWER:35;
hence thesis by A8,A10,FDIFF_1:def 7;
end;
for y being object st y in Z holds y in dom (f^) by A6,FUNCT_1:11;
then
A11: Z c= dom (f^);
now
let x;
assume
A12: x in Z;
then
((g(#)(cos*(f^)))`|Z).x = ((cos*(f^)).x)*diff(g,x) + (g.x)*diff(cos*(
f^),x) by A2,A7,A8,FDIFF_1:21
.=((cos*(f^)).x)*(g`|Z).x+ (g.x)*diff(cos*(f^),x) by A8,A12,FDIFF_1:def 7
.=((cos*(f^)).x)*(2*x)+(g.x)*diff(cos*(f^),x) by A9,A12
.=((cos*(f^)).x)*(2*x)+(x #Z 2)*diff(cos*(f^),x) by A3,TAYLOR_1:def 1
.=((cos*(f^)).x)*(2*x)+(x #Z 2)*(((cos*(f^))`|Z).x ) by A7,A12,
FDIFF_1:def 7
.=((cos*(f^)).x)*(2*x)+(x #Z (1+1))*((1/x^2)*sin.(1/x)) by A1,A6,A12,Th6
.=((cos*(f^)).x)*(2*x) +((x #Z 1)*(x #Z 1))*((1/x^2)*sin.(1/x)) by
TAYLOR_1:1
.=((cos*(f^)).x)*(2*x) +(x*(x #Z 1))*((1/x^2)*sin.(1/x)) by PREPOWER:35
.=((cos*(f^)).x)*(2*x) +(x*x)*(((1*1)/(x*x))*sin.(1/x)) by PREPOWER:35
.=((cos*(f^)).x)*(2*x) +(x*x)*(((1/x)*(1/x))*sin.(1/x)) by XCMPLX_1:102
.=((cos*(f^)).x)*(2*x) +(x*(1/x))*(x*(1/x))*sin.(1/x)
.=((cos*(f^)).x)*(2*x) +(x*(1/x))*(1)*sin.(1/x)by A1,A12,XCMPLX_1:106
.=((cos*(f^)).x)*(2*x) +(1)*(1)*sin.(1/x) by A1,A12,XCMPLX_1:106
.=(cos.((f^).x))*(2*x) +sin.(1/x) by A6,A12,FUNCT_1:12
.=(cos.((f.x)"))*(2*x) +sin.(1/x) by A11,A12,RFUNCT_1:def 2
.=(cos.(1*x"))*(2*x) +sin.(1/x) by A12,FUNCT_1:18
.=2*x*cos.(1/x)+sin.(1/x) by XCMPLX_0:def 9;
hence ((g(#)(cos*(f^)))`|Z).x = 2*x*cos.(1/x)+sin.(1/x);
end;
hence thesis by A2,A7,A8,FDIFF_1:21;
end;
:: 19 f.x=ln(x) - TAYLOR_1:18
Lm5: x in dom ln implies x > 0 by TAYLOR_1:18,XXREAL_1:4;
theorem Th19:
Z c= dom ln implies ln is_differentiable_on Z & for x st x in Z
holds (ln`|Z).x = 1/x
proof
assume
A1: Z c= dom ln;
then
A2: for x st x in Z holds ln is_differentiable_in x by Lm5,TAYLOR_1:18;
then
A3: ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (ln`|Z).x = 1/x
proof
let x;
assume
A4: x in Z;
then diff(ln,x) = 1/x by A1,TAYLOR_1:18;
hence thesis by A3,A4,FDIFF_1:def 7;
end;
hence thesis by A1,A2,FDIFF_1:9;
end;
:: 20 f.x=x*ln(x)
theorem
Z c= dom ((id Z)(#)ln) implies (id Z)(#)ln is_differentiable_on Z &
for x st x in Z holds (((id Z)(#)ln)`|Z).x = 1+ln.x
proof
set f = ln;
assume
A1: Z c= dom ((id Z)(#)ln);
then
A2: Z c= dom id Z /\ dom f by VALUED_1:def 4;
then
A3: Z c= dom id Z by XBOOLE_1:18;
A4: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
then
A5: id Z is_differentiable_on Z by A3,FDIFF_1:23;
A6: Z c= dom f by A2,XBOOLE_1:18;
then
A7: f is_differentiable_on Z by Th19;
for x st x in Z holds (((id Z)(#)f)`|Z).x =1+ln.x
proof
let x;
assume
A8: x in Z;
then
A9: x<>0 by A6,TAYLOR_1:18,XXREAL_1:4;
(((id Z)(#)f)`|Z).x =((id Z).x)*diff(f,x)+(f.x)*diff((id Z),x) by A1,A5,A7
,A8,FDIFF_1:21
.=((id Z).x)*((f`|Z).x)+(f.x)*diff((id Z),x) by A7,A8,FDIFF_1:def 7
.=((id Z).x)*(1/x) + (f.x)*diff((id Z),x) by A6,A8,Th19
.=x*(1/x) + (f.x)*diff((id Z),x) by A8,FUNCT_1:18
.=x*(1/x) + (f.x)*(((id Z)`|Z).x) by A5,A8,FDIFF_1:def 7
.=x*(1/x) + (f.x)*1 by A3,A4,A8,FDIFF_1:23
.= 1 + ln.x by A9,XCMPLX_1:106;
hence thesis;
end;
hence thesis by A1,A5,A7,FDIFF_1:21;
end;
:: 21 f.x=x^2*ln(x)
theorem
Z c= dom (g(#)ln) & g=#Z 2 & (for x st x in Z holds x>0) implies g(#)
ln is_differentiable_on Z & for x st x in Z holds ((g(#)ln)`|Z).x = x+2*x*ln.x
proof
set f = ln;
assume that
A1: Z c= dom (g(#)f) and
A2: g=#Z 2 and
A3: for x st x in Z holds x>0;
A4: for x st x in Z holds g is_differentiable_in x by A2,TAYLOR_1:2;
A5: Z c= dom (g) /\ dom (f) by A1,VALUED_1:def 4;
then
A6: Z c= dom (f) by XBOOLE_1:18;
then
A7: f is_differentiable_on Z by Th19;
Z c= dom g by A5,XBOOLE_1:18;
then
A8: g is_differentiable_on Z by A4,FDIFF_1:9;
A9: for x st x in Z holds (g`|Z).x = 2*x
proof
let x;
assume
A10: x in Z;
diff(g,x) = 2 * (x #Z (2-1)) by A2,TAYLOR_1:2
.=2*x by PREPOWER:35;
hence thesis by A8,A10,FDIFF_1:def 7;
end;
now
let x;
assume
A11: x in Z;
then
A12: x<>0 by A3;
((g(#)f)`|Z).x =(g.x)*diff(f,x) + (f.x)*diff(g,x) by A1,A8,A7,A11,
FDIFF_1:21
.=(g.x)*((f`|Z).x)+(f.x)*diff(g,x) by A7,A11,FDIFF_1:def 7
.=(g.x)*(1/x) + (f.x)*diff(g,x) by A6,A11,Th19
.=(x #Z 2)*(1/x) + (f.x)*diff(g,x) by A2,TAYLOR_1:def 1
.=(x #Z 2)*(1/x) + (f.x)*((g`|Z).x) by A8,A11,FDIFF_1:def 7
.=(x #Z (1+1))*(1/x) + 2*x*(ln.x) by A9,A11
.=((x #Z 1)*(x #Z 1))*(1/x) + 2*x*(ln.x) by TAYLOR_1:1
.=((x #Z 1)*x)*(1/x) + 2*x*(ln.x) by PREPOWER:35
.=(x*x)*(1/x) + 2*x*(ln.x) by PREPOWER:35
.=x*(x*(1/x)) + 2*x*(ln.x)
.=x*1 + 2*x*(ln.x) by A12,XCMPLX_1:106
.=x+2*x*(ln.x);
hence ((g(#)f)`|Z).x = x+2*x*ln.x;
end;
hence thesis by A1,A8,A7,FDIFF_1:21;
end;
:: 22 f.x=(a+x^2)/(a-x^2)
theorem Th22:
Z c= dom ((f1+f2)/(f1-f2)) & (for x st x in Z holds f1.x=a) & f2
=#Z 2 & (for x st x in Z holds (f1-f2).x>0) implies (f1+f2)/(f1-f2)
is_differentiable_on Z & for x st x in Z holds (((f1+f2)/(f1-f2))`|Z).x = (4*a*
x)/(a-x|^2)|^2
proof
assume that
A1: Z c= dom ((f1+f2)/(f1-f2)) and
A2: for x st x in Z holds f1.x=a and
A3: f2=#Z 2 and
A4: for x st x in Z holds (f1-f2).x>0;
A5: Z c= dom (f1+f2) /\ (dom (f1-f2)\(f1-f2)"{0}) by A1,RFUNCT_1:def 1;
then
A6: Z c= dom (f1+f2) by XBOOLE_1:18;
then
A7: f1+f2 is_differentiable_on Z by A2,A3,Lm1;
A8: Z c= dom (f1-f2) by A5,XBOOLE_1:1;
then
A9: f1-f2 is_differentiable_on Z by A2,A3,Lm2;
A10: for x st x in Z holds (f1-f2).x <> 0 by A4;
then
A11: (f1+f2)/(f1-f2) is_differentiable_on Z by A7,A9,FDIFF_2:21;
for x st x in Z holds (((f1+f2)/(f1-f2))`|Z).x = (4*a*x)/(a-x|^2)|^2
proof
let x;
assume
A12: x in Z;
then
A13: f1.x=a by A2;
A14: (f1-f2).x <>0 by A4,A12;
f1+f2 is_differentiable_in x & f1-f2 is_differentiable_in x by A7,A9,A12,
FDIFF_1:9;
then
diff((f1+f2)/(f1-f2),x) =(diff((f1+f2),x)*(f1-f2).x - diff((f1-f2),x)
*(f1+f2).x)/((f1-f2).x)^2 by A14,FDIFF_2:14
.=(diff((f1+f2),x)*(f1.x-f2.x)- diff((f1-f2),x)*(f1+f2).x)/((f1-f2).x)
^2 by A8,A12,VALUED_1:13
.=(diff((f1+f2),x)*(f1.x-f2.x)- diff((f1-f2),x)* (f1.x+f2.x))/((f1-f2)
.x)^2 by A6,A12,VALUED_1:def 1
.=(diff((f1+f2),x)*(f1.x-f2.x)- diff((f1-f2),x)* (f1.x+f2.x))/(f1.x-f2
.x)^2 by A8,A12,VALUED_1:13
.=((((f1+f2)`|Z).x)*(f1.x-f2.x)- diff((f1-f2),x)* (f1.x+f2.x))/(f1.x-
f2.x)^2 by A7,A12,FDIFF_1:def 7
.=((2*x)*(f1.x-f2.x)-diff((f1-f2),x)*(f1.x+f2.x))/(f1.x-f2.x)^2 by A2,A3
,A6,A12,Lm1
.=((2*x)*(f1.x-f2.x)-(((f1-f2)`|Z).x)*(f1.x+f2.x))/(f1.x-f2.x)^2 by A9
,A12,FDIFF_1:def 7
.=((2*x)*(f1.x-f2.x)-(-2*x)*(f1.x+f2.x))/(f1.x-f2.x)^2 by A2,A3,A8,A12
,Lm2
.=(4*x*a)/(a-(x #Z 2))^2 by A3,A13,TAYLOR_1:def 1
.=(4*x*a)/(a-x|^2)^2 by PREPOWER:36
.=(4*x*a)/((a-x|^2)|^1*(a- x|^2))
.=(4*x*a)/(a-x|^2)|^(1+1)by NEWTON:6
.= (4*a*x)/(a-x|^2)|^2;
hence thesis by A11,A12,FDIFF_1:def 7;
end;
hence thesis by A7,A9,A10,FDIFF_2:21;
end;
:: 23 f.x=ln((a+x^2)/(a-x^2))
theorem
Z c= dom (ln*((f1+f2)/(f1-f2))) & (for x st x in Z holds f1.x=a) & f2=
#Z 2 & (for x st x in Z holds (f1-f2).x>0) & (for x st x in Z holds (f1+f2).x>0
) implies ln*((f1+f2)/(f1-f2)) is_differentiable_on Z & for x st x in Z holds (
(ln*((f1+f2)/(f1-f2)))`|Z).x = (4*a*x)/(a|^2-x|^4)
proof
assume that
A1: Z c= dom (ln*((f1+f2)/(f1-f2))) and
A2: for x st x in Z holds f1.x=a and
A3: f2=#Z 2 and
A4: for x st x in Z holds (f1-f2).x>0 and
A5: for x st x in Z holds (f1+f2).x >0;
for y being object st y in Z holds y in dom ((f1+f2)/(f1-f2))
by A1,FUNCT_1:11;
then
A6: Z c= dom ((f1+f2)/(f1-f2));
then
A7: (f1+f2)/(f1-f2) is_differentiable_on Z by A2,A3,A4,Th22;
A8: Z c= dom (f1+f2) /\ (dom (f1-f2) \ (f1-f2)"{0}) by A6,RFUNCT_1:def 1;
then
A9: Z c= dom (f1+f2) by XBOOLE_1:18;
A10: Z c= dom (f1-f2) by A8,XBOOLE_1:1;
A11: for x st x in Z holds ((f1+f2)/(f1-f2)).x >0
proof
let x;
assume
A12: x in Z;
then x in dom ((f1+f2)/(f1-f2)) by A1,FUNCT_1:11;
then
A13: ((f1+f2)/(f1-f2)).x=(f1+f2).x * ((f1-f2).x)" by RFUNCT_1:def 1
.=(f1+f2).x / (f1-f2).x by XCMPLX_0:def 9;
(f1+f2).x >0 & (f1-f2).x >0 by A4,A5,A12;
hence thesis by A13,XREAL_1:139;
end;
A14: for x st x in Z holds ln*((f1+f2)/(f1-f2)) is_differentiable_in x
proof
let x;
assume x in Z;
then (f1+f2)/(f1-f2) is_differentiable_in x & ((f1+f2)/(f1-f2)).x >0 by A7
,A11,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A15: ln*((f1+f2)/(f1-f2)) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*((f1+f2)/(f1-f2)))`|Z).x = (4*a*x)/(a|^2-x|^ 4)
proof
let x;
assume
A16: x in Z;
then
A17: x in dom ((f1+f2)/(f1-f2)) by A1,FUNCT_1:11;
A18: (f1-f2).x <>0 by A4,A16;
A19: f1.x=a by A2,A16;
((f1+f2)/(f1-f2)) is_differentiable_in x & ((f1+f2)/(f1-f2)).x > 0 by A7
,A11,A16,FDIFF_1:9;
then diff(ln*((f1+f2)/(f1-f2)),x) = diff(((f1+f2)/(f1-f2)),x)/(((f1+f2)/(
f1-f2)).x) by TAYLOR_1:20
.=(((f1+f2)/(f1-f2))`|Z).x/(((f1+f2)/(f1-f2)).x) by A7,A16,FDIFF_1:def 7
.=(((f1+f2)/(f1-f2))`|Z).x/((f1+f2).x *((f1-f2).x)") by A17,
RFUNCT_1:def 1
.= ((4*a*x)/(f1.x-x|^2)|^2)/(((f1+f2).x) *((f1-f2).x)") by A2,A3,A4,A6
,A16,A19,Th22
.= ((4*a*x)/(f1.x-(x #Z 2))|^2)/(((f1+f2).x) *((f1-f2).x)") by
PREPOWER:36
.= ((4*a*x)/(f1.x-f2.x)|^2)/(((f1+f2).x) *((f1-f2).x)") by A3,
TAYLOR_1:def 1
.= ((4*a*x)/((f1-f2).x)|^2)/(((f1+f2).x) *((f1-f2).x)") by A10,A16,
VALUED_1:13
.= ((4*a*x)/(((f1-f2).x)|^(1+1)))/((f1+f2).x/(f1-f2).x) by XCMPLX_0:def 9
.= ((4*a*x)/(((f1-f2).x)|^1*(f1-f2).x))/((f1+f2).x/(f1-f2).x) by NEWTON:6
.= ((4*a*x)/((f1-f2).x*(f1-f2).x))/((f1+f2).x/(f1-f2).x)
.= ((4*a*x)/(f1-f2).x/(f1-f2).x)/((f1+f2).x/(f1-f2).x) by XCMPLX_1:78
.= ((4*a*x)/(f1-f2).x)/((f1+f2).x/(f1-f2).x)/(f1-f2).x by XCMPLX_1:48
.= (4*a*x)/(f1+f2).x/(f1-f2).x by A18,XCMPLX_1:55
.= (4*a*x)/((f1+f2).x*(f1-f2).x) by XCMPLX_1:78
.= (4*a*x)/((f1.x+f2.x)*(f1-f2).x) by A9,A16,VALUED_1:def 1
.= (4*a*x)/((f1.x+f2.x)*(f1.x-f2.x)) by A10,A16,VALUED_1:13
.= (4*a*x)/(a*a-f2.x*f2.x) by A19
.= (4*a*x)/(a*a-(x #Z 2)*f2.x) by A3,TAYLOR_1:def 1
.= (4*a*x)/(a*a-(x #Z 2)*(x #Z 2)) by A3,TAYLOR_1:def 1
.= (4*a*x)/(a|^1*a- (x #Z 2)*(x #Z 2))
.= (4*a*x)/(a|^(1+1)- (x #Z 2)*(x #Z 2)) by NEWTON:6
.= (4*a*x)/(a|^(1+1)- (x|^2)*(x #Z 2)) by PREPOWER:36
.= (4*a*x)/(a|^2- (x|^2)*(x|^2)) by PREPOWER:36
.= (4*a*x)/(a|^2- x|^(2+2)) by NEWTON:8
.= (4*a*x)/(a|^2- x|^4);
hence thesis by A15,A16,FDIFF_1:def 7;
end;
hence thesis by A1,A14,FDIFF_1:9;
end;
:: 24 f.x=(1/x)*ln(x)
theorem
Z c= dom (((id Z)^)(#)ln) & (for x st x in Z holds x >0) implies ((id
Z)^)(#)ln is_differentiable_on Z & for x st x in Z holds ((((id Z)^)(#)ln)`|Z).
x = (1/x^2)*(1-ln.x)
proof
set f = id Z, g = ln;
assume that
A1: Z c= dom ((f^)(#)g) and
A2: for x st x in Z holds x >0;
A3: not 0 in Z by A2;
then
A4: f^ is_differentiable_on Z by Th4;
A5: Z c= dom (f^) /\ dom g by A1,VALUED_1:def 4;
then
A6: Z c= dom g by XBOOLE_1:18;
then
A7: g is_differentiable_on Z by Th19;
A8: Z c= dom (f^) by A5,XBOOLE_1:18;
now
let x;
assume
A9: x in Z;
then (((f^)(#)g)`|Z).x = (g.x)*diff((f^),x)+((f^).x)*diff(g,x) by A1,A4,A7,
FDIFF_1:21
.=(g.x)*((f^)`|Z).x+ ((f^).x)*diff(g,x) by A4,A9,FDIFF_1:def 7
.=(g.x)*(-1/x^2)+ ((f^).x)*diff(g,x) by A3,A9,Th4
.=(g.x)*(-1/x^2)+ ((f^).x)*((g`|Z).x) by A7,A9,FDIFF_1:def 7
.=(g.x)*(-1/x^2)+((f^).x)*(1/x) by A6,A9,Th19
.=(g.x)*(-1/x^2)+((f.x)")*(1/x) by A8,A9,RFUNCT_1:def 2
.=(g.x)*(-1/x^2)+(1*x")*(1/x) by A9,FUNCT_1:18
.=-(1/x^2)*(g.x)+(1/x)*(1/x) by XCMPLX_0:def 9
.=-(1/x^2)*(ln.x)+1/(x^2) by XCMPLX_1:102
.=(1/x^2)*(1-ln.x);
hence (((f^)(#)g)`|Z).x =(1/x^2)*(1-ln.x);
end;
hence thesis by A1,A4,A7,FDIFF_1:21;
end;
:: 25 f.x=1/ln(x)
theorem
Z c= dom (ln^) & (for x st x in Z holds ln.x<>0) implies (ln^)
is_differentiable_on Z & for x st x in Z holds ((ln^)`|Z).x =-1/(x*(ln.x)^2)
proof
set f = ln;
assume that
A1: Z c= dom (ln^) and
A2: for x st x in Z holds ln.x<>0;
dom (f^) c= dom f by RFUNCT_1:1;
then
A3: Z c= dom f by A1;
then
A4: f is_differentiable_on Z by Th19;
then
A5: f^ is_differentiable_on Z by A2,FDIFF_2:22;
for x st x in Z holds ((f^)`|Z).x= - 1/(x*(ln.x)^2)
proof
let x;
assume
A6: x in Z;
then
A7: f.x<>0 & f is_differentiable_in x by A2,A4,FDIFF_1:9;
((f^)`|Z).x= diff(f^,x) by A5,A6,FDIFF_1:def 7
.= -diff(f,x)/(f.x)^2 by A7,FDIFF_2:15
.= -((f`|Z).x)/(f.x)^2 by A4,A6,FDIFF_1:def 7
.= -(1/x)/(ln.x)^2 by A3,A6,Th19
.= -1/(x*(ln.x)^2) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A2,A4,FDIFF_2:22;
end;