:: Several Differentiable Formulas of Special Functions -- Part {II}
:: by Yan Zhang , Bo Li and Xiquan Liang
::
:: Received November 23, 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 NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, ARYTM_1, SIN_COS,
RELAT_1, SQUARE_1, ARYTM_3, FUNCT_1, XXREAL_0, CARD_1, PREPOWER, POWER,
TARSKI, FDIFF_1, VALUED_1, NEWTON, XBOOLE_0, TAYLOR_1, ORDINAL4,
COMPLEX1, LIMFUNC1;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, LIMFUNC1,
RCOMP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1,
VALUED_1, FDIFF_1, NEWTON, INT_2, PREPOWER, POWER, TAYLOR_1, SIN_COS,
RFUNCT_1, SQUARE_1;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1,
LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, TAYLOR_1, VALUED_1,
RELSET_1, NEWTON;
registrations ORDINAL1, RELSET_1, XXREAL_0, INT_1, MEMBERED, RCOMP_1,
VALUED_0, XREAL_0, NEWTON, SIN_COS, SQUARE_1, PREPOWER;
requirements SUBSET, REAL, NUMERALS, ARITHM;
equalities SQUARE_1, TAYLOR_1, VALUED_1;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FUNCT_1, TARSKI,
PREPOWER, RFUNCT_1, SQUARE_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS,
SIN_COS2, WSIERP_1, FDIFF_4, POWER, ABSVALUE, VALUED_1;
begin
reserve y for set,
x,a for Real,
n for Element of NAT,
Z for open Subset of REAL,
f,f1,f2 for PartFunc of REAL,REAL;
Lm1: 1-cos(2*x)=2*(sin x)^2
proof
1-cos(2*x)=1-cos(x+x) .=1-((cos x) *(cos x)-(sin x) * (sin x)) by SIN_COS:75
.=(cos x)^2+(sin x)^2-((cos x)^2-(sin x)^2) by SIN_COS:29
.=2*(sin x)^2;
hence thesis;
end;
Lm2: 1+cos(2*x)=2*(cos x)^2
proof
1+cos(2*x)=1+cos(x+x) .=1+((cos x)^2-(sin x)^2) by SIN_COS:75
.=(cos x)^2+(sin x)^2+((cos x)^2-(sin x)^2) by SIN_COS:29
.=2*(cos x)^2;
hence thesis;
end;
:: 39 f.x=2*(1-cos.x) ^ (1/2)
Lm3: sin.x>0 implies sin.x=((1-cos.x)*(1+cos.x)) #R (1/2)
proof
assume
A1: sin.x>0;
then sin.x=(sin.x) #R (2*(1/2)) by PREPOWER:72
.=(sin.x) #R (1+1) #R (1/2) by A1,PREPOWER:91
.=((sin.x) #R 1 * (sin.x) #R 1) #R (1/2) by A1,PREPOWER:75
.=(sin.x * (sin.x) #R 1) #R (1/2) by A1,PREPOWER:72
.=((sin.x)^2+(cos.x)^2-(cos.x)^2) #R (1/2) by A1,PREPOWER:72
.=(1^2-(cos.x)^2) #R (1/2) by SIN_COS:28
.=((1-cos.x)*(1+cos.x)) #R (1/2);
hence thesis;
end;
Lm4: sin.x>0 & cos.x<1 & cos.x>-1 implies sin.x/(1-cos.x) #R (1/2) =(1+cos.x)
#R (1/2)
proof
assume that
A1: sin.x>0 and
A2: cos.x<1 and
A3: cos.x>-1;
A4: 1-cos.x>1-1 by A2,XREAL_1:15;
1+cos.x>1+-1 by A3,XREAL_1:8;
then
A5: (1-cos.x)*(1+cos.x)>0 by A4,XREAL_1:129;
sin.x/(1-cos.x) #R (1/2) =((1-cos.x)*(1+cos.x)) #R (1/2)/(1-cos.x) #R (1
/2) by A1,Lm3
.=(((1-cos.x)*(1+cos.x))/(1-cos.x)) #R (1/2) by A4,A5,PREPOWER:80
.=(1+cos.x) #R (1/2) by A4,XCMPLX_1:89;
hence thesis;
end;
:: a ^ x=exp.(x*ln a)
theorem Th1:
a>0 implies exp_R.(x*log(number_e,a))=a #R x
proof
assume
A1: a>0;
number_e<>1 by TAYLOR_1:11;
then exp_R.(x*log(number_e,a)) =exp_R.(log(number_e,a to_power x)) by A1,
POWER:55,TAYLOR_1:11
.=exp_R.(log(number_e,a #R x)) by A1,POWER:def 2
.=a #R x by A1,PREPOWER:81,TAYLOR_1:15;
hence thesis;
end;
:: 15 a ^ (-x)=exp.(-x*ln a)
theorem Th2:
a>0 implies exp_R.(-x*log(number_e,a))=a #R (-x)
proof
A1: number_e<>1 by TAYLOR_1:11;
assume
A2: a>0;
exp_R.(-x*log(number_e,a)) =exp_R.((-x)*log(number_e,a))
.=exp_R.(log(number_e,a to_power (-x))) by A2,A1,POWER:55,TAYLOR_1:11
.=exp_R.(log(number_e,a #R (-x))) by A2,POWER:def 2
.=a #R (-x) by A2,PREPOWER:81,TAYLOR_1:15;
hence thesis;
end;
:: 40 f.x=-2*(1+cos.x) ^ (1/2)
Lm5: sin.x>0 & cos.x<1 & cos.x>-1 implies sin.x/(1+cos.x) #R (1/2) =(1-cos.x)
#R (1/2)
proof
assume that
A1: sin.x>0 and
A2: cos.x<1 and
A3: cos.x>-1;
A4: 1+cos.x>1+-1 by A3,XREAL_1:8;
1-cos.x>1-1 by A2,XREAL_1:15;
then
A5: (1-cos.x)*(1+cos.x)>0 by A4,XREAL_1:129;
sin.x/(1+cos.x) #R (1/2) =((1-cos.x)*(1+cos.x)) #R (1/2)/(1+cos.x) #R (1
/2) by A1,Lm3
.=(((1-cos.x)*(1+cos.x))/(1+cos.x)) #R (1/2) by A4,A5,PREPOWER:80
.=(1-cos.x) #R (1/2) by A4,XCMPLX_1:89;
hence thesis;
end;
:: 1 f.x=a^2-x^2
theorem Th3:
Z c= dom (f1-f2) & (for x st x in Z holds f1.x=a^2) & 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^2 and
A3: f2=#Z 2;
A4: for x st x in Z holds f1.x=a^2+0*x by A2;
for x st x in Z holds ((f1-f2)`|Z).x = -2*x
proof
let x;
assume x in Z;
hence ((f1-f2)`|Z).x =0+2*(-1)*x by A1,A3,A4,FDIFF_4:12
.=-2*x;
end;
hence thesis by A1,A3,A4,FDIFF_4:12;
end;
:: 2 f.x=(a^2+x^2)/(a^2-x^2)
theorem Th4:
Z c= dom ((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.
x=a^2 & (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^2*x/(a^2-x|^2)^2
proof
assume that
A1: Z c= dom ((f1+f2)/(f1-f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & (f1-f2).x<>0;
A4: for x st x in Z holds f1.x=a^2 by A3;
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,A4,FDIFF_4:17;
A8: Z c= dom (f1-f2) by A5,XBOOLE_1:1;
then
A9: f1-f2 is_differentiable_on Z by A2,A4,Th3;
A10: for x st x in Z holds (f1-f2).x <> 0 by A3;
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^2*x/(a^2-x|^2)^2
proof
let x;
A12: f2.x=x #Z 2 by A2,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
assume
A13: x in Z;
then
A14: (f1-f2).x<>0 by A3;
A15: (f1-f2).x=f1.x-f2.x by A8,A13,VALUED_1:13
.=a^2-x |^2 by A3,A13,A12;
A16: (f1+f2).x=f1.x+f2.x by A6,A13,VALUED_1:def 1
.=a^2+x |^2 by A3,A13,A12;
f1+f2 is_differentiable_in x & f1-f2 is_differentiable_in x by A7,A9,A13,
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
.=(((f1+f2)`|Z).x * (f1-f2).x-diff(f1-f2,x) * (f1+f2).x)/((f1-f2).x)^2
by A7,A13,FDIFF_1:def 7
.= (((f1+f2)`|Z).x * (f1-f2).x-((f1-f2)`|Z).x * (f1+f2).x)/((f1-f2).x)
^2 by A9,A13,FDIFF_1:def 7
.=((2*x)*(f1-f2).x-((f1-f2)`|Z).x * (f1+f2).x)/((f1-f2).x)^2 by A2,A6,A4
,A13,FDIFF_4:17
.=((2*x)*(f1-f2).x-(-2*x) * (f1+f2).x)/((f1-f2).x)^2 by A2,A8,A4,A13,Th3
.=4*a^2*x/(a^2-x|^2)^2 by A16,A15;
hence thesis by A11,A13,FDIFF_1:def 7;
end;
hence thesis by A7,A9,A10,FDIFF_2:21;
end;
:: 3 f.x=ln((a^2+x^2)/(a^2-x^2))
theorem Th5:
Z c= dom f & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z
holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies f is_differentiable_on Z & for x
st x in Z holds (f`|Z).x =4*a^2*x/(a|^4-x|^4)
proof
assume that
A1: Z c= dom f and
A2: f=ln*((f1+f2)/(f1-f2)) and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0;
for y being object
st y in Z holds y in dom ((f1+f2)/(f1-f2)) by A1,A2,FUNCT_1:11;
then
A5: Z c= dom ((f1+f2)/(f1-f2)) by TARSKI:def 3;
then
A6: Z c=dom (f1+f2) /\ (dom (f1-f2) \ (f1-f2)"{0}) by RFUNCT_1:def 1;
then
A7: Z c= dom (f1-f2) by XBOOLE_1:1;
A8: for x st x in Z holds f1.x=a^2 & (f1-f2).x<>0 by A4;
then
A9: (f1+f2)/(f1-f2) is_differentiable_on Z by A3,A5,Th4;
A10: Z c= dom (f1+f2) by A6,XBOOLE_1:18;
A11: for x st x in Z holds ((f1+f2)/(f1-f2)).x >0
proof
let x;
A12: f2.x=x #Z 2 by A3,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
assume
A13: x in Z;
then
A14: (f1-f2).x>0 by A4;
a<>0 by A4,A13;
then
A15: a^2>0 by SQUARE_1:12;
x |^2 = x^2 by NEWTON:81;
then
A16: a^2+x |^2>0+0 by A15,XREAL_1:8,63;
A17: ((f1+f2)/(f1-f2)).x =(f1+f2).x * ((f1-f2).x)" by A5,A13,RFUNCT_1:def 1
.=(f1+f2).x / (f1-f2).x by XCMPLX_0:def 9;
(f1+f2).x=f1.x+f2.x by A10,A13,VALUED_1:def 1
.=a^2+x |^2 by A4,A13,A12;
hence thesis by A14,A16,A17,XREAL_1:139;
end;
A18: 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 A9
,A11,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A19: f is_differentiable_on Z by A1,A2,FDIFF_1:9;
for x st x in Z holds (f`|Z).x = 4*a^2*x/(a|^4-x|^4)
proof
let x;
A20: (a^2)^2=(a|^2)*(a^2) by NEWTON:81
.=(a|^2)*(a|^2) by NEWTON:81
.=(a|^2)|^2 by WSIERP_1:1
.=a|^(2*2) by NEWTON:9
.=a|^4;
A21: (x |^2)^2=(x |^2)|^2 by WSIERP_1:1
.=x|^(2*2) by NEWTON:9
.=x|^4;
A22: f2.x=x #Z 2 by A3,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
assume
A23: x in Z;
then
A24: (f1+f2).x=f1.x+f2.x by A10,VALUED_1:def 1
.=a^2+x |^2 by A4,A23,A22;
A25: (f1-f2).x=f1.x-f2.x by A7,A23,VALUED_1:13
.=a^2-x |^2 by A4,A23,A22;
then
A26: a^2-x |^2>0 by A4,A23;
A27: ((f1+f2)/(f1-f2)).x =(f1+f2).x * ((f1-f2).x)" by A5,A23,RFUNCT_1:def 1
.=(a^2+x |^2)/(a^2-x |^2) by A24,A25,XCMPLX_0:def 9;
(f1+f2)/(f1-f2) is_differentiable_in x & ((f1+f2)/(f1-f2)).x >0 by A9,A11
,A23,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 A9,A23,FDIFF_1:def 7
.= (4*a^2*x/(a^2-x|^2)^2)/((a^2+x |^2)/(a^2-x |^2)) by A3,A5,A8,A23,A27
,Th4
.=(4*a^2*x/(a^2-x|^2)/(a^2-x|^2))/((a^2+x |^2)/(a^2-x |^2)) by
XCMPLX_1:78
.=(4*a^2*x/(a^2-x|^2))/((a^2+x |^2)/(a^2-x |^2))/(a^2-x|^2) by
XCMPLX_1:48
.=(4*a^2*x)/(a^2+x |^2)/(a^2-x|^2) by A26,XCMPLX_1:55
.=(4*a^2*x)/((a^2+x |^2)*(a^2-x|^2)) by XCMPLX_1:78
.=4*a^2*x/(a|^4-x|^4) by A20,A21;
hence thesis by A2,A19,A23,FDIFF_1:def 7;
end;
hence thesis by A1,A2,A18,FDIFF_1:9;
end;
:: 4 f.x=(1/(4*a^2))*ln((a^2+x^2)/(a^2-x^2))
theorem
Z c= dom ((1/(4*a^2))(#)f) & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x
st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies (1/(4*a^2))(#)f
is_differentiable_on Z & for x st x in Z holds (((1/(4*a^2))(#)f)`|Z).x =x/(a|^
4-x|^4)
proof
assume that
A1: Z c= dom ((1/(4*a^2))(#)f) and
A2: f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0;
A4: Z c= dom f by A1,VALUED_1:def 5;
then
A5: f is_differentiable_on Z by A2,A3,Th5;
for x st x in Z holds (((1/(4*a^2))(#)f)`|Z).x =x/(a|^4-x|^4)
proof
let x;
assume
A6: x in Z;
then a<>0 by A3;
then a^2>0 by SQUARE_1:12;
then
A7: 4*a^2>4*0 by XREAL_1:68;
(((1/(4*a^2))(#)f)`|Z).x =(1/(4*a^2))*diff(f,x) by A1,A5,A6,FDIFF_1:20
.=(1/(4*a^2))*(f`|Z).x by A5,A6,FDIFF_1:def 7
.=(1/(4*a^2))*(4*a^2*x/(a|^4-x|^4)) by A2,A3,A4,A6,Th5
.=(1/(4*a^2))*((4*a^2)*(x/(a|^4-x|^4))) by XCMPLX_1:74
.=(x/(a|^4-x|^4))*(1/(4*a^2)*(4*a^2))
.=x/(a|^4-x|^4) by A7,XCMPLX_1:108;
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:20;
end;
:: 5 f.x=x^2/(1+x^2)
theorem Th7:
Z c= dom (f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z holds f2.x=1 &
x<>0) implies f1/(f2+f1) is_differentiable_on Z & for x st x in Z holds ((f1/(
f2+f1))`|Z).x =2*x/(1+x^2)^2
proof
assume that
A1: Z c= dom (f1/(f2+f1)) and
A2: f1=#Z 2 and
A3: for x st x in Z holds f2.x=1 & x<>0;
A4: Z c= dom f1 /\ (dom (f2+f1) \ (f2+f1)"{0}) by A1,RFUNCT_1:def 1;
then
A5: Z c= dom (f2+f1) by XBOOLE_1:1;
A6: for x st x in Z holds f1 is_differentiable_in x by A2,TAYLOR_1:2;
Z c= dom f1 by A4,XBOOLE_1:18;
then
A7: f1 is_differentiable_on Z by A6,FDIFF_1:9;
A8: for x st x in Z holds (f1`|Z).x=2*x
proof
let x;
2 * (x #Z (2-1))=2 * x by PREPOWER:35;
then
A9: diff(f1,x) =2 * x by A2,TAYLOR_1:2;
assume x in Z;
hence thesis by A7,A9,FDIFF_1:def 7;
end;
A10: for x st x in Z holds f2.x=1^2 by A3;
then
A11: f2+f1 is_differentiable_on Z by A2,A5,FDIFF_4:17;
A12: for x st x in Z holds (f2+f1).x <> 0
proof
let x;
A13: 1+x^2>0+0 by XREAL_1:8,63;
assume
A14: x in Z;
then (f2+f1).x=f2.x+f1.x by A5,VALUED_1:def 1
.=1+f1.x by A3,A14
.=1+x #Z 2 by A2,TAYLOR_1:def 1
.=1+x |^2 by PREPOWER:36
.=1+x^2 by NEWTON:81;
hence thesis by A13;
end;
then
A15: f1/(f2+f1) is_differentiable_on Z by A11,A7,FDIFF_2:21;
for x st x in Z holds ((f1/(f2+f1))`|Z).x =2*x/(1+x^2)^2
proof
let x;
A16: f1 is_differentiable_in x by A2,TAYLOR_1:2;
A17: f1.x=x #Z 2 by A2,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36
.=x^2 by NEWTON:81;
assume
A18: x in Z;
then
A19: (f2+f1).x=f2.x+f1.x by A5,VALUED_1:def 1
.=1+f1.x by A3,A18
.=1+x #Z 2 by A2,TAYLOR_1:def 1
.=1+x |^2 by PREPOWER:36
.=1+x^2 by NEWTON:81;
f2+f1 is_differentiable_in x & (f2+f1).x<>0 by A11,A12,A18,FDIFF_1:9;
then
diff(f1/(f2+f1),x) =(diff(f1,x)*(f2+f1).x - diff(f2+f1,x)*f1.x)/((f2+
f1).x)^2 by A16,FDIFF_2:14
.=((f1`|Z).x * (f2+f1).x-diff(f2+f1,x) * f1.x)/((f2+f1).x)^2 by A7,A18,
FDIFF_1:def 7
.= ((f1`|Z).x * (f2+f1).x-((f2+f1)`|Z).x * f1.x)/((f2+f1).x)^2 by A11,A18
,FDIFF_1:def 7
.=((2*x)*(f2+f1).x-((f2+f1)`|Z).x * f1.x)/((f2+f1).x)^2 by A8,A18
.=((2*x)*(1+x^2)-(2*x)*x^2)/(1+x^2)^2 by A2,A10,A5,A18,A17,A19,FDIFF_4:17
.=2*x/(1+x^2)^2;
hence thesis by A15,A18,FDIFF_1:def 7;
end;
hence thesis by A11,A7,A12,FDIFF_2:21;
end;
:: 6 f.x=(1/2)*ln(x^2/(1+x^2))
theorem
Z c= dom ((1/2)(#)f) & f=ln*(f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z
holds f2.x=1 & x<>0) implies (1/2)(#)f is_differentiable_on Z & for x st x in Z
holds (((1/2)(#)f)`|Z).x =1/(x*(1+x^2))
proof
assume that
A1: Z c= dom ((1/2)(#)f) and
A2: f=ln*(f1/(f2+f1)) and
A3: f1=#Z 2 and
A4: for x st x in Z holds f2.x=1 & x<>0;
A5: Z c= dom f by A1,VALUED_1:def 5;
then for y being object
st y in Z holds y in dom (f1/(f2+f1)) by A2,FUNCT_1:11;
then
A6: Z c= dom (f1/(f2+f1)) by TARSKI:def 3;
then
A7: f1/(f2+f1) is_differentiable_on Z by A3,A4,Th7;
Z c= dom f1 /\ (dom (f2+f1) \ (f2+f1)"{0}) by A6,RFUNCT_1:def 1;
then
A8: Z c= dom (f2+f1) by XBOOLE_1:1;
A9: for x st x in Z holds (f1/(f1+f2)).x >0
proof
let x;
assume
A10: x in Z;
then
A11: (f1/(f2+f1)).x=f1.x * ((f2+f1).x)" by A6,RFUNCT_1:def 1
.=f1.x/(f2+f1).x by XCMPLX_0:def 9;
A12: x<>0 by A4,A10;
then
A13: 1+x^2>0+0 by SQUARE_1:12,XREAL_1:8;
A14: f1.x=x #Z 2 by A3,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36
.=x^2 by NEWTON:81;
then
A15: f1.x>0 by A12,SQUARE_1:12;
(f2+f1).x=f2.x+f1.x by A8,A10,VALUED_1:def 1
.=1+x^2 by A4,A10,A14;
hence thesis by A15,A13,A11,XREAL_1:139;
end;
for x st x in Z holds ln*(f1/(f2+f1)) is_differentiable_in x
proof
let x;
assume x in Z;
then f1/(f2+f1) is_differentiable_in x & (f1/(f1+f2)).x >0 by A7,A9,
FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A16: f is_differentiable_on Z by A2,A5,FDIFF_1:9;
for x st x in Z holds (((1/2)(#)f)`|Z).x =1/(x*(1+x^2))
proof
let x;
A17: f1.x=x #Z 2 by A3,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36
.=x^2 by NEWTON:81;
assume
A18: x in Z;
then
A19: f1/(f2+f1) is_differentiable_in x & (f1/(f1+f2)).x >0 by A7,A9,FDIFF_1:9;
x<>0 by A4,A18;
then
A20: 1+x^2>0+0 by SQUARE_1:12,XREAL_1:8;
A21: (f2+f1).x=f2.x+f1.x by A8,A18,VALUED_1:def 1
.=1+x^2 by A4,A18,A17;
A22: (f1/(f2+f1)).x=f1.x * ((f2+f1).x)" by A6,A18,RFUNCT_1:def 1
.=x^2/(1+x^2) by A17,A21,XCMPLX_0:def 9;
(((1/2)(#)f)`|Z).x =(1/2)*diff(ln*(f1/(f2+f1)),x) by A1,A2,A16,A18,
FDIFF_1:20
.=(1/2)*(diff((f1/(f2+f1)),x)/(f1/(f2+f1)).x) by A19,TAYLOR_1:20
.=(1/2)*(((f1/(f2+f1))`|Z).x/(f1/(f2+f1)).x) by A7,A18,FDIFF_1:def 7
.=(1/2)*((2*x/(1+x^2)^2)/(x^2/(1+x^2))) by A3,A4,A6,A18,A22,Th7
.=(1/2)*((2*x)/(1+x^2)^2)/(x^2/(1+x^2)) by XCMPLX_1:74
.=((1/2)*(2*x))/(1+x^2)^2/(x^2/(1+x^2)) by XCMPLX_1:74
.=x/(1+x^2)/(1+x^2)/(x^2/(1+x^2)) by XCMPLX_1:78
.=x/(1+x^2)/(x^2/(1+x^2))/(1+x^2) by XCMPLX_1:48
.=x/x^2/(1+x^2) by A20,XCMPLX_1:55
.=x/x/x/(1+x^2) by XCMPLX_1:78
.=1/x/(1+x^2) by A4,A18,XCMPLX_1:60
.=1/(x*(1+x^2)) by XCMPLX_1:78;
hence thesis;
end;
hence thesis by A1,A16,FDIFF_1:20;
end;
:: 7 f.x=ln(x^n)
theorem
Z c= dom (ln*( #Z n)) & (for x st x in Z holds x>0) implies ln*( #Z n)
is_differentiable_on Z & for x st x in Z holds ((ln*( #Z n))`|Z).x =n/x
proof
assume that
A1: Z c= dom (ln*( #Z n)) and
A2: for x st x in Z holds x > 0;
A3: for x st x in Z holds ln*( #Z n) is_differentiable_in x
proof
let x;
A4: #Z n.x=x #Z n by TAYLOR_1:def 1;
assume x in Z;
then #Z n is_differentiable_in x & #Z n.x>0 by A2,A4,PREPOWER:39,TAYLOR_1:2
;
hence thesis by TAYLOR_1:20;
end;
then
A5: ln*( #Z n) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*( #Z n))`|Z).x =n/x
proof
let x;
A6: #Z n is_differentiable_in x & diff(( #Z n),x) = n * x #Z (n-1) by
TAYLOR_1:2;
assume
A7: x in Z;
then
A8: x>0 by A2;
A9: x |^n >0 by A2,A7,NEWTON:83;
A10: #Z n.x=x #Z n by TAYLOR_1:def 1;
then #Z n.x>0 by A2,A7,PREPOWER:39;
then diff(ln*( #Z n),x) = n * x #Z (n-1)/x #Z n by A6,A10,TAYLOR_1:20
.=n * x #Z (n-1)/x |^ n by PREPOWER:36
.=n * (x |^ n/x |^ 1)/x |^ n by A8,PREPOWER:43
.=n * (x |^ n/x |^ 1/x |^ n) by XCMPLX_1:74
.=n * (x |^ n/x |^ n/x |^ 1) by XCMPLX_1:48
.=n * (1/(x |^ 1)) by A9,XCMPLX_1:60
.=n * (1/x)
.=n*1/x by XCMPLX_1:74
.=n/x;
hence thesis by A5,A7,FDIFF_1:def 7;
end;
hence thesis by A1,A3,FDIFF_1:9;
end;
:: 8 f.x=1/x+ln((x-1)/x)
theorem
Z c= dom (f2^+ln*(f1/f2)) & (for x st x in Z holds f2.x = x & f2.x>0 &
f1.x=x-1 & f1.x >0 ) implies f2^+ln*(f1/f2) is_differentiable_on Z & for x st x
in Z holds ( (f2^+ln*(f1/f2))`|Z).x= 1/(x^2*(x-1))
proof
assume that
A1: Z c= dom (f2^+ln*(f1/f2)) and
A2: for x st x in Z holds f2.x = x & f2.x>0 & f1.x=x-1 & f1.x >0;
A3: Z c= dom (f2^) /\ dom (ln*(f1/f2)) by A1,VALUED_1:def 1;
then
A4: Z c=dom (ln*(f1/f2)) by XBOOLE_1:18;
A5: dom (f2^) c= dom f2 by RFUNCT_1:1;
Z c= dom (f2^) by A3,XBOOLE_1:18;
then
A6: Z c= dom f2 by A5,XBOOLE_1:1;
A7: for x st x in Z holds f1.x=x-1 & f1.x >0 & f2.x = x-0 & f2.x>0 by A2;
then
A8: ln*(f1/f2) is_differentiable_on Z by A4,FDIFF_4:24;
A9: for x st x in Z holds f2.x = 0+x & f2.x<>0 by A2;
then
A10: f2^ is_differentiable_on Z by A6,FDIFF_4:14;
for x st x in Z holds ((f2^+ln*(f1/f2))`|Z).x= 1/(x^2*(x-1))
proof
let x;
assume
A11: x in Z;
then
A12: f2.x = x & f2.x>0 by A2;
A13: f1.x=x-1 & f1.x >0 by A2,A11;
((f2^+ln*(f1/f2))`|Z).x =diff(f2^,x) + diff(ln*(f1/f2),x) by A1,A10,A8,A11,
FDIFF_1:18
.=((f2^)`|Z).x+ diff(ln*(f1/f2),x) by A10,A11,FDIFF_1:def 7
.=((f2^)`|Z).x+((ln*(f1/f2))`|Z).x by A8,A11,FDIFF_1:def 7
.= -1/(0+x)^2+((ln*(f1/f2))`|Z).x by A6,A9,A11,FDIFF_4:14
.=-1/(0+x)^2+(1-0)/((x-1)*(x-0)) by A4,A7,A11,FDIFF_4:24
.=-(1*(x-1))/(x^2*(x-1))+1/((x-1)*x) by A13,XCMPLX_1:91
.=-(1*(x-1))/(x^2*(x-1))+(1*x)/((x-1)*x*x) by A12,XCMPLX_1:91
.=(-(x-1))/(x^2*(x-1))+x/(x^2*(x-1)) by XCMPLX_1:187
.=((-x+1)+x)/(x^2*(x-1)) by XCMPLX_1:62
.=1/(x^2*(x-1));
hence thesis;
end;
hence thesis by A1,A10,A8,FDIFF_1:18;
end;
:: 10 f.x=a ^ x=exp.(x*ln a)
theorem Th11:
Z c= dom (exp_R*f) & (for x st x in Z holds f.x=x*log(number_e,a
)) & a>0 implies exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R
*f)`|Z).x =a #R x*log(number_e,a)
proof
assume that
A1: Z c= dom (exp_R*f) and
A2: for x st x in Z holds f.x=x*log(number_e,a) and
A3: a>0;
for y being object
st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x = log(number_e,a)*x+0 by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds exp_R*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x by A6,FDIFF_1:9;
hence thesis by TAYLOR_1:19;
end;
then
A8: exp_R*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*f)`|Z).x = a #R x*log(number_e,a)
proof
let x;
assume
A9: x in Z;
then f is_differentiable_in x by A6,FDIFF_1:9;
then diff(exp_R*f,x) = exp_R.(f.x)*diff(f,x) by TAYLOR_1:19
.=exp_R.(f.x)*(f`|Z).x by A6,A9,FDIFF_1:def 7
.=exp_R.(f.x)*(log(number_e,a)) by A4,A5,A9,FDIFF_1:23
.=exp_R.(x*log(number_e,a))*(log(number_e,a)) by A2,A9
.=a #R x*log(number_e,a) by A3,Th1;
hence thesis by A8,A9,FDIFF_1:def 7;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 11 f.x=(a ^ x)*(x-1/ln a)/ln a
theorem
Z c= dom ((1/log(number_e,a))(#)((exp_R*f1)(#)f2)) & (for x st x in Z
holds f1.x=x*log(number_e,a) & f2.x=x-1/log(number_e,a)) & a>0 & a<>1 implies (
1/log(number_e,a))(#)((exp_R*f1)(#)f2) is_differentiable_on Z & for x st x in Z
holds (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =x * a #R x
proof
assume that
A1: Z c= dom ((1/log(number_e,a))(#)((exp_R*f1)(#)f2)) and
A2: for x st x in Z holds f1.x=x*log(number_e,a) & f2.x=x-1/log(
number_e,a) and
A3: a>0 and
A4: a<>1;
A5: Z c= dom ((exp_R*f1)(#)f2) by A1,VALUED_1:def 5;
then
A6: Z c= dom (exp_R*f1) /\ dom f2 by VALUED_1:def 4;
then
A7: Z c= dom (exp_R*f1) by XBOOLE_1:18;
A8: for x st x in Z holds f2.x = 1*x+-1/log(number_e,a)
proof
let x;
A9: 1*x+-1/log(number_e,a)=1*x-1/log(number_e,a);
assume x in Z;
hence thesis by A2,A9;
end;
A10: for x st x in Z holds f1.x=x*log(number_e,a) by A2;
then
A11: exp_R*f1 is_differentiable_on Z by A3,A7,Th11;
A12: Z c= dom f2 by A6,XBOOLE_1:18;
then
A13: f2 is_differentiable_on Z by A8,FDIFF_1:23;
then
A14: ((exp_R*f1)(#)f2) is_differentiable_on Z by A5,A11,FDIFF_1:21;
A15: log(number_e,a)<>0
proof
A16: number_e<>1 by TAYLOR_1:11;
assume log(number_e,a)=0;
then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13;
then a=(number_e) to_power log(number_e,1) by A3,A16,POWER:def 3
,TAYLOR_1:11
.=1 by A16,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4;
end;
for x st x in Z holds (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x
=x * a #R x
proof
let x;
assume
A17: x in Z;
then
A18: (exp_R*f1).x=exp_R.(f1.x) by A7,FUNCT_1:12
.=exp_R.(x*log(number_e,a)) by A2,A17
.=a #R x by A3,Th1;
(((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =(1/log(number_e,a))
*diff((exp_R*f1)(#)f2,x) by A1,A14,A17,FDIFF_1:20
.=(1/log(number_e,a))*(((exp_R*f1)(#)f2)`|Z).x by A14,A17,FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*diff(exp_R*f1,x)+(exp_R*f1).x*diff(f2,x))
by A5,A11,A13,A17,FDIFF_1:21
.=(1/log(number_e,a))*(f2.x*((exp_R*f1)`|Z).x+(exp_R*f1).x*diff(f2,x))
by A11,A17,FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*((exp_R*f1)`|Z).x+(exp_R*f1).x*(f2`|Z).x)
by A13,A17,FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*(a #R x*log(number_e,a)) +(exp_R*f1).x*(f2
`|Z).x) by A3,A10,A7,A17,Th11
.=(1/log(number_e,a))*(f2.x*(a#R x*log(number_e,a))+(exp_R*f1).x*1) by
A12,A8,A17,FDIFF_1:23
.=(1/log(number_e,a))*((f2.x*log(number_e,a)+1)*a #R x) by A18
.=(1/log(number_e,a))*(((x-1/log(number_e,a))* log(number_e,a)+1)*a #R
x) by A2,A17
.=(1/log(number_e,a))*(x*log(number_e,a) -1/log(number_e,a)*log(
number_e,a)+1)*a #R x
.=(1/log(number_e,a))*(x*log(number_e,a)-1+1)*a #R x by A15,XCMPLX_1:106
.=1/log(number_e,a)*log(number_e,a)*x*a #R x
.=1*x*a #R x by A15,XCMPLX_1:106
.=x*a #R x;
hence thesis;
end;
hence thesis by A1,A14,FDIFF_1:20;
end;
:: 12 f.x=a ^ x*exp(x)/(1+ln a)
theorem
Z c= dom ((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) & (for x st x
in Z holds f.x=x*log(number_e,a)) & a>0 & a<>1/number_e implies (1/(1+log(
number_e,a)))(#)((exp_R*f)(#)exp_R) is_differentiable_on Z & for x st x in Z
holds (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))`|Z).x =a #R x*exp_R.x
proof
assume that
A1: Z c= dom ((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) and
A2: for x st x in Z holds f.x=x*log(number_e,a) and
A3: a>0 and
A4: a<>1/number_e;
A5: Z c= dom ((exp_R*f)(#)exp_R) by A1,VALUED_1:def 5;
then Z c= dom (exp_R*f) /\ dom exp_R by VALUED_1:def 4;
then
A6: Z c= dom (exp_R*f) by XBOOLE_1:18;
then
A7: exp_R*f is_differentiable_on Z by A2,A3,Th11;
A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A9: (exp_R*f)(#)exp_R is_differentiable_on Z by A5,A7,FDIFF_1:21;
A10: 1+log(number_e,a)<>0
proof
A11: number_e*a>0*a by A3,TAYLOR_1:11,XREAL_1:68;
assume
A12: 1+log(number_e,a)=0;
A13: number_e<>1 by TAYLOR_1:11;
log(number_e,1)=0 by SIN_COS2:13,TAYLOR_1:13
.=log(number_e,number_e)+log(number_e,a) by A12,A13,POWER:52,TAYLOR_1:11
.=log(number_e,number_e*a) by A3,A13,POWER:53,TAYLOR_1:11;
then number_e*a=(number_e) to_power log(number_e,1) by A13,A11,POWER:def 3
,TAYLOR_1:11
.=1 by A13,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4,XCMPLX_1:73;
end;
for x st x in Z holds (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))
`|Z).x =a #R x*exp_R.x
proof
let x;
assume
A14: x in Z;
then
A15: (exp_R*f).x=exp_R.(f.x) by A6,FUNCT_1:12
.=exp_R.(x*log(number_e,a)) by A2,A14
.=a #R x by A3,Th1;
(((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))`|Z).x =(1/(1+log(
number_e,a)))*diff((exp_R*f)(#)exp_R,x) by A1,A9,A14,FDIFF_1:20
.=(1/(1+log(number_e,a)))*(((exp_R*f)(#)exp_R)`|Z).x by A9,A14,
FDIFF_1:def 7
.=(1/(1+log(number_e,a)))*(exp_R.x*diff(exp_R*f,x)+ (exp_R*f).x*diff(
exp_R,x)) by A5,A7,A8,A14,FDIFF_1:21
.=(1/(1+log(number_e,a)))*(exp_R.x*((exp_R*f)`|Z).x+ (exp_R*f).x*diff(
exp_R,x)) by A7,A14,FDIFF_1:def 7
.=(1/(1+log(number_e,a)))*(exp_R.x*((exp_R*f)`|Z).x+(exp_R*f).x*exp_R.
x) by TAYLOR_1:16
.=(1/(1+log(number_e,a)))*((((exp_R*f)`|Z).x+(exp_R*f).x)*exp_R.x)
.=(1/(1+log(number_e,a)))*((a #R x*log(number_e,a)+(exp_R*f).x)*exp_R.
x) by A2,A3,A6,A14,Th11
.=(1/(1+log(number_e,a)))*(log(number_e,a)+1)*a #R x*exp_R.x by A15
.=1*a #R x*exp_R.x by A10,XCMPLX_1:106
.=a #R x*exp_R.x;
hence thesis;
end;
hence thesis by A1,A9,FDIFF_1:20;
end;
:: 13 f.x=exp_R(-x)
theorem Th14:
Z c= dom (exp_R*f) & (for x st x in Z holds f.x=-x) implies
exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R*f)`|Z).x = -
exp_R(-x)
proof
assume that
A1: Z c= dom (exp_R*f) and
A2: for x st x in Z holds f.x=-x;
A3: for x st x in Z holds f.x=(-1)*x+0
proof
let x;
assume x in Z;
then f.x=-x by A2
.=(-1)*x+0;
hence thesis;
end;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom f by TARSKI:def 3;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds exp_R*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x by A5,FDIFF_1:9;
hence thesis by TAYLOR_1:19;
end;
then
A7: exp_R*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((exp_R*f)`|Z).x = -exp_R(-x)
proof
let x;
assume
A8: x in Z;
then f is_differentiable_in x by A5,FDIFF_1:9;
then diff(exp_R*f,x) = exp_R.(f.x)*diff(f,x) by TAYLOR_1:19
.=exp_R.(f.x)*(f`|Z).x by A5,A8,FDIFF_1:def 7
.=exp_R.(f.x)*(-1) by A4,A3,A8,FDIFF_1:23
.=exp_R.(-x)*(-1) by A2,A8
.=-exp_R.(-x)
.=-exp_R(-x) by SIN_COS:def 23;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: 14 f.x=-(x+1)*exp_R(-x)
theorem
Z c= dom (f1(#)(exp_R*f2)) & (for x st x in Z holds f1.x=-x-1 & f2.x=-
x) implies f1(#)(exp_R*f2) is_differentiable_on Z & for x st x in Z holds ((f1
(#)(exp_R*f2))`|Z).x = x/exp_R(x)
proof
assume that
A1: Z c= dom (f1(#)(exp_R*f2)) and
A2: for x st x in Z holds f1.x=-x-1 & f2.x=-x;
A3: Z c= dom f1 /\ dom (exp_R*f2) by A1,VALUED_1:def 4;
then
A4: Z c= dom f1 by XBOOLE_1:18;
A5: Z c= dom (exp_R*f2) by A3,XBOOLE_1:18;
A6: for x st x in Z holds f1.x=(-1)*x+-1
proof
let x;
assume x in Z;
then f1.x=-x-1 by A2
.=(-1)*x+-1;
hence thesis;
end;
then
A7: f1 is_differentiable_on Z by A4,FDIFF_1:23;
A8: for x st x in Z holds f2.x=-x by A2;
then
A9: exp_R*f2 is_differentiable_on Z by A5,Th14;
for x st x in Z holds ((f1(#)(exp_R*f2))`|Z).x = x/exp_R(x)
proof
let x;
assume
A10: x in Z;
then
A11: (exp_R*f2).x=exp_R.(f2.x) by A5,FUNCT_1:12
.=exp_R.(-x) by A2,A10
.=exp_R(-x) by SIN_COS:def 23;
((f1(#)(exp_R*f2))`|Z).x =((exp_R*f2).x)*diff(f1,x) + (f1.x)*diff(
exp_R*f2,x) by A1,A7,A9,A10,FDIFF_1:21
.=exp_R(-x)*diff(f1,x) + (-x-1)*diff(exp_R*f2,x) by A2,A10,A11
.=exp_R(-x)*(f1`|Z).x + (-x-1)*diff(exp_R*f2,x) by A7,A10,FDIFF_1:def 7
.=exp_R(-x)*(f1`|Z).x + (-x-1)*((exp_R*f2)`|Z).x by A9,A10,FDIFF_1:def 7
.=exp_R(-x)*(-1) + (-x-1)*((exp_R*f2)`|Z).x by A4,A6,A10,FDIFF_1:23
.=exp_R(-x)*(-1) + (-x-1)*(-exp_R(-x)) by A8,A5,A10,Th14
.=x*exp_R(-x)
.=x*(1/exp_R(x)) by TAYLOR_1:4
.=x/exp_R(x) by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A7,A9,FDIFF_1:21;
end;
:: 16 f.x=a ^ (-x)=exp_R.(-x*ln a)
theorem Th16:
Z c= dom -(exp_R*f) & (for x st x in Z holds f.x=-x*log(number_e
,a)) & a>0 implies -(exp_R*f) is_differentiable_on Z & for x st x in Z holds ((
-(exp_R*f))`|Z).x =a #R (-x)*log(number_e,a)
proof
assume that
A1: Z c= dom -(exp_R*f) and
A2: for x st x in Z holds f.x=-x*log(number_e,a) and
A3: a>0;
A4: Z c= dom (exp_R*f) by A1,VALUED_1:8;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A5: Z c= dom f by TARSKI:def 3;
A6: for x st x in Z holds f.x = (-log(number_e,a))*x+0
proof
let x;
assume x in Z;
then f.x=-log(number_e,a)*x by A2
.=(-log(number_e,a))*x+0;
hence thesis;
end;
then
A7: f is_differentiable_on Z by A5,FDIFF_1:23;
for x st x in Z holds exp_R*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x by A7,FDIFF_1:9;
hence thesis by TAYLOR_1:19;
end;
then
A8: exp_R*f is_differentiable_on Z by A4,FDIFF_1:9;
A9: for x st x in Z holds ((-(exp_R*f))`|Z).x = a #R (-x)*log(number_e,a)
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x by A7,FDIFF_1:9;
((-(exp_R*f))`|Z).x=(-1)*diff(exp_R*f,x) by A1,A8,A10,FDIFF_1:20
.=(-1)*(exp_R.(f.x)*diff(f,x)) by A11,TAYLOR_1:19
.=(-1)*(exp_R.(f.x)*(f`|Z).x ) by A7,A10,FDIFF_1:def 7
.=(-1)*(exp_R.(f.x)*(-log(number_e,a))) by A5,A6,A10,FDIFF_1:23
.=(-1)*(exp_R.(-x*log(number_e,a))*(-log(number_e,a))) by A2,A10
.=(-1)*(a #R (-x)*(-log(number_e,a))) by A3,Th2
.=a #R (-x)*log(number_e,a);
hence thesis;
end;
Z c= dom ((-1)(#)(exp_R*f)) by A1;
hence thesis by A8,A9,FDIFF_1:20;
end;
:: 17 f.x=-(a ^ -x)*(x+1/ln a)/ln a
theorem
Z c= dom ((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2)) & (for x st x in
Z holds f1.x=-x*log(number_e,a) & f2.x=x+1/log(number_e,a)) & a>0 & a<>1
implies (1/log(number_e,a))(#)((-(exp_R*f1))(#)f2) is_differentiable_on Z & for
x st x in Z holds (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z).x =x /a #R
x
proof
assume that
A1: Z c= dom ((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2)) and
A2: for x st x in Z holds f1.x=-x*log(number_e,a) & f2.x=x+1/log(
number_e,a) and
A3: a>0 and
A4: a<>1;
A5: for x st x in Z holds f2.x = 1*x+1/log(number_e,a) by A2;
A6: Z c= dom ((-(exp_R*f1))(#)f2) by A1,VALUED_1:def 5;
then
A7: Z c= dom (-(exp_R*f1)) /\ dom f2 by VALUED_1:def 4;
then
A8: Z c= dom (-(exp_R*f1)) by XBOOLE_1:18;
A9: for x st x in Z holds f1.x=-x*log(number_e,a) by A2;
then
A10: -(exp_R*f1) is_differentiable_on Z by A3,A8,Th16;
A11: Z c= dom f2 by A7,XBOOLE_1:18;
then
A12: f2 is_differentiable_on Z by A5,FDIFF_1:23;
then
A13: (-(exp_R*f1))(#)f2 is_differentiable_on Z by A6,A10,FDIFF_1:21;
A14: log(number_e,a)<>0
proof
A15: number_e<>1 by TAYLOR_1:11;
assume log(number_e,a)=0;
then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13;
then a=(number_e) to_power log(number_e,1) by A3,A15,POWER:def 3
,TAYLOR_1:11
.=1 by A15,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4;
end;
for x st x in Z holds (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z)
.x =x /a #R x
proof
let x;
assume
A16: x in Z;
then x in dom -(exp_R*f1) by A8;
then
A17: x in dom (exp_R*f1) by VALUED_1:8;
A18: (-(exp_R*f1)).x=-((exp_R*f1).x) by VALUED_1:8
.=-(exp_R.(f1.x)) by A17,FUNCT_1:12
.=-(exp_R.(-x*log(number_e,a))) by A2,A16
.=-a #R (-x) by A3,Th2;
(((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z).x =(1/log(number_e,
a))*diff((-(exp_R*f1))(#)f2,x) by A1,A13,A16,FDIFF_1:20
.=(1/log(number_e,a))*(((-(exp_R*f1))(#)f2)`|Z).x by A13,A16,
FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*diff(-(exp_R*f1),x)+ (-(exp_R*f1)).x*diff(
f2,x)) by A6,A10,A12,A16,FDIFF_1:21
.=(1/log(number_e,a))*(f2.x*((-(exp_R*f1))`|Z).x+ (-(exp_R*f1)).x*diff
(f2,x)) by A10,A16,FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*((-(exp_R*f1))`|Z).x+ (-(exp_R*f1)).x*(f2
`|Z).x) by A12,A16,FDIFF_1:def 7
.=(1/log(number_e,a))*(f2.x*(a #R (-x)*log(number_e,a)) +(-(exp_R*f1))
.x*(f2`|Z).x) by A3,A9,A8,A16,Th16
.=(1/log(number_e,a))*(f2.x*(a #R (-x)*log(number_e,a)) +(-(exp_R*f1))
.x*1) by A11,A5,A16,FDIFF_1:23
.=(1/log(number_e,a))*((f2.x*log(number_e,a)-1)*a #R (-x)) by A18
.=(1/log(number_e,a))*(((x+1/log(number_e,a))* log(number_e,a)-1)*a #R
(-x)) by A2,A16
.=(1/log(number_e,a))* (x*log(number_e,a)+1/log(number_e,a)*log(
number_e,a)-1)*a #R (-x)
.=(1/log(number_e,a))*(x*log(number_e,a)+1-1)*a #R (-x) by A14,
XCMPLX_1:106
.=(1/log(number_e,a))*log(number_e,a)*x*a #R (-x)
.=1*x*a #R (-x) by A14,XCMPLX_1:106
.=x*(1/a #R x) by A3,PREPOWER:76
.=x/a #R x by XCMPLX_1:99;
hence thesis;
end;
hence thesis by A1,A13,FDIFF_1:20;
end;
:: 18 f.x=(1/(ln a-1))*a ^ x/exp_R(x)
theorem
Z c= dom ((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R)) & (for x st x
in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(log(number_e,
a)-1))(#)((exp_R*f)/exp_R) is_differentiable_on Z & for x st x in Z holds (((1/
(log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z).x =a #R x/exp_R.x
proof
assume that
A1: Z c= dom ((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R)) and
A2: for x st x in Z holds f.x=x*log(number_e,a) and
A3: a>0 and
A4: a<>number_e;
Z c= dom ((exp_R*f)/exp_R) by A1,VALUED_1:def 5;
then Z c= dom (exp_R*f) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A5: Z c= dom (exp_R*f) by XBOOLE_1:18;
then
A6: exp_R*f is_differentiable_on Z by A2,A3,Th11;
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: (exp_R*f)/exp_R is_differentiable_on Z by A6,FDIFF_2:21;
A8: log(number_e,a)-1<>0
proof
A9: number_e<>1 by TAYLOR_1:11;
assume log(number_e,a)-1=0;
then log(number_e,a)=log(number_e,number_e) by A9,POWER:52,TAYLOR_1:11;
then a=(number_e) to_power log(number_e,number_e) by A3,A9,POWER:def 3
,TAYLOR_1:11
.=number_e by A9,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4;
end;
for x st x in Z holds (((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z
).x =a #R x/exp_R.x
proof
let x;
A10: exp_R.x <>0 by SIN_COS:54;
assume
A11: x in Z;
then
A12: (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12
.=exp_R.(x*log(number_e,a)) by A2,A11
.=a #R x by A3,Th1;
A13: exp_R is_differentiable_in x & exp_R*f is_differentiable_in x by A6,A11,
FDIFF_1:9,SIN_COS:65;
(((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z).x =(1/(log(
number_e,a)-1))*diff(((exp_R*f)/exp_R),x) by A1,A7,A11,FDIFF_1:20
.=(1/(log(number_e,a)-1))* ((diff(exp_R*f,x) * exp_R.x - diff(exp_R,x)
*(exp_R*f).x)/(exp_R.x)^2) by A13,A10,FDIFF_2:14
.=(1/(log(number_e,a)-1))*((diff(exp_R*f,x)* exp_R.x-exp_R.x*a #R x)/(
exp_R.x)^2) by A12,SIN_COS:65
.=(1/(log(number_e,a)-1))*(((diff(exp_R*f,x)-a #R x)*exp_R.x)/ ((exp_R
.x)*(exp_R.x)))
.=(1/(log(number_e,a)-1))*((diff(exp_R*f,x)-a #R x)/(exp_R.x)) by A10,
XCMPLX_1:91
.=(1/(log(number_e,a)-1))*(diff(exp_R*f,x)-a #R x)/(exp_R.x) by
XCMPLX_1:74
.=(1/(log(number_e,a)-1))*(((exp_R*f)`|Z).x-a #R x)/(exp_R.x) by A6,A11,
FDIFF_1:def 7
.=(1/(log(number_e,a)-1))*(a #R x*log(number_e,a)-a #R x)/(exp_R.x) by A2
,A3,A5,A11,Th11
.=(1/(log(number_e,a)-1))*(log(number_e,a)-1)*a #R x/exp_R.x
.=1* a #R x/exp_R.x by A8,XCMPLX_1:106
.=a #R x/exp_R.x;
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 19 f.x=(1/(1-ln a))*exp_R(x)/a ^ x
theorem
Z c= dom ((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f))) & (for x st x
in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(1-log(
number_e,a)))(#)(exp_R/(exp_R*f)) is_differentiable_on Z & for x st x in Z
holds (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z).x =exp_R.x/a #R x
proof
assume that
A1: Z c= dom ((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f))) and
A2: for x st x in Z holds f.x=x*log(number_e,a) and
A3: a>0 and
A4: a<>number_e;
Z c= dom (exp_R/(exp_R*f)) by A1,VALUED_1:def 5;
then Z c= dom exp_R /\ (dom (exp_R*f) \ (exp_R*f)"{0}) by RFUNCT_1:def 1;
then
A5: Z c= dom (exp_R*f) by XBOOLE_1:1;
then
A6: exp_R*f is_differentiable_on Z by A2,A3,Th11;
A7: for x st x in Z holds (exp_R*f).x<>0
proof
let x;
assume x in Z;
then (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12;
hence thesis by SIN_COS:54;
end;
exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A8: exp_R/(exp_R*f) is_differentiable_on Z by A6,A7,FDIFF_2:21;
A9: 1-log(number_e,a)<>0
proof
A10: number_e<>1 by TAYLOR_1:11;
assume 1-log(number_e,a)=0;
then log(number_e,a)=log(number_e,number_e) by A10,POWER:52,TAYLOR_1:11;
then a=(number_e) to_power log(number_e,number_e) by A3,A10,POWER:def 3
,TAYLOR_1:11
.=number_e by A10,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4;
end;
for x st x in Z holds (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z
).x =exp_R.x/a #R x
proof
let x;
A11: exp_R is_differentiable_in x by SIN_COS:65;
A12: a #R x >0 by A3,PREPOWER:81;
assume
A13: x in Z;
then
A14: (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12
.=exp_R.(x*log(number_e,a)) by A2,A13
.=a #R x by A3,Th1;
A15: exp_R*f is_differentiable_in x & (exp_R*f).x <>0 by A6,A7,A13,FDIFF_1:9;
(((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z).x =(1/(1-log(
number_e,a)))*diff((exp_R/(exp_R*f)),x) by A1,A8,A13,FDIFF_1:20
.=(1/(1-log(number_e,a)))* ((diff(exp_R,x) * (exp_R*f).x - diff((exp_R
*f),x) * exp_R.x)/((exp_R*f).x)^2) by A11,A15,FDIFF_2:14
.=(1/(1-log(number_e,a)))* ((exp_R.x * a #R x - diff((exp_R*f),x)*
exp_R.x)/(a #R x)^2) by A14,SIN_COS:65
.=(1/(1-log(number_e,a)))*((exp_R.x*(a #R x -diff((exp_R*f),x)))/(a #R
x)^2)
.=(1/(1-log(number_e,a)))*((exp_R.x*(a #R x - ((exp_R*f)`|Z).x))/(a #R
x)^2) by A6,A13,FDIFF_1:def 7
.=(1/(1-log(number_e,a)))* ((exp_R.x*(a #R x -a #R x*log(number_e,a)))
/(a #R x)^2) by A2,A3,A5,A13,Th11
.=(1/(1-log(number_e,a)))*((1-log(number_e,a))*exp_R.x*a #R x)/ (a #R
x)^2 by XCMPLX_1:74
.=(1/(1-log(number_e,a)))*(1-log(number_e,a))*exp_R.x*a #R x/(a #R x)
^2
.=1*exp_R.x*a #R x/(a #R x)^2 by A9,XCMPLX_1:106
.=exp_R.x/a #R x by A12,XCMPLX_1:91;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:20;
end;
:: 20 f.x=ln(exp_R.x+1)
theorem
Z c= dom (ln*(exp_R+f)) & (for x st x in Z holds f.x=1 ) implies ln*(
exp_R+f) is_differentiable_on Z & for x st x in Z holds ((ln*(exp_R+f))`|Z).x =
exp_R.x/(exp_R.x+1)
proof
assume that
A1: Z c= dom (ln*(exp_R+f)) and
A2: for x st x in Z holds f.x=1;
A3: for x st x in Z holds f.x=0*x+1 by A2;
for y being object st y in Z holds y in dom (exp_R+f) by A1,FUNCT_1:11;
then
A4: Z c= dom (exp_R+f) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:def 1;
then
A5: Z c= dom f by XBOOLE_1:18;
then
A6: f is_differentiable_on Z by A3,FDIFF_1:23;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A8: exp_R+f is_differentiable_on Z by A4,A6,FDIFF_1:18;
A9: for x st x in Z holds ((exp_R+f)`|Z).x =exp_R.x
proof
let x;
assume
A10: x in Z;
hence ((exp_R+f)`|Z).x = diff(exp_R,x) + diff(f,x) by A4,A6,A7,FDIFF_1:18
.=exp_R.x+ diff(f,x) by SIN_COS:65
.=exp_R.x+(f`|Z).x by A6,A10,FDIFF_1:def 7
.=exp_R.x+0 by A5,A3,A10,FDIFF_1:23
.=exp_R.x;
end;
A11: for x st x in Z holds (exp_R+f).x>0
proof
let x;
assume
A12: x in Z;
then (exp_R+f).x=exp_R.x + f.x by A4,VALUED_1:def 1
.=exp_R.x +1 by A2,A12;
hence thesis by SIN_COS:54,XREAL_1:34;
end;
A13: for x st x in Z holds ln*(exp_R+f) is_differentiable_in x
proof
let x;
assume x in Z;
then exp_R+f is_differentiable_in x & (exp_R+f).x >0 by A8,A11,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A14: ln*(exp_R+f) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(exp_R+f))`|Z).x = exp_R.x/(exp_R.x+1)
proof
let x;
assume
A15: x in Z;
then
A16: (exp_R+f).x=exp_R.x + f.x by A4,VALUED_1:def 1
.=exp_R.x +1 by A2,A15;
exp_R+f is_differentiable_in x & (exp_R+f).x>0 by A8,A11,A15,FDIFF_1:9;
then diff(ln*(exp_R+f),x) =diff((exp_R+f),x)/((exp_R+f).x) by TAYLOR_1:20
.=((exp_R+f)`|Z).x/((exp_R+f).x) by A8,A15,FDIFF_1:def 7
.=exp_R.x/(exp_R.x +1) by A9,A15,A16;
hence thesis by A14,A15,FDIFF_1:def 7;
end;
hence thesis by A1,A13,FDIFF_1:9;
end;
:: 21 f.x=ln(exp_R.x-1)
theorem
Z c= dom (ln*(exp_R-f)) & (for x st x in Z holds f.x=1 & (exp_R-f).x>0
) implies ln*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((ln*(
exp_R-f))`|Z).x = exp_R.x/(exp_R.x-1)
proof
assume that
A1: Z c= dom (ln*(exp_R-f)) and
A2: for x st x in Z holds f.x=1 & (exp_R-f).x>0;
A3: for x st x in Z holds f.x=0*x+1 by A2;
for y being object st y in Z holds y in dom (exp_R-f) by A1,FUNCT_1:11;
then
A4: Z c= dom (exp_R-f) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:12;
then
A5: Z c= dom f by XBOOLE_1:18;
then
A6: f is_differentiable_on Z by A3,FDIFF_1:23;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A8: exp_R-f is_differentiable_on Z by A4,A6,FDIFF_1:19;
A9: for x st x in Z holds ((exp_R-f)`|Z).x =exp_R.x
proof
let x;
assume
A10: x in Z;
hence ((exp_R-f)`|Z).x = diff(exp_R,x) - diff(f,x) by A4,A6,A7,FDIFF_1:19
.= exp_R.x- diff(f,x) by SIN_COS:65
.= exp_R.x-(f`|Z).x by A6,A10,FDIFF_1:def 7
.= exp_R.x-0 by A5,A3,A10,FDIFF_1:23
.= exp_R.x;
end;
A11: for x st x in Z holds ln*(exp_R-f) is_differentiable_in x
proof
let x;
assume x in Z;
then exp_R-f is_differentiable_in x & (exp_R-f).x >0 by A2,A8,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A12: ln*(exp_R-f) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(exp_R-f))`|Z).x = exp_R.x/(exp_R.x-1)
proof
let x;
assume
A13: x in Z;
then
A14: (exp_R-f).x=exp_R.x - f.x by A4,VALUED_1:13
.=exp_R.x -1 by A2,A13;
(exp_R-f) is_differentiable_in x & (exp_R-f).x >0 by A2,A8,A13,FDIFF_1:9;
then diff(ln*(exp_R-f),x) =diff((exp_R-f),x)/((exp_R-f).x) by TAYLOR_1:20
.=((exp_R-f)`|Z).x/((exp_R-f).x) by A8,A13,FDIFF_1:def 7
.=exp_R.x/(exp_R.x -1) by A9,A13,A14;
hence thesis by A12,A13,FDIFF_1:def 7;
end;
hence thesis by A1,A11,FDIFF_1:9;
end;
:: 22 f.x=-ln(1-exp_R.x)
theorem
Z c= dom -(ln*(f-exp_R)) & (for x st x in Z holds f.x=1 & (f-exp_R).x>
0) implies -(ln*(f-exp_R)) is_differentiable_on Z & for x st x in Z holds ( (-
ln*(f-exp_R)) `|Z).x = exp_R.x/(1-exp_R.x)
proof
assume that
A1: Z c= dom -(ln*(f-exp_R)) and
A2: for x st x in Z holds f.x=1 & (f-exp_R).x>0;
A3: for x st x in Z holds f.x=0*x+1 by A2;
A4: Z c= dom (ln*(f-exp_R)) by A1,VALUED_1:8;
then for y being object st y in Z holds y in dom (f-exp_R) by FUNCT_1:11;
then
A5: Z c= dom (f-exp_R) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:12;
then
A6: Z c= dom f by XBOOLE_1:18;
then
A7: f is_differentiable_on Z by A3,FDIFF_1:23;
A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A9: f-exp_R is_differentiable_on Z by A5,A7,FDIFF_1:19;
for x st x in Z holds ln*(f-exp_R) is_differentiable_in x
proof
let x;
assume x in Z;
then f-exp_R is_differentiable_in x & (f-exp_R).x >0 by A2,A9,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A10: ln*(f-exp_R) is_differentiable_on Z by A4,FDIFF_1:9;
A11: for x st x in Z holds ((f-exp_R)`|Z).x =-exp_R.x
proof
let x;
assume
A12: x in Z;
hence ((f-exp_R)`|Z).x =diff(f,x)-diff(exp_R,x) by A5,A7,A8,FDIFF_1:19
.= diff(f,x)-exp_R.x by SIN_COS:65
.= (f`|Z).x-exp_R.x by A7,A12,FDIFF_1:def 7
.=0-exp_R.x by A6,A3,A12,FDIFF_1:23
.=-exp_R.x;
end;
A13: for x st x in Z holds ( (-ln*(f-exp_R)) `|Z).x = exp_R.x/(1-exp_R.x)
proof
let x;
assume
A14: x in Z;
then
A15: (f-exp_R).x=f.x-exp_R.x by A5,VALUED_1:13
.=1-exp_R.x by A2,A14;
A16: (f-exp_R) is_differentiable_in x & (f-exp_R).x >0 by A2,A9,A14,FDIFF_1:9;
(((-1)(#)(ln*(f-exp_R)))`|Z).x =(-1)*diff((ln*(f-exp_R)),x) by A1,A10,A14,
FDIFF_1:20
.=(-1)*(diff((f-exp_R),x)/((f-exp_R).x)) by A16,TAYLOR_1:20
.=(-1)*(((f-exp_R)`|Z).x/(f-exp_R).x) by A9,A14,FDIFF_1:def 7
.=(-1)*((-exp_R.x)/(1-exp_R.x)) by A11,A14,A15
.=((-1)*(-exp_R.x))/(1-exp_R.x) by XCMPLX_1:74
.=exp_R.x/(1-exp_R.x);
hence thesis;
end;
Z c= dom ((-1)(#)(ln*(f-exp_R))) by A1;
hence thesis by A10,A13,FDIFF_1:20;
end;
:: 23 f.x=exp_R(2*x)+1
theorem Th23:
Z c= dom ((( #Z 2)*exp_R)+f) & (for x st x in Z holds f.x=1)
implies (( #Z 2)*exp_R)+f is_differentiable_on Z & for x st x in Z holds ((((
#Z 2)*exp_R)+f)`|Z).x =2*exp_R(2*x)
proof
assume that
A1: Z c= dom ((( #Z 2)*exp_R)+f) and
A2: for x st x in Z holds f.x=1;
A3: Z c= dom (( #Z 2)*exp_R) /\ dom f by A1,VALUED_1:def 1;
then
A4: Z c= dom f by XBOOLE_1:18;
A5: now
let x;
assume x in Z;
exp_R is_differentiable_in x by SIN_COS:65;
hence ( #Z 2)*exp_R is_differentiable_in x by TAYLOR_1:3;
end;
A6: for x st x in Z holds f.x=0*x+1 by A2;
then
A7: f is_differentiable_on Z by A4,FDIFF_1:23;
Z c= dom (( #Z 2)*exp_R) by A3,XBOOLE_1:18;
then
A8: ( #Z 2)*exp_R is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds (((( #Z 2)*exp_R)+f)`|Z).x =2*exp_R(2*x)
proof
let x;
A9: exp_R is_differentiable_in x by SIN_COS:65;
assume
A10: x in Z;
then
(((( #Z 2)*exp_R)+f)`|Z).x =diff(( #Z 2)*exp_R,x)+diff(f,x) by A1,A7,A8,
FDIFF_1:18
.=(2*( (exp_R.x) #Z (2-1)) * diff(exp_R,x))+diff(f,x) by A9,TAYLOR_1:3
.=2*( (exp_R.x) #Z (2-1)) * exp_R.x+diff(f,x) by SIN_COS:65
.=2* exp_R.x * exp_R.x+diff(f,x) by PREPOWER:35
.=2*( exp_R.x * exp_R.x)+diff(f,x)
.=2*( exp_R( x )* exp_R.x)+diff(f,x) by SIN_COS:def 23
.=2*( exp_R( x )* exp_R(x))+diff(f,x) by SIN_COS:def 23
.=2*(exp_R(x+x))+diff(f,x) by SIN_COS:50
.=2* exp_R(2*x)+(f`|Z).x by A7,A10,FDIFF_1:def 7
.= 2* exp_R(2*x)+0 by A4,A6,A10,FDIFF_1:23
.=2* exp_R(2*x);
hence thesis;
end;
hence thesis by A1,A7,A8,FDIFF_1:18;
end;
:: 24 f.x=(1/2)*ln(exp_R(2*x)+1)
theorem
Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)+f1 & (for x st x in Z
holds f1.x=1) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z
holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)+exp_R(-x))
proof
assume that
A1: Z c= dom ((1/2)(#)(ln*f)) and
A2: f=(( #Z 2)*exp_R)+f1 and
A3: for x st x in Z holds f1.x=1;
A4: Z c= dom (ln*f) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A5: Z c= dom ((( #Z 2)*exp_R)+f1) by A2,TARSKI:def 3;
then
A6: (( #Z 2)*exp_R)+f1 is_differentiable_on Z by A3,Th23;
Z c= dom (( #Z 2)*exp_R) /\ dom f1 by A5,VALUED_1:def 1;
then
A7: Z c= dom (( #Z 2)*exp_R) by XBOOLE_1:18;
A8: for x st x in Z holds f.x >0
proof
let x;
A9: (exp_R.x) #Z 2>0 by PREPOWER:39,SIN_COS:54;
assume
A10: x in Z;
then ((( #Z 2)*exp_R)+f1).x =(( #Z 2)*exp_R).x+f1.x by A5,VALUED_1:def 1
.=( #Z 2).(exp_R.x)+f1.x by A7,A10,FUNCT_1:12
.=(exp_R.x) #Z 2+f1.x by TAYLOR_1:def 1
.=(exp_R.x) #Z 2+1 by A3,A10;
hence thesis by A2,A9;
end;
for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A11: ln*f is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)+exp_R (-x))
proof
let x;
A12: exp_R(x)>0 by SIN_COS:55;
assume
A13: x in Z;
then
A14: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
A15: ((( #Z 2)*exp_R)+f1).x =(( #Z 2)*exp_R).x+f1.x by A5,A13,VALUED_1:def 1
.=( #Z 2).(exp_R.x)+f1.x by A7,A13,FUNCT_1:12
.=(exp_R.x) #Z 2+f1.x by TAYLOR_1:def 1
.=(exp_R.x) #Z 2+1 by A3,A13
.=(exp_R(x)) #Z (1+1)+1 by SIN_COS:def 23
.=(exp_R(x)) #Z 1 * (exp_R(x)) #Z 1 +1 by A12,PREPOWER:44
.=exp_R(x) * (exp_R(x)) #Z 1 +1 by PREPOWER:35
.=exp_R(x) * exp_R(x) +1 by PREPOWER:35;
(((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A11,A13,FDIFF_1:20
.=(1/2)*(diff(f,x)/f.x) by A14,TAYLOR_1:20
.=(1/2)*((((( #Z 2)*exp_R)+f1)`|Z).x/((( #Z 2)*exp_R)+f1).x) by A2,A6,A13
,FDIFF_1:def 7
.=(1/2)*((2*exp_R(2*x))/(exp_R(x) * exp_R(x) +1)) by A3,A5,A13,A15,Th23
.=(1/2)*(2*exp_R(2*x))/(exp_R(x) * exp_R(x) +1) by XCMPLX_1:74
.=(exp_R(x+x)/exp_R(x))/((exp_R(x) * exp_R(x)+1)/exp_R(x)) by A12,
XCMPLX_1:55
.=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x) * exp_R(x)+1)/exp_R(x)) by
SIN_COS:50
.=(exp_R(x)*exp_R(x)/exp_R(x))/(exp_R(x) * exp_R(x)/exp_R(x)+1/exp_R(x
)) by XCMPLX_1:62
.=exp_R(x)/(exp_R(x) * exp_R(x)/exp_R(x)+1/exp_R(x)) by A12,XCMPLX_1:89
.=exp_R(x)/(exp_R(x)+1/exp_R(x)) by A12,XCMPLX_1:89
.=exp_R(x)/(exp_R(x)+exp_R(-x)) by TAYLOR_1:4;
hence thesis;
end;
hence thesis by A1,A11,FDIFF_1:20;
end;
:: 25 f.x=exp_R(2*x)-1
theorem Th25:
Z c= dom ((( #Z 2)*exp_R)-f) & (for x st x in Z holds f.x=1)
implies (( #Z 2)*exp_R)-f is_differentiable_on Z & for x st x in Z holds ((((
#Z 2)*exp_R)-f)`|Z).x =2*exp_R(2*x)
proof
assume that
A1: Z c= dom ((( #Z 2)*exp_R)-f) and
A2: for x st x in Z holds f.x=1;
A3: Z c= dom (( #Z 2)*exp_R) /\ dom f by A1,VALUED_1:12;
then
A4: Z c= dom f by XBOOLE_1:18;
A5: now
let x;
assume x in Z;
exp_R is_differentiable_in x by SIN_COS:65;
hence ( #Z 2)*exp_R is_differentiable_in x by TAYLOR_1:3;
end;
A6: for x st x in Z holds f.x=0*x+1 by A2;
then
A7: f is_differentiable_on Z by A4,FDIFF_1:23;
Z c= dom (( #Z 2)*exp_R) by A3,XBOOLE_1:18;
then
A8: ( #Z 2)*exp_R is_differentiable_on Z by A5,FDIFF_1:9;
for x st x in Z holds (((( #Z 2)*exp_R)-f)`|Z).x =2*exp_R(2*x)
proof
let x;
A9: exp_R is_differentiable_in x by SIN_COS:65;
assume
A10: x in Z;
then
(((( #Z 2)*exp_R)-f)`|Z).x =diff(( #Z 2)*exp_R,x)-diff(f,x) by A1,A7,A8,
FDIFF_1:19
.=(2*((exp_R.x) #Z (2-1)) * diff(exp_R,x))-diff(f,x) by A9,TAYLOR_1:3
.=2*((exp_R.x) #Z 1) * exp_R.x-diff(f,x) by SIN_COS:65
.=2* exp_R.x * exp_R.x-diff(f,x) by PREPOWER:35
.=2*(exp_R.x * exp_R.x)-diff(f,x)
.=2*(exp_R(x)* exp_R.x)-diff(f,x) by SIN_COS:def 23
.=2*(exp_R(x)* exp_R(x))-diff(f,x) by SIN_COS:def 23
.=2*(exp_R(x+x))-diff(f,x) by SIN_COS:50
.=2* exp_R(2*x)-(f`|Z).x by A7,A10,FDIFF_1:def 7
.= 2* exp_R(2*x)-0 by A4,A6,A10,FDIFF_1:23
.=2* exp_R(2*x);
hence thesis;
end;
hence thesis by A1,A7,A8,FDIFF_1:19;
end;
:: 26 f.x=(1/2)*ln(exp_R(2*x)-1)
theorem
Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)-f1 & (for x st x in Z
holds f1.x=1 & f.x>0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st
x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)-exp_R(-x))
proof
assume that
A1: Z c= dom ((1/2)(#)(ln*f)) and
A2: f=(( #Z 2)*exp_R)-f1 and
A3: for x st x in Z holds f1.x=1 & f.x>0;
A4: Z c= dom (ln*f) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A5: Z c= dom ((( #Z 2)*exp_R)-f1) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=1 by A3;
then
A7: (( #Z 2)*exp_R)-f1 is_differentiable_on Z by A5,Th25;
for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A3,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom (( #Z 2)*exp_R) /\ dom f1 by A5,VALUED_1:12;
then
A9: Z c= dom (( #Z 2)*exp_R) by XBOOLE_1:18;
for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)-exp_R (-x))
proof
let x;
A10: exp_R(x)>0 by SIN_COS:55;
assume
A11: x in Z;
then
A12: f is_differentiable_in x & f.x >0 by A2,A3,A7,FDIFF_1:9;
A13: ((( #Z 2)*exp_R)-f1).x =(( #Z 2)*exp_R).x-f1.x by A5,A11,VALUED_1:13
.=( #Z 2).(exp_R.x)-f1.x by A9,A11,FUNCT_1:12
.=(exp_R.x) #Z 2-f1.x by TAYLOR_1:def 1
.=(exp_R.x) #Z 2-1 by A3,A11
.=(exp_R(x)) #Z (1+1)-1 by SIN_COS:def 23
.=(exp_R(x)) #Z 1 * (exp_R(x)) #Z 1 -1 by A10,PREPOWER:44
.=exp_R(x) * (exp_R(x)) #Z 1 -1 by PREPOWER:35
.=exp_R(x) * exp_R(x) -1 by PREPOWER:35;
(((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A8,A11,FDIFF_1:20
.=(1/2)*(diff(f,x)/f.x) by A12,TAYLOR_1:20
.=(1/2)*((((( #Z 2)*exp_R)-f1)`|Z).x/((( #Z 2)*exp_R)-f1).x) by A2,A7,A11
,FDIFF_1:def 7
.=(1/2)*((2*exp_R(2*x))/(exp_R(x) * exp_R(x) -1)) by A6,A5,A11,A13,Th25
.=(1/2)*(2*exp_R(2*x))/(exp_R(x) * exp_R(x) -1) by XCMPLX_1:74
.=(exp_R(x+x)/exp_R(x))/((exp_R(x) * exp_R(x)-1)/exp_R(x)) by A10,
XCMPLX_1:55
.=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x) * exp_R(x)-1)/exp_R(x)) by
SIN_COS:50
.=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x)*exp_R(x))/exp_R(x)- 1/
exp_R(x)) by XCMPLX_1:120
.=exp_R(x)/(exp_R(x) * exp_R(x)/exp_R(x)-1/exp_R(x)) by A10,XCMPLX_1:89
.=exp_R(x)/(exp_R(x)-1/exp_R(x)) by A10,XCMPLX_1:89
.=exp_R(x)/(exp_R(x)-exp_R(-x)) by TAYLOR_1:4;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:20;
end;
:: 27 f.x=(exp_R.x-1)^2
theorem Th27:
Z c= dom (( #Z 2)*(exp_R-f)) & (for x st x in Z holds f.x=1)
implies ( #Z 2)*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((( #Z
2)*(exp_R-f))`|Z).x =2*exp_R.x*(exp_R.x-1)
proof
assume that
A1: Z c= dom (( #Z 2)*(exp_R-f)) and
A2: for x st x in Z holds f.x=1;
for y being object st y in Z holds y in dom (exp_R-f) by A1,FUNCT_1:11;
then
A3: Z c= dom (exp_R-f) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:12;
then
A4: Z c= dom f by XBOOLE_1:18;
A5: for x st x in Z holds f.x=0*x+1 by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds ( #Z 2)*(exp_R-f) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: f is_differentiable_in x by A6,FDIFF_1:9;
exp_R is_differentiable_in x by SIN_COS:65;
then exp_R-f is_differentiable_in x by A8,FDIFF_1:14;
hence thesis by TAYLOR_1:3;
end;
then
A9: ( #Z 2)*(exp_R-f) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z 2)*(exp_R-f))`|Z).x =2*exp_R.x*(exp_R.x-1)
proof
let x;
A10: exp_R is_differentiable_in x by SIN_COS:65;
assume
A11: x in Z;
then
A12: (exp_R-f).x=exp_R.x-f.x by A3,VALUED_1:13
.= exp_R.x-1 by A2,A11;
A13: f is_differentiable_in x by A6,A11,FDIFF_1:9;
then
A14: diff((exp_R-f),x)=diff(exp_R,x)-diff(f,x) by A10,FDIFF_1:14
.=diff(exp_R,x)-(f`|Z).x by A6,A11,FDIFF_1:def 7
.=exp_R.x-(f`|Z).x by SIN_COS:65
.=exp_R.x-0 by A4,A5,A11,FDIFF_1:23
.=exp_R.x;
A15: exp_R-f is_differentiable_in x by A13,A10,FDIFF_1:14;
((( #Z 2)*(exp_R-f))`|Z).x =diff((( #Z 2)*(exp_R-f)),x) by A9,A11,
FDIFF_1:def 7
.=2* ((exp_R-f).x) #Z (2-1) * diff((exp_R-f),x) by A15,TAYLOR_1:3
.=2*(exp_R.x-1)*exp_R.x by A14,A12,PREPOWER:35
.=2*exp_R.x*(exp_R.x-1);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 28 f.x=ln((exp_R.x-1)^2/exp_R.x)
theorem
Z c= dom f & f=ln*((( #Z 2)*(exp_R-f1))/exp_R) & (for x st x in Z
holds f1.x=1 & (exp_R-f1).x>0) implies f is_differentiable_on Z & for x st x in
Z holds (f`|Z).x =(exp_R.x+1)/(exp_R.x-1)
proof
assume that
A1: Z c= dom f and
A2: f=ln*((( #Z 2)*(exp_R-f1))/exp_R) and
A3: for x st x in Z holds f1.x=1 & (exp_R-f1).x>0;
for y being object st y in Z
holds y in dom ((( #Z 2)*(exp_R-f1))/exp_R) by A1,A2,
FUNCT_1:11;
then
A4: Z c= dom ((( #Z 2)*(exp_R-f1))/exp_R) by TARSKI:def 3;
then Z c=dom (( #Z 2)*(exp_R-f1))/\(dom (exp_R)\(exp_R)"{0}) by
RFUNCT_1:def 1;
then
A5: Z c= dom (( #Z 2)*(exp_R-f1)) by XBOOLE_1:18;
then for y being object st y in Z holds y in dom (exp_R-f1) by FUNCT_1:11;
then
A6: Z c= dom (exp_R-f1) by TARSKI:def 3;
A7: for x st x in Z holds ((( #Z 2)*(exp_R-f1))/exp_R).x >0
proof
let x;
A8: exp_R.x>0 by SIN_COS:54;
assume
A9: x in Z;
then
A10: ((exp_R-f1).x) #Z 2>0 by A3,PREPOWER:39;
((( #Z 2)*(exp_R-f1))/exp_R).x =(( #Z 2)*(exp_R-f1)).x*(exp_R.x)" by A4,A9,
RFUNCT_1:def 1
.=(( #Z 2)*(exp_R-f1)).x*(1/exp_R.x) by XCMPLX_1:215
.=(( #Z 2)*(exp_R-f1)).x/exp_R.x by XCMPLX_1:99
.=( #Z 2).((exp_R-f1).x)/exp_R.x by A5,A9,FUNCT_1:12
.=((exp_R-f1).x) #Z 2/exp_R.x by TAYLOR_1:def 1;
hence thesis by A10,A8,XREAL_1:139;
end;
A11: for x st x in Z holds f1.x=1 by A3;
then
A12: ( #Z 2)*(exp_R-f1) is_differentiable_on Z by A5,Th27;
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
A13: (( #Z 2)*(exp_R-f1))/exp_R is_differentiable_on Z by A12,FDIFF_2:21;
A14: for x st x in Z holds ln*((( #Z 2)*(exp_R-f1))/exp_R)
is_differentiable_in x
proof
let x;
assume x in Z;
then
(( #Z 2)*(exp_R-f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R-
f1))/ exp_R).x >0 by A13,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A15: f is_differentiable_on Z by A1,A2,FDIFF_1:9;
for x st x in Z holds (f`|Z).x =(exp_R.x+1)/(exp_R.x-1)
proof
let x;
A16: exp_R.x>0 by SIN_COS:54;
A17: exp_R is_differentiable_in x by SIN_COS:65;
assume
A18: x in Z;
then
A19: (exp_R-f1).x=exp_R.x - f1.x by A6,VALUED_1:13
.=exp_R.x -1 by A3,A18;
then
A20: exp_R.x-1>0 by A3,A18;
A21: ((( #Z 2)*(exp_R-f1))/exp_R).x =(( #Z 2)*(exp_R-f1)).x*(exp_R.x)" by A4
,A18,RFUNCT_1:def 1
.=(( #Z 2)*(exp_R-f1)).x*(1/exp_R.x) by XCMPLX_1:215
.=(( #Z 2)*(exp_R-f1)).x/exp_R.x by XCMPLX_1:99
.=( #Z 2).((exp_R-f1).x)/exp_R.x by A5,A18,FUNCT_1:12
.=((exp_R.x-1) #Z (1+1))/exp_R.x by A19,TAYLOR_1:def 1
.=((exp_R.x-1) #Z 1*(exp_R.x-1) #Z 1)/exp_R.x by A20,PREPOWER:44
.=((exp_R.x-1) *(exp_R.x-1) #Z 1)/exp_R.x by PREPOWER:35
.=((exp_R.x-1) *(exp_R.x-1))/exp_R.x by PREPOWER:35;
A22: (( #Z 2)*(exp_R-f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R-
f1))/ exp_R).x >0 by A13,A7,A18,FDIFF_1:9;
( #Z 2)*(exp_R-f1) is_differentiable_in x by A12,A18,FDIFF_1:9;
then
A23: diff(((( #Z 2)*(exp_R-f1))/exp_R),x) =(diff((( #Z 2)*(exp_R-f1)),x)*
exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R-f1)).x)/(exp_R.x)^2 by A16,A17,
FDIFF_2:14
.=(((( #Z 2)*(exp_R-f1))`|Z).x*exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R-
f1)).x)/(exp_R.x)^2 by A12,A18,FDIFF_1:def 7
.=(2*exp_R.x*(exp_R.x-1)*exp_R.x- diff(exp_R,x)*(( #Z 2)*(exp_R-f1)).x
)/(exp_R.x)^2 by A11,A5,A18,Th27
.=(2*exp_R.x*(exp_R.x-1)*exp_R.x-exp_R.x* (( #Z 2)*(exp_R-f1)).x)/(
exp_R.x)^2 by SIN_COS:65
.=((2*exp_R.x*(exp_R.x-1)-(( #Z 2)*(exp_R-f1)).x)*exp_R.x)/ (exp_R.x*
exp_R.x)
.=(2*exp_R.x*(exp_R.x-1)-(( #Z 2)*(exp_R-f1)).x)/exp_R.x by A16,
XCMPLX_1:91
.=(2*exp_R.x*(exp_R.x-1)-( #Z 2).((exp_R-f1).x))/exp_R.x by A5,A18,
FUNCT_1:12
.=(2*exp_R.x*(exp_R.x-1)-((exp_R-f1).x) #Z 2)/exp_R.x by TAYLOR_1:def 1
.=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-f1.x) #Z 2)/exp_R.x by A6,A18,
VALUED_1:13
.=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) #Z (1+1))/exp_R.x by A3,A18
.=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) #Z 1*(exp_R.x-1) #Z 1)/exp_R.x by
A20,PREPOWER:44
.=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) *(exp_R.x-1) #Z 1)/exp_R.x by
PREPOWER:35
.=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) *(exp_R.x-1))/exp_R.x by PREPOWER:35
.=((exp_R.x+1)*(exp_R.x-1))/exp_R.x;
(f`|Z).x =diff(ln*((( #Z 2)*(exp_R-f1))/exp_R),x) by A2,A15,A18,
FDIFF_1:def 7
.=(((exp_R.x+1)*(exp_R.x-1))/exp_R.x)/(((exp_R.x-1)* (exp_R.x-1))/
exp_R.x) by A22,A23,A21,TAYLOR_1:20
.=((exp_R.x+1)*(exp_R.x-1))/((exp_R.x-1) *(exp_R.x-1)) by A16,XCMPLX_1:55
.=(exp_R.x+1)/(exp_R.x-1) by A20,XCMPLX_1:91;
hence thesis;
end;
hence thesis by A1,A2,A14,FDIFF_1:9;
end;
:: 29 f.x=(exp_R.x+1)^2
theorem Th29:
Z c= dom (( #Z 2)*(exp_R+f)) & (for x st x in Z holds f.x=1)
implies ( #Z 2)*(exp_R+f) is_differentiable_on Z & for x st x in Z holds ((( #Z
2)*(exp_R+f))`|Z).x =2*exp_R.x*(exp_R.x+1)
proof
assume that
A1: Z c= dom (( #Z 2)*(exp_R+f)) and
A2: for x st x in Z holds f.x=1;
for y being object st y in Z holds y in dom (exp_R+f) by A1,FUNCT_1:11;
then
A3: Z c= dom (exp_R+f) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:def 1;
then
A4: Z c= dom f by XBOOLE_1:18;
A5: for x st x in Z holds f.x=0*x+1 by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds ( #Z 2)*(exp_R+f) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: f is_differentiable_in x by A6,FDIFF_1:9;
exp_R is_differentiable_in x by SIN_COS:65;
then exp_R+f is_differentiable_in x by A8,FDIFF_1:13;
hence thesis by TAYLOR_1:3;
end;
then
A9: ( #Z 2)*(exp_R+f) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z 2)*(exp_R+f))`|Z).x =2*exp_R.x*(exp_R.x+1)
proof
let x;
A10: exp_R is_differentiable_in x by SIN_COS:65;
assume
A11: x in Z;
then
A12: (exp_R+f).x=exp_R.x+f.x by A3,VALUED_1:def 1
.= exp_R.x+1 by A2,A11;
A13: f is_differentiable_in x by A6,A11,FDIFF_1:9;
then
A14: diff((exp_R+f),x)=diff(exp_R,x)+diff(f,x) by A10,FDIFF_1:13
.=diff(exp_R,x)+(f`|Z).x by A6,A11,FDIFF_1:def 7
.=exp_R.x+(f`|Z).x by SIN_COS:65
.=exp_R.x+0 by A4,A5,A11,FDIFF_1:23
.=exp_R.x;
A15: exp_R+f is_differentiable_in x by A13,A10,FDIFF_1:13;
((( #Z 2)*(exp_R+f))`|Z).x =diff((( #Z 2)*(exp_R+f)),x) by A9,A11,
FDIFF_1:def 7
.=2* ((exp_R+f).x) #Z (2-1) * diff((exp_R+f),x) by A15,TAYLOR_1:3
.=2*(exp_R.x+1)*exp_R.x by A14,A12,PREPOWER:35
.=2*exp_R.x*(exp_R.x+1);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 30 f.x=ln((exp_R.x+1)^2/exp_R.x)
theorem
Z c= dom f & f=ln*((( #Z 2)*(exp_R+f1))/exp_R) & (for x st x in Z
holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x
=(exp_R.x-1)/(exp_R.x+1)
proof
assume that
A1: Z c= dom f and
A2: f=ln*((( #Z 2)*(exp_R+f1))/exp_R) and
A3: for x st x in Z holds f1.x=1;
for y being object
st y in Z holds y in dom ((( #Z 2)*(exp_R+f1))/exp_R) by A1,A2,
FUNCT_1:11;
then
A4: Z c= dom ((( #Z 2)*(exp_R+f1))/exp_R) by TARSKI:def 3;
then Z c=dom (( #Z 2)*(exp_R+f1))/\(dom (exp_R)\(exp_R)"{0}) by
RFUNCT_1:def 1;
then
A5: Z c= dom (( #Z 2)*(exp_R+f1)) by XBOOLE_1:18;
then
A6: ( #Z 2)*(exp_R+f1) is_differentiable_on Z by A3,Th29;
for y being object st y in Z holds y in dom (exp_R+f1) by A5,FUNCT_1:11;
then
A7: Z c= dom (exp_R+f1) by TARSKI:def 3;
A8: for x st x in Z holds ((( #Z 2)*(exp_R+f1))/exp_R).x >0
proof
let x;
A9: exp_R.x>0 by SIN_COS:54;
assume
A10: x in Z;
then (exp_R+f1).x=exp_R.x + f1.x by A7,VALUED_1:def 1
.=exp_R.x +1 by A3,A10;
then (exp_R+f1).x>0 by SIN_COS:54,XREAL_1:34;
then
A11: ((exp_R+f1).x) #Z 2>0 by PREPOWER:39;
((( #Z 2)*(exp_R+f1))/exp_R).x =(( #Z 2)*(exp_R+f1)).x*(exp_R.x)" by A4,A10
,RFUNCT_1:def 1
.=(( #Z 2)*(exp_R+f1)).x*(1/exp_R.x) by XCMPLX_1:215
.=(( #Z 2)*(exp_R+f1)).x/exp_R.x by XCMPLX_1:99
.=( #Z 2).((exp_R+f1).x)/exp_R.x by A5,A10,FUNCT_1:12
.=((exp_R+f1).x) #Z 2/exp_R.x by TAYLOR_1:def 1;
hence thesis by A11,A9,XREAL_1:139;
end;
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
A12: (( #Z 2)*(exp_R+f1))/exp_R is_differentiable_on Z by A6,FDIFF_2:21;
A13: for x st x in Z holds ln*((( #Z 2)*(exp_R+f1))/exp_R)
is_differentiable_in x
proof
let x;
assume x in Z;
then
(( #Z 2)*(exp_R+f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R+
f1))/ exp_R).x >0 by A12,A8,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A14: f is_differentiable_on Z by A1,A2,FDIFF_1:9;
for x st x in Z holds (f`|Z).x =(exp_R.x-1)/(exp_R.x+1)
proof
let x;
A15: exp_R.x>0 by SIN_COS:54;
A16: exp_R is_differentiable_in x by SIN_COS:65;
A17: exp_R.x +1>0 by SIN_COS:54,XREAL_1:34;
assume
A18: x in Z;
then
A19: (exp_R+f1).x=exp_R.x + f1.x by A7,VALUED_1:def 1
.=exp_R.x +1 by A3,A18;
A20: (( #Z 2)*(exp_R+f1)).x =( #Z 2).((exp_R+f1).x) by A5,A18,FUNCT_1:12
.=(exp_R.x+1) #Z (1+1) by A19,TAYLOR_1:def 1
.=(exp_R.x+1) #Z 1*(exp_R.x+1) #Z 1 by A17,PREPOWER:44
.=(exp_R.x+1) *(exp_R.x+1) #Z 1 by PREPOWER:35
.=(exp_R.x+1) *(exp_R.x+1) by PREPOWER:35;
A21: (( #Z 2)*(exp_R+f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R+
f1))/ exp_R).x >0 by A12,A8,A18,FDIFF_1:9;
( #Z 2)*(exp_R+f1) is_differentiable_in x by A6,A18,FDIFF_1:9;
then
A22: diff(((( #Z 2)*(exp_R+f1))/exp_R),x) =(diff((( #Z 2)*(exp_R+f1)),x)*
exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R+f1)).x)/(exp_R.x)^2 by A15,A16,
FDIFF_2:14
.=(((( #Z 2)*(exp_R+f1))`|Z).x*exp_R.x-diff(exp_R,x)*(( #Z 2)* (exp_R+
f1)).x)/(exp_R.x)^2 by A6,A18,FDIFF_1:def 7
.=(2*exp_R.x*(exp_R.x+1)*exp_R.x-diff(exp_R,x)*(( #Z 2)* (exp_R+f1)).x
)/(exp_R.x)^2 by A3,A5,A18,Th29
.=(2*exp_R.x*(exp_R.x+1)*exp_R.x-exp_R.x*(( #Z 2)* (exp_R+f1)).x)/(
exp_R.x)^2 by SIN_COS:65
.=((2*exp_R.x*(exp_R.x+1)-(( #Z 2)*(exp_R+f1)).x)*exp_R.x)/ (exp_R.x*
exp_R.x)
.=(exp_R.x-1)*(exp_R.x+1)/exp_R.x by A15,A20,XCMPLX_1:91;
A23: ((( #Z 2)*(exp_R+f1))/exp_R).x =(( #Z 2)*(exp_R+f1)).x*(exp_R.x)" by A4
,A18,RFUNCT_1:def 1
.=(( #Z 2)*(exp_R+f1)).x*(1/exp_R.x) by XCMPLX_1:215
.=((exp_R.x+1) *(exp_R.x+1))/exp_R.x by A20,XCMPLX_1:99;
(f`|Z).x =diff(ln*((( #Z 2)*(exp_R+f1))/exp_R),x) by A2,A14,A18,
FDIFF_1:def 7
.=(((exp_R.x+1)*(exp_R.x-1))/exp_R.x)/(((exp_R.x+1) * (exp_R.x+1))/
exp_R.x) by A21,A22,A23,TAYLOR_1:20
.=((exp_R.x+1)*(exp_R.x-1))/((exp_R.x+1) *(exp_R.x+1)) by A15,XCMPLX_1:55
.=(exp_R.x-1)/(exp_R.x+1) by A17,XCMPLX_1:91;
hence thesis;
end;
hence thesis by A1,A2,A13,FDIFF_1:9;
end;
:: 31 f.x=(1-exp_R.x)^2
theorem Th31:
Z c= dom (( #Z 2)*(f-exp_R)) & (for x st x in Z holds f.x=1)
implies ( #Z 2)*(f-exp_R) is_differentiable_on Z & for x st x in Z holds ((( #Z
2)*(f-exp_R))`|Z).x =-2*exp_R.x*(1-exp_R.x)
proof
assume that
A1: Z c= dom (( #Z 2)*(f-exp_R)) and
A2: for x st x in Z holds f.x=1;
for y being object st y in Z holds y in dom (f-exp_R) by A1,FUNCT_1:11;
then
A3: Z c= dom (f-exp_R) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:12;
then
A4: Z c= dom f by XBOOLE_1:18;
A5: for x st x in Z holds f.x=0*x+1 by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds ( #Z 2)*(f-exp_R) is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: f is_differentiable_in x by A6,FDIFF_1:9;
exp_R is_differentiable_in x by SIN_COS:65;
then f-exp_R is_differentiable_in x by A8,FDIFF_1:14;
hence thesis by TAYLOR_1:3;
end;
then
A9: ( #Z 2)*(f-exp_R) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #Z 2)*(f-exp_R))`|Z).x =-2*exp_R.x*(1-exp_R.x )
proof
let x;
A10: exp_R is_differentiable_in x by SIN_COS:65;
assume
A11: x in Z;
then
A12: (f-exp_R).x=f.x-exp_R.x by A3,VALUED_1:13
.=1- exp_R.x by A2,A11;
A13: f is_differentiable_in x by A6,A11,FDIFF_1:9;
then
A14: diff((f-exp_R),x)=diff(f,x)-diff(exp_R,x) by A10,FDIFF_1:14
.=(f`|Z).x-diff(exp_R,x) by A6,A11,FDIFF_1:def 7
.=(f`|Z).x-exp_R.x by SIN_COS:65
.=0-exp_R.x by A4,A5,A11,FDIFF_1:23
.=-exp_R.x;
A15: f-exp_R is_differentiable_in x by A13,A10,FDIFF_1:14;
((( #Z 2)*(f-exp_R))`|Z).x =diff((( #Z 2)*(f-exp_R)),x) by A9,A11,
FDIFF_1:def 7
.=2* ((f-exp_R).x) #Z (2-1) * diff((f-exp_R),x) by A15,TAYLOR_1:3
.=2*(1-exp_R.x)*(-exp_R.x) by A14,A12,PREPOWER:35
.=-2*exp_R.x*(1-exp_R.x);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 32 f.x=ln(exp_R.x/(1-exp_R.x)^2)
theorem
Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1-exp_R))) & (for x st x in Z
holds f1.x=1 & (f1-exp_R).x>0) implies f is_differentiable_on Z & for x st x in
Z holds (f`|Z).x =(1+exp_R.x)/(1-exp_R.x)
proof
assume that
A1: Z c= dom f and
A2: f=ln*(exp_R/(( #Z 2)*(f1-exp_R))) and
A3: for x st x in Z holds f1.x=1 & (f1-exp_R).x>0;
for y being object
st y in Z holds y in dom (exp_R/(( #Z 2)*(f1-exp_R))) by A1,A2,
FUNCT_1:11;
then
A4: Z c= dom (exp_R/(( #Z 2)*(f1-exp_R))) by TARSKI:def 3;
then
Z c=dom exp_R/\(dom ((( #Z 2)*(f1-exp_R)))\((( #Z 2)*(f1-exp_R)))"{0} )
by RFUNCT_1:def 1;
then
A5: Z c= dom (( #Z 2)*(f1-exp_R)) by XBOOLE_1:1;
then for y being object st y in Z holds y in dom (f1-exp_R) by FUNCT_1:11;
then
A6: Z c= dom (f1-exp_R) by TARSKI:def 3;
A7: for x st x in Z holds (( #Z 2)*(f1-exp_R)).x>0
proof
let x;
assume
A8: x in Z;
then (( #Z 2)*(f1-exp_R)) .x =( #Z 2).((f1-exp_R).x) by A5,FUNCT_1:12
.=((f1-exp_R).x) #Z 2 by TAYLOR_1:def 1;
hence thesis by A3,A8,PREPOWER:39;
end;
A9: for x st x in Z holds (exp_R/(( #Z 2)*(f1-exp_R))).x >0
proof
let x;
A10: exp_R.x>0 by SIN_COS:54;
assume
A11: x in Z;
then
A12: (( #Z 2)*(f1-exp_R)).x>0 by A7;
(exp_R/(( #Z 2)*(f1-exp_R))).x =exp_R.x*((( #Z 2)*(f1-exp_R)).x)" by A4,A11
,RFUNCT_1:def 1
.=exp_R.x*(1/(( #Z 2)*(f1-exp_R)).x) by XCMPLX_1:215
.=exp_R.x/(( #Z 2)*(f1-exp_R)).x by XCMPLX_1:99;
hence thesis by A12,A10,XREAL_1:139;
end;
A13: for x st x in Z holds f1.x=1 by A3;
then
A14: ( #Z 2)*(f1-exp_R) is_differentiable_on Z by A5,Th31;
exp_R is_differentiable_on Z & for x st x in Z holds (( #Z 2)*(f1-exp_R
)).x <>0 by A7,FDIFF_1:26,TAYLOR_1:16;
then
A15: exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_on Z by A14,FDIFF_2:21;
A16: for x st x in Z holds ln*(exp_R/(( #Z 2)*(f1-exp_R)))
is_differentiable_in x
proof
let x;
assume x in Z;
then
exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*(
f1- exp_R))).x >0 by A15,A9,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A17: f is_differentiable_on Z by A1,A2,FDIFF_1:9;
for x st x in Z holds (f`|Z).x =(1+exp_R.x)/(1-exp_R.x)
proof
let x;
A18: exp_R is_differentiable_in x by SIN_COS:65;
assume
A19: x in Z;
then
A20: (( #Z 2)*(f1-exp_R)) .x =( #Z 2).((f1-exp_R).x) by A5,FUNCT_1:12
.=((f1-exp_R).x) #Z 2 by TAYLOR_1:def 1
.=(f1.x-exp_R.x) #Z 2 by A6,A19,VALUED_1:13
.=(1-exp_R.x) #Z 2 by A3,A19;
A21: (exp_R/(( #Z 2)*(f1-exp_R))).x =exp_R.x*((( #Z 2)*(f1-exp_R)).x)" by A4
,A19,RFUNCT_1:def 1
.=exp_R.x*(1/(( #Z 2)*(f1-exp_R)).x) by XCMPLX_1:215
.=exp_R.x/(1-exp_R.x) #Z 2 by A20,XCMPLX_1:99;
A22: exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*(
f1- exp_R))).x >0 by A15,A9,A19,FDIFF_1:9;
A23: (f1-exp_R).x>0 by A3,A19;
(( #Z 2)*(f1-exp_R)).x<>0 & ( #Z 2)*(f1-exp_R) is_differentiable_in x
by A14,A7,A19,FDIFF_1:9;
then
A24: diff((exp_R/(( #Z 2)*(f1-exp_R))),x) =(diff(exp_R,x)*(( #Z 2)*(f1-
exp_R)).x- diff((( #Z 2)*(f1-exp_R)),x)*exp_R.x) /((( #Z 2)*(f1-exp_R)).x)^2
by A18,FDIFF_2:14
.=(exp_R.x*(( #Z 2)*(f1-exp_R)).x-diff((( #Z 2)*(f1-exp_R)),x)*exp_R.x
) /((( #Z 2)*(f1-exp_R)).x)^2 by SIN_COS:65
.=(exp_R.x*(( #Z 2)*(f1-exp_R)).x-((( #Z 2)*(f1-exp_R))`|Z).x*exp_R.x)
/((( #Z 2)*(f1-exp_R)).x)^2 by A14,A19,FDIFF_1:def 7
.=(exp_R.x*((1-exp_R.x) #Z 2)-(-2*exp_R.x*(1-exp_R.x))*exp_R.x)/ ((1-
exp_R.x) #Z 2)^2 by A13,A5,A19,A20,Th31
.=(exp_R.x*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x)) /((1-exp_R.x) #Z
2*(1-exp_R.x) #Z 2)
.=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x)
) /(1-exp_R.x) #Z 2 by XCMPLX_1:83;
A25: exp_R.x>0 by SIN_COS:54;
A26: (f1-exp_R).x=f1.x-exp_R.x by A6,A19,VALUED_1:13
.=1-exp_R.x by A3,A19;
then (1-exp_R.x) #Z 2>0 by A3,A19,PREPOWER:39;
then
A27: exp_R.x/(1-exp_R.x) #Z 2<>0 by A25,XREAL_1:139;
A28: (1-exp_R.x) #Z 2=(1-exp_R.x) #Z (1+1)
.=(1-exp_R.x) #Z 1 * (1-exp_R.x) #Z 1 by A23,A26,PREPOWER:44
.=(1-exp_R.x) * (1-exp_R.x) #Z 1 by PREPOWER:35
.=(1-exp_R.x) * (1-exp_R.x) by PREPOWER:35;
(f`|Z).x =diff(ln*(exp_R/(( #Z 2)*(f1-exp_R))),x) by A2,A17,A19,
FDIFF_1:def 7
.=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x)
) /(1-exp_R.x) #Z 2/(exp_R.x/(1-exp_R.x) #Z 2) by A22,A24,A21,TAYLOR_1:20
.=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x)
) /((exp_R.x/(1-exp_R.x) #Z 2)*(1-exp_R.x) #Z 2) by XCMPLX_1:78
.=((1-exp_R.x) * (1+exp_R.x))/((1-exp_R.x) * (1-exp_R.x)) by A27,A28,
XCMPLX_1:91
.=(1+exp_R.x)/ (1-exp_R.x) by A23,A26,XCMPLX_1:91;
hence thesis;
end;
hence thesis by A1,A2,A16,FDIFF_1:9;
end;
:: 33 f.x=ln(exp_R.x/(1+exp_R.x)^2)
theorem
Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1+exp_R))) & (for x st x in Z
holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x
=(1-exp_R.x)/(1+exp_R.x)
proof
assume that
A1: Z c= dom f and
A2: f=ln*(exp_R/(( #Z 2)*(f1+exp_R))) and
A3: for x st x in Z holds f1.x=1;
for y being object
st y in Z holds y in dom (exp_R/(( #Z 2)*(f1+exp_R))) by A1,A2,
FUNCT_1:11;
then
A4: Z c= dom (exp_R/(( #Z 2)*(f1+exp_R))) by TARSKI:def 3;
then
Z c=dom exp_R/\(dom ((( #Z 2)*(f1+exp_R)))\((( #Z 2)*(f1+exp_R)))"{0} )
by RFUNCT_1:def 1;
then
A5: Z c= dom (( #Z 2)*(f1+exp_R)) by XBOOLE_1:1;
then
A6: ( #Z 2)*(f1+exp_R) is_differentiable_on Z by A3,Th29;
for y being object st y in Z holds y in dom (f1+exp_R) by A5,FUNCT_1:11;
then
A7: Z c= dom (f1+exp_R) by TARSKI:def 3;
A8: for x st x in Z holds (( #Z 2)*(f1+exp_R)).x>0
proof
let x;
assume
A9: x in Z;
then (f1+exp_R).x=f1.x+exp_R.x by A7,VALUED_1:def 1
.=1+exp_R.x by A3,A9;
then
A10: (f1+exp_R).x>0 by SIN_COS:54,XREAL_1:34;
(( #Z 2)*(f1+exp_R)) .x =( #Z 2).((f1+exp_R).x) by A5,A9,FUNCT_1:12
.=((f1+exp_R).x) #Z 2 by TAYLOR_1:def 1;
hence thesis by A10,PREPOWER:39;
end;
A11: for x st x in Z holds (exp_R/(( #Z 2)*(f1+exp_R))).x >0
proof
let x;
A12: exp_R.x>0 by SIN_COS:54;
assume
A13: x in Z;
then
A14: (( #Z 2)*(f1+exp_R)).x>0 by A8;
(exp_R/(( #Z 2)*(f1+exp_R))).x =exp_R.x*((( #Z 2)*(f1+exp_R)).x)" by A4,A13
,RFUNCT_1:def 1
.=exp_R.x*(1/(( #Z 2)*(f1+exp_R)).x) by XCMPLX_1:215
.=exp_R.x/(( #Z 2)*(f1+exp_R)).x by XCMPLX_1:99;
hence thesis by A14,A12,XREAL_1:139;
end;
exp_R is_differentiable_on Z & for x st x in Z holds (( #Z 2)*(f1+exp_R
)).x <>0 by A8,FDIFF_1:26,TAYLOR_1:16;
then
A15: exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_on Z by A6,FDIFF_2:21;
A16: for x st x in Z holds ln*(exp_R/(( #Z 2)*(f1+exp_R)))
is_differentiable_in x
proof
let x;
assume x in Z;
then
exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*(
f1+ exp_R))).x >0 by A15,A11,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A17: f is_differentiable_on Z by A1,A2,FDIFF_1:9;
for x st x in Z holds (f`|Z).x =(1-exp_R.x)/(1+exp_R.x)
proof
let x;
A18: exp_R is_differentiable_in x by SIN_COS:65;
assume
A19: x in Z;
then
A20: (( #Z 2)*(f1+exp_R)) .x =( #Z 2).((f1+exp_R).x) by A5,FUNCT_1:12
.=((f1+exp_R).x) #Z 2 by TAYLOR_1:def 1
.=(f1.x+exp_R.x) #Z 2 by A7,A19,VALUED_1:def 1
.=(1+exp_R.x) #Z 2 by A3,A19;
(( #Z 2)*(f1+exp_R)).x<>0 & ( #Z 2)*(f1+exp_R) is_differentiable_in x
by A6,A8,A19,FDIFF_1:9;
then
A21: diff((exp_R/(( #Z 2)*(f1+exp_R))),x) =(diff(exp_R,x)*(( #Z 2)*(f1+
exp_R)).x-diff((( #Z 2)*(f1+exp_R)),x)* exp_R.x) /((( #Z 2)*(f1+exp_R)).x)^2
by A18,FDIFF_2:14
.=(exp_R.x*(( #Z 2)*(f1+exp_R)).x-diff((( #Z 2)*(f1+exp_R)),x)*exp_R.x
) /((( #Z 2)*(f1+exp_R)).x)^2 by SIN_COS:65
.=(exp_R.x*(( #Z 2)*(f1+exp_R)).x-((( #Z 2)*(f1+exp_R))`|Z).x*exp_R.x)
/((( #Z 2)*(f1+exp_R)).x)^2 by A6,A19,FDIFF_1:def 7
.=(exp_R.x*(1+exp_R.x) #Z 2-2*exp_R.x*(1+exp_R.x)*exp_R.x)/((1+exp_R.x
) #Z 2)^2 by A3,A5,A19,A20,Th29
.=(exp_R.x*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x)) /((1+exp_R.x) #Z
2*(1+exp_R.x) #Z 2)
.=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x)
) /(1+exp_R.x) #Z 2 by XCMPLX_1:83;
A22: 1+exp_R.x>0 by SIN_COS:54,XREAL_1:34;
then exp_R.x>0 & (1+exp_R.x) #Z 2>0 by PREPOWER:39,SIN_COS:54;
then
A23: exp_R.x/(1+exp_R.x) #Z 2<>0 by XREAL_1:139;
A24: (exp_R/(( #Z 2)*(f1+exp_R))).x =exp_R.x*((( #Z 2)*(f1+exp_R)).x)" by A4
,A19,RFUNCT_1:def 1
.=exp_R.x*(1/(( #Z 2)*(f1+exp_R)).x) by XCMPLX_1:215
.=exp_R.x/(1+exp_R.x) #Z 2 by A20,XCMPLX_1:99;
A25: exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*(
f1+ exp_R))).x >0 by A15,A11,A19,FDIFF_1:9;
A26: (1+exp_R.x) #Z 2=(1+exp_R.x) #Z (1+1)
.=(1+exp_R.x) #Z 1 * (1+exp_R.x) #Z 1 by A22,PREPOWER:44
.=(1+exp_R.x) * (1+exp_R.x) #Z 1 by PREPOWER:35
.=(1+exp_R.x) * (1+exp_R.x) by PREPOWER:35;
(f`|Z).x =diff(ln*(exp_R/(( #Z 2)*(f1+exp_R))),x) by A2,A17,A19,
FDIFF_1:def 7
.=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x)
) /(1+exp_R.x) #Z 2/(exp_R.x/(1+exp_R.x) #Z 2) by A25,A21,A24,TAYLOR_1:20
.=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x)
) /((exp_R.x/(1+exp_R.x) #Z 2)*(1+exp_R.x) #Z 2) by XCMPLX_1:78
.=((1+exp_R.x) * (1-exp_R.x))/((1+exp_R.x) * (1+exp_R.x)) by A23,A26,
XCMPLX_1:91
.=(1-exp_R.x)/ (1+exp_R.x) by A22,XCMPLX_1:91;
hence thesis;
end;
hence thesis by A1,A2,A16,FDIFF_1:9;
end;
:: 34 f.x=ln(exp_R(x)+exp_R(-x))
theorem
Z c= dom (ln*f) & f=exp_R+(exp_R*f1) & (for x st x in Z holds f1.x=-x)
implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z).x =(
exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x))
proof
assume that
A1: Z c= dom (ln*f) and
A2: f=exp_R+(exp_R*f1) and
A3: for x st x in Z holds f1.x=-x;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom (exp_R+(exp_R*f1)) by A2,TARSKI:def 3;
then Z c= dom exp_R /\ dom (exp_R*f1) by VALUED_1:def 1;
then
A5: Z c= dom (exp_R*f1) by XBOOLE_1:18;
then
A6: exp_R*f1 is_differentiable_on Z by A3,Th14;
A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A8: f is_differentiable_on Z by A2,A4,A6,FDIFF_1:18;
A9: for x st x in Z holds ((exp_R+(exp_R*f1))`|Z).x =exp_R(x)-exp_R(-x)
proof
let x;
assume
A10: x in Z;
hence
((exp_R+(exp_R*f1))`|Z).x = diff(exp_R,x) + diff((exp_R*f1),x) by A4,A6,A7,
FDIFF_1:18
.=exp_R.x+ diff((exp_R*f1),x) by SIN_COS:65
.=exp_R.x+((exp_R*f1)`|Z).x by A6,A10,FDIFF_1:def 7
.=exp_R.x+(-exp_R(-x)) by A3,A5,A10,Th14
.=exp_R(x)+(-exp_R(-x)) by SIN_COS:def 23
.=exp_R(x)-exp_R(-x);
end;
A11: for x st x in Z holds (exp_R+(exp_R*f1)).x>0
proof
let x;
A12: exp_R(x)>0 by SIN_COS:55;
assume
A13: x in Z;
then (exp_R+(exp_R*f1)).x=exp_R.x + (exp_R*f1).x by A4,VALUED_1:def 1
.=exp_R.x +exp_R.(f1.x) by A5,A13,FUNCT_1:12
.=exp_R.x +exp_R.(-x) by A3,A13
.=exp_R(x) +exp_R.(-x) by SIN_COS:def 23
.=exp_R(x) +exp_R(-x) by SIN_COS:def 23;
hence thesis by A12,SIN_COS:55,XREAL_1:34;
end;
A14: for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A8,A11,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A15: ln*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*f)`|Z).x =(exp_R(x)-exp_R(-x))/(exp_R(x)+
exp_R(-x))
proof
let x;
assume
A16: x in Z;
then
A17: f.x=exp_R.x + (exp_R*f1).x by A2,A4,VALUED_1:def 1
.=exp_R.x +exp_R.(f1.x) by A5,A16,FUNCT_1:12
.=exp_R.x +exp_R.(-x) by A3,A16
.=exp_R(x) +exp_R.(-x) by SIN_COS:def 23
.=exp_R(x) +exp_R(-x) by SIN_COS:def 23;
f is_differentiable_in x & f.x>0 by A2,A8,A11,A16,FDIFF_1:9;
then diff((ln*f),x) =diff(f,x)/f.x by TAYLOR_1:20
.=(f`|Z).x/f.x by A8,A16,FDIFF_1:def 7
.=(exp_R(x)-exp_R(-x))/(exp_R(x) +exp_R(-x)) by A2,A9,A16,A17;
hence thesis by A15,A16,FDIFF_1:def 7;
end;
hence thesis by A1,A14,FDIFF_1:9;
end;
:: 35 f.x=ln(exp_R(x)-exp_R(-x))
theorem
Z c= dom (ln*f) & f=exp_R-(exp_R*f1) & (for x st x in Z holds f1.x=-x
& f.x>0) implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z
).x=(exp_R(x)+exp_R(-x))/ (exp_R(x)-exp_R(-x))
proof
assume that
A1: Z c= dom (ln*f) and
A2: f=exp_R-(exp_R*f1) and
A3: for x st x in Z holds f1.x=-x & f.x>0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A4: Z c= dom (exp_R-(exp_R*f1)) by A2,TARSKI:def 3;
then Z c= dom exp_R /\ dom (exp_R*f1) by VALUED_1:12;
then
A5: Z c= dom (exp_R*f1) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=-x by A3;
then
A7: exp_R*f1 is_differentiable_on Z by A5,Th14;
A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A9: f is_differentiable_on Z by A2,A4,A7,FDIFF_1:19;
A10: for x st x in Z holds ((exp_R-(exp_R*f1))`|Z).x =exp_R(x)+exp_R(-x)
proof
let x;
assume
A11: x in Z;
hence
((exp_R-(exp_R*f1))`|Z).x = diff(exp_R,x) - diff((exp_R*f1),x) by A4,A7,A8,
FDIFF_1:19
.=exp_R.x- diff((exp_R*f1),x) by SIN_COS:65
.=exp_R.x-((exp_R*f1)`|Z).x by A7,A11,FDIFF_1:def 7
.=exp_R.x-(-exp_R(-x)) by A6,A5,A11,Th14
.=exp_R.x+exp_R(-x)
.=exp_R(x)+exp_R(-x) by SIN_COS:def 23;
end;
A12: for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A3,A9,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A13: ln*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*f)`|Z).x =(exp_R(x)+exp_R(-x))/(exp_R(x)-
exp_R(-x))
proof
let x;
assume
A14: x in Z;
then
A15: f.x=exp_R.x - (exp_R*f1).x by A2,A4,VALUED_1:13
.=exp_R.x -exp_R.(f1.x) by A5,A14,FUNCT_1:12
.=exp_R.x -exp_R.(-x) by A3,A14
.=exp_R(x) -exp_R.(-x) by SIN_COS:def 23
.=exp_R(x) -exp_R(-x) by SIN_COS:def 23;
f is_differentiable_in x & f.x>0 by A3,A9,A14,FDIFF_1:9;
then diff((ln*f),x) =diff(f,x)/f.x by TAYLOR_1:20
.=(f`|Z).x/f.x by A9,A14,FDIFF_1:def 7
.=(exp_R(x)+exp_R(-x))/(exp_R(x) -exp_R(-x)) by A2,A10,A14,A15;
hence thesis by A13,A14,FDIFF_1:def 7;
end;
hence thesis by A1,A12,FDIFF_1:9;
end;
:: 36 f.x=(2/3)*((1+exp_R.x) ^ (3/2))
theorem
Z c= dom ((2/3)(#)(( #R (3/2))*(f+exp_R))) & (for x st x in Z holds f.
x=1) implies (2/3)(#)(( #R (3/2))*(f+exp_R)) is_differentiable_on Z & for x st
x in Z holds (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =exp_R.x*(1+exp_R.x) #R (
1/2)
proof
assume that
A1: Z c= dom ((2/3)(#)(( #R (3/2))*(f+exp_R))) and
A2: for x st x in Z holds f.x=1;
A3: for x st x in Z holds f.x=0*x+1 by A2;
A4: Z c= dom (( #R (3/2))*(f+exp_R)) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom (f+exp_R) by FUNCT_1:11;
then
A5: Z c= dom (f+exp_R) by TARSKI:def 3;
then Z c= dom exp_R /\ dom f by VALUED_1:def 1;
then
A6: Z c= dom f by XBOOLE_1:18;
then
A7: f is_differentiable_on Z by A3,FDIFF_1:23;
A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
then
A9: f+exp_R is_differentiable_on Z by A5,A7,FDIFF_1:18;
A10: for x st x in Z holds (f+exp_R).x>0
proof
let x;
assume
A11: x in Z;
then (f+exp_R).x=f.x+exp_R.x by A5,VALUED_1:def 1
.=1+exp_R.x by A2,A11;
hence thesis by SIN_COS:54,XREAL_1:34;
end;
now
let x;
assume x in Z;
then f+exp_R is_differentiable_in x & (f+exp_R).x>0 by A9,A10,FDIFF_1:9;
hence ( #R (3/2))*(f+exp_R) is_differentiable_in x by TAYLOR_1:22;
end;
then
A12: ( #R (3/2))*(f+exp_R) is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =exp_R.x
*(1+exp_R.x) #R (1/2)
proof
let x;
assume
A13: x in Z;
then
A14: ((f+exp_R)`|Z).x = diff(f,x)+diff(exp_R,x) by A5,A7,A8,FDIFF_1:18
.=diff(f,x)+exp_R.x by SIN_COS:65
.=(f`|Z).x+exp_R.x by A7,A13,FDIFF_1:def 7
.=0+exp_R.x by A6,A3,A13,FDIFF_1:23
.=exp_R.x;
A15: f+exp_R is_differentiable_in x & (f+exp_R).x>0 by A9,A10,A13,FDIFF_1:9;
A16: (f+exp_R).x=f.x+exp_R.x by A5,A13,VALUED_1:def 1
.=1+exp_R.x by A2,A13;
(((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =(2/3)*diff((( #R (3/2))*(f+
exp_R)),x) by A1,A12,A13,FDIFF_1:20
.=(2/3)*((3/2)*(((f+exp_R).x) #R (3/2-1)) * diff((f+exp_R),x)) by A15,
TAYLOR_1:22
.=(2/3)*((3/2)*(((f+exp_R).x) #R (3/2-1)) *((f+exp_R)`|Z).x ) by A9,A13,
FDIFF_1:def 7
.=exp_R.x*(1+exp_R.x) #R (1/2) by A16,A14;
hence thesis;
end;
hence thesis by A1,A12,FDIFF_1:20;
end;
:: 37 f.x=(2/(3*lna))*((1+a |^x) ^ (3/2))
theorem
Z c= dom ((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1)))) & (
for x st x in Z holds f.x=1 & f1.x=x*log(number_e,a)) & a>0 & a<>1 implies (2/(
3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))) is_differentiable_on Z & for
x st x in Z holds (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))))`|Z)
.x =a #R x * (1+a #R x) #R (1/2)
proof
assume that
A1: Z c= dom ((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1)))) and
A2: for x st x in Z holds f.x=1 & f1.x=x*log(number_e,a) and
A3: a>0 and
A4: a<>1;
A5: for x st x in Z holds f.x=0*x+1 by A2;
A6: Z c= dom (( #R (3/2))*(f+(exp_R*f1))) by A1,VALUED_1:def 5;
then for y being object
st y in Z holds y in dom (f+(exp_R*f1)) by FUNCT_1:11;
then
A7: Z c= dom (f+(exp_R*f1)) by TARSKI:def 3;
then
A8: Z c= dom (exp_R*f1) /\ dom f by VALUED_1:def 1;
then
A9: Z c= dom (exp_R*f1) by XBOOLE_1:18;
A10: for x st x in Z holds f1.x=x*log(number_e,a) by A2;
then
A11: exp_R*f1 is_differentiable_on Z by A3,A9,Th11;
A12: Z c= dom f by A8,XBOOLE_1:18;
then
A13: f is_differentiable_on Z by A5,FDIFF_1:23;
then
A14: f+(exp_R*f1) is_differentiable_on Z by A7,A11,FDIFF_1:18;
A15: for x st x in Z holds (f+(exp_R*f1)).x>0
proof
let x;
assume
A16: x in Z;
then (f+(exp_R*f1)).x=f.x+(exp_R*f1).x by A7,VALUED_1:def 1
.=f.x+exp_R.(f1.x) by A9,A16,FUNCT_1:12
.=1+exp_R.(f1.x) by A2,A16
.=1+exp_R.(x*log(number_e,a)) by A2,A16;
hence thesis by SIN_COS:54,XREAL_1:34;
end;
now
let x;
assume x in Z;
then f+(exp_R*f1) is_differentiable_in x & (f+(exp_R*f1)).x>0 by A14,A15,
FDIFF_1:9;
hence ( #R (3/2))*(f+(exp_R*f1)) is_differentiable_in x by TAYLOR_1:22;
end;
then
A17: ( #R (3/2))*(f+(exp_R*f1)) is_differentiable_on Z by A6,FDIFF_1:9;
A18: log(number_e,a)<>0
proof
A19: number_e<>1 by TAYLOR_1:11;
assume log(number_e,a)=0;
then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13;
then a=(number_e) to_power log(number_e,1) by A3,A19,POWER:def 3
,TAYLOR_1:11
.=1 by A19,POWER:def 3,TAYLOR_1:11;
hence contradiction by A4;
end;
for x st x in Z holds (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(
exp_R*f1))))`|Z).x =a #R x * (1+a #R x) #R (1/2)
proof
let x;
A20: 3*log(number_e,a) <> 0 by A18;
assume
A21: x in Z;
then
A22: ((f+(exp_R*f1))`|Z).x=diff(f,x)+diff((exp_R*f1),x) by A7,A13,A11,
FDIFF_1:18
.=diff(f,x)+((exp_R*f1)`|Z).x by A11,A21,FDIFF_1:def 7
.=(f`|Z).x+((exp_R*f1)`|Z).x by A13,A21,FDIFF_1:def 7
.=0+((exp_R*f1)`|Z).x by A12,A5,A21,FDIFF_1:23
.=a #R x*log(number_e,a) by A3,A10,A9,A21,Th11;
A23: (f+(exp_R*f1)).x=f.x+(exp_R*f1).x by A7,A21,VALUED_1:def 1
.=f.x+exp_R.(f1.x) by A9,A21,FUNCT_1:12
.=1+exp_R.(f1.x) by A2,A21
.=1+exp_R.(x*log(number_e,a)) by A2,A21
.=1+a #R x by A3,Th1;
f+(exp_R*f1) is_differentiable_in x & (f+(exp_R*f1)).x>0 by A14,A15,A21,
FDIFF_1:9;
then
diff((( #R (3/2))*(f+(exp_R*f1))),x) =(3/2)*(((f+(exp_R*f1)).x) #R (3
/2-1)) * diff((f+(exp_R*f1)),x) by TAYLOR_1:22
.=(3/2)*((1+a #R x) #R (1/2)) *(a #R x*log(number_e,a)) by A14,A21,A23
,A22,FDIFF_1:def 7
.=(3*log(number_e,a))/2*a #R x*(1+a #R x) #R (1/2);
then
(((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))))`|Z).x =(2/(
3*log(number_e,a)))*((3*log(number_e,a))/2*a #R x*(1+a #R x) #R (1/2)) by A1
,A17,A21,FDIFF_1:20
.=(2/(3*log(number_e,a)))*((3*log(number_e,a))/2) *a #R x*(1+a #R x)
#R (1/2)
.=1*a #R x*(1+a #R x) #R (1/2) by A20,XCMPLX_1:112
.=a #R x*(1+a #R x) #R (1/2);
hence thesis;
end;
hence thesis by A1,A17,FDIFF_1:20;
end;
:: 38 f.x=(-1/2)*cos(2*x)
theorem
Z c= dom ((-1/2)(#)(cos*f)) & (for x st x in Z holds f.x=2*x) implies
(-1/2)(#)(cos*f) is_differentiable_on Z & for x st x in Z holds (((-1/2)(#)(cos
*f))`|Z).x =sin(2*x)
proof
assume that
A1: Z c= dom ((-1/2)(#)(cos*f)) and
A2: for x st x in Z holds f.x=2*x;
A3: Z c= dom (cos*f) & for x st x in Z holds f.x=2*x+0 by A1,A2,VALUED_1:def 5;
then
A4: cos*f is_differentiable_on Z by FDIFF_4:38;
for x st x in Z holds (((-1/2)(#)(cos*f))`|Z).x =sin(2*x)
proof
let x;
assume
A5: x in Z;
then (((-1/2)(#)(cos*f))`|Z).x =(-1/2)*diff((cos*f),x) by A1,A4,FDIFF_1:20
.=(-1/2)*((cos*f)`|Z).x by A4,A5,FDIFF_1:def 7
.=(-1/2)*(-2* sin.(2*x+0)) by A3,A5,FDIFF_4:38
.=sin(2*x) by SIN_COS:def 17;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
theorem
Z c= dom (2(#)(( #R (1/2))*(f-cos))) & (for x st x in Z holds f.x=1 &
sin.x>0 & cos.x<1 & cos.x>-1) implies 2(#)(( #R (1/2))*(f-cos))
is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1/2))*(f-cos)))`|Z)
.x =(1+cos.x) #R (1/2)
proof
assume that
A1: Z c= dom (2(#)(( #R (1/2))*(f-cos))) and
A2: for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1;
A3: for x st x in Z holds f.x=0*x+1 by A2;
A4: Z c= dom (( #R (1/2))*(f-cos)) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom (f-cos) by FUNCT_1:11;
then
A5: Z c= dom (f-cos) by TARSKI:def 3;
then Z c= dom cos /\ dom f by VALUED_1:12;
then
A6: Z c= dom f by XBOOLE_1:18;
then
A7: f is_differentiable_on Z by A3,FDIFF_1:23;
A8: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A9: f-cos is_differentiable_on Z by A5,A7,FDIFF_1:19;
A10: for x st x in Z holds (f-cos).x>0
proof
let x;
assume
A11: x in Z;
then cos.x<1 by A2;
then
A12: 1-cos.x>1-1 by XREAL_1:15;
(f-cos).x=f.x-cos.x by A5,A11,VALUED_1:13
.=1-cos.x by A2,A11;
hence thesis by A12;
end;
now
let x;
assume x in Z;
then f-cos is_differentiable_in x & (f-cos).x >0 by A9,A10,FDIFF_1:9;
hence ( #R (1/2))*(f-cos) is_differentiable_in x by TAYLOR_1:22;
end;
then
A13: ( #R (1/2))*(f-cos) is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds ((2(#)(( #R (1/2))*(f-cos)))`|Z).x =(1+cos.x) #R (1/2)
proof
let x;
assume
A14: x in Z;
then
A15: diff((f-cos),x)=((f-cos)`|Z).x by A9,FDIFF_1:def 7
.=diff(f,x)-diff(cos,x) by A5,A7,A8,A14,FDIFF_1:19
.=(f`|Z).x-diff(cos,x) by A7,A14,FDIFF_1:def 7
.=0- diff(cos,x) by A6,A3,A14,FDIFF_1:23
.=0-(-sin.x) by SIN_COS:63
.=sin.x;
A16: cos.x>-1 by A2,A14;
A17: (f-cos).x=f.x-cos.x by A5,A14,VALUED_1:13
.=1-cos.x by A2,A14;
A18: f-cos is_differentiable_in x & (f-cos).x >0 by A9,A10,A14,FDIFF_1:9;
A19: sin.x>0 & cos.x<1 by A2,A14;
((2(#)(( #R (1/2))*(f-cos)))`|Z).x =2*diff((( #R (1/2))*(f-cos)),x)
by A1,A13,A14,FDIFF_1:20
.=2*((1/2)*( ((f-cos).x) #R (1/2-1)) * diff((f-cos),x)) by A18,
TAYLOR_1:22
.=sin.x*((1-cos.x) #R (-1/2)) by A17,A15
.=sin.x*(1 / (1-cos.x) #R (1/2)) by A10,A14,A17,PREPOWER:76
.=sin.x/(1-cos.x) #R (1/2) by XCMPLX_1:99
.=(1+cos.x) #R (1/2) by A19,A16,Lm4;
hence thesis;
end;
hence thesis by A1,A13,FDIFF_1:20;
end;
theorem
Z c= dom ((-2)(#)(( #R (1/2))*(f+cos))) & (for x st x in Z holds f.x=1
& sin.x>0 & cos.x<1 & cos.x>-1) implies (-2)(#)(( #R (1/2))*(f+cos))
is_differentiable_on Z & for x st x in Z holds (((-2)(#)(( #R (1/2))*(f+cos)))
`|Z).x =(1-cos.x) #R (1/2)
proof
assume that
A1: Z c= dom ((-2)(#)(( #R (1/2))*(f+cos))) and
A2: for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1;
A3: for x st x in Z holds f.x=0*x+1 by A2;
A4: Z c= dom (( #R (1/2))*(f+cos)) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom (f+cos) by FUNCT_1:11;
then
A5: Z c= dom (f+cos) by TARSKI:def 3;
then Z c= dom cos /\ dom f by VALUED_1:def 1;
then
A6: Z c= dom f by XBOOLE_1:18;
then
A7: f is_differentiable_on Z by A3,FDIFF_1:23;
A8: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A9: f+cos is_differentiable_on Z by A5,A7,FDIFF_1:18;
A10: for x st x in Z holds (f+cos).x>0
proof
let x;
assume
A11: x in Z;
then cos.x>-1 by A2;
then
A12: 1+cos.x>1+-1 by XREAL_1:8;
(f+cos).x=f.x+cos.x by A5,A11,VALUED_1:def 1
.=1+cos.x by A2,A11;
hence thesis by A12;
end;
now
let x;
assume x in Z;
then f+cos is_differentiable_in x & (f+cos).x >0 by A9,A10,FDIFF_1:9;
hence ( #R (1/2))*(f+cos) is_differentiable_in x by TAYLOR_1:22;
end;
then
A13: ( #R (1/2))*(f+cos) is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds (((-2)(#)(( #R (1/2))*(f+cos)))`|Z).x =(1-cos.x)
#R (1/2)
proof
let x;
assume
A14: x in Z;
then
A15: diff((f+cos),x)=((f+cos)`|Z).x by A9,FDIFF_1:def 7
.=diff(f,x)+diff(cos,x) by A5,A7,A8,A14,FDIFF_1:18
.=(f`|Z).x+diff(cos,x) by A7,A14,FDIFF_1:def 7
.=0+diff(cos,x) by A6,A3,A14,FDIFF_1:23
.=-sin.x by SIN_COS:63;
A16: cos.x>-1 by A2,A14;
A17: (f+cos).x=f.x+cos.x by A5,A14,VALUED_1:def 1
.=1+cos.x by A2,A14;
A18: f+cos is_differentiable_in x & (f+cos).x >0 by A9,A10,A14,FDIFF_1:9;
A19: sin.x>0 & cos.x<1 by A2,A14;
(((-2)(#)(( #R (1/2))*(f+cos)))`|Z).x =(-2)*diff((( #R (1/2))*(f+cos)
),x) by A1,A13,A14,FDIFF_1:20
.=(-2)*((1/2)*( ((f+cos).x) #R (1/2-1)) * diff((f+cos),x)) by A18,
TAYLOR_1:22
.=--sin.x*((1+cos.x) #R (-1/2)) by A17,A15
.=sin.x*(1/(1+cos.x) #R (1/2)) by A10,A14,A17,PREPOWER:76
.=sin.x/(1+cos.x) #R (1/2) by XCMPLX_1:99
.=(1-cos.x) #R (1/2) by A19,A16,Lm5;
hence thesis;
end;
hence thesis by A1,A13,FDIFF_1:20;
end;
:: 41 f.x=1/2*ln(1+2*sin.x)
Lm6: Z c= dom (f1+2(#)sin) & (for x st x in Z holds f1.x=1) implies f1+2(#)sin
is_differentiable_on Z & for x st x in Z holds ((f1+2(#)sin)`|Z).x =2*cos.x
proof
assume that
A1: Z c= dom (f1+2(#)sin) and
A2: for x st x in Z holds f1.x=1;
A3: Z c= dom f1 /\ dom (2(#)sin) by A1,VALUED_1:def 1;
then
A4: Z c= dom f1 by XBOOLE_1:18;
A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
A6: for x st x in Z holds f1.x=0*x+1 by A2;
then
A7: f1 is_differentiable_on Z by A4,FDIFF_1:23;
Z c= dom (2(#)sin) by A3,XBOOLE_1:18;
then
A8: 2(#)sin is_differentiable_on Z by A5,FDIFF_1:20;
for x st x in Z holds ((f1+2(#)sin)`|Z).x = 2*cos.x
proof
let x;
A9: sin is_differentiable_in x by SIN_COS:64;
assume
A10: x in Z;
then ((f1+2(#)sin)`|Z).x =diff(f1,x) + diff(2(#)sin,x) by A1,A7,A8,
FDIFF_1:18
.=(f1`|Z).x+ diff(2(#)sin,x) by A7,A10,FDIFF_1:def 7
.=(f1`|Z).x+2*diff(sin,x) by A9,FDIFF_1:15
.=0+2*diff(sin,x) by A4,A6,A10,FDIFF_1:23
.=2*cos.x by SIN_COS:64;
hence thesis;
end;
hence thesis by A1,A7,A8,FDIFF_1:18;
end;
theorem
Z c= dom ((1/2)(#)(ln*f)) & f=f1+2(#)sin & (for x st x in Z holds f1.x
=1 & f.x >0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z
holds (((1/2)(#)(ln*f))`|Z).x =cos.x/(1+2*sin.x)
proof
assume that
A1: Z c= dom ((1/2)(#)(ln*f)) and
A2: f=f1+2(#)sin and
A3: for x st x in Z holds f1.x=1 & f.x >0;
A4: Z c= dom (ln*f) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A5: Z c= dom (f1+2(#)sin) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=1 by A3;
then
A7: f is_differentiable_on Z by A2,A5,Lm6;
for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A3,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom f1 /\ dom (2(#)sin) by A5,VALUED_1:def 1;
then
A9: Z c= dom (2(#)sin) by XBOOLE_1:18;
for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =cos.x/(1+2*sin.x)
proof
let x;
assume
A10: x in Z;
then
A11: f.x=f1.x+(2(#)sin).x by A2,A5,VALUED_1:def 1
.=1+(2(#)sin).x by A3,A10
.=1+2*sin.x by A9,A10,VALUED_1:def 5;
A12: f is_differentiable_in x & f.x>0 by A3,A7,A10,FDIFF_1:9;
(((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A8,A10,FDIFF_1:20
.=(1/2)*(diff(f,x)/(f.x)) by A12,TAYLOR_1:20
.=(1/2)*((f`|Z).x/(f.x)) by A7,A10,FDIFF_1:def 7
.=(1/2)*((2*cos.x)/(f.x)) by A2,A6,A5,A10,Lm6
.=(1/2)*(2*cos.x)/(f.x) by XCMPLX_1:74
.=cos.x/(1+2*sin.x) by A11;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:20;
end;
:: 42 f.x=(-1/2)*ln(1+2*cos.x)
Lm7: Z c= dom (f1+2(#)cos) & (for x st x in Z holds f1.x=1) implies f1+2(#)cos
is_differentiable_on Z & for x st x in Z holds ((f1+2(#)cos)`|Z).x =-2*sin.x
proof
assume that
A1: Z c= dom (f1+2(#)cos) and
A2: for x st x in Z holds f1.x=1;
A3: Z c= dom f1 /\ dom (2(#)cos) by A1,VALUED_1:def 1;
then
A4: Z c= dom f1 by XBOOLE_1:18;
A5: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
A6: for x st x in Z holds f1.x=0*x+1 by A2;
then
A7: f1 is_differentiable_on Z by A4,FDIFF_1:23;
Z c= dom (2(#)cos) by A3,XBOOLE_1:18;
then
A8: 2(#)cos is_differentiable_on Z by A5,FDIFF_1:20;
for x st x in Z holds ((f1+2(#)cos)`|Z).x = -2*sin.x
proof
let x;
A9: cos is_differentiable_in x by SIN_COS:63;
assume
A10: x in Z;
then ((f1+2(#)cos)`|Z).x =diff(f1,x) + diff(2(#)cos,x) by A1,A7,A8,
FDIFF_1:18
.=(f1`|Z).x+ diff(2(#)cos,x) by A7,A10,FDIFF_1:def 7
.=(f1`|Z).x+2*diff(cos,x) by A9,FDIFF_1:15
.=0+2*diff(cos,x) by A4,A6,A10,FDIFF_1:23
.=0+2*(-sin.x) by SIN_COS:63
.=-2*sin.x;
hence thesis;
end;
hence thesis by A1,A7,A8,FDIFF_1:18;
end;
theorem
Z c= dom ((-1/2)(#)(ln*f)) & f=f1+2(#)cos & (for x st x in Z holds f1.
x=1 & f.x >0) implies (-1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z
holds (((-1/2)(#)(ln*f))`|Z).x =sin.x/(1+2*cos.x)
proof
assume that
A1: Z c= dom ((-1/2)(#)(ln*f)) and
A2: f=f1+2(#)cos and
A3: for x st x in Z holds f1.x=1 & f.x >0;
A4: Z c= dom (ln*f) by A1,VALUED_1:def 5;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A5: Z c= dom (f1+2(#)cos) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=1 by A3;
then
A7: f is_differentiable_on Z by A2,A5,Lm7;
for x st x in Z holds ln*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A3,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9;
Z c= dom f1 /\ dom (2(#)cos) by A5,VALUED_1:def 1;
then
A9: Z c= dom (2(#)cos) by XBOOLE_1:18;
for x st x in Z holds (((-1/2)(#)(ln*f))`|Z).x =sin.x/(1+2*cos.x)
proof
let x;
assume
A10: x in Z;
then
A11: f.x=f1.x+(2(#)cos).x by A2,A5,VALUED_1:def 1
.=1+(2(#)cos).x by A3,A10
.=1+2*cos.x by A9,A10,VALUED_1:def 5;
A12: f is_differentiable_in x & f.x>0 by A3,A7,A10,FDIFF_1:9;
(((-1/2)(#)(ln*f))`|Z).x =(-1/2)*diff((ln*f),x) by A1,A8,A10,FDIFF_1:20
.=(-1/2)*(diff(f,x)/(f.x)) by A12,TAYLOR_1:20
.=(-1/2)*((f`|Z).x/(f.x)) by A7,A10,FDIFF_1:def 7
.=(-1/2)*((-2*sin.x)/(f.x)) by A2,A6,A5,A10,Lm7
.=(-1/2)*(-2*sin.x)/(f.x) by XCMPLX_1:74
.=sin.x/(1+2*cos.x) by A11;
hence thesis;
end;
hence thesis by A1,A8,FDIFF_1:20;
end;
:: 43 f.x=1/(4*a)*sin(2*a*x)
theorem Th43:
Z c= dom ((1/(4*a))(#)(sin*f)) & (for x st x in Z holds f.x=2*a*
x) & a<>0 implies (1/(4*a))(#)(sin*f) is_differentiable_on Z & for x st x in Z
holds (((1/(4*a))(#)(sin*f))`|Z).x =1/2 * cos(2*a*x)
proof
assume that
A1: Z c= dom ((1/(4*a))(#)(sin*f)) and
A2: for x st x in Z holds f.x=2*a*x and
A3: a<>0;
A4: Z c= dom (sin*f) & for x st x in Z holds f.x=(2*a)*x+0 by A1,A2,
VALUED_1:def 5;
then
A5: sin*f is_differentiable_on Z by FDIFF_4:37;
for x st x in Z holds (((1/(4*a))(#)(sin*f))`|Z).x =1/2 * cos(2*a*x)
proof
let x;
assume
A6: x in Z;
then (((1/(4*a))(#)(sin*f))`|Z).x =(1/(4*a))*diff((sin*f),x) by A1,A5,
FDIFF_1:20
.=(1/(4*a))*((sin*f)`|Z).x by A5,A6,FDIFF_1:def 7
.=(1/(4*a))*((2*a)* cos.((2*a)*x+0)) by A4,A6,FDIFF_4:37
.=1/(4*a)*(2*a)* cos.((2*a)*x+0)
.=(1/4)*(1/a)*(2*a)* cos.((2*a)*x) by XCMPLX_1:102
.=(1/4)*2*(1/a*a)* cos.(2*a*x)
.=(1/2)*1*cos.(2*a*x) by A3,XCMPLX_1:106
.=1/2*cos(2*a*x) by SIN_COS:def 19;
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:20;
end;
:: 44 f.x=x/2-1/(4*a)*sin(2*a*x)
theorem
Z c= dom (f1-((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2
& f.x=2*a*x) & a<>0 implies f1-((1/(4*a))(#)(sin*f)) is_differentiable_on Z &
for x st x in Z holds ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =(sin(a*x))^2
proof
assume that
A1: Z c= dom (f1-((1/(4*a))(#)(sin*f))) and
A2: for x st x in Z holds f1.x=x/2 & f.x=2*a*x and
A3: a<>0;
A4: Z c= dom f1 /\ dom ((1/(4*a))(#)(sin*f)) by A1,VALUED_1:12;
then
A5: Z c= dom ((1/(4*a))(#)(sin*f)) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=(1/2)*x+0
proof
let x;
assume x in Z;
then f1.x=x/2 by A2
.= (1/2)*x+0;
hence thesis;
end;
A7: for x st x in Z holds f.x=2*a*x by A2;
then
A8: (1/(4*a))(#)(sin*f) is_differentiable_on Z by A3,A5,Th43;
A9: Z c= dom f1 by A4,XBOOLE_1:18;
then
A10: f1 is_differentiable_on Z by A6,FDIFF_1:23;
for x st x in Z holds ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =(sin(a*x))^2
proof
let x;
assume
A11: x in Z;
then
((f1-((1/(4*a))(#)(sin*f)))`|Z).x =diff(f1,x)-diff(((1/(4*a))(#)(sin*
f)),x) by A1,A8,A10,FDIFF_1:19
.=(f1`|Z).x-diff(((1/(4*a))(#)(sin*f)),x) by A10,A11,FDIFF_1:def 7
.=(f1`|Z).x-(((1/(4*a))(#)(sin*f))`|Z).x by A8,A11,FDIFF_1:def 7
.=(f1`|Z).x-1/2 * cos(2*a*x) by A3,A7,A5,A11,Th43
.=1/2-1/2 * cos(2*a*x) by A9,A6,A11,FDIFF_1:23
.=(1/2)*(1-cos(2*(a*x)))
.=(1/2)*(2*(sin(a*x))^2) by Lm1
.=(sin(a*x))^2;
hence thesis;
end;
hence thesis by A1,A8,A10,FDIFF_1:19;
end;
:: 45 f.x=x/2+1/(4*a)*sin(2*a*x)
theorem
Z c= dom (f1+((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2
& f.x=2*a*x) & a<>0 implies f1+((1/(4*a))(#)(sin*f)) is_differentiable_on Z &
for x st x in Z holds ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =(cos(a*x))^2
proof
assume that
A1: Z c= dom (f1+((1/(4*a))(#)(sin*f))) and
A2: for x st x in Z holds f1.x=x/2 & f.x=2*a*x and
A3: a<>0;
A4: Z c= dom f1 /\ dom ((1/(4*a))(#)(sin*f)) by A1,VALUED_1:def 1;
then
A5: Z c= dom ((1/(4*a))(#)(sin*f)) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=(1/2)*x+0
proof
let x;
assume x in Z;
then f1.x=x/2 by A2
.= (1/2)*x+0;
hence thesis;
end;
A7: for x st x in Z holds f.x=2*a*x by A2;
then
A8: (1/(4*a))(#)(sin*f) is_differentiable_on Z by A3,A5,Th43;
A9: Z c= dom f1 by A4,XBOOLE_1:18;
then
A10: f1 is_differentiable_on Z by A6,FDIFF_1:23;
for x st x in Z holds ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =(cos(a*x))^2
proof
let x;
assume
A11: x in Z;
then
((f1+((1/(4*a))(#)(sin*f)))`|Z).x =diff(f1,x)+diff(((1/(4*a))(#)(sin*
f)),x) by A1,A8,A10,FDIFF_1:18
.=(f1`|Z).x+diff(((1/(4*a))(#)(sin*f)),x) by A10,A11,FDIFF_1:def 7
.=(f1`|Z).x+(((1/(4*a))(#)(sin*f))`|Z).x by A8,A11,FDIFF_1:def 7
.=(f1`|Z).x+1/2 * cos(2*a*x) by A3,A7,A5,A11,Th43
.=1/2+1/2 * cos(2*a*x) by A9,A6,A11,FDIFF_1:23
.=(1/2)*(1+cos(2*(a*x)))
.=(1/2)*(2*(cos(a*x))^2) by Lm2
.=(cos(a*x))^2;
hence thesis;
end;
hence thesis by A1,A8,A10,FDIFF_1:18;
end;
:: 46 f.x=(1/n)*(cos.x ^ n)
theorem Th46:
Z c= dom ((1/n)(#)(( #Z n)*cos)) & n>0 implies (1/n)(#)(( #Z n)*
cos) is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*cos))`|Z
).x =-(cos.x) #Z (n-1)*sin.x
proof
assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*cos)) and
A2: n>0;
A3: 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;
Z c= dom (( #Z n)*cos) by A1,VALUED_1:def 5;
then
A4: ( #Z n)*cos is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((1/n)(#)(( #Z n)*cos))`|Z).x =-(cos.x) #Z (n-1)
*sin.x
proof
let x;
A5: cos is_differentiable_in x by SIN_COS:63;
assume x in Z;
then
(((1/n)(#)(( #Z n)*cos))`|Z).x =(1/n)*diff((( #Z n)*cos),x) by A1,A4,
FDIFF_1:20
.=(1/n)*(n*( (cos.x) #Z (n-1)) * diff(cos,x)) by A5,TAYLOR_1:3
.=(1/n)*(n*( (cos.x) #Z (n-1)) *(-sin.x)) by SIN_COS:63
.=((1/n)*n)*( (cos.x) #Z (n-1)) *(-sin.x)
.=((n")*n)*( (cos.x) #Z (n-1)) *(-sin.x) by XCMPLX_1:215
.=1*( (cos.x) #Z (n-1)) *(-sin.x) by A2,XCMPLX_0:def 7
.=-(cos.x) #Z (n-1) *sin.x;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
:: 47 f.x=(1/3)*(cos.x ^ 3)-cos.x
theorem
Z c= dom (((1/3)(#)(( #Z 3)*cos))-cos) implies (1/3)(#)(( #Z 3)*cos)-
cos is_differentiable_on Z & for x st x in Z holds ((((1/3)(#)(( #Z 3)*cos))-
cos)`|Z).x =(sin.x)|^3
proof
assume
A1: Z c= dom (((1/3)(#)(( #Z 3)*cos))-cos);
then Z c= dom ((1/3)(#)(( #Z 3)*cos)) /\ dom cos by VALUED_1:12;
then
A2: Z c= dom ((1/3)(#)(( #Z 3)*cos)) by XBOOLE_1:18;
then
A3: ((1/3)(#)(( #Z 3)*cos)) is_differentiable_on Z by Th46;
A4: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
now
let x;
assume
A5: x in Z;
then
((((1/3)(#)(( #Z 3)*cos))-cos)`|Z).x = diff(((1/3)(#)(( #Z 3)*cos)),x
) - diff(cos,x) by A1,A3,A4,FDIFF_1:19
.=diff(((1/3)(#)(( #Z 3)*cos)),x)-(-sin.x) by SIN_COS:63
.=(((1/3)(#)(( #Z 3)*cos))`|Z).x-(-sin.x) by A3,A5,FDIFF_1:def 7
.=-(cos.x) #Z (3-1)*sin.x--sin.x by A2,A5,Th46
.=sin.x*(1-(cos.x) #Z 2 )
.=sin.x*(1-(cos.x) |^ |.2.| ) by PREPOWER:def 3
.=sin.x*(1-(cos.x) |^ 2 ) by ABSVALUE:def 1
.=sin.x*(1-(cos.x)*(cos.x)) by WSIERP_1:1
.=sin.x*((cos.x)*(cos.x)+(sin.x)*(sin.x)-(cos.x)*(cos.x)) by SIN_COS:28
.=sin.x*((sin.x)|^2) by WSIERP_1:1
.=((sin.x)|^(2+1)) by NEWTON:6
.=(sin.x)|^3;
hence ((((1/3)(#)(( #Z 3)*cos))-cos)`|Z).x =(sin.x)|^3;
end;
hence thesis by A1,A3,A4,FDIFF_1:19;
end;
:: 48 f.x=sin.x-(1/3)*(sin.x ^ 3)
theorem
Z c= dom (sin-((1/3)(#)(( #Z 3)*sin))) implies sin-((1/3)(#)(( #Z 3)*
sin)) is_differentiable_on Z & for x st x in Z holds ((sin-((1/3)(#)(( #Z 3)*
sin)))`|Z).x =(cos.x)|^3
proof
assume
A1: Z c= dom (sin-((1/3)(#)(( #Z 3)*sin)));
then Z c= dom ((1/3)(#)(( #Z 3)*sin)) /\ dom sin by VALUED_1:12;
then
A2: Z c= dom ((1/3)(#)(( #Z 3)*sin)) by XBOOLE_1:18;
then
A3: ((1/3)(#)(( #Z 3)*sin)) is_differentiable_on Z by FDIFF_4:54;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A5: x in Z;
then
((sin-((1/3)(#)(( #Z 3)*sin)))`|Z).x = diff(sin,x) - diff(((1/3)(#)((
#Z 3)*sin)),x) by A1,A3,A4,FDIFF_1:19
.=cos.x - diff(((1/3)(#)(( #Z 3)*sin)),x) by SIN_COS:64
.=cos.x -(((1/3)(#)(( #Z 3)*sin))`|Z).x by A3,A5,FDIFF_1:def 7
.=cos.x -((sin.x) #Z (3-1) *cos.x) by A2,A5,FDIFF_4:54
.=cos.x*(1-(sin.x) #Z 2)
.=cos.x*(1-(sin.x) |^ |.2.| ) by PREPOWER:def 3
.=cos.x*(1-(sin.x) |^ 2 ) by ABSVALUE:def 1
.=cos.x*(1-(sin.x)*(sin.x)) by WSIERP_1:1
.=cos.x*((cos.x)*(cos.x)+(sin.x)*(sin.x)-(sin.x)*(sin.x)) by SIN_COS:28
.=cos.x*((cos.x)|^2) by WSIERP_1:1
.=((cos.x)|^(2+1)) by NEWTON:6
.=(cos.x)|^3;
hence ((sin-((1/3)(#)(( #Z 3)*sin)))`|Z).x =(cos.x)|^3;
end;
hence thesis by A1,A3,A4,FDIFF_1:19;
end;
:: 49 f.x=sin(ln x)
theorem
Z c= dom (sin*ln) implies sin*ln is_differentiable_on Z & for x st x
in Z holds ((sin*ln)`|Z).x =cos.(log(number_e,x))/x
proof
assume
A1: Z c= dom (sin*ln);
then for y being object st y in Z holds y in dom ln by FUNCT_1:11;
then
A2: Z c= dom ln by TARSKI:def 3;
then
A3: ln is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:18;
A4: for x st x in Z holds sin*ln is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: ln is_differentiable_in x by A3,FDIFF_1:9;
sin is_differentiable_in ln.x by SIN_COS:64;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: sin*ln is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*ln)`|Z).x =cos.(log(number_e,x))/x
proof
let x;
A7: sin is_differentiable_in ln.x by SIN_COS:64;
assume
A8: x in Z;
then
A9: x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18;
ln is_differentiable_in x by A3,A8,FDIFF_1:9;
then diff(sin*ln,x) = diff(sin,ln.x)*diff(ln,x) by A7,FDIFF_2:13
.=cos.(ln.x)*diff(ln,x) by SIN_COS:64
.=cos.(log(number_e,x))*diff(ln,x) by A9,TAYLOR_1:def 2
.=cos.(log(number_e,x))*(1/x) by A2,A8,TAYLOR_1:18
.=cos.(log(number_e,x))/x by XCMPLX_1:99;
hence thesis by A6,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: 50 f.x=-cos(ln x)
theorem
Z c= dom (-(cos*ln)) implies -(cos*ln) is_differentiable_on Z & for x
st x in Z holds ((-(cos*ln))`|Z).x =sin.(log(number_e,x))/x
proof
assume
A1: Z c= dom (-(cos*ln));
then
A2: Z c= dom (cos*ln) by VALUED_1:8;
then for y being object st y in Z holds y in dom ln by FUNCT_1:11;
then
A3: Z c= dom ln by TARSKI:def 3;
then
A4: ln is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:18;
for x st x in Z holds cos*ln is_differentiable_in x
proof
let x;
assume x in Z;
then
A5: ln is_differentiable_in x by A4,FDIFF_1:9;
cos is_differentiable_in ln.x by SIN_COS:63;
hence thesis by A5,FDIFF_2:13;
end;
then
A6: cos*ln is_differentiable_on Z by A2,FDIFF_1:9;
A7: for x st x in Z holds ((-(cos*ln))`|Z).x =sin.(log(number_e,x))/x
proof
let x;
A8: cos is_differentiable_in ln.x by SIN_COS:63;
assume
A9: x in Z;
then
A10: x in right_open_halfline(0) by A2,FUNCT_1:11,TAYLOR_1:18;
A11: ln is_differentiable_in x by A4,A9,FDIFF_1:9;
((-(cos*ln))`|Z).x =(-1)*diff((cos*ln),x) by A1,A6,A9,FDIFF_1:20
.=(-1)*(diff(cos,ln.x)*diff(ln,x)) by A11,A8,FDIFF_2:13
.=(-1)*((-sin.(ln.x))*diff(ln,x)) by SIN_COS:63
.=(-1)*(-sin.(ln.x))*diff(ln,x)
.=(-1)*(-sin.(log(number_e,x)))*diff(ln,x) by A10,TAYLOR_1:def 2
.=(-1)*(-sin.(log(number_e,x)))*(1/x) by A3,A9,TAYLOR_1:18
.=sin.(log(number_e,x))/x by XCMPLX_1:99;
hence thesis;
end;
Z c= dom ((-1)(#)(cos*ln)) by A1;
hence thesis by A6,A7,FDIFF_1:20;
end;