:: Several Differentiable Formulas of Special Functions
:: by Yan Zhang and Xiquan Liang
::
:: Received July 6, 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, TARSKI, RELAT_1,
TAYLOR_1, FUNCT_1, ARYTM_3, XXREAL_0, CARD_1, FDIFF_1, ARYTM_1, VALUED_1,
XBOOLE_0, PREPOWER, NEWTON, ORDINAL4, SQUARE_1, SIN_COS;
notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, PARTFUN2,
RCOMP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1,
VALUED_1, FDIFF_1, NEWTON, PREPOWER, TAYLOR_1, SIN_COS, RFUNCT_1,
SQUARE_1, SIN_COS4;
constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1,
LIMFUNC1, FDIFF_1, PREPOWER, SIN_COS, SIN_COS4, TAYLOR_1, VALUED_1,
RELSET_1, NEWTON;
registrations RELSET_1, NUMBERS, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0,
PREPOWER, NEWTON, SQUARE_1, SIN_COS;
requirements SUBSET, REAL, NUMERALS, ARITHM;
equalities SQUARE_1, VALUED_1;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FUNCT_1, TARSKI,
PREPOWER, RFUNCT_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS, SIN_COS5,
SIN_COS4, WSIERP_1, VALUED_1;
begin
reserve y for set;
reserve x,a,b,c for Real;
reserve n for Element of NAT;
reserve Z for open Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
:: 1 $f.x=ln(a+x)$
theorem Th1:
Z c= dom (ln*f) & (for x st x in Z holds f.x = a+x & f.x > 0)
implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z).x = 1/(
a+x)
proof
assume that
A1: Z c= dom (ln*f) and
A2: for x st x in Z holds f.x = a+x & f.x > 0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
A4: for x st x in Z holds f.x = 1*x+a by A2;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: 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,A5,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A7: ln*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*f)`|Z).x = 1/(a+x)
proof
let x;
assume
A8: x in Z;
then
A9: f.x = a+x by A2;
f is_differentiable_in x & f.x >0 by A2,A5,A8,FDIFF_1:9;
then diff(ln*f,x) =diff(f,x)/( f.x) by TAYLOR_1:20
.=(f`|Z).x/( f.x) by A5,A8,FDIFF_1:def 7
.=1/(a+x) by A3,A4,A8,A9,FDIFF_1:23;
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: 2 $f.x=ln(x-a)$
theorem Th2:
Z c= dom (ln*f) & (for x st x in Z holds f.x = x-a & f.x >0)
implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z).x = 1/(
x-a)
proof
assume that
A1: Z c= dom (ln*f) and
A2: for x st x in Z holds f.x = x-a & f.x >0;
A3: for x st x in Z holds f.x = 1*x+-a
proof
let x;
A4: 1*x+-a=1*x-a;
assume x in Z;
hence thesis by A2,A4;
end;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A5: Z c= dom f by TARSKI:def 3;
then
A6: f is_differentiable_on Z by A3,FDIFF_1:23;
A7: 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,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A8: ln*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*f)`|Z).x = 1/(x-a)
proof
let x;
assume
A9: x in Z;
then
A10: f.x = x-a by A2;
f is_differentiable_in x & f.x >0 by A2,A6,A9,FDIFF_1:9;
then diff(ln*f,x) =diff(f,x)/( f.x) by TAYLOR_1:20
.=(f`|Z).x/( f.x) by A6,A9,FDIFF_1:def 7
.=1/(x-a) by A5,A3,A9,A10,FDIFF_1:23;
hence thesis by A8,A9,FDIFF_1:def 7;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 3 $f.x=-ln(a-x)$
theorem
Z c= dom (-(ln*f)) & (for x st x in Z holds f.x =a-x & f.x >0) implies
- (ln*f) is_differentiable_on Z & for x st x in Z holds ((-(ln*f))`|Z).x = 1/(a
-x)
proof
assume that
A1: Z c= dom (-(ln*f)) and
A2: for x st x in Z holds f.x =a-x & f.x > 0;
now
let y be object;
assume y in Z;
then y in dom ( (-1)(#)(ln*f)) by A1;
hence y in dom (ln*f) by VALUED_1:def 5;
end;
then
A3: Z c=dom (ln*f) by TARSKI:def 3;
then for y being object st y in Z holds y in dom f by FUNCT_1:11;
then
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x =(-1)*x+a
proof
let x;
assume x in Z;
then f.x =a-x by A2;
hence thesis;
end;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ln*f is_differentiable_in x by TAYLOR_1:20;
end;
then
A7: ln*f is_differentiable_on Z by A3,FDIFF_1:9;
A8: for x st x in Z holds ((-(ln*f))`|Z).x =1/(a-x)
proof
let x;
assume
A9: x in Z;
then
A10: f.x =a-x by A2;
f.x >0 & f is_differentiable_in x by A2,A6,A9,FDIFF_1:9;
then diff(ln*f,x) =diff(f,x)/( f.x) by TAYLOR_1:20
.=(f`|Z).x/( f.x) by A6,A9,FDIFF_1:def 7
.=(-1)/(a-x) by A4,A5,A9,A10,FDIFF_1:23;
then (((-1)(#)(ln*f))`|Z).x =(-1)*((-1)/(a-x)) by A1,A7,A9,FDIFF_1:20
.=(-1)*(-1)/(a-x) by XCMPLX_1:74
.=1/(a-x);
hence thesis;
end;
Z c= dom ((-1)(#)(ln*f)) by A1;
hence thesis by A7,A8,FDIFF_1:20;
end;
:: 4 f.x=x-a*ln(a+x)
theorem
Z c= dom (id Z - a(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=a+x
& f1.x>0) implies (id Z - a(#)f) is_differentiable_on Z & for x st x in Z holds
((id Z - a(#)f)`|Z).x = x/(a+x)
proof
assume that
A1: Z c= dom (id Z - a(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=a+x & f1.x>0;
A4: Z c= dom id Z /\ dom (a(#)f) by A1,VALUED_1:12;
then
A5: Z c= dom (a(#)f) by XBOOLE_1:18;
then
A6: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A7: f is_differentiable_on Z by A2,A3,Th1;
then
A8: a(#)f is_differentiable_on Z by A5,FDIFF_1:20;
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom id Z by A4,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds ((a(#)f)`|Z).x =a/(a+x)
proof
let x;
assume
A13: x in Z;
hence ((a(#)f)`|Z).x=a*diff(f,x) by A5,A7,FDIFF_1:20
.=a*(f`|Z).x by A7,A13,FDIFF_1:def 7
.=a*(1/(a+x)) by A2,A3,A6,A13,Th1
.=a/(a+x) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z - a(#)f)`|Z).x = x/(a+x)
proof
let x;
assume
A14: x in Z;
then
A15: f1.x=a+x & f1.x>0 by A3;
((id Z - a(#)f)`|Z).x= diff(id Z,x) - diff(a(#)f,x) by A1,A11,A8,A14,
FDIFF_1:19
.=((id Z)`|Z).x - diff(a(#)f,x) by A11,A14,FDIFF_1:def 7
.=((id Z)`|Z).x - ((a(#)f)`|Z).x by A8,A14,FDIFF_1:def 7
.=1 - ((a(#)f)`|Z).x by A10,A9,A14,FDIFF_1:23
.=1 - a/(a+x) by A12,A14
.=(1*(a+x) - a)/(a+x) by A15,XCMPLX_1:127
.=x/(a+x);
hence thesis;
end;
hence thesis by A1,A11,A8,FDIFF_1:19;
end;
:: 5 f.x=(2*a)*ln(a+x)-x
theorem
Z c= dom ((2*a)(#)f - id Z) & f = ln*f1 & (for x st x in Z holds f1.x=
a+x & f1.x>0) implies ((2*a)(#)f - id Z) is_differentiable_on Z & for x st x in
Z holds (((2*a)(#)f - id Z)`|Z).x = (a-x)/(a+x)
proof
assume that
A1: Z c= dom ((2*a)(#)f - id Z) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=a+x & f1.x>0;
A4: Z c= dom ((2*a)(#)f) /\ dom id Z by A1,VALUED_1:12;
then
A5: Z c= dom ((2*a)(#)f) by XBOOLE_1:18;
then
A6: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A7: f is_differentiable_on Z by A2,A3,Th1;
then
A8: (2*a)(#)f is_differentiable_on Z by A5,FDIFF_1:20;
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom id Z by A4,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds (((2*a)(#)f)`|Z).x =(2*a)/(a+x)
proof
let x;
assume
A13: x in Z;
hence (((2*a)(#)f)`|Z).x =(2*a)*diff(f,x) by A5,A7,FDIFF_1:20
.=(2*a)*(f`|Z).x by A7,A13,FDIFF_1:def 7
.=(2*a)*(1/(a+x)) by A2,A3,A6,A13,Th1
.=(2*a)/(a+x) by XCMPLX_1:99;
end;
for x st x in Z holds (((2*a)(#)f - id Z)`|Z).x =(a-x)/(a+x)
proof
let x;
assume
A14: x in Z;
then
A15: f1.x=a+x & f1.x>0 by A3;
(((2*a)(#)f - id Z)`|Z).x = diff((2*a)(#)f,x) - diff(id Z,x) by A1,A11,A8
,A14,FDIFF_1:19
.=diff((2*a)(#)f,x)-((id Z)`|Z).x by A11,A14,FDIFF_1:def 7
.=(((2*a)(#)f)`|Z).x-((id Z)`|Z).x by A8,A14,FDIFF_1:def 7
.=(((2*a)(#)f)`|Z).x - 1 by A10,A9,A14,FDIFF_1:23
.=(2*a)/(a+x) - 1 by A12,A14
.=(2*a-1*(a+x))/(a+x) by A15,XCMPLX_1:126
.=(a-x)/(a+x);
hence thesis;
end;
hence thesis by A1,A11,A8,FDIFF_1:19;
end;
:: 6 f.x=x-(2*a)*ln(x+a)
theorem
Z c= dom (id Z - (2*a)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x+a & f1.x>0) implies (id Z - (2*a)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z -(2*a)(#)f)`|Z).x = (x-a)/(x+a)
proof
assume that
A1: Z c= dom (id Z - (2*a)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x+a & f1.x>0;
A4: for x st x in Z holds f1.x=a+x & f1.x>0 by A3;
A5: Z c= dom id Z /\ dom ((2*a)(#)f) by A1,VALUED_1:12;
then
A6: Z c= dom ((2*a)(#)f) by XBOOLE_1:18;
then
A7: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A8: f is_differentiable_on Z by A2,A4,Th1;
then
A9: (2*a)(#)f is_differentiable_on Z by A6,FDIFF_1:20;
A10: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A11: Z c= dom id Z by A5,XBOOLE_1:18;
then
A12: id Z is_differentiable_on Z by A10,FDIFF_1:23;
A13: for x st x in Z holds (((2*a)(#)f)`|Z).x =(2*a)/(x+a)
proof
let x;
assume
A14: x in Z;
hence (((2*a)(#)f)`|Z).x =(2*a)*diff(f,x) by A6,A8,FDIFF_1:20
.=(2*a)*(f`|Z).x by A8,A14,FDIFF_1:def 7
.=(2*a)*(1/(x+a)) by A2,A7,A4,A14,Th1
.=(2*a)/(x+a) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z - (2*a)(#)f)`|Z).x = (x-a)/(x+a)
proof
let x;
assume
A15: x in Z;
then
A16: f1.x=x+a & f1.x>0 by A3;
((id Z - (2*a)(#)f)`|Z).x = diff(id Z,x) - diff((2*a)(#)f,x) by A1,A12,A9
,A15,FDIFF_1:19
.=((id Z)`|Z).x - diff((2*a)(#)f,x) by A12,A15,FDIFF_1:def 7
.=((id Z)`|Z).x - (((2*a)(#)f)`|Z).x by A9,A15,FDIFF_1:def 7
.=1 - (((2*a)(#)f)`|Z).x by A11,A10,A15,FDIFF_1:23
.=1 - (2*a)/(x+a) by A13,A15
.=(1*(x+a) - (2*a))/(x+a) by A16,XCMPLX_1:127
.=(x-a)/(x+a);
hence thesis;
end;
hence thesis by A1,A12,A9,FDIFF_1:19;
end;
:: 7 f.x=x + (2*a)*ln(x-a)
theorem
Z c= dom (id Z + (2*a)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x-a & f1.x>0) implies (id Z + (2*a)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z +(2*a)(#)f)`|Z).x = (x+a)/(x-a)
proof
assume that
A1: Z c= dom (id Z + (2*a)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x-a & f1.x>0;
A4: Z c= dom id Z /\ dom ((2*a)(#)f) by A1,VALUED_1:def 1;
then
A5: Z c= dom ((2*a)(#)f) by XBOOLE_1:18;
then
A6: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A7: f is_differentiable_on Z by A2,A3,Th2;
then
A8: (2*a)(#)f is_differentiable_on Z by A5,FDIFF_1:20;
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom id Z by A4,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds (((2*a)(#)f)`|Z).x =(2*a)/(x-a)
proof
let x;
assume
A13: x in Z;
hence (((2*a)(#)f)`|Z).x =(2*a)*diff(f,x) by A5,A7,FDIFF_1:20
.=(2*a)*(f`|Z).x by A7,A13,FDIFF_1:def 7
.=(2*a)*(1/(x-a)) by A2,A3,A6,A13,Th2
.=(2*a)/(x-a) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z + (2*a)(#)f)`|Z).x = (x+a)/(x-a)
proof
let x;
assume
A14: x in Z;
then
A15: f1.x=x-a & f1.x>0 by A3;
((id Z + (2*a)(#)f)`|Z).x = diff(id Z,x) + diff((2*a)(#)f,x) by A1,A11,A8
,A14,FDIFF_1:18
.=((id Z)`|Z).x + diff((2*a)(#)f,x) by A11,A14,FDIFF_1:def 7
.=((id Z)`|Z).x + (((2*a)(#)f)`|Z).x by A8,A14,FDIFF_1:def 7
.=1 + (((2*a)(#)f)`|Z).x by A10,A9,A14,FDIFF_1:23
.=1 + (2*a)/(x-a) by A12,A14
.=(1*(x-a) + (2*a))/(x-a) by A15,XCMPLX_1:113
.=(x+a)/(x-a);
hence thesis;
end;
hence thesis by A1,A11,A8,FDIFF_1:18;
end;
:: 8 f.x=x+ (a-b)*ln(x+b)
theorem
Z c= dom (id Z + (a-b)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x+b & f1.x>0) implies (id Z + (a-b)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z +(a-b)(#)f)`|Z).x = (x+a)/(x+b)
proof
assume that
A1: Z c= dom (id Z + (a-b)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x+b & f1.x>0;
A4: for x st x in Z holds f1.x=b+x & f1.x>0 by A3;
A5: Z c= dom id Z /\ dom ((a-b)(#)f) by A1,VALUED_1:def 1;
then
A6: Z c= dom ((a-b)(#)f) by XBOOLE_1:18;
then
A7: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A8: f is_differentiable_on Z by A2,A4,Th1;
then
A9: (a-b)(#)f is_differentiable_on Z by A6,FDIFF_1:20;
A10: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A11: Z c= dom id Z by A5,XBOOLE_1:18;
then
A12: id Z is_differentiable_on Z by A10,FDIFF_1:23;
A13: for x st x in Z holds (((a-b)(#)f)`|Z).x =(a-b)/(x+b)
proof
let x;
assume
A14: x in Z;
hence (((a-b)(#)f)`|Z).x =(a-b)*diff(f,x) by A6,A8,FDIFF_1:20
.=(a-b)*(f`|Z).x by A8,A14,FDIFF_1:def 7
.=(a-b)*(1/(x+b)) by A2,A7,A4,A14,Th1
.=(a-b)/(x+b) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z + (a-b)(#)f)`|Z).x = (x+a)/(x+b)
proof
let x;
assume
A15: x in Z;
then
A16: f1.x=x+b & f1.x>0 by A3;
((id Z + (a-b)(#)f)`|Z).x = diff(id Z,x) + diff((a-b)(#)f,x) by A1,A12,A9
,A15,FDIFF_1:18
.=((id Z)`|Z).x + diff((a-b)(#)f,x) by A12,A15,FDIFF_1:def 7
.=((id Z)`|Z).x + (((a-b)(#)f)`|Z).x by A9,A15,FDIFF_1:def 7
.=1 + (((a-b)(#)f)`|Z).x by A11,A10,A15,FDIFF_1:23
.=1 + (a-b)/(x+b) by A13,A15
.=(1*(x+b) + (a-b))/(x+b) by A16,XCMPLX_1:113
.=(x+a)/(x+b);
hence thesis;
end;
hence thesis by A1,A12,A9,FDIFF_1:18;
end;
:: 9 f.x=x+ (a+b)*ln(x-b)
theorem
Z c= dom (id Z + (a+b)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x-b & f1.x>0) implies (id Z + (a+b)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z +(a+b)(#)f)`|Z).x = (x+a)/(x-b)
proof
assume that
A1: Z c= dom (id Z + (a+b)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x-b & f1.x>0;
A4: Z c= dom id Z /\ dom ((a+b)(#)f) by A1,VALUED_1:def 1;
then
A5: Z c= dom ((a+b)(#)f) by XBOOLE_1:18;
then
A6: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A7: f is_differentiable_on Z by A2,A3,Th2;
then
A8: (a+b)(#)f is_differentiable_on Z by A5,FDIFF_1:20;
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom id Z by A4,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds (((a+b)(#)f)`|Z).x =(a+b)/(x-b)
proof
let x;
assume
A13: x in Z;
hence (((a+b)(#)f)`|Z).x =(a+b)*diff(f,x) by A5,A7,FDIFF_1:20
.=(a+b)*(f`|Z).x by A7,A13,FDIFF_1:def 7
.=(a+b)*(1/(x-b)) by A2,A3,A6,A13,Th2
.=(a+b)/(x-b) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z + (a+b)(#)f)`|Z).x = (x+a)/(x-b)
proof
let x;
assume
A14: x in Z;
then
A15: f1.x=x-b & f1.x>0 by A3;
((id Z + (a+b)(#)f)`|Z).x = diff(id Z,x) + diff((a+b)(#)f,x) by A1,A11,A8
,A14,FDIFF_1:18
.=((id Z)`|Z).x + diff((a+b)(#)f,x) by A11,A14,FDIFF_1:def 7
.=((id Z)`|Z).x + (((a+b)(#)f)`|Z).x by A8,A14,FDIFF_1:def 7
.=1 + (((a+b)(#)f)`|Z).x by A10,A9,A14,FDIFF_1:23
.=1 + (a+b)/(x-b) by A12,A14
.=(1*(x-b) + (a+b))/(x-b) by A15,XCMPLX_1:113
.=(x+a)/(x-b);
hence thesis;
end;
hence thesis by A1,A11,A8,FDIFF_1:18;
end;
:: 10 f.x=x- (a+b)*ln(x+b)
theorem
Z c= dom (id Z - (a+b)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x+b & f1.x>0) implies (id Z - (a+b)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z -(a+b)(#)f)`|Z).x = (x-a)/(x+b)
proof
assume that
A1: Z c= dom (id Z - (a+b)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x+b & f1.x>0;
A4: for x st x in Z holds f1.x=b+x & f1.x>0 by A3;
A5: Z c= dom id Z /\ dom ((a+b)(#)f) by A1,VALUED_1:12;
then
A6: Z c= dom ((a+b)(#)f) by XBOOLE_1:18;
then
A7: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A8: f is_differentiable_on Z by A2,A4,Th1;
then
A9: (a+b)(#)f is_differentiable_on Z by A6,FDIFF_1:20;
A10: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A11: Z c= dom id Z by A5,XBOOLE_1:18;
then
A12: id Z is_differentiable_on Z by A10,FDIFF_1:23;
A13: for x st x in Z holds (((a+b)(#)f)`|Z).x =(a+b)/(x+b)
proof
let x;
assume
A14: x in Z;
hence (((a+b)(#)f)`|Z).x=(a+b)*diff(f,x) by A6,A8,FDIFF_1:20
.=(a+b)*(f`|Z).x by A8,A14,FDIFF_1:def 7
.=(a+b)*(1/(x+b)) by A2,A7,A4,A14,Th1
.=(a+b)/(x+b) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z - (a+b)(#)f)`|Z).x = (x-a)/(x+b)
proof
let x;
assume
A15: x in Z;
then
A16: f1.x=x+b & f1.x>0 by A3;
((id Z - (a+b)(#)f)`|Z).x = diff(id Z,x) - diff((a+b)(#)f,x) by A1,A12,A9
,A15,FDIFF_1:19
.=((id Z)`|Z).x - diff((a+b)(#)f,x) by A12,A15,FDIFF_1:def 7
.=((id Z)`|Z).x - (((a+b)(#)f)`|Z).x by A9,A15,FDIFF_1:def 7
.=1 - (((a+b)(#)f)`|Z).x by A11,A10,A15,FDIFF_1:23
.=1 - (a+b)/(x+b) by A13,A15
.=(1*(x+b) - (a+b))/(x+b) by A16,XCMPLX_1:127
.=(x-a)/(x+b);
hence thesis;
end;
hence thesis by A1,A12,A9,FDIFF_1:19;
end;
:: 11 f.x=x+ (b-a)*ln(x-b)
theorem
Z c= dom (id Z + (b-a)(#)f) & f = ln*f1 & (for x st x in Z holds f1.x=
x-b & f1.x>0) implies (id Z + (b-a)(#)f) is_differentiable_on Z & for x st x in
Z holds ((id Z +(b-a)(#)f)`|Z).x = (x-a)/(x-b)
proof
assume that
A1: Z c= dom (id Z + (b-a)(#)f) and
A2: f = ln*f1 and
A3: for x st x in Z holds f1.x=x-b & f1.x>0;
A4: Z c= dom id Z /\ dom ((b-a)(#)f) by A1,VALUED_1:def 1;
then
A5: Z c= dom ((b-a)(#)f) by XBOOLE_1:18;
then
A6: Z c= dom (ln*f1) by A2,VALUED_1:def 5;
then
A7: f is_differentiable_on Z by A2,A3,Th2;
then
A8: (b-a)(#)f is_differentiable_on Z by A5,FDIFF_1:20;
A9: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
A10: Z c= dom id Z by A4,XBOOLE_1:18;
then
A11: id Z is_differentiable_on Z by A9,FDIFF_1:23;
A12: for x st x in Z holds (((b-a)(#)f)`|Z).x =(b-a)/(x-b)
proof
let x;
assume
A13: x in Z;
hence (((b-a)(#)f)`|Z).x =(b-a)*diff(f,x) by A5,A7,FDIFF_1:20
.=(b-a)*(f`|Z).x by A7,A13,FDIFF_1:def 7
.=(b-a)*(1/(x-b)) by A2,A3,A6,A13,Th2
.=(b-a)/(x-b) by XCMPLX_1:99;
end;
for x st x in Z holds ((id Z + (b-a)(#)f)`|Z).x = (x-a)/(x-b)
proof
let x;
assume
A14: x in Z;
then
A15: f1.x=x-b & f1.x>0 by A3;
((id Z + (b-a)(#)f)`|Z).x = diff(id Z,x) + diff((b-a)(#)f,x) by A1,A11,A8
,A14,FDIFF_1:18
.=((id Z)`|Z).x + diff((b-a)(#)f,x) by A11,A14,FDIFF_1:def 7
.=((id Z)`|Z).x + (((b-a)(#)f)`|Z).x by A8,A14,FDIFF_1:def 7
.=1 + (((b-a)(#)f)`|Z).x by A10,A9,A14,FDIFF_1:23
.=1 + (b-a)/(x-b) by A12,A14
.=(1*(x-b) + (b-a))/(x-b) by A15,XCMPLX_1:113
.=(x-a)/(x-b);
hence thesis;
end;
hence thesis by A1,A11,A8,FDIFF_1:18;
end;
:: 12 f.x=a+b*x+c*x^2
theorem Th12:
Z c= dom (f1+c(#)f2) & (for x st x in Z holds f1.x=a+b*x) & f2=
#Z 2 implies f1+c(#)f2 is_differentiable_on Z & for x st x in Z holds ((f1+c(#)
f2)`|Z).x = b+2*c*x
proof
assume that
A1: Z c= dom (f1+c(#)f2) and
A2: for x st x in Z holds f1.x=a+b*x and
A3: f2=#Z 2;
A4: for x st x in Z holds f2 is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom f1 /\ dom (c(#)f2) by A1,VALUED_1:def 1;
then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x=b*x+a by A2;
then
A8: f1 is_differentiable_on Z by A6,FDIFF_1:23;
A9: Z c= dom (c(#)f2) by A5,XBOOLE_1:18;
then Z c= dom f2 by VALUED_1:def 5;
then
A10: f2 is_differentiable_on Z by A4,FDIFF_1:9;
then
A11: (c(#)f2) is_differentiable_on Z by A9,FDIFF_1:20;
A12: for x st x in Z holds (f2`|Z).x=2*x
proof
let x;
2 * (x #Z (2-1))=2 * x by PREPOWER:35;
then
A13: diff(f2,x) =2 * x by A3,TAYLOR_1:2;
assume x in Z;
hence thesis by A10,A13,FDIFF_1:def 7;
end;
A14: for x st x in Z holds ((c(#)f2)`|Z).x=2*c*x
proof
let x;
assume
A15: x in Z;
hence ((c(#)f2)`|Z).x=c*diff(f2,x) by A9,A10,FDIFF_1:20
.=c*(f2`|Z).x by A10,A15,FDIFF_1:def 7
.=c*(2*x) by A12,A15
.=2*c*x;
end;
for x st x in Z holds ((f1+c(#)f2)`|Z).x = b+2*c*x
proof
let x;
assume
A16: x in Z;
then ((f1+c(#)f2)`|Z).x =diff(f1,x) + diff(c(#)f2,x) by A1,A8,A11,
FDIFF_1:18
.=(f1`|Z).x+ diff((c(#)f2),x) by A8,A16,FDIFF_1:def 7
.=(f1`|Z).x+((c(#)f2)`|Z).x by A11,A16,FDIFF_1:def 7
.=b+((c(#)f2)`|Z).x by A6,A7,A16,FDIFF_1:23
.=b+2*c*x by A14,A16;
hence thesis;
end;
hence thesis by A1,A8,A11,FDIFF_1:18;
end;
:: 13 f.x=ln(a+b*x+c*x^2)
theorem Th13:
Z c= dom (ln*(f1+c(#)f2)) & f2=#Z 2 & (for x st x in Z holds f1.
x=a+b*x & (f1+c(#)f2).x >0) implies (ln*(f1+c(#)f2)) is_differentiable_on Z &
for x st x in Z holds ((ln*(f1+c(#)f2))`|Z).x = (b+2*c*x)/(a+b*x+c*x |^2)
proof
assume that
A1: Z c= dom (ln*(f1+c(#)f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x=a+b*x & (f1+c(#)f2).x >0;
for y being object st y in Z holds y in dom (f1+c(#)f2) by A1,FUNCT_1:11;
then
A4: Z c= dom (f1+c(#)f2) by TARSKI:def 3;
then Z c= dom f1 /\ dom (c(#)f2) by VALUED_1:def 1;
then
A5: Z c= dom (c(#)f2) by XBOOLE_1:18;
A6: for x st x in Z holds f1.x=a+b*x by A3;
then
A7: (f1+c(#)f2) is_differentiable_on Z by A2,A4,Th12;
A8: for x st x in Z holds ln*(f1+c(#)f2) is_differentiable_in x
proof
let x;
assume x in Z;
then (f1+c(#)f2) is_differentiable_in x & (f1+c(#)f2).x >0 by A3,A7,
FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A9: ln*(f1+c(#)f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1+c(#)f2))`|Z).x = (b+2*c*x)/(a+b*x+c*x |^ 2)
proof
let x;
assume
A10: x in Z;
then x in dom (f1+c(#)f2) by A1,FUNCT_1:11;
then
A11: ( f1+c(#)f2).x=f1.x + (c(#)f2).x by VALUED_1:def 1
.=f1.x +c*f2.x by A5,A10,VALUED_1:def 5
.=a+b*x +c*(f2.x) by A3,A10
.=a+b*x +c*(x #Z 2) by A2,TAYLOR_1:def 1
.=a+b*x +c*(x |^2) by PREPOWER:36;
(f1+c(#)f2) is_differentiable_in x & ( f1+c(#)f2).x >0 by A3,A7,A10,
FDIFF_1:9;
then
diff(ln*( f1+c(#)f2),x) =diff(( f1+c(#)f2),x)/(( f1+c(#)f2).x) by TAYLOR_1:20
.=(( f1+c(#)f2)`|Z).x/(( f1+c(#)f2).x) by A7,A10,FDIFF_1:def 7
.=(b+2*c*x )/(a+b*x+c*(x |^2)) by A2,A4,A6,A10,A11,Th12;
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
:: 14 f.x=1/(a+x)
theorem Th14:
Z c= dom f & (for x st x in Z holds f.x = a+x & f.x<>0) implies
f^ is_differentiable_on Z & for x st x in Z holds ( (f^)`|Z).x= -1/(a+x)^2
proof
assume that
A1: Z c= dom f and
A2: for x st x in Z holds f.x = a+x & f.x<>0;
A3: for x st x in Z holds f.x = 1*x+a by A2;
then
A4: f is_differentiable_on Z by A1,FDIFF_1:23;
A5: for x st x in Z holds f.x<>0 by A2;
then
A6: f^ is_differentiable_on Z by A4,FDIFF_2:22;
now
let x;
assume
A7: x in Z;
then
A8: f.x<>0 & f is_differentiable_in x by A2,A4,FDIFF_1:9;
( (f^)`|Z).x= diff(f^,x) by A6,A7,FDIFF_1:def 7
.= - diff(f,x)/( f.x)^2 by A8,FDIFF_2:15
.=- (f`|Z).x/( f.x)^2 by A4,A7,FDIFF_1:def 7
.=-1/( f.x)^2 by A1,A3,A7,FDIFF_1:23
.=-1/(a+x)^2 by A2,A7;
hence ( (f^)`|Z).x=-1/(a+x)^2;
end;
hence thesis by A4,A5,FDIFF_2:22;
end;
:: 15 f.x=-1/(a+x)
theorem
Z c= dom ((-1)(#)(f^)) & (for x st x in Z holds f.x=a+x & f.x <>0)
implies (-1)(#)(f^) is_differentiable_on Z & for x st x in Z holds (((-1)(#)(f^
))`|Z).x = 1/(a+x)^2
proof
assume that
A1: Z c= dom ((-1)(#)(f^)) and
A2: for x st x in Z holds f.x=a+x & f.x <>0;
A3: dom (f^) c= dom f by RFUNCT_1:1;
Z c= dom (f^) by A1,VALUED_1:def 5;
then
A4: Z c= dom f by A3,XBOOLE_1:1;
then
A5: f^ is_differentiable_on Z by A2,Th14;
now
let x;
assume
A6: x in Z;
hence (((-1)(#)(f^))`|Z).x =(-1)*diff((f^),x) by A1,A5,FDIFF_1:20
.=(-1)*((f^)`|Z).x by A5,A6,FDIFF_1:def 7
.=(-1)*(-1/(a+x)^2) by A2,A4,A6,Th14
.=1/(a+x)^2;
end;
hence thesis by A1,A5,FDIFF_1:20;
end;
:: 16 f.x=1/(a-x)
theorem
Z c= dom f & (for x st x in Z holds f.x = a-x & f.x<>0) implies f^
is_differentiable_on Z & for x st x in Z holds ( (f^)`|Z).x= 1/(a-x)^2
proof
assume that
A1: Z c= dom f and
A2: for x st x in Z holds f.x = a-x & f.x<>0;
A3: for x st x in Z holds f.x =(-1)*x+a
proof
let x;
assume x in Z;
then f.x =a-x by A2;
hence thesis;
end;
then
A4: f is_differentiable_on Z by A1,FDIFF_1:23;
A5: for x st x in Z holds f.x<>0 by A2;
then
A6: f^ is_differentiable_on Z by A4,FDIFF_2:22;
now
let x;
assume
A7: x in Z;
then
A8: f.x<>0 & f is_differentiable_in x by A2,A4,FDIFF_1:9;
( (f^)`|Z).x= diff(f^,x) by A6,A7,FDIFF_1:def 7
.= - diff(f,x)/( f.x)^2 by A8,FDIFF_2:15
.=- (f`|Z).x/( f.x)^2 by A4,A7,FDIFF_1:def 7
.=-(-1)/( f.x)^2 by A1,A3,A7,FDIFF_1:23
.=-(-1/( f.x)^2) by XCMPLX_1:187
.=1/(a-x)^2 by A2,A7;
hence ( (f^)`|Z).x=1/(a-x)^2;
end;
hence thesis by A4,A5,FDIFF_2:22;
end;
:: 17 f.x=a^2+x^2
theorem Th17:
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) & for x st x in Z holds f1.x=a^2 and
A2: f2=#Z 2;
A3: Z c= dom (f1+1(#)f2) & for x st x in Z holds f1.x=a^2 + 0*x by A1,
RFUNCT_1:21;
A4: for x st x in Z holds ((f1+f2)`|Z).x = 2*x
proof
let x;
assume
A5: x in Z;
((f1+f2)`|Z).x=((f1+1(#)f2)`|Z).x by RFUNCT_1:21
.= 0+2*1*x by A2,A3,A5,Th12
.= 2*x;
hence thesis;
end;
f1+1(#)f2 is_differentiable_on Z by A2,A3,Th12;
hence thesis by A4,RFUNCT_1:21;
end;
:: 18 f.x=ln(a^2+x^2)
theorem
Z c= dom (ln*(f1+f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (
f1+f2).x >0) implies (ln*(f1+f2)) is_differentiable_on Z & for x st x in Z
holds ((ln*(f1+f2))`|Z).x = (2*x)/(a^2+x|^2)
proof
assume that
A1: Z c= dom (ln*(f1+f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x=a^2 & (f1+f2).x >0;
f2=1(#)f2 by RFUNCT_1:21;
then
A4: for x st x in Z holds f1.x=a^2+0*x & (f1+1(#)f2).x >0 by A3;
A5: Z c= dom (ln*(f1+1(#)f2)) by A1,RFUNCT_1:21;
A6: for x st x in Z holds ((ln*(f1+f2))`|Z).x = (2*x)/(a^2+x |^2)
proof
let x;
assume
A7: x in Z;
((ln*(f1+f2))`|Z).x =((ln*(f1+1(#)f2))`|Z).x by RFUNCT_1:21
.= (0+2*1*x)/(a^2+0*x+1*x |^2) by A2,A5,A4,A7,Th13
.=(2*x)/(a^2+x |^2);
hence thesis;
end;
(ln*(f1+1(#)f2)) is_differentiable_on Z by A2,A5,A4,Th13;
hence thesis by A6,RFUNCT_1:21;
end;
:: 19 f.x=-ln(a^2-x^2)
theorem
Z c= dom -(ln*(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (
f1-f2).x >0) implies -(ln*(f1-f2)) is_differentiable_on Z & for x st x in Z
holds ((-(ln*(f1-f2)))`|Z).x = 2*x/(a^2-x |^2)
proof
assume that
A1: Z c= dom -(ln*(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: Z c= dom (ln*(f1+(-1)(#)f2)) & for x st x in Z holds f1.x=a^2+0*x & ( f1
+(-1 )(#)f2).x >0 by A1,A3,VALUED_1:8;
then
A5: ln*(f1+(-1)(#)f2) is_differentiable_on Z by A2,Th13;
for x st x in Z holds ((-(ln*(f1-f2)))`|Z).x =2*x/(a^2-x |^2)
proof
let x;
assume
A6: x in Z;
then ((-(ln*(f1-f2)))`|Z).x =(-1)*diff((ln*(f1+(-1)(#)f2)),x) by A1,A5,
FDIFF_1:20
.=(-1)*((ln*(f1+(-1)(#)f2))`|Z).x by A5,A6,FDIFF_1:def 7
.=(-1)*((0+2*(-1)*x)/(a^2+0*x+(-1)*x |^2)) by A2,A4,A6,Th13
.=(-1)*(2*(-1)*x)/(a^2+(-1)*x |^2) by XCMPLX_1:74
.=2*x/(a^2-x |^2);
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:20;
end;
:: 20 f.x=a+x^3
theorem Th20:
Z c= dom (f1+f2) & (for x st x in Z holds f1.x=a) & f2=#Z 3
implies f1+f2 is_differentiable_on Z & for x st x in Z holds ((f1+f2)`|Z).x = 3
*x |^2
proof
assume that
A1: Z c= dom (f1+f2) and
A2: for x st x in Z holds f1.x=a and
A3: f2=#Z 3;
A4: for x st x in Z holds f2 is_differentiable_in x by A3,TAYLOR_1:2;
A5: Z c= dom f1 /\ dom f2 by A1,VALUED_1:def 1;
then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x = 0*x+a by A2;
then
A8: f1 is_differentiable_on Z by A6,FDIFF_1:23;
Z c= dom f2 by A5,XBOOLE_1:18;
then
A9: f2 is_differentiable_on Z by A4,FDIFF_1:9;
A10: for x st x in Z holds (f2`|Z).x = 3 * x #Z (3-1)
proof
let x;
assume
A11: x in Z;
diff(f2,x) = 3 * x #Z (3-1) by A3,TAYLOR_1:2;
hence thesis by A9,A11,FDIFF_1:def 7;
end;
for x st x in Z holds ((f1+f2)`|Z).x = 3*x|^2
proof
let x;
assume
A12: x in Z;
then ((f1+f2)`|Z).x=diff(f1,x)+diff(f2,x) by A1,A8,A9,FDIFF_1:18;
hence ((f1+f2)`|Z).x=(f1`|Z).x +diff(f2,x) by A8,A12,FDIFF_1:def 7
.=(f1`|Z).x +(f2`|Z).x by A9,A12,FDIFF_1:def 7
.=0+(f2`|Z).x by A6,A7,A12,FDIFF_1:23
.=3 * x #Z (3-1) by A10,A12
.=3*x |^2 by PREPOWER:36;
end;
hence thesis by A1,A8,A9,FDIFF_1:18;
end;
:: 21 f.x=ln(a+x^3)
theorem
Z c= dom (ln*(f1+f2)) & f2=#Z 3 & (for x st x in Z holds f1.x=a & (f1+
f2).x >0) implies (ln*(f1+f2)) is_differentiable_on Z & for x st x in Z holds (
(ln*(f1+f2))`|Z).x = (3*x |^2)/(a+x |^3)
proof
assume that
A1: Z c= dom (ln*(f1+f2)) and
A2: f2=#Z 3 and
A3: for x st x in Z holds f1.x=a & (f1+f2).x >0;
for y being object st y in Z holds y in dom (f1+f2) by A1,FUNCT_1:11;
then
A4: Z c= dom (f1+f2) by TARSKI:def 3;
A5: for x st x in Z holds f1.x=a by A3;
then
A6: f1+f2 is_differentiable_on Z by A2,A4,Th20;
A7: for x st x in Z holds ln*(f1+f2) is_differentiable_in x
proof
let x;
assume x in Z;
then f1+f2 is_differentiable_in x & (f1+f2).x >0 by A3,A6,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A8: ln*(f1+f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1+f2))`|Z).x = (3*x |^2)/(a+x |^3)
proof
let x;
assume
A9: x in Z;
then
A10: x in dom (f1+f2) by A1,FUNCT_1:11;
f1+f2 is_differentiable_in x & (f1+f2).x >0 by A3,A6,A9,FDIFF_1:9;
then diff(ln*(f1+f2),x) =diff((f1+f2),x)/((f1+f2).x) by TAYLOR_1:20
.=((f1+f2)`|Z).x/((f1+f2).x) by A6,A9,FDIFF_1:def 7
.=(3*x |^2)/((f1+f2).x) by A2,A4,A5,A9,Th20
.=(3*x |^2)/(f1.x+f2.x) by A10,VALUED_1:def 1
.=(3*x |^2)/(a+f2.x) by A3,A9
.=(3*x |^2)/(a+x #Z 3) by A2,TAYLOR_1:def 1
.=(3*x |^2)/(a+x |^3 ) by PREPOWER:36;
hence thesis by A8,A9,FDIFF_1:def 7;
end;
hence thesis by A1,A7,FDIFF_1:9;
end;
:: 22 f.x=ln((a+x)/(a-x))
theorem
Z c= dom (ln*(f1/f2)) & (for x st x in Z holds f1.x=a+x & f1.x >0 & f2
.x=a-x & f2.x >0) implies ln*(f1/f2) is_differentiable_on Z & for x st x in Z
holds ((ln*(f1/f2))`|Z).x = (2*a)/(a^2-x^2)
proof
assume that
A1: Z c= dom (ln*(f1/f2)) and
A2: for x st x in Z holds f1.x=a+x & f1.x >0 & f2.x=a-x & f2.x >0;
for y being object st y in Z holds y in dom (f1/f2) by A1,FUNCT_1:11;
then Z c= dom (f1/f2) by TARSKI:def 3;
then
A3: Z c= dom f1 /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then
A4: Z c= dom f1 by XBOOLE_1:18;
A5: for x st x in Z holds f1.x=1*x+a by A2;
then
A6: f1 is_differentiable_on Z by A4,FDIFF_1:23;
A7: for x st x in Z holds f2.x =(-1)*x+a
proof
let x;
assume x in Z;
then f2.x =a-x by A2;
hence thesis;
end;
A8: Z c= dom f2 by A3,XBOOLE_1:1;
then
A9: f2 is_differentiable_on Z by A7,FDIFF_1:23;
for x st x in Z holds f2.x <> 0 by A2;
then
A10: f1/f2 is_differentiable_on Z by A6,A9,FDIFF_2:21;
A11: for x st x in Z holds ((f1/f2)`|Z).x = (2*a)/(a-x)^2
proof
let x;
assume
A12: x in Z;
then
A13: f2.x <>0 by A2;
A14: f1.x=a+x & f2.x=a-x by A2,A12;
f1 is_differentiable_in x & f2 is_differentiable_in x by A6,A9,A12,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A13
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A6,A12,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A9,A12,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A4,A5,A12,FDIFF_1:23
.=(1* f2.x-(-1)* f1.x)/(f2.x)^2 by A8,A7,A12,FDIFF_1:23
.=(2*a)/(a-x)^2 by A14;
hence thesis by A10,A12,FDIFF_1:def 7;
end;
A15: for x st x in Z holds (f1/f2).x >0
proof
let x;
assume
A16: x in Z;
then x in dom (f1/f2) by A1,FUNCT_1:11;
then
A17: (f1/f2).x=f1.x * (f2.x)" by RFUNCT_1:def 1
.=f1.x / f2.x by XCMPLX_0:def 9;
f1.x >0 & f2.x >0 by A2,A16;
hence thesis by A17,XREAL_1:139;
end;
A18: for x st x in Z holds ln*(f1/f2) is_differentiable_in x
proof
let x;
assume x in Z;
then f1/f2 is_differentiable_in x & (f1/f2).x >0 by A10,A15,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A19: ln*(f1/f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1/f2))`|Z).x = (2*a)/(a^2-x^2)
proof
let x;
assume
A20: x in Z;
then
A21: f2.x=a-x & f2.x>0 by A2;
A22: f1.x=a+x & f2.x=a-x by A2,A20;
A23: x in dom (f1/f2) by A1,A20,FUNCT_1:11;
(f1/f2) is_differentiable_in x & (f1/f2).x >0 by A10,A15,A20,FDIFF_1:9;
then diff(ln*(f1/f2),x) =diff((f1/f2),x)/((f1/f2).x) by TAYLOR_1:20
.=((f1/f2)`|Z).x/((f1/f2).x) by A10,A20,FDIFF_1:def 7
.=((2*a)/(a-x)^2)/((f1/f2).x) by A11,A20
.=((2*a)/(a-x)^2)/(f1.x * (f2.x)") by A23,RFUNCT_1:def 1
.=((2*a)/((a-x)*(a-x)))/((a+x)/(a-x)) by A22,XCMPLX_0:def 9
.=((2*a)/(a-x)/(a-x))/((a+x)/(a-x)) by XCMPLX_1:78
.=((2*a)/(a-x))/((a+x)/(a-x))/(a-x) by XCMPLX_1:48
.=(2*a)/(a+x)/(a-x) by A21,XCMPLX_1:55
.=(2*a)/((a+x)*(a-x)) by XCMPLX_1:78
.=(2*a)/(a^2-x^2);
hence thesis by A19,A20,FDIFF_1:def 7;
end;
hence thesis by A1,A18,FDIFF_1:9;
end;
:: 23 f.x=ln((x-a)/(x+a))
theorem
Z c= dom (ln*(f1/f2)) & (for x st x in Z holds f1.x=x-a & f1.x >0 & f2
.x=x+a & f2.x >0) implies ln*(f1/f2) is_differentiable_on Z & for x st x in Z
holds ((ln*(f1/f2))`|Z).x = (2*a)/(x^2-a^2)
proof
assume that
A1: Z c= dom (ln*(f1/f2)) and
A2: for x st x in Z holds f1.x=x-a & f1.x >0 & f2.x=x+a & f2.x >0;
A3: for x st x in Z holds f2.x = 1*x+a by A2;
for y being object st y in Z holds y in dom (f1/f2) by A1,FUNCT_1:11;
then Z c= dom (f1/f2) by TARSKI:def 3;
then
A4: Z c= dom f1 /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then
A5: Z c= dom f1 by XBOOLE_1:18;
A6: Z c= dom f2 by A4,XBOOLE_1:1;
then
A7: f2 is_differentiable_on Z by A3,FDIFF_1:23;
A8: for x st x in Z holds f1.x = 1*x+-a
proof
let x;
A9: 1*x+-a=1*x-a;
assume x in Z;
hence thesis by A2,A9;
end;
then
A10: f1 is_differentiable_on Z by A5,FDIFF_1:23;
for x st x in Z holds f2.x <> 0 by A2;
then
A11: f1/f2 is_differentiable_on Z by A10,A7,FDIFF_2:21;
A12: for x st x in Z holds ((f1/f2)`|Z).x = (2*a)/(x+a)^2
proof
let x;
assume
A13: x in Z;
then
A14: f2.x <>0 by A2;
A15: f1.x=x-a & f2.x=x+a by A2,A13;
f1 is_differentiable_in x & f2 is_differentiable_in x by A10,A7,A13,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A14
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A10,A13,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A7,A13,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A5,A8,A13,FDIFF_1:23
.=(1* f2.x-1* f1.x)/(f2.x)^2 by A6,A3,A13,FDIFF_1:23
.=(2*a)/(x+a)^2 by A15;
hence thesis by A11,A13,FDIFF_1:def 7;
end;
A16: for x st x in Z holds (f1/f2).x >0
proof
let x;
assume
A17: x in Z;
then x in dom (f1/f2) by A1,FUNCT_1:11;
then
A18: (f1/f2).x=f1.x * (f2.x)" by RFUNCT_1:def 1
.=f1.x / f2.x by XCMPLX_0:def 9;
f1.x >0 & f2.x >0 by A2,A17;
hence thesis by A18,XREAL_1:139;
end;
A19: for x st x in Z holds ln*(f1/f2) is_differentiable_in x
proof
let x;
assume x in Z;
then f1/f2 is_differentiable_in x & (f1/f2).x >0 by A11,A16,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A20: ln*(f1/f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1/f2))`|Z).x = (2*a)/(x^2-a^2)
proof
let x;
assume
A21: x in Z;
then
A22: f2.x=x+a & f2.x>0 by A2;
A23: f1.x=x-a & f2.x=x+a by A2,A21;
A24: x in dom (f1/f2) by A1,A21,FUNCT_1:11;
(f1/f2) is_differentiable_in x & (f1/f2).x >0 by A11,A16,A21,FDIFF_1:9;
then diff(ln*(f1/f2),x) =diff((f1/f2),x)/((f1/f2).x) by TAYLOR_1:20
.=((f1/f2)`|Z).x/((f1/f2).x) by A11,A21,FDIFF_1:def 7
.=((2*a)/(x+a)^2)/((f1/f2).x) by A12,A21
.=((2*a)/(x+a)^2)/(f1.x * (f2.x)") by A24,RFUNCT_1:def 1
.=((2*a)/((x+a)*(x+a)))/((x-a)/(x+a)) by A23,XCMPLX_0:def 9
.=((2*a)/(x+a)/(x+a))/((x-a)/(x+a)) by XCMPLX_1:78
.=((2*a)/(x+a))/((x-a)/(x+a))/(x+a) by XCMPLX_1:48
.=(2*a)/(x-a)/(x+a) by A22,XCMPLX_1:55
.=(2*a)/((x-a)*(x+a)) by XCMPLX_1:78
.=(2*a)/(x^2-a^2);
hence thesis by A20,A21,FDIFF_1:def 7;
end;
hence thesis by A1,A19,FDIFF_1:9;
end;
:: 24 f.x=ln((x-a)/(x-b))
theorem Th24:
Z c= dom (ln*(f1/f2)) & (for x st x in Z holds f1.x=x-a & f1.x >
0 & f2.x=x-b & f2.x >0) implies ln*(f1/f2) is_differentiable_on Z & for x st x
in Z holds ((ln*(f1/f2))`|Z).x = (a-b)/((x-a)*(x-b))
proof
assume that
A1: Z c= dom (ln*(f1/f2)) and
A2: for x st x in Z holds f1.x=x-a & f1.x >0 & f2.x=x-b & f2.x >0;
A3: for x st x in Z holds f1.x = 1*x+-a & f2.x = 1*x+-b
proof
let x;
A4: 1*x+-a=1*x-a & 1*x+-b=1*x-b;
assume x in Z;
hence thesis by A2,A4;
end;
then
A5: for x st x in Z holds f1.x = 1*x+-a;
for y being object st y in Z holds y in dom (f1/f2) by A1,FUNCT_1:11;
then Z c= dom (f1/f2) by TARSKI:def 3;
then
A6: Z c= dom f1 /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then
A7: Z c= dom f1 by XBOOLE_1:18;
then
A8: f1 is_differentiable_on Z by A5,FDIFF_1:23;
A9: for x st x in Z holds f2.x = 1*x+-b by A3;
A10: Z c= dom f2 by A6,XBOOLE_1:1;
then
A11: f2 is_differentiable_on Z by A9,FDIFF_1:23;
for x st x in Z holds f2.x <> 0 by A2;
then
A12: f1/f2 is_differentiable_on Z by A8,A11,FDIFF_2:21;
A13: for x st x in Z holds ((f1/f2)`|Z).x = (a-b)/(x-b)^2
proof
let x;
assume
A14: x in Z;
then
A15: f2.x <>0 by A2;
A16: f1.x=x-a & f2.x=x-b by A2,A14;
f1 is_differentiable_in x & f2 is_differentiable_in x by A8,A11,A14,
FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A15
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A8,A14,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A11,A14,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A7,A5,A14,FDIFF_1:23
.=(1* f2.x-1* f1.x)/(f2.x)^2 by A10,A9,A14,FDIFF_1:23
.=(a-b)/(x-b)^2 by A16;
hence thesis by A12,A14,FDIFF_1:def 7;
end;
A17: for x st x in Z holds (f1/f2).x >0
proof
let x;
assume
A18: x in Z;
then x in dom (f1/f2) by A1,FUNCT_1:11;
then
A19: (f1/f2).x=f1.x * (f2.x)" by RFUNCT_1:def 1
.=f1.x / f2.x by XCMPLX_0:def 9;
f1.x >0 & f2.x >0 by A2,A18;
hence thesis by A19,XREAL_1:139;
end;
A20: for x st x in Z holds ln*(f1/f2) is_differentiable_in x
proof
let x;
assume x in Z;
then f1/f2 is_differentiable_in x & (f1/f2).x >0 by A12,A17,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A21: ln*(f1/f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1/f2))`|Z).x = (a-b)/((x-a)*(x-b))
proof
let x;
assume
A22: x in Z;
then
A23: f2.x=x-b & f2.x>0 by A2;
A24: f1.x=x-a & f2.x=x-b by A2,A22;
A25: x in dom (f1/f2) by A1,A22,FUNCT_1:11;
(f1/f2) is_differentiable_in x & (f1/f2).x >0 by A12,A17,A22,FDIFF_1:9;
then diff(ln*(f1/f2),x) =diff((f1/f2),x)/((f1/f2).x) by TAYLOR_1:20
.=((f1/f2)`|Z).x/((f1/f2).x) by A12,A22,FDIFF_1:def 7
.=((a-b)/(x-b)^2)/((f1/f2).x) by A13,A22
.=((a-b)/(x-b)^2)/(f1.x * (f2.x)") by A25,RFUNCT_1:def 1
.=((a-b)/((x-b)*(x-b)))/((x-a)/(x-b)) by A24,XCMPLX_0:def 9
.=((a-b)/(x-b)/(x-b))/((x-a)/(x-b)) by XCMPLX_1:78
.=((a-b)/(x-b))/((x-a)/(x-b))/(x-b) by XCMPLX_1:48
.=(a-b)/(x-a)/(x-b) by A23,XCMPLX_1:55
.=(a-b)/((x-a)*(x-b)) by XCMPLX_1:78;
hence thesis by A21,A22,FDIFF_1:def 7;
end;
hence thesis by A1,A20,FDIFF_1:9;
end;
:: 25 f.x=(1/(a-b))*ln((x-a)/(x-b))
theorem
Z c= dom ((1/(a-b))(#)f) & f=ln*(f1/f2) & (for x st x in Z holds f1.x=
x-a & f1.x >0 & f2.x=x-b & f2.x >0 & a-b<>0) implies (1/(a-b))(#)f
is_differentiable_on Z & for x st x in Z holds (((1/(a-b))(#)f)`|Z).x =1/((x-a)
*(x-b))
proof
assume that
A1: Z c= dom ((1/(a-b))(#)f) and
A2: f=ln*(f1/f2) and
A3: for x st x in Z holds f1.x=x-a & f1.x >0 & f2.x=x-b & f2.x >0 & a-b <>0;
A4: ( for x st x in Z holds f1.x=x-a & f1.x >0 & f2.x=x-b & f2.x >0)& Z c=
dom f by A1,A3,VALUED_1:def 5;
then
A5: f is_differentiable_on Z by A2,Th24;
for x st x in Z holds (((1/(a-b))(#)f)`|Z).x =1/((x-a)*(x-b))
proof
let x;
assume
A6: x in Z;
then
A7: a-b<>0 by A3;
(((1/(a-b))(#)f)`|Z).x =(1/(a-b))*diff(f,x) by A1,A5,A6,FDIFF_1:20
.=(1/(a-b))*(f`|Z).x by A5,A6,FDIFF_1:def 7
.=(1/(a-b))*((a-b)/((x-a)*(x-b))) by A2,A4,A6,Th24
.=(1/(a-b))*(a-b)/((x-a)*(x-b)) by XCMPLX_1:74
.=1/((x-a)*(x-b)) by A7,XCMPLX_1:106;
hence thesis;
end;
hence thesis by A1,A5,FDIFF_1:20;
end;
:: 26 f.x=ln((x-a)/x^2)
theorem
Z c= dom (ln*(f1/f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=x-a & f1
.x >0 & f2.x >0 & x <>0) implies ln*(f1/f2) is_differentiable_on Z & for x st x
in Z holds ((ln*(f1/f2))`|Z).x = (2*a-x)/(x*(x-a))
proof
assume that
A1: Z c= dom (ln*(f1/f2)) and
A2: f2=#Z 2 and
A3: for x st x in Z holds f1.x=x-a & f1.x >0 & f2.x >0 & x <>0;
A4: for x st x in Z holds f2 is_differentiable_in x by A2,TAYLOR_1:2;
for y being object st y in Z holds y in dom (f1/f2) by A1,FUNCT_1:11;
then Z c= dom (f1/f2) by TARSKI:def 3;
then
A5: Z c= dom f1 /\ (dom f2 \ f2"{0}) by RFUNCT_1:def 1;
then
A6: Z c= dom f1 by XBOOLE_1:18;
A7: for x st x in Z holds f1.x = 1*x+-a
proof
let x;
A8: 1*x+-a=1*x-a;
assume x in Z;
hence thesis by A3,A8;
end;
then
A9: f1 is_differentiable_on Z by A6,FDIFF_1:23;
A10: Z c= dom f2 by A5,XBOOLE_1:1;
then
A11: f2 is_differentiable_on Z by A4,FDIFF_1:9;
for x st x in Z holds f2.x <> 0 by A3;
then
A12: f1/f2 is_differentiable_on Z by A9,A11,FDIFF_2:21;
A13: f2 is_differentiable_on Z by A10,A4,FDIFF_1:9;
A14: for x st x in Z holds (f2`|Z).x=2*x
proof
let x;
2 * (x #Z (2-1))=2 * x by PREPOWER:35;
then
A15: diff(f2,x) =2 * x by A2,TAYLOR_1:2;
assume x in Z;
hence thesis by A13,A15,FDIFF_1:def 7;
end;
A16: for x st x in Z holds ((f1/f2)`|Z).x = (2*a-x)/x |^3
proof
let x;
A17: f2 is_differentiable_in x by A2,TAYLOR_1:2;
A18: f2.x=x #Z 2 by A2,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
assume
A19: x in Z;
then
A20: x<>0 by A3;
f1 is_differentiable_in x & f2.x <>0 by A3,A9,A19,FDIFF_1:9;
then diff(f1/f2,x) =(diff(f1,x) * f2.x - diff(f2,x) * f1.x)/(f2.x)^2 by A17
,FDIFF_2:14
.=((f1`|Z).x * f2.x-diff(f2,x) * f1.x)/(f2.x)^2 by A9,A19,FDIFF_1:def 7
.= ((f1`|Z).x * f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A11,A19,FDIFF_1:def 7
.=(1* f2.x-(f2`|Z).x * f1.x)/(f2.x)^2 by A6,A7,A19,FDIFF_1:23
.=(1* f2.x-(2*x)* f1.x)/(f2.x)^2 by A14,A19
.=((x |^(1+1))-(2*x)*(x-a))/(x |^2)^2 by A3,A19,A18
.=((x |^1*x)-(2*x)*(x-a))/(x |^2)^2 by NEWTON:6
.=((x *x)-(2*x)*(x-a))/(x |^2)^2
.=(x *(2*a-x))/(x |^(2+2)) by NEWTON:8
.=(x *(2*a-x))/(x |^(3+1))
.=(x *(2*a-x))/(x |^3 *x) by NEWTON:6
.=(2*a-x)/x |^3 by A20,XCMPLX_1:91;
hence thesis by A12,A19,FDIFF_1:def 7;
end;
A21: for x st x in Z holds (f1/f2).x >0
proof
let x;
assume
A22: x in Z;
then x in dom (f1/f2) by A1,FUNCT_1:11;
then
A23: (f1/f2).x=f1.x * (f2.x)" by RFUNCT_1:def 1
.=f1.x / f2.x by XCMPLX_0:def 9;
f1.x >0 & f2.x >0 by A3,A22;
hence thesis by A23,XREAL_1:139;
end;
A24: for x st x in Z holds ln*(f1/f2) is_differentiable_in x
proof
let x;
assume x in Z;
then f1/f2 is_differentiable_in x & (f1/f2).x >0 by A12,A21,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A25: ln*(f1/f2) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(f1/f2))`|Z).x = (2*a-x)/(x*(x-a))
proof
let x;
assume
A26: x in Z;
then
A27: x in dom (f1/f2) by A1,FUNCT_1:11;
A28: f2.x=x #Z 2 by A2,TAYLOR_1:def 1
.=x |^2 by PREPOWER:36;
then
A29: x |^2>0 by A3,A26;
A30: f1.x=x-a by A3,A26;
(f1/f2) is_differentiable_in x & (f1/f2).x >0 by A12,A21,A26,FDIFF_1:9;
then diff(ln*(f1/f2),x) =diff((f1/f2),x)/((f1/f2).x) by TAYLOR_1:20
.=((f1/f2)`|Z).x/((f1/f2).x) by A12,A26,FDIFF_1:def 7
.=((2*a-x)/x |^3)/((f1/f2).x) by A16,A26
.=((2*a-x)/x |^3)/(f1.x * (f2.x)") by A27,RFUNCT_1:def 1
.=((2*a-x)/x |^(2+1))/((x-a)/x |^2) by A28,A30,XCMPLX_0:def 9
.=((2*a-x)/(x |^2*x))/((x-a)/x |^2) by NEWTON:6
.=(2*a-x)/x |^2/x/((x-a)/x |^2) by XCMPLX_1:78
.=((2*a-x)/x |^2)/((x-a)/x |^2)/x by XCMPLX_1:48
.=(2*a-x)/(x-a)/x by A29,XCMPLX_1:55
.=(2*a-x)/(x*(x-a)) by XCMPLX_1:78;
hence thesis by A25,A26,FDIFF_1:def 7;
end;
hence thesis by A1,A24,FDIFF_1:9;
end;
:: irrational function
:: 27 f.x=(a+x) ^ (3/2)
theorem Th27:
Z c= dom (( #R (3/2))*f) & (for x st x in Z holds f.x=a+x & f.x>
0) implies ( #R (3/2))*f is_differentiable_on Z & for x st x in Z holds ((( #R
(3/2))*f)`|Z).x =(3/2)* (a+x) #R (1/2)
proof
assume that
A1: Z c= dom (( #R (3/2))*f) and
A2: for x st x in Z holds f.x=a+x & f.x>0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
A4: for x st x in Z holds f.x = 1*x+a by A2;
then
A5: f is_differentiable_on Z by A3,FDIFF_1:23;
A6: for x st x in Z holds ( #R (3/2))*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A5,FDIFF_1:9;
hence thesis by TAYLOR_1:22;
end;
then
A7: ( #R (3/2))*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #R (3/2))*f)`|Z).x =(3/2)*(a+x) #R (1/2)
proof
let x;
assume
A8: x in Z;
then
A9: f.x = a+x by A2;
f is_differentiable_in x & f.x >0 by A2,A5,A8,FDIFF_1:9;
then diff(( #R (3/2)) *f,x) = (3/2)*( ( f.x) #R (3/2-1)) * diff(f,x) by
TAYLOR_1:22
.= (3/2)*( ( f.x) #R (3/2-1))*(f`|Z).x by A5,A8,FDIFF_1:def 7
.= (3/2)*( (a+x) #R (3/2-1))*1 by A3,A4,A8,A9,FDIFF_1:23
.=(3/2)* (a+x) #R (1/2);
hence thesis by A7,A8,FDIFF_1:def 7;
end;
hence thesis by A1,A6,FDIFF_1:9;
end;
:: 28 f.x=(a+x) ^ (2/3)
theorem
Z c= dom ((2/3)(#)(( #R (3/2))*f)) & (for x st x in Z holds f.x=a+x &
f.x>0) implies (2/3)(#)(( #R (3/2))*f) is_differentiable_on Z & for x st x in Z
holds (((2/3)(#)(( #R (3/2))*f))`|Z).x =(a+x) #R (1/2)
proof
assume that
A1: Z c= dom ((2/3)(#)(( #R (3/2))*f)) and
A2: for x st x in Z holds f.x=a+x & f.x>0;
A3: Z c= dom (( #R (3/2))*f) by A1,VALUED_1:def 5;
then
A4: (( #R (3/2))*f) is_differentiable_on Z by A2,Th27;
for x st x in Z holds (((2/3)(#)(( #R (3/2))*f))`|Z).x =(a+x) #R (1/2)
proof
let x;
assume
A5: x in Z;
hence
(((2/3)(#)(( #R (3/2))*f))`|Z).x =(2/3)*diff((( #R (3/2))*f),x) by A1,A4,
FDIFF_1:20
.=(2/3)*((( #R (3/2))*f)`|Z).x by A4,A5,FDIFF_1:def 7
.=(2/3)*((3/2)* (a+x) #R (1/2)) by A2,A3,A5,Th27
.=(a+x) #R (1/2);
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
:: 29 f.x=(-2/3)*(a+x) ^ (2/3)
theorem
Z c= dom ((-2/3)(#)(( #R (3/2))*f)) & (for x st x in Z holds f.x=a-x &
f.x> 0 ) implies (-2/3)(#)(( #R (3/2))*f) is_differentiable_on Z & for x st x
in Z holds (((-2/3)(#)(( #R (3/2))*f))`|Z).x =(a-x) #R (1/2)
proof
assume that
A1: Z c= dom ((-2/3)(#)(( #R (3/2))*f)) and
A2: for x st x in Z holds f.x=a-x & f.x>0;
A3: Z c= dom (( #R (3/2))*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
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x =(-1)*x+a
proof
let x;
assume x in Z;
then f.x =a-x by A2;
hence thesis;
end;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ( #R (3/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A7: ( #R (3/2))*f is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((-2/3)(#)(( #R (3/2))*f))`|Z).x =(a-x) #R (1/2)
proof
let x;
assume
A8: x in Z;
then
A9: f.x = a-x by A2;
A10: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
(((-2/3)(#)(( #R (3/2))*f))`|Z).x =(-2/3)*diff((( #R (3/2))*f),x) by A1,A7
,A8,FDIFF_1:20
.=(-2/3)* ((3/2)*( ( f.x) #R (3/2-1)) * diff(f,x)) by A10,TAYLOR_1:22
.=(-2/3)* ((3/2)*( ( f.x) #R (3/2-1))*(f`|Z).x) by A6,A8,FDIFF_1:def 7
.=(-2/3)* ((3/2)*( (a-x) #R (3/2-1))*(-1)) by A4,A5,A8,A9,FDIFF_1:23
.=(a-x) #R (1/2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 30 f.x=2*(a+x) ^ (1/2)
theorem
Z c= dom ((2(#)(( #R (1/2))*f))) & (for x st x in Z holds f.x=a+x & f.
x>0) implies 2(#)(( #R (1/2))*f) is_differentiable_on Z & for x st x in Z holds
((2(#)(( #R (1/2))*f))`|Z).x =(a+x) #R (-1/2)
proof
assume that
A1: Z c= dom ((2(#)(( #R (1/2))*f))) and
A2: for x st x in Z holds f.x=a+x & f.x>0;
A3: Z c= dom (( #R (1/2))*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
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x = 1*x+a by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ( #R (1/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A7: ( #R (1/2))*f is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((2(#)(( #R (1/2))*f))`|Z).x =(a+x) #R (-1/2)
proof
let x;
assume
A8: x in Z;
then
A9: f.x = a+x by A2;
A10: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
((2(#)(( #R (1/2))*f))`|Z).x =2*diff((( #R (1/2))*f),x) by A1,A7,A8,
FDIFF_1:20
.=2*((1/2)*( ( f.x) #R (1/2-1)) * diff(f,x)) by A10,TAYLOR_1:22
.=2*((1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x) by A6,A8,FDIFF_1:def 7
.=2*((1/2)*( (a+x) #R (1/2-1))*1) by A4,A5,A8,A9,FDIFF_1:23
.= (a+x) #R (-1/2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 31 f.x=(-2)*(a-x) ^ (1/2)
theorem
Z c= dom (((-2)(#)(( #R (1/2))*f))) & (for x st x in Z holds f.x=a-x &
f.x>0) implies (-2)(#)(( #R (1/2))*f) is_differentiable_on Z & for x st x in Z
holds (((-2)(#)(( #R (1/2))*f))`|Z).x =(a-x) #R (-1/2)
proof
assume that
A1: Z c= dom (((-2)(#)(( #R (1/2))*f))) and
A2: for x st x in Z holds f.x=a-x & f.x>0;
A3: Z c= dom (( #R (1/2))*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
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x =(-1)*x+a
proof
let x;
assume x in Z;
then f.x =a-x by A2;
hence thesis;
end;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ( #R (1/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A7: ( #R (1/2))*f is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((-2)(#)(( #R (1/2))*f))`|Z).x =(a-x) #R (-1/2)
proof
let x;
assume
A8: x in Z;
then
A9: f.x = a-x by A2;
A10: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
(((-2)(#)(( #R (1/2))*f))`|Z).x =(-2)*diff((( #R (1/2))*f),x) by A1,A7,A8,
FDIFF_1:20
.=(-2)*((1/2)*( ( f.x) #R (1/2-1)) * diff(f,x)) by A10,TAYLOR_1:22
.=(-2)*((1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x) by A6,A8,FDIFF_1:def 7
.=(-2)*((1/2)*( (a-x) #R (1/2-1))*(-1)) by A4,A5,A8,A9,FDIFF_1:23
.= (a-x) #R (-1/2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 32 f.x=(2/(3*b))*((a+b*x) ^ (3/2))
theorem
Z c= dom ((2/(3*b))(#)(( #R (3/2))*f)) & (for x st x in Z holds f.x=a+
b*x & b<>0 & f.x>0) implies (2/(3*b))(#)(( #R (3/2))*f) is_differentiable_on Z
& for x st x in Z holds (((2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(a+b*x) #R (1/2)
proof
assume that
A1: Z c= dom ((2/(3*b))(#)(( #R (3/2))*f)) and
A2: for x st x in Z holds f.x=a+b*x & b<>0 & f.x>0;
A3: Z c= dom (( #R (3/2))*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
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x = b*x+a by A2;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ( #R (3/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A7: ( #R (3/2))*f is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(a+b*x) #R (1/2)
proof
let x;
assume
A8: x in Z;
then
A9: 3*b <>0 by A2;
A10: f.x = a+b*x by A2,A8;
A11: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
(((2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(2/(3*b))*diff((( #R (3/2))*f),
x) by A1,A7,A8,FDIFF_1:20
.=(2/(3*b))*((3/2)*( ( f.x) #R (3/2-1)) * diff(f,x)) by A11,TAYLOR_1:22
.=(2/(3*b))*((3/2)*( ( f.x) #R (3/2-1))*(f`|Z).x) by A6,A8,FDIFF_1:def 7
.=(2/(3*b))*((3/2)*( (a+b*x) #R (3/2-1))*b) by A4,A5,A8,A10,FDIFF_1:23
.=(2/(3*b))*((3*b)/2)*( (a+b*x) #R (3/2-1))
.=1*( (a+b*x) #R (3/2-1)) by A9,XCMPLX_1:112
.=(a+b*x) #R (1/2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 33 f.x=(-2/(3*b))*((a-b*x) ^ (3/2))
theorem
Z c= dom ((-2/(3*b))(#)(( #R (3/2))*f)) & (for x st x in Z holds f.x=a
-b*x & b<>0 & f.x>0) implies (-2/(3*b))(#)(( #R (3/2))*f) is_differentiable_on
Z & for x st x in Z holds (((-2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(a-b*x) #R (1/
2)
proof
assume that
A1: Z c= dom ((-2/(3*b))(#)(( #R (3/2))*f)) and
A2: for x st x in Z holds f.x=a-b*x & b<>0 & f.x>0;
A3: Z c= dom (( #R (3/2))*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
A4: Z c= dom f by TARSKI:def 3;
A5: for x st x in Z holds f.x =(-b)*x+a
proof
let x;
assume x in Z;
then f.x =a-b*x by A2;
hence thesis;
end;
then
A6: f is_differentiable_on Z by A4,FDIFF_1:23;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A6,FDIFF_1:9;
hence ( #R (3/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A7: ( #R (3/2))*f is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((-2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(a-b*x) #R (1/2)
proof
let x;
assume
A8: x in Z;
then
A9: 3*b <>0 by A2;
A10: f.x = a-b*x by A2,A8;
A11: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9;
(((-2/(3*b))(#)(( #R (3/2))*f))`|Z).x =(-2/(3*b))*diff((( #R (3/2))*f
), x ) by A1,A7,A8,FDIFF_1:20
.=(-2/(3*b))* ((3/2)*( ( f.x) #R (3/2-1)) * diff(f,x)) by A11,TAYLOR_1:22
.=(-2/(3*b))* ((3/2)*( ( f.x) #R (3/2-1))*(f`|Z).x) by A6,A8,
FDIFF_1:def 7
.=(-2/(3*b))* ((3/2)*( (a-b*x) #R (3/2-1))*(-b)) by A4,A5,A8,A10,
FDIFF_1:23
.=(2/(3*b))* ((3*b)/2)*( (a-b*x) #R (3/2-1))
.=1*( (a-b*x) #R (3/2-1)) by A9,XCMPLX_1:112
.=(a-b*x) #R (1/2);
hence thesis;
end;
hence thesis by A1,A7,FDIFF_1:20;
end;
:: 34 f.x=(a^2+x|^2) ^ (1/2)
theorem
Z c= dom (( #R (1/2))*f) & f=f1+f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=a^2 & f.x>0) implies ( #R (1/2))*f is_differentiable_on Z & for x st x in
Z holds ((( #R (1/2))*f)`|Z).x =x * (a^2+x |^2) #R (-1/2)
proof
assume that
A1: Z c= dom (( #R (1/2))*f) and
A2: f=f1+f2 and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=a^2 & f.x>0;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A5: Z c= dom (f1+f2) by A2,TARSKI:def 3;
A6: for x st x in Z holds f1.x=a^2 by A4;
then
A7: f is_differentiable_on Z by A2,A3,A5,Th17;
A8: for x st x in Z holds ( #R (1/2))*f is_differentiable_in x
proof
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A4,A7,FDIFF_1:9;
hence thesis by TAYLOR_1:22;
end;
then
A9: ( #R (1/2))*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((( #R (1/2))*f)`|Z).x =x * (a^2+x |^2) #R (-1/2)
proof
let x;
assume
A10: x in Z;
then x in dom (f1+f2) by A1,A2,FUNCT_1:11;
then
A11: ( f1+f2).x=f1.x + f2.x by VALUED_1:def 1
.=a^2 +(f2.x) by A4,A10
.=a^2 +(x #Z 2) by A3,TAYLOR_1:def 1
.=a^2 +(x |^2) by PREPOWER:36;
f is_differentiable_in x & f.x >0 by A4,A7,A10,FDIFF_1:9;
then diff(( #R (1/2)) *f,x) = (1/2)*( ( f.x) #R (1/2-1)) * diff(f,x) by
TAYLOR_1:22
.= (1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x by A7,A10,FDIFF_1:def 7
.= (1/2)*( (a^2+x |^2) #R (1/2-1))*(2*x) by A2,A3,A5,A6,A10,A11,Th17
.=x* (a^2+x |^2) #R (-1/2);
hence thesis by A9,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A8,FDIFF_1:9;
end;
:: 35 f.x=-(a^2-x|^2) ^ (1/2)
theorem
Z c= dom -(( #R (1/2))*f) & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds
f1.x=a^2 & f.x >0) implies -(( #R (1/2))*f) is_differentiable_on Z & for x st x
in Z holds ((-(( #R (1/2))*f))`|Z).x = x* (a^2-x |^2) #R (-1/2)
proof
assume that
A1: Z c= dom -(( #R (1/2))*f) and
A2: f=f1-f2 and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=a^2 & f.x >0;
A5: for x st x in Z holds f1.x=a^2+0*x by A4;
A6: Z c= dom (( #R (1/2))*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
A7: Z c= dom ((f1+(-1)(#)f2)) by A2,TARSKI:def 3;
then
A8: f is_differentiable_on Z by A2,A3,A5,Th12;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A4,A8,FDIFF_1:9;
hence ( #R (1/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A9: ( #R (1/2))*f is_differentiable_on Z by A6,FDIFF_1:9;
for x st x in Z holds (((-1)(#)(( #R (1/2))*f))`|Z).x =x* (a^2-x |^2)
#R (-1/2)
proof
let x;
assume
A10: x in Z;
then
A11: f is_differentiable_in x & f.x >0 by A4,A8,FDIFF_1:9;
x in dom (f1-f2) by A2,A6,A10,FUNCT_1:11;
then
A12: ( f1-f2).x=f1.x - f2.x by VALUED_1:13
.=a^2 -(f2.x) by A4,A10
.=a^2 -(x #Z 2) by A3,TAYLOR_1:def 1
.=a^2 -(x |^2) by PREPOWER:36;
(((-1)(#)(( #R (1/2))*f))`|Z).x =(-1)*diff((( #R (1/2))*f),x) by A1,A9,A10,
FDIFF_1:20
.=(-1)*((1/2)*( ( f.x) #R (1/2-1)) * diff(f,x)) by A11,TAYLOR_1:22
.=(-1)*((1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x) by A8,A10,FDIFF_1:def 7
.=(-1)*((1/2)*( ( f.x) #R (1/2-1))*(0+2*(-1)*x)) by A2,A3,A7,A5,A10,Th12
.=x* (a^2-x |^2) #R (-1/2) by A2,A12;
hence thesis;
end;
hence thesis by A1,A9,FDIFF_1:20;
end;
:: 36 f.x=(x+x|^2) ^ (1/2)
theorem
Z c= dom ((2(#)(( #R (1/2))*f))) & f=f1+f2 & f2=#Z 2 & (for x st x in
Z holds f1.x=x & f.x>0) implies 2(#)(( #R (1/2))*f) is_differentiable_on Z &
for x st x in Z holds ((2(#)(( #R (1/2))*f))`|Z).x =(2*x+1)*(x |^2+x) #R (-1/2)
proof
assume that
A1: Z c= dom ((2(#)(( #R (1/2))*f))) and
A2: f=f1+f2 and
A3: f2=#Z 2 and
A4: for x st x in Z holds f1.x=x & f.x>0;
A5: for x st x in Z holds f1.x=0+1*x by A4;
A6: f2=1(#)f2 by RFUNCT_1:21;
A7: Z c= dom (( #R (1/2))*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
A8: Z c= dom (f1+1(#)f2) by A2,A6,TARSKI:def 3;
then
A9: f1+f2 is_differentiable_on Z by A3,A6,A5,Th12;
now
let x;
assume x in Z;
then f is_differentiable_in x & f.x >0 by A2,A4,A9,FDIFF_1:9;
hence ( #R (1/2))*f is_differentiable_in x by TAYLOR_1:22;
end;
then
A10: ( #R (1/2))*f is_differentiable_on Z by A7,FDIFF_1:9;
A11: for x st x in Z holds ((f1+f2)`|Z).x = 1+2*1*x by A3,A6,A8,A5,Th12;
for x st x in Z holds ((2(#)(( #R (1/2))*f))`|Z).x =(2*x+1)*(x |^2+x)
#R (-1/2)
proof
let x;
assume
A12: x in Z;
then
A13: f is_differentiable_in x & f.x >0 by A2,A4,A9,FDIFF_1:9;
x in dom (f1+f2) by A2,A7,A12,FUNCT_1:11;
then
A14: ( f1+f2).x=f1.x + f2.x by VALUED_1:def 1
.=x +(f2.x) by A4,A12
.=x +(x #Z 2) by A3,TAYLOR_1:def 1
.=x +x |^2 by PREPOWER:36;
((2(#)(( #R (1/2))*f))`|Z).x =2*diff((( #R (1/2))*f),x) by A1,A10,A12,
FDIFF_1:20
.=2*((1/2)*( ( f.x) #R (1/2-1)) * diff(f,x)) by A13,TAYLOR_1:22
.=2*((1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x) by A2,A9,A12,FDIFF_1:def 7
.=2*(1/2)*( ( f.x) #R (1/2-1))*(f`|Z).x
.=(2*x+1)* (x |^2+x) #R (-1/2) by A2,A11,A12,A14;
hence thesis;
end;
hence thesis by A1,A10,FDIFF_1:20;
end;
:: trigonometric functions
:: 37 f.x=sin(a*x+b)
theorem
Z c= dom (sin*f) & (for x st x in Z holds f.x=a*x+b) implies sin*f
is_differentiable_on Z & for x st x in Z holds ((sin*f)`|Z).x = a* cos.(a*x+b)
proof
assume that
A1: Z c= dom (sin*f) and
A2: for x st x in Z holds f.x=a*x+b;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
then
A4: f is_differentiable_on Z by A2,FDIFF_1:23;
A5: for x st x in Z holds sin*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A6: f is_differentiable_in x by A4,FDIFF_1:9;
sin is_differentiable_in f.x by SIN_COS:64;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: sin*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((sin*f)`|Z).x = a* cos.(a*x+b)
proof
let x;
A8: sin is_differentiable_in f.x by SIN_COS:64;
assume
A9: x in Z;
then f is_differentiable_in x by A4,FDIFF_1:9;
then diff(sin*f,x) = diff(sin, f.x)*diff(f,x) by A8,FDIFF_2:13
.=cos.( f.x)*diff(f,x) by SIN_COS:64
.=cos.(a*x+b)*diff(f,x) by A2,A9
.=cos.(a*x+b)*(f`|Z).x by A4,A9,FDIFF_1:def 7
.=a* cos.(a*x+b) by A2,A3,A9,FDIFF_1:23;
hence thesis by A7,A9,FDIFF_1:def 7;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: 38 f.x=sin(a*x+b)
theorem
Z c= dom (cos*f) & (for x st x in Z holds f.x=a*x+b) implies cos*f
is_differentiable_on Z & for x st x in Z holds ((cos*f)`|Z).x = -a* sin.(a*x+b)
proof
assume that
A1: Z c= dom (cos*f) and
A2: for x st x in Z holds f.x=a*x+b;
for y being object st y in Z holds y in dom f by A1,FUNCT_1:11;
then
A3: Z c= dom f by TARSKI:def 3;
then
A4: f is_differentiable_on Z by A2,FDIFF_1:23;
A5: for x st x in Z holds cos*f is_differentiable_in x
proof
let x;
assume x in Z;
then
A6: f is_differentiable_in x by A4,FDIFF_1:9;
cos is_differentiable_in f.x by SIN_COS:63;
hence thesis by A6,FDIFF_2:13;
end;
then
A7: cos*f is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((cos*f)`|Z).x = -a* sin.(a*x+b)
proof
let x;
A8: diff(cos, f.x)=-sin.( f.x) by SIN_COS:63;
A9: cos is_differentiable_in f.x by SIN_COS:63;
assume
A10: x in Z;
then f is_differentiable_in x by A4,FDIFF_1:9;
then diff(cos*f,x) = diff(cos, f.x)*diff(f,x) by A9,FDIFF_2:13
.=-sin.( f.x)*diff(f,x) by A8
.=-sin.(a*x+b)*diff(f,x) by A2,A10
.=-sin.(a*x+b)*(f`|Z).x by A4,A10,FDIFF_1:def 7
.=-a*sin.(a*x+b) by A2,A3,A10,FDIFF_1:23;
hence thesis by A7,A10,FDIFF_1:def 7;
end;
hence thesis by A1,A5,FDIFF_1:9;
end;
:: 39 f.x=1/cos.x
theorem
(for x st x in Z holds cos.x<>0) implies cos^ is_differentiable_on Z &
for x st x in Z holds ( (cos^)`|Z).x= sin.x/(cos.x)^2
proof
assume
A1: for x st x in Z holds cos.x<>0;
A2: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A3: cos^ is_differentiable_on Z by A1,FDIFF_2:22;
for x st x in Z holds ( (cos^)`|Z).x= sin.x/(cos.x)^2
proof
let x;
A4: cos is_differentiable_in x by SIN_COS:63;
assume
A5: x in Z;
then
A6: cos.x<>0 by A1;
( (cos^)`|Z).x= diff(cos^,x) by A3,A5,FDIFF_1:def 7
.= - diff(cos,x)/(cos.x)^2 by A6,A4,FDIFF_2:15
.=- (-sin.x)/(cos.x)^2 by SIN_COS:63
.=- -(sin.x/(cos.x)^2) by XCMPLX_1:187
.=sin.x/(cos.x)^2;
hence thesis;
end;
hence thesis by A1,A2,FDIFF_2:22;
end;
:: 40 f.x=1/sin.x
theorem
(for x st x in Z holds sin.x<>0) implies sin^ is_differentiable_on Z &
for x st x in Z holds ( (sin^)`|Z).x= -cos.x/(sin.x)^2
proof
A1: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
assume
A2: for x st x in Z holds sin.x<>0;
then
A3: sin^ is_differentiable_on Z by A1,FDIFF_2:22;
for x st x in Z holds ( (sin^)`|Z).x= -cos.x/(sin.x)^2
proof
let x;
assume
A4: x in Z;
then
A5: sin.x<>0 & sin is_differentiable_in x by A2,A1,FDIFF_1:9;
( (sin^)`|Z).x= diff(sin^,x) by A3,A4,FDIFF_1:def 7
.= - diff(sin,x)/(sin.x)^2 by A5,FDIFF_2:15
.=- cos.x/(sin.x)^2 by SIN_COS:64;
hence thesis;
end;
hence thesis by A2,A1,FDIFF_2:22;
end;
:: 41 f.x=sin.x*cos.x
theorem
Z c= dom (sin(#)cos) implies sin(#)cos is_differentiable_on Z & for x
st x in Z holds ((sin(#)cos)`|Z).x = cos(2*x)
proof
A1: sin is_differentiable_on Z & cos is_differentiable_on Z by FDIFF_1:26
,SIN_COS:67,68;
assume
A2: Z c= dom (sin(#)cos);
now
let x;
assume x in Z;
hence ((sin(#)cos)`|Z).x =(cos.x)*diff(sin,x) + (sin.x)*diff(cos,x) by A2
,A1,FDIFF_1:21
.=cos.x * cos.x + (sin.x)*diff(cos,x) by SIN_COS:64
.=cos.x * cos.x + (sin.x)*(-sin.x) by SIN_COS:63
.=(cos.x)^2-sin.x*sin.x
.=(cos(x))^2-(sin.x)^2 by SIN_COS:def 19
.=(cos(x))^2-(sin(x))^2 by SIN_COS:def 17
.=cos(2*x) by SIN_COS5:7;
end;
hence thesis by A2,A1,FDIFF_1:21;
end;
:: 42 f.x=ln(cos.x)
theorem
Z c= dom (ln*cos) & (for x st x in Z holds cos.x >0) implies ln*cos
is_differentiable_on Z & for x st x in Z holds ((ln*cos)`|Z).x =- tan(x)
proof
assume that
A1: Z c= dom (ln*cos) and
A2: for x st x in Z holds cos.x >0;
A3: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
A4: for x st x in Z holds ln*cos is_differentiable_in x
proof
let x;
assume x in Z;
then cos is_differentiable_in x & cos.x >0 by A2,A3,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A5: ln*cos is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*cos)`|Z).x =- tan(x)
proof
let x;
assume
A6: x in Z;
then cos is_differentiable_in x & cos.x >0 by A2,A3,FDIFF_1:9;
then diff(ln*cos,x) =diff(cos,x)/(cos.x) by TAYLOR_1:20
.=(-sin.x)/cos.x by SIN_COS:63
.=- (sin.x/cos.x) by XCMPLX_1:187
.=- (sin(x)/cos.x) by SIN_COS:def 17
.=- (sin(x)/cos(x)) by SIN_COS:def 19
.=- tan(x) by SIN_COS4:def 1;
hence thesis by A5,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: 43 f.x=ln(sin.x)
theorem
Z c= dom (ln*sin) & (for x st x in Z holds sin.x >0) implies ln*sin
is_differentiable_on Z & for x st x in Z holds ((ln*sin)`|Z).x = cot(x)
proof
assume that
A1: Z c= dom (ln*sin) and
A2: for x st x in Z holds sin.x >0;
A3: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
A4: for x st x in Z holds ln*sin is_differentiable_in x
proof
let x;
assume x in Z;
then sin is_differentiable_in x & sin.x >0 by A2,A3,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A5: ln*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*sin)`|Z).x =cot(x)
proof
let x;
assume
A6: x in Z;
then sin is_differentiable_in x & sin.x >0 by A2,A3,FDIFF_1:9;
then diff(ln*sin,x) =diff(sin,x)/(sin.x) by TAYLOR_1:20
.=cos.x/sin.x by SIN_COS:64
.=cos(x)/sin.x by SIN_COS:def 19
.=cos(x)/sin(x) by SIN_COS:def 17
.=cot(x) by SIN_COS4:def 2;
hence thesis by A5,A6,FDIFF_1:def 7;
end;
hence thesis by A1,A4,FDIFF_1:9;
end;
:: 44 f.x=-x*cos.x
theorem Th44:
Z c= dom ((-id Z)(#)cos) implies (-id Z)(#)cos
is_differentiable_on Z & for x st x in Z holds (((-id Z)(#)cos)`|Z).x =-cos.x+x
*sin.x
proof
A1: for x st x in Z holds (-id Z).x =(-1)*x +0
proof
let x;
assume
A2: x in Z;
(-id Z).x = -(id Z.x) by VALUED_1:8
.=-x by A2,FUNCT_1:18
.=(-1)*x +0;
hence thesis;
end;
assume
A3: Z c= dom ((-id Z)(#)cos);
then Z c= dom (-id Z) /\ dom cos by VALUED_1:def 4;
then
A4: Z c= dom (-id Z) by XBOOLE_1:18;
then
A5: -id Z is_differentiable_on Z by A1,FDIFF_1:23;
A6: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
now
let x;
assume
A7: x in Z;
hence (((-id Z)(#)cos)`|Z).x = (cos.x)*diff((-id Z),x) + ((-id Z).x)*diff(
cos,x) by A3,A5,A6,FDIFF_1:21
.=(cos.x)*((-id Z)`|Z).x+ ((-id Z).x)*diff(cos,x) by A5,A7,FDIFF_1:def 7
.=(cos.x)*(-1)+ ((-id Z).x)*diff(cos,x) by A4,A1,A7,FDIFF_1:23
.=(cos.x)*(-1)+((-id Z).x)*(-sin.x) by SIN_COS:63
.=-cos.x+((-1)*x +0)*(-sin.x) by A1,A7
.=-cos.x+x*sin.x;
end;
hence thesis by A3,A5,A6,FDIFF_1:21;
end;
:: f.x=x*sin.x
theorem Th45:
Z c= dom ((id Z)(#)sin) implies (id Z)(#)sin
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)sin)`|Z).x =sin.x+x*
cos.x
proof
A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18;
assume
A2: Z c= dom ((id Z)(#)sin);
then Z c= dom (id Z) /\ dom sin by VALUED_1:def 4;
then
A3: Z c= dom (id Z) by XBOOLE_1:18;
then
A4: id Z is_differentiable_on Z by A1,FDIFF_1:23;
A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A6: x in Z;
hence
(((id Z)(#)sin)`|Z).x = (sin.x)*diff((id Z),x) + ((id Z).x)*diff(sin,
x) by A2,A4,A5,FDIFF_1:21
.=(sin.x)*((id Z)`|Z).x+ ((id Z).x)*diff(sin,x) by A4,A6,FDIFF_1:def 7
.=(sin.x)*1+ ((id Z).x)*diff(sin,x) by A3,A1,A6,FDIFF_1:23
.=(sin.x)*1+((id Z).x)*(cos.x) by SIN_COS:64
.=sin.x+ x*cos.x by A6,FUNCT_1:18;
end;
hence thesis by A2,A4,A5,FDIFF_1:21;
end;
:: 46 f.x=-x*cos.x+sin.x
theorem
Z c= dom ((-id Z)(#)cos+sin) implies (-id Z)(#)cos+sin
is_differentiable_on Z & for x st x in Z holds (((-id Z)(#)cos+sin)`|Z).x =x*
sin.x
proof
assume
A1: Z c= dom ((-id Z)(#)cos+sin);
then Z c= dom ((-id Z)(#)cos) /\ dom sin by VALUED_1:def 1;
then
A2: Z c= dom ((-id Z)(#)cos) by XBOOLE_1:18;
then
A3: (-id Z)(#)cos is_differentiable_on Z by Th44;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A5: x in Z;
hence (((-id Z)(#)cos+sin)`|Z).x = diff((-id Z)(#)cos,x) + diff(sin,x) by
A1,A3,A4,FDIFF_1:18
.=(((-id Z)(#)cos)`|Z).x + diff(sin,x) by A3,A5,FDIFF_1:def 7
.=-cos.x+x*sin.x+ diff(sin,x) by A2,A5,Th44
.=-cos.x+x*sin.x+cos.x by SIN_COS:64
.=x*sin.x;
end;
hence thesis by A1,A3,A4,FDIFF_1:18;
end;
:: 47 f.x=x*sin.x+cos.x
theorem
Z c= dom ((id Z)(#)sin+cos) implies (id Z)(#)sin+cos
is_differentiable_on Z & for x st x in Z holds (((id Z)(#)sin+cos)`|Z).x =x*cos
.x
proof
assume
A1: Z c= dom ((id Z)(#)sin+cos);
then Z c= dom ((id Z)(#)sin) /\ dom cos by VALUED_1:def 1;
then
A2: Z c= dom ((id Z)(#)sin) by XBOOLE_1:18;
then
A3: (id Z)(#)sin is_differentiable_on Z by Th45;
A4: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
now
let x;
assume
A5: x in Z;
hence
(((id Z)(#)sin+cos)`|Z).x = diff((id Z)(#)sin,x) + diff(cos,x) by A1,A3,A4,
FDIFF_1:18
.=(((id Z)(#)sin)`|Z).x + diff(cos,x) by A3,A5,FDIFF_1:def 7
.=sin.x+ x*cos.x+ diff(cos,x) by A2,A5,Th45
.=sin.x+ x*cos.x+(-sin.x) by SIN_COS:63
.=x*cos.x;
end;
hence thesis by A1,A3,A4,FDIFF_1:18;
end;
:: 48 f.x=2*(sin.x ^ (1/2))
theorem
Z c= dom ((2(#)(( #R (1/2))*sin))) & (for x st x in Z holds sin.x>0)
implies 2(#)(( #R (1/2))*sin) is_differentiable_on Z & for x st x in Z holds ((
2(#)(( #R (1/2))*sin))`|Z).x =cos.x*(sin.x) #R (-1/2)
proof
assume that
A1: Z c= dom ((2(#)(( #R (1/2))*sin))) and
A2: for x st x in Z holds sin.x>0;
A3: now
let x;
assume x in Z;
then sin is_differentiable_in x & sin.x >0 by A2,SIN_COS:64;
hence ( #R (1/2))*sin is_differentiable_in x by TAYLOR_1:22;
end;
Z c= dom (( #R (1/2))*sin) by A1,VALUED_1:def 5;
then
A4: ( #R (1/2))*sin is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds ((2(#)(( #R (1/2))*sin))`|Z).x =cos.x*(sin.x) #R (-1/2)
proof
let x;
assume
A5: x in Z;
then
A6: sin is_differentiable_in x & sin.x >0 by A2,SIN_COS:64;
((2(#)(( #R (1/2))*sin))`|Z).x =2*diff((( #R (1/2))*sin),x) by A1,A4,A5,
FDIFF_1:20
.=2*((1/2)*( (sin.x) #R (1/2-1)) * diff(sin,x)) by A6,TAYLOR_1:22
.=2*((1/2)*( (sin.x) #R (1/2-1)) *cos.x) by SIN_COS:64
.=cos.x*(sin.x) #R (-1/2);
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
theorem Th49:
Z c= dom ((1/2)(#)(( #Z 2)*sin)) implies (1/2)(#)(( #Z 2)*sin)
is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(( #Z 2)*sin))`|Z).x =
sin.x*cos.x
proof
A1: now
let x;
assume x in Z;
sin is_differentiable_in x by SIN_COS:64;
hence ( #Z 2)*sin is_differentiable_in x by TAYLOR_1:3;
end;
assume
A2: Z c= dom ((1/2)(#)(( #Z 2)*sin));
then Z c= dom (( #Z 2)*sin) by VALUED_1:def 5;
then
A3: ( #Z 2)*sin is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds (((1/2)(#)(( #Z 2)*sin))`|Z).x =sin.x*cos.x
proof
let x;
A4: sin is_differentiable_in x by SIN_COS:64;
assume x in Z;
then
(((1/2)(#)(( #Z 2)*sin))`|Z).x =(1/2)*diff((( #Z 2)*sin),x) by A2,A3,
FDIFF_1:20
.=(1/2)*(2*( (sin.x) #Z (2-1)) * diff(sin,x)) by A4,TAYLOR_1:3
.=(1/2)*(2*( (sin.x) #Z (2-1)) *cos.x) by SIN_COS:64
.=( (sin.x) #Z (2-1)) *cos.x
.=sin.x*cos.x by PREPOWER:35;
hence thesis;
end;
hence thesis by A2,A3,FDIFF_1:20;
end;
:: 50 f.x=sin.x+(1/2)*(sin.x ^ 2)
theorem
Z c= dom (sin+(1/2)(#)(( #Z 2)*sin)) & (for x st x in Z holds sin.x>0
& sin.x<1) implies sin+(1/2)(#)(( #Z 2)*sin) is_differentiable_on Z & for x st
x in Z holds ((sin+(1/2)(#)(( #Z 2)*sin))`|Z).x =(cos.x)|^3/(1-sin.x)
proof
assume that
A1: Z c= dom (sin+(1/2)(#)(( #Z 2)*sin)) and
A2: for x st x in Z holds sin.x>0 & sin.x<1;
Z c= dom ((1/2)(#)(( #Z 2)*sin)) /\ dom sin by A1,VALUED_1:def 1;
then
A3: Z c= dom ((1/2)(#)(( #Z 2)*sin)) by XBOOLE_1:18;
then
A4: (1/2)(#)(( #Z 2)*sin) is_differentiable_on Z by Th49;
A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A6: x in Z;
then sin.x<1 by A2;
then
A7: 1-sin.x>0 by XREAL_1:50;
((sin+(1/2)(#)(( #Z 2)*sin))`|Z).x = diff(sin,x) + diff((1/2)(#)(( #Z
2)*sin),x) by A1,A4,A5,A6,FDIFF_1:18
.=cos.x + diff((1/2)(#)(( #Z 2)*sin),x) by SIN_COS:64
.=cos.x +(((1/2)(#)(( #Z 2)*sin))`|Z).x by A4,A6,FDIFF_1:def 7
.=cos.x +sin.x*cos.x by A3,A6,Th49
.=cos.x*(1+sin.x)*(1-sin.x)/(1-sin.x) by A7,XCMPLX_1:89
.=cos.x*(1-(sin.x)^2)/(1-sin.x)
.=cos.x*(1-(sin(x))^2)/(1-sin.x) by SIN_COS:def 17
.=cos.x*(cos(x)*cos(x))/(1-sin.x) by SIN_COS4:5
.=cos.x*((cos(x))|^2)/(1-sin.x) by WSIERP_1:1
.=(cos.x*((cos.x)|^2))/(1-sin.x) by SIN_COS:def 19
.=((cos.x)|^(2+1))/(1-sin.x) by NEWTON:6
.=(cos.x)|^3/(1-sin.x);
hence ((sin+(1/2)(#)(( #Z 2)*sin))`|Z).x=(cos.x)|^3/(1-sin.x);
end;
hence thesis by A1,A4,A5,FDIFF_1:18;
end;
:: 51 f.x=(1/2)*(sin.x ^ 2)-cos.x
theorem
Z c= dom ((1/2)(#)(( #Z 2)*sin)-cos) & (for x st x in Z holds sin.x>0
& cos.x<1) implies ((1/2)(#)(( #Z 2)*sin)-cos) is_differentiable_on Z & for x
st x in Z holds ( ((1/2)(#)(( #Z 2)*sin)-cos) `|Z).x =(sin.x)|^3/(1-cos.x)
proof
assume that
A1: Z c= dom ((1/2)(#)(( #Z 2)*sin)-cos) and
A2: for x st x in Z holds sin.x>0 & cos.x<1;
Z c= dom ((1/2)(#)(( #Z 2)*sin)) /\ dom cos by A1,VALUED_1:12;
then
A3: Z c= dom ((1/2)(#)(( #Z 2)*sin)) by XBOOLE_1:18;
then
A4: (1/2)(#)(( #Z 2)*sin) is_differentiable_on Z by Th49;
A5: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
now
let x;
assume
A6: x in Z;
then
A7: 1-cos.x>0 by A2,XREAL_1:50;
(((1/2)(#)(( #Z 2)*sin)-cos)`|Z).x = diff((1/2)(#)(( #Z 2)*sin),x) -
diff(cos,x) by A1,A4,A5,A6,FDIFF_1:19
.=diff((1/2)(#)(( #Z 2)*sin),x)-(-sin.x) by SIN_COS:63
.=(((1/2)(#)(( #Z 2)*sin))`|Z).x-(-sin.x) by A4,A6,FDIFF_1:def 7
.=sin.x*cos.x--sin.x by A3,A6,Th49
.=sin.x*(1+cos.x)*(1-cos.x)/(1-cos.x) by A7,XCMPLX_1:89
.=sin.x*(1-(cos.x)^2)/(1-cos.x)
.=sin.x*(1-(cos(x))^2)/(1-cos.x) by SIN_COS:def 19
.=sin.x*(sin(x)*sin(x))/(1-cos.x) by SIN_COS4:4
.=sin.x*((sin(x))|^2)/(1-cos.x) by WSIERP_1:1
.=(sin.x*((sin.x)|^2))/(1-cos.x) by SIN_COS:def 17
.=((sin.x)|^(2+1))/(1-cos.x) by NEWTON:6
.=(sin.x)|^3/(1-cos.x);
hence (((1/2)(#)(( #Z 2)*sin)-cos)`|Z).x=(sin.x)|^3/(1-cos.x);
end;
hence thesis by A1,A4,A5,FDIFF_1:19;
end;
:: 52 f.x=sin.x-(1/2)*(sin ^ 2)
theorem
Z c= dom (sin-(1/2)(#)(( #Z 2)*sin)) & (for x st x in Z holds sin.x>0
& sin.x>-1) implies sin-(1/2)(#)(( #Z 2)*sin) is_differentiable_on Z & for x st
x in Z holds ((sin-(1/2)(#)(( #Z 2)*sin))`|Z).x =(cos.x)|^3/(1+sin.x)
proof
assume that
A1: Z c= dom (sin-(1/2)(#)(( #Z 2)*sin)) and
A2: for x st x in Z holds sin.x>0 & sin.x>-1;
Z c= dom ((1/2)(#)(( #Z 2)*sin)) /\ dom sin by A1,VALUED_1:12;
then
A3: Z c= dom ((1/2)(#)(( #Z 2)*sin)) by XBOOLE_1:18;
then
A4: (1/2)(#)(( #Z 2)*sin) is_differentiable_on Z by Th49;
A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
now
let x;
assume
A6: x in Z;
then sin.x>-1 by A2;
then
A7: sin.x--1>0 by XREAL_1:50;
((sin-(1/2)(#)(( #Z 2)*sin))`|Z).x = diff(sin,x) - diff((1/2)(#)(( #Z
2)*sin),x) by A1,A4,A5,A6,FDIFF_1:19
.=cos.x - diff((1/2)(#)(( #Z 2)*sin),x) by SIN_COS:64
.=cos.x -(((1/2)(#)(( #Z 2)*sin))`|Z).x by A4,A6,FDIFF_1:def 7
.=cos.x -sin.x*cos.x by A3,A6,Th49
.=cos.x*(1-sin.x)*(1+sin.x)/(1+sin.x) by A7,XCMPLX_1:89
.=cos.x*(1-(sin.x)^2)/(1+sin.x)
.=cos.x*(1-(sin(x))^2)/(1+sin.x) by SIN_COS:def 17
.=cos.x*(cos(x)*cos(x))/(1+sin.x) by SIN_COS4:5
.=cos.x*((cos(x))|^2)/(1+sin.x) by WSIERP_1:1
.=(cos.x*((cos.x)|^2))/(1+sin.x) by SIN_COS:def 19
.=((cos.x)|^(2+1))/(1+sin.x) by NEWTON:6
.=(cos.x)|^3/(1+sin.x);
hence ((sin-(1/2)(#)(( #Z 2)*sin))`|Z).x=(cos.x)|^3/(1+sin.x);
end;
hence thesis by A1,A4,A5,FDIFF_1:19;
end;
:: 53 f.x=-cos.x-(1/2)*(sin.x ^ 2)
theorem
Z c= dom (-cos-(1/2)(#)(( #Z 2)*sin)) & (for x st x in Z holds sin.x>0
& cos.x>-1) implies -cos-(1/2)(#)(( #Z 2)*sin) is_differentiable_on Z & for x
st x in Z holds ((-cos-(1/2)(#)(( #Z 2)*sin))`|Z).x =(sin.x)|^3/(1+cos.x)
proof
assume that
A1: Z c= dom (-cos-(1/2)(#)(( #Z 2)*sin)) and
A2: for x st x in Z holds sin.x>0 & cos.x>-1;
A3: Z c= dom ((1/2)(#)(( #Z 2)*sin)) /\ dom (-cos) by A1,VALUED_1:12;
then
A4: Z c= dom (-cos) by XBOOLE_1:18;
A5: Z c= dom ((1/2)(#)(( #Z 2)*sin)) by A3,XBOOLE_1:18;
then
A6: (1/2)(#)(( #Z 2)*sin) is_differentiable_on Z by Th49;
A7: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
A8: -cos is_differentiable_on Z by A4,A7,FDIFF_1:20;
now
let x;
assume
A9: x in Z;
then
A10: cos.x--1>0 by A2,XREAL_1:50;
((-cos-(1/2)(#)(( #Z 2)*sin))`|Z).x =diff((-cos),x)-diff((1/2)(#)((
#Z 2)*sin),x) by A1,A6,A8,A9,FDIFF_1:19
.=((-cos)`|Z).x-diff((1/2)(#)(( #Z 2)*sin),x) by A8,A9,FDIFF_1:def 7
.=(-1)*diff(cos,x)-diff((1/2)(#)(( #Z 2)*sin),x) by A4,A7,A9,FDIFF_1:20
.=(-1)*(-sin.x)-diff((1/2)(#)(( #Z 2)*sin),x) by SIN_COS:63
.=sin.x-(((1/2)(#)(( #Z 2)*sin))`|Z).x by A6,A9,FDIFF_1:def 7
.=sin.x-sin.x*cos.x by A5,A9,Th49
.=sin.x*(1-cos.x)*(1+cos.x)/(1+cos.x) by A10,XCMPLX_1:89
.=sin.x*(1-(cos.x)^2)/(1+cos.x)
.=sin.x*(1-(cos(x))^2)/(1+cos.x) by SIN_COS:def 19
.=sin.x*(sin(x)*sin(x))/(1+cos.x) by SIN_COS4:4
.=sin.x*((sin(x))|^2)/(1+cos.x) by WSIERP_1:1
.=(sin.x*((sin.x)|^2))/(1+cos.x) by SIN_COS:def 17
.=((sin.x)|^(2+1))/(1+cos.x) by NEWTON:6
.=(sin.x)|^3/(1+cos.x);
hence ((-cos-(1/2)(#)(( #Z 2)*sin))`|Z).x=(sin.x)|^3/(1+cos.x);
end;
hence thesis by A1,A6,A8,FDIFF_1:19;
end;
:: 54 f.x=(1/n)*(sin.x ^ n)
theorem
Z c= dom ((1/n)(#)(( #Z n)*sin)) & n>0 implies (1/n)(#)(( #Z n)*sin)
is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*sin))`|Z).x =
(sin.x) #Z (n-1) *cos.x
proof
assume that
A1: Z c= dom ((1/n)(#)(( #Z n)*sin)) and
A2: n>0;
A3: now
let x;
assume x in Z;
sin is_differentiable_in x by SIN_COS:64;
hence ( #Z n)*sin is_differentiable_in x by TAYLOR_1:3;
end;
Z c= dom (( #Z n)*sin) by A1,VALUED_1:def 5;
then
A4: ( #Z n)*sin is_differentiable_on Z by A3,FDIFF_1:9;
for x st x in Z holds (((1/n)(#)(( #Z n)*sin))`|Z).x =(sin.x) #Z (n-1) *
cos.x
proof
let x;
A5: sin is_differentiable_in x by SIN_COS:64;
assume x in Z;
then
(((1/n)(#)(( #Z n)*sin))`|Z).x =(1/n)*diff((( #Z n)*sin),x) by A1,A4,
FDIFF_1:20
.=(1/n)*(n*( (sin.x) #Z (n-1)) * diff(sin,x)) by A5,TAYLOR_1:3
.=(1/n)*(n*( (sin.x) #Z (n-1)) *cos.x) by SIN_COS:64
.=((1/n)*n)*( (sin.x) #Z (n-1)) *cos.x
.=((n")*n)*( (sin.x) #Z (n-1)) *cos.x by XCMPLX_1:215
.=1*( (sin.x) #Z (n-1)) *cos.x by A2,XCMPLX_0:def 7
.=(sin.x) #Z (n-1) *cos.x;
hence thesis;
end;
hence thesis by A1,A4,FDIFF_1:20;
end;
:: exponential function
:: 55 f.x=exp.x*(x-1)
theorem
Z c= dom (exp_R(#)f) & (for x st x in Z holds f.x=x-1) implies exp_R
(#)f is_differentiable_on Z & for x st x in Z holds ((exp_R(#)f)`|Z).x = 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-1;
A3: for x st x in Z holds f.x = 1*x+-1
proof
let x;
A4: 1*x+-1=1*x-1;
assume x in Z;
hence thesis by A2,A4;
end;
Z c= dom f /\ dom exp_R by A1,VALUED_1:def 4;
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;
now
let x;
assume
A8: x in Z;
hence
((exp_R(#)f)`|Z).x = (f.x)*diff(exp_R,x) + (exp_R.x)*diff(f,x) by A1,A6,A7,
FDIFF_1:21
.=(x-1)*diff(exp_R,x)+ (exp_R.x)*diff(f,x) by A2,A8
.=(x-1)*(exp_R.x)+ (exp_R.x)*diff(f,x) by TAYLOR_1:16
.=(x-1)*(exp_R.x)+(exp_R.x)*(f`|Z).x by A6,A8,FDIFF_1:def 7
.=(x-1)*(exp_R.x)+(exp_R.x)*1 by A5,A3,A8,FDIFF_1:23
.=x*(exp_R.x);
end;
hence thesis by A1,A6,A7,FDIFF_1:21;
end;
:: 56 f.x=ln(exp.x/(exp.x+1))
theorem
Z c= dom (ln*(exp_R/(exp_R+f))) & (for x st x in Z holds f.x=1)
implies ln*(exp_R/(exp_R+f)) is_differentiable_on Z & for x st x in Z holds ((
ln*(exp_R/(exp_R+f)))`|Z).x = 1/(exp_R.x+1)
proof
assume that
A1: Z c= dom (ln*(exp_R/(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/(exp_R+f))
by A1,FUNCT_1:11;
then Z c= dom (exp_R/(exp_R+f)) by TARSKI:def 3;
then Z c= dom exp_R /\ (dom (exp_R+f)\(exp_R+f)"{0}) by RFUNCT_1:def 1;
then
A4: Z c= dom (exp_R+f) by XBOOLE_1:1;
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).x>0
proof
let x;
assume
A10: 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,A10;
hence thesis by SIN_COS:54,XREAL_1:34;
end;
then for x st x in Z holds (exp_R+f).x<>0;
then
A11: exp_R/(exp_R+f) is_differentiable_on Z by A7,A8,FDIFF_2:21;
A12: for x st x in Z holds ((exp_R+f)`|Z).x =exp_R.x
proof
let x;
assume
A13: 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,A13,FDIFF_1:def 7
.=exp_R.x+0 by A5,A3,A13,FDIFF_1:23
.=exp_R.x;
end;
A14: for x st x in Z holds ((exp_R/(exp_R+f))`|Z).x=exp_R.x/(exp_R.x +1)^2
proof
let x;
A15: exp_R is_differentiable_in x by SIN_COS:65;
assume
A16: x in Z;
then
A17: (exp_R+f).x=exp_R.x + f.x by A4,VALUED_1:def 1
.=exp_R.x +1 by A2,A16;
exp_R+f is_differentiable_in x & (exp_R+f).x <>0 by A8,A9,A16,FDIFF_1:9;
then
diff(exp_R/(exp_R+f),x) =(diff(exp_R,x) * (exp_R+f).x - diff((exp_R+f
),x) * exp_R.x)/((exp_R+f).x)^2 by A15,FDIFF_2:14
.=(exp_R.x*(exp_R+f).x-diff((exp_R+f),x) * exp_R.x)/((exp_R+f).x)^2 by
SIN_COS:65
.=(exp_R.x*(exp_R.x +1)-((exp_R+f)`|Z).x * exp_R.x)/(exp_R.x +1)^2 by A8
,A16,A17,FDIFF_1:def 7
.=(exp_R.x*(exp_R.x +1)-exp_R.x * exp_R.x)/(exp_R.x +1)^2 by A12,A16
.=exp_R.x/(exp_R.x +1)^2;
hence thesis by A11,A16,FDIFF_1:def 7;
end;
A18: for x st x in Z holds (exp_R/(exp_R+f)).x >0
proof
let x;
A19: exp_R.x>0 by SIN_COS:54;
assume
A20: x in Z;
then x in dom (exp_R/(exp_R+f)) by A1,FUNCT_1:11;
then
A21: (exp_R/(exp_R+f)).x=exp_R.x*((exp_R+f).x)" by RFUNCT_1:def 1
.=exp_R.x*(1/(exp_R+f).x) by XCMPLX_1:215
.=exp_R.x/(exp_R+f).x by XCMPLX_1:99;
(exp_R+f).x>0 by A9,A20;
hence thesis by A21,A19,XREAL_1:139;
end;
A22: for x st x in Z holds ln*(exp_R/(exp_R+f)) is_differentiable_in x
proof
let x;
assume x in Z;
then exp_R/(exp_R+f) is_differentiable_in x & (exp_R/(exp_R+f)).x >0 by A11
,A18,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A23: ln*(exp_R/(exp_R+f)) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*(exp_R/(exp_R+f)))`|Z).x = 1/(exp_R.x+1)
proof
let x;
assume
A24: x in Z;
then x in dom (exp_R/(exp_R+f)) by A1,FUNCT_1:11;
then
A25: (exp_R/(exp_R+f)).x=(exp_R.x)*((exp_R+f).x)" by RFUNCT_1:def 1
.=(exp_R.x)*(1/(exp_R+f).x) by XCMPLX_1:215
.=(exp_R.x)/(exp_R+f).x by XCMPLX_1:99
.=(exp_R.x)/(exp_R.x + f.x) by A4,A24,VALUED_1:def 1
.=(exp_R.x)/(exp_R.x +1) by A2,A24;
then
A26: exp_R.x/(exp_R.x +1)>0 by A18,A24;
(exp_R/(exp_R+f)) is_differentiable_in x & (exp_R/(exp_R+f)).x >0 by A11
,A18,A24,FDIFF_1:9;
then diff(ln*(exp_R/(exp_R+f)),x) =diff((exp_R/(exp_R+f)),x)/((exp_R/(
exp_R+f)).x) by TAYLOR_1:20
.=((exp_R/(exp_R+f))`|Z).x/((exp_R/(exp_R+f)).x) by A11,A24,FDIFF_1:def 7
.=(exp_R.x/(exp_R.x +1)^2)/(exp_R.x/(exp_R.x +1)) by A14,A24,A25
.=(exp_R.x/(exp_R.x +1)/(exp_R.x+1))/(exp_R.x/(exp_R.x +1)) by
XCMPLX_1:78
.=(exp_R.x/(exp_R.x +1))/(exp_R.x/(exp_R.x +1))/(exp_R.x +1) by
XCMPLX_1:48
.=1/(exp_R.x +1) by A26,XCMPLX_1:60;
hence thesis by A23,A24,FDIFF_1:def 7;
end;
hence thesis by A1,A22,FDIFF_1:9;
end;
:: 57 f.x=ln((exp.x-1)/exp.x)
theorem
Z c= dom (ln*((exp_R-f)/exp_R)) & (for x st x in Z holds f.x=1 & (
exp_R-f).x>0) implies ln*((exp_R-f)/exp_R) is_differentiable_on Z & for x st x
in Z holds ((ln*((exp_R-f)/exp_R))`|Z).x = 1/(exp_R.x-1)
proof
assume that
A1: Z c= dom (ln*((exp_R-f)/exp_R)) 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)/exp_R)
by A1,FUNCT_1:11;
then Z c= dom ((exp_R-f)/exp_R) by TARSKI:def 3;
then Z c= dom (exp_R-f) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1;
then
A4: Z c= dom (exp_R-f) by XBOOLE_1:18;
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;
for x st x in Z holds exp_R.x<>0 by SIN_COS:54;
then
A9: (exp_R-f)/exp_R is_differentiable_on Z by A7,A8,FDIFF_2:21;
A10: for x st x in Z holds ((exp_R-f)`|Z).x =exp_R.x
proof
let x;
assume
A11: 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,A11,FDIFF_1:def 7
.= exp_R.x-0 by A5,A3,A11,FDIFF_1:23
.= exp_R.x;
end;
A12: for x st x in Z holds (((exp_R-f)/exp_R)`|Z).x=1/exp_R.x
proof
let x;
A13: exp_R.x <>0 by SIN_COS:54;
assume
A14: x in Z;
then
A15: (exp_R-f).x=exp_R.x - f.x by A4,VALUED_1:13
.=exp_R.x -1 by A2,A14;
exp_R is_differentiable_in x & exp_R-f is_differentiable_in x by A8,A14,
FDIFF_1:9,SIN_COS:65;
then diff((exp_R-f)/exp_R,x) =(diff((exp_R-f),x)*exp_R.x-diff(exp_R,x)*(
exp_R-f).x)/(exp_R.x)^2 by A13,FDIFF_2:14
.=(((exp_R-f)`|Z).x*exp_R.x-diff(exp_R,x)*(exp_R-f).x)/(exp_R.x)^2 by A8
,A14,FDIFF_1:def 7
.=(exp_R.x*exp_R.x-diff(exp_R,x)*(exp_R-f).x)/(exp_R.x)^2 by A10,A14
.=(exp_R.x*exp_R.x-exp_R.x*(exp_R.x-1))/(exp_R.x)^2 by A15,SIN_COS:65
.=(exp_R.x)/(exp_R.x)/(exp_R.x) by XCMPLX_1:78
.=1/exp_R.x by A13,XCMPLX_1:60;
hence thesis by A9,A14,FDIFF_1:def 7;
end;
A16: for x st x in Z holds ((exp_R-f)/exp_R).x >0
proof
let x;
A17: exp_R.x>0 by SIN_COS:54;
assume
A18: x in Z;
then x in dom ((exp_R-f)/exp_R) by A1,FUNCT_1:11;
then
A19: ((exp_R-f)/exp_R).x=(exp_R-f).x*(exp_R.x)" by RFUNCT_1:def 1
.=(exp_R-f).x*(1/exp_R.x) by XCMPLX_1:215
.=(exp_R-f).x/exp_R.x by XCMPLX_1:99;
(exp_R-f).x>0 by A2,A18;
hence thesis by A19,A17,XREAL_1:139;
end;
A20: for x st x in Z holds ln*((exp_R-f)/exp_R) is_differentiable_in x
proof
let x;
assume x in Z;
then (exp_R-f)/exp_R is_differentiable_in x & ((exp_R-f)/exp_R).x >0 by A9
,A16,FDIFF_1:9;
hence thesis by TAYLOR_1:20;
end;
then
A21: ln*((exp_R-f)/exp_R) is_differentiable_on Z by A1,FDIFF_1:9;
for x st x in Z holds ((ln*((exp_R-f)/exp_R))`|Z).x = 1/(exp_R.x-1)
proof
let x;
A22: exp_R.x>0 by SIN_COS:54;
assume
A23: x in Z;
then x in dom ((exp_R-f)/exp_R) by A1,FUNCT_1:11;
then
A24: ((exp_R-f)/exp_R).x=(exp_R-f).x*(exp_R.x)" by RFUNCT_1:def 1
.=(exp_R-f).x*(1/exp_R.x) by XCMPLX_1:215
.=(exp_R-f).x/exp_R.x by XCMPLX_1:99
.=(exp_R.x-f.x)/exp_R.x by A4,A23,VALUED_1:13
.=(exp_R.x-1)/exp_R.x by A2,A23;
((exp_R-f)/exp_R) is_differentiable_in x & ((exp_R-f)/exp_R).x >0 by A9,A16
,A23,FDIFF_1:9;
then diff(ln*((exp_R-f)/exp_R),x) =diff(((exp_R-f)/exp_R),x)/(((exp_R-f)/
exp_R).x) by TAYLOR_1:20
.=(((exp_R-f)/exp_R)`|Z).x/(((exp_R-f)/exp_R).x) by A9,A23,FDIFF_1:def 7
.=(1/exp_R.x)/((exp_R.x-1)/exp_R.x) by A12,A23,A24
.=1/(exp_R.x-1) by A22,XCMPLX_1:55;
hence thesis by A21,A23,FDIFF_1:def 7;
end;
hence thesis by A1,A20,FDIFF_1:9;
end;