:: Several Higher Differentiation Formulas of Special Functions
:: by Junjie Zhao , Xiquan Liang and Li Yan
::
:: Received March 18, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, NAT_1, FUNCT_1,
RELAT_1, XBOOLE_0, ARYTM_1, VALUED_1, TARSKI, XXREAL_0, PREPOWER,
ORDINAL4, CARD_1, NEWTON, ARYTM_3, FDIFF_1, SIN_COS, ABIAN, SQUARE_1,
REALSET1, TAYLOR_1, TAYLOR_2, XXREAL_1, COMPLEX1, FUNCOP_1, FUNCT_7;
notations SUBSET_1, FUNCT_1, PARTFUN1, RCOMP_1, XXREAL_0, ORDINAL1, NUMBERS,
XCMPLX_0, COMPLEX1, FUNCT_2, XREAL_0, FUNCOP_1, REAL_1, NAT_1, NAT_D,
VALUED_1, TAYLOR_2, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN,
XBOOLE_0, TARSKI, PREPOWER, RFUNCT_1, SQUARE_1, RELSET_1;
constructors REAL_1, NAT_1, RCOMP_1, LIMFUNC1, TAYLOR_2, FDIFF_1, SIN_COS,
ABIAN, TAYLOR_1, RFUNCT_1, SQUARE_1, PREPOWER, BINARITH, PARTFUN2,
VALUED_1, BINOP_2, NAT_D, SEQFUNC, RELSET_1, NEWTON, NUMBERS;
registrations RELSET_1, NUMBERS, NAT_1, MEMBERED, VALUED_0, RCOMP_1, FUNCT_1,
INT_1, ORDINAL1, FUNCT_2, XREAL_0, NEWTON, PREPOWER, SQUARE_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
definitions TAYLOR_1, TARSKI, XBOOLE_0;
equalities VALUED_1, SQUARE_1, XBOOLE_0;
expansions TAYLOR_1, TARSKI;
theorems RFUNCT_1, XBOOLE_0, NEWTON, XCMPLX_1, FUNCT_1, XBOOLE_1, ABSVALUE,
PARTFUN1, RELAT_1, RCOMP_1, SIN_COS, NAT_1, FDIFF_1, FDIFF_2, TAYLOR_1,
SIN_COS2, XREAL_1, ABIAN, XXREAL_0, TAYLOR_2, INT_1, WSIERP_1, FUNCT_2,
TARSKI, XCMPLX_0, VALUED_1, PREPOWER, ZFMISC_1, FDIFF_7, FDIFF_8,
FDIFF_4, FUNCOP_1, XREAL_0, ORDINAL1;
schemes NAT_1;
begin
reserve x,r,a,x0,p for Real;
reserve n,i,m for Element of NAT;
reserve Z for open Subset of REAL;
reserve f,f1,f2 for PartFunc of REAL,REAL;
reserve k for Nat;
theorem Th1:
for f being Function of REAL, REAL holds dom (f | Z) = Z
proof
let f be Function of REAL, REAL;
A1: dom f = REAL by FUNCT_2:def 1;
thus dom (f|Z) = dom f /\ Z by RELAT_1:61
.= Z by A1,XBOOLE_1:28;
end;
theorem Th2:
(-f1)(#)(-f2)=f1(#)f2
proof
dom(-f1) = dom f1 & dom(-f2) = dom f2 by VALUED_1:def 5;
then
A1: dom ((-f1)(#)(-f2)) = dom f1/\dom f2 by VALUED_1:def 4
.=dom(f1(#)f2) by VALUED_1:def 4;
for x be Element of REAL
st x in dom(f1(#)f2) holds ((-f1)(#)(-f2)).x=(f1(#)f2).x
proof
let x be Element of REAL;
assume
A2: x in dom(f1(#)f2);
dom(f1(#)f2) = dom f2/\dom f1 by VALUED_1:def 4;
then dom(f2(#)f1) c= dom f2 by XBOOLE_1:17;
then x in dom f2 by A2;
then
A3: x in dom((-1)(#)f2) by VALUED_1:def 5;
dom f1/\dom f2 c= dom f1 by XBOOLE_1:17;
then dom(f1(#)f2) c= dom f1 by VALUED_1:def 4;
then x in dom f1 by A2;
then
A4: x in dom((-1)(#)f1) by VALUED_1:def 5;
((-f1)(#)(-f2)).x =(-f1).x*(-f2).x by A1,A2,VALUED_1:def 4
.=(-1)*f1.x*((-1)(#)f2).x by A4,VALUED_1:def 5
.=(-1)*f1.x*((-1)*f2.x) by A3,VALUED_1:def 5
.=f1.x*f2.x;
hence thesis by A2,VALUED_1:def 4;
end;
hence thesis by A1,PARTFUN1:5;
end;
theorem Th3:
n>=1 implies dom(( #Z n)^) = REAL\{0} & ( #Z n)"{0}={0}
proof
assume
A1: n >= 1;
A2: ( #Z n)"{0} = {0}
proof
thus ( #Z n)"{0} c= {0}
proof
let x be object;
assume
A3: x in ( #Z n)"{0};
then reconsider x as Element of REAL;
( #Z n).x in {0} by A3,FUNCT_1:def 7;
then ( #Z n).x = 0 by TARSKI:def 1;
then x #Z n = 0 by TAYLOR_1:def 1;
then x |^ n = 0 by PREPOWER:36;
then x = 0 by PREPOWER:5;
hence thesis by TARSKI:def 1;
end;
let x be object;
A4: 0 in {0} by TARSKI:def 1;
assume x in {0};
then
A5: x = 0 by TARSKI:def 1;
{In(0,REAL)} c= REAL by ZFMISC_1:31;
then
A6: {0} c= dom( #Z n) by FUNCT_2:def 1;
( #Z n).0 = 0 #Z n by TAYLOR_1:def 1
.=0|^n by PREPOWER:36
.=0 by A1,NEWTON:11;
hence thesis by A5,A6,A4,FUNCT_1:def 7;
end;
then dom(( #Z n)^) = dom ( #Z n) \ {0} by RFUNCT_1:def 2
.= REAL \ {0} by FUNCT_2:def 1;
hence thesis by A2;
end;
theorem
(r*p)(#)(( #Z n)^)=r(#)(p(#)(( #Z n)^))
proof
A1: dom ((r*p) (#) (( #Z n)^)) = dom((( #Z n)^)) by VALUED_1:def 5
.= dom (p(#)(( #Z n)^)) by VALUED_1:def 5
.= dom (r(#)(p(#)(( #Z n)^))) by VALUED_1:def 5;
now
let c be object;
assume
A2: c in dom ((r*p)(#)(( #Z n)^));
then
A3: c in dom (p(#)(( #Z n)^)) by A1,VALUED_1:def 5;
thus ((r*p)(#)(( #Z n)^)).c = r*p * (( #Z n)^).c by A2,VALUED_1:def 5
.= r*(p * (( #Z n)^).c)
.= r * (p(#)(( #Z n)^)).c by A3,VALUED_1:def 5
.= (r(#)(p(#)(( #Z n)^))).c by A1,A2,VALUED_1:def 5;
end;
hence thesis by A1,FUNCT_1:2;
end;
theorem Th5:
for n,m be Real holds n(#)f1+m(#)f1=(n+m)(#)f1
proof
let n,m be Real;
A1: dom(n(#)f1+m(#)f1) = dom (n(#)f1)/\dom (m(#)f1) by VALUED_1:def 1
.= dom f1/\dom (m(#)f1)by VALUED_1:def 5
.= dom f1/\dom f1 by VALUED_1:def 5
.=dom f1;
A2: for x being Element of REAL st x in dom f1
holds (n(#)f1+m(#)f1).x=((n+m)(#)f1).x
proof
let x be Element of REAL;
assume
A3: x in dom f1;
then
A4: x in dom(n(#)f1) by VALUED_1:def 5;
x in dom((n+m)(#)f1) by A3,VALUED_1:def 5;
then
A5: ((n+m)(#)f1).x = (n+m)*f1.x by VALUED_1:def 5
.=n*f1.x +m*f1.x;
A6: x in dom(m(#)f1) by A3,VALUED_1:def 5;
(n(#)f1+m(#)f1).x = (n(#)f1).x+(m(#)f1).x by A1,A3,VALUED_1:def 1
.=n*f1.x +(m(#)f1).x by A4,VALUED_1:def 5
.=n*f1.x +m*f1.x by A6,VALUED_1:def 5;
hence thesis by A5;
end;
dom(n(#)f1+m(#)f1) = dom((n+m)(#)f1) by A1,VALUED_1:def 5;
hence thesis by A1,A2,PARTFUN1:5;
end;
theorem Th6:
f|Z is_differentiable_on Z implies f is_differentiable_on Z
proof
A1: dom (f|Z) c= dom f by RELAT_1:60;
assume
A2: f|Z is_differentiable_on Z;
then
A3: for x st x in Z holds f|Z is_differentiable_in x by FDIFF_1:9;
Z c= dom (f|Z) by A2,FDIFF_1:9;
then Z c= dom f by A1;
hence thesis by A3,FDIFF_1:def 6;
end;
theorem Th7:
n>=1 & f1 is_differentiable_on n,Z implies f1 is_differentiable_on Z
proof
assume that
A1: n>=1 and
A2: f1 is_differentiable_on n,Z;
1-1<=n-1 by A1,XREAL_1:9;
then diff(f1,Z).0 is_differentiable_on Z by A2;
then f1|Z is_differentiable_on Z by TAYLOR_1:def 5;
hence thesis by Th6;
end;
theorem Th8:
#Z n is_differentiable_on REAL
proof
A1: dom( #Z n) = REAL by FUNCT_2:def 1;
for x st x in REAL holds ( #Z n)|REAL is_differentiable_in x
proof
let x ;
assume x in REAL;
#Z n is_differentiable_in x by TAYLOR_1:2;
hence thesis by A1,RELAT_1:68;
end;
hence thesis by A1,FDIFF_1:def 6;
end;
:: 1 f.x = sin.x
theorem
x in Z implies (diff(sin,Z).2).x = -sin.x
proof
assume
A1: x in Z;
A2: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
A3: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
(diff(sin,Z).(2*1)).x = (diff(sin,Z).(1 +1) ).x
.=(diff(sin,Z).(1+0)`|Z).x by TAYLOR_1:def 5
.=((diff(sin,Z).0 `|Z)`|Z).x by TAYLOR_1:def 5
.=((sin | Z`|Z)`|Z).x by TAYLOR_1:def 5
.=((sin `| Z)`|Z).x by A3,FDIFF_2:16
.=((cos | Z)`|Z).x by TAYLOR_2:17
.=(cos `| Z).x by A2,FDIFF_2:16
.=diff(cos,x) by A1,A2,FDIFF_1:def 7
.=-sin.x by SIN_COS:63;
hence thesis;
end;
theorem
x in Z implies (diff(sin,Z).3).x = (-cos).x
proof
assume x in Z;
then
A1: x in dom (cos|Z) by TAYLOR_2:17;
dom ((-cos)|Z) = dom (-cos) /\ Z by RELAT_1:61
.= dom cos /\ Z by VALUED_1:8
.= dom (cos|Z) by RELAT_1:61
.= dom (-(cos|Z)) by VALUED_1:8;
then
A2: x in dom ((-cos)|Z) by A1,VALUED_1:8;
(diff(sin,Z).3).x = (diff(sin,Z).(2*1+1)).x
.= (((-1) |^ 1) (#) (cos | Z)).x by TAYLOR_2:19
.=((-1)(#)(cos | Z)).x
.=((-cos)|Z).x by RFUNCT_1:49
.=(-cos).x by A2,FUNCT_1:47;
hence thesis;
end;
theorem Th11:
x in Z implies (diff(sin,Z).n).x = sin.(x + n*PI/2)
proof
assume
A1: x in Z;
dom(((-1)(#) cos)|Z) = dom((-1)(#) cos)/\ Z by RELAT_1:61
.= dom(cos) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
then
A2: Z c= dom((-1)(#) cos) by RELAT_1:60;
dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by RELAT_1:61
.= dom(sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
then
A3: Z c= dom((-1)(#) sin) by RELAT_1:60;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A5: (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
A6: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A7: (-1)(#)cos is_differentiable_on Z by FDIFF_2:19;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
now
per cases;
suppose
i is even;
then consider j be Nat such that
A8: i = 2*j by ABIAN:def 2;
per cases;
suppose
j is even;
then consider m be Nat such that
A9: j = 2*m by ABIAN:def 2;
(diff(sin,Z).(i+1)).x = (diff(sin,Z).(2*j) `| Z).x by A8,
TAYLOR_1:def 5
.=((-1) |^ j (#) sin | Z`| Z).x by TAYLOR_2:19
.=( 1 |^ (2*m) (#) sin | Z`| Z).x by A9,WSIERP_1:2
.= (1 (#) sin | Z`| Z).x
.=(sin | Z`| Z).x by RFUNCT_1:21
.=(sin`| Z).x by A4,FDIFF_2:16
.=diff(sin,x) by A1,A4,FDIFF_1:def 7
.=cos.x by SIN_COS:64
.=cos.(x+(2*PI*m)) by SIN_COS2:11
.=sin.(x+((i/2)*PI)+PI/2) by A8,A9,SIN_COS:78
.=sin.(x + n*PI/2);
hence thesis;
end;
suppose
j is odd;
then consider s be Nat such that
A10: j = 2*s+1 by ABIAN:9;
(diff(sin,Z).(i+1)).x = (diff(sin,Z).(2*j) `| Z).x by A8,
TAYLOR_1:def 5
.=((-1) |^ (2*s+1) (#) sin | Z`| Z).x by A10,TAYLOR_2:19
.=(((-1) |^ (2*s)*(-1)) (#) sin | Z`| Z).x by NEWTON:6
.=((1|^ (2*s)*(-1)) (#) sin | Z`| Z).x by WSIERP_1:2
.=((1*(-1)) (#) sin | Z`| Z).x
.=((-sin)| Z`| Z).x by RFUNCT_1:49
.=(((-1) (#) sin)`| Z).x by A5,FDIFF_2:16
.=(-1)*diff(sin,x) by A1,A3,A4,FDIFF_1:20
.=(-1)*(cos.x) by SIN_COS:64
.=-cos.x
.=cos.(x+PI) by SIN_COS:78
.=cos.(x+PI+(2*PI*s)) by SIN_COS2:11
.=sin.(x+((i/2)*PI)+PI/2) by A8,A10,SIN_COS:78
.=sin.(x + n*PI/2);
hence thesis;
end;
end;
suppose
i is odd;
then consider j be Nat such that
A11: i = 2*j +1 by ABIAN:9;
per cases;
suppose
j is even;
then consider m be Nat such that
A12: j = 2*m by ABIAN:def 2;
(diff(sin,Z).(i+1)).x = (diff(sin,Z).(2*j+1) `| Z).x by A11,
TAYLOR_1:def 5
.=((-1) |^ (2*m) (#) cos | Z`| Z).x by A12,TAYLOR_2:19
.=( 1 |^ (2*m) (#) cos | Z`| Z).x by WSIERP_1:2
.= (1 (#) cos | Z`| Z).x
.=(cos | Z`| Z).x by RFUNCT_1:21
.=(cos`| Z).x by A6,FDIFF_2:16
.=diff(cos,x) by A1,A6,FDIFF_1:def 7
.=-sin.x by SIN_COS:63
.=sin.(x+PI) by SIN_COS:78
.=sin.(x+PI+(2*PI*m)) by SIN_COS2:10
.=sin.(x+(((i-1)/2)*PI)+PI) by A11,A12
.=sin.(x + n*PI/2);
hence thesis;
end;
suppose
j is odd;
then consider s be Nat such that
A13: j = 2*s+1 by ABIAN:9;
(diff(sin,Z).(i+1)).x = (diff(sin,Z).(2*j+1) `| Z).x by A11,
TAYLOR_1:def 5
.=((-1) |^ j (#) cos | Z`| Z).x by TAYLOR_2:19
.=(((-1) |^ (2*s)*(-1)) (#) cos | Z`| Z).x by A13,NEWTON:6
.=((1|^ (2*s)*(-1)) (#) cos | Z`| Z).x by WSIERP_1:2
.=((1*(-1)) (#) cos |Z`| Z).x
.=((-cos)| Z`| Z).x by RFUNCT_1:49
.=(((-1) (#) cos)`|Z).x by A7,FDIFF_2:16
.=(-1)*diff(cos,x) by A1,A2,A6,FDIFF_1:20
.=(-1)*(-sin.x) by SIN_COS:63
.=sin.(x+2*PI*s) by SIN_COS2:10
.=sin.(x+(((i-3)/2)*PI)+2*PI) by A11,A13,SIN_COS:78
.=sin.(x + n*PI/2);
hence thesis;
end;
end;
end;
hence thesis;
end;
suppose
A14: n=0;
then (diff(sin,Z).n).x = (sin|Z).x by TAYLOR_1:def 5
.=sin.(x+n*PI/2) by A1,A14,FUNCT_1:49;
hence thesis;
end;
end;
:: 2 f.x = cos.x
theorem
x in Z implies (diff(cos,Z).2).x = -cos.x
proof
assume
A1: x in Z;
A2: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by RELAT_1:61
.= dom(sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
then
A3: Z c= dom((-1)(#) sin) by RELAT_1:60;
A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A5: (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
(diff(cos,Z).2).x = (diff(cos,Z).(1 +1) ).x
.=(diff(cos,Z).(1+0)`|Z).x by TAYLOR_1:def 5
.=((diff(cos,Z).0 `|Z)`|Z).x by TAYLOR_1:def 5
.=((cos | Z`|Z)`|Z).x by TAYLOR_1:def 5
.=((cos `| Z)`|Z).x by A2,FDIFF_2:16
.=(((-sin) | Z)`|Z).x by TAYLOR_2:17
.=(((-1) (#) sin)`| Z).x by A5,FDIFF_2:16
.=(-1)*diff(sin,x) by A1,A4,A3,FDIFF_1:20
.=(-1)*(cos.x) by SIN_COS:64
.=-cos.x;
hence thesis;
end;
theorem
x in Z implies (diff(cos,Z).3).x = sin.x
proof
assume x in Z;
then
A1: x in dom (sin|Z) by TAYLOR_2:17;
(diff(cos,Z).3).x = (diff(cos,Z).(2*1+1)).x
.= (((-1) |^ (1+1)) (#) (sin | Z)).x by TAYLOR_2:19
.=(((1|^2)(#)sin| Z)).x by WSIERP_1:1
.=(((1*1)(#)sin| Z)).x
.=((sin)|Z).x by RFUNCT_1:21
.=(sin).x by A1,FUNCT_1:47;
hence thesis;
end;
theorem Th14:
x in Z implies (diff(cos,Z).n).x = cos.(x + n*PI/2)
proof
assume
A1: x in Z;
dom(((-1)(#) sin)|Z) = dom((-1)(#) sin)/\ Z by RELAT_1:61
.= dom(sin) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
then
A2: Z c= dom((-1)(#) sin) by RELAT_1:60;
dom(((-1)(#) cos)|Z) =dom((-1)(#) cos)/\ Z by RELAT_1:61
.= dom(cos) /\ Z by VALUED_1:def 5
.= Z by SIN_COS:24,XBOOLE_1:28;
then
A3: Z c= dom((-1)(#) cos) by RELAT_1:60;
A4: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A5: (-1)(#)cos is_differentiable_on Z by FDIFF_2:19;
A6: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A7: (-1)(#)sin is_differentiable_on Z by FDIFF_2:19;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
now
per cases;
suppose
i is even;
then consider j be Nat such that
A8: i = 2*j by ABIAN:def 2;
per cases;
suppose
j is even;
then consider m be Nat such that
A9: j = 2*m by ABIAN:def 2;
(diff(cos,Z).(i+1)).x = (diff(cos,Z).(2*j) `| Z).x by A8,
TAYLOR_1:def 5
.=((-1) |^ (2*m) (#) cos | Z`| Z).x by A9,TAYLOR_2:19
.=( 1 |^ (2*m) (#) cos | Z`| Z).x by WSIERP_1:2
.= (1 (#) cos | Z`| Z).x
.=(cos | Z`| Z).x by RFUNCT_1:21
.=(cos`| Z).x by A4,FDIFF_2:16
.=diff(cos,x) by A1,A4,FDIFF_1:def 7
.=-sin.x by SIN_COS:63
.=cos.(x+PI/2) by SIN_COS:78
.=cos.(x+PI/2+(2*PI*m)) by SIN_COS2:11
.=cos.(x+PI/2+((i/2)*PI)) by A8,A9
.=cos.(x+n*PI/2);
hence thesis;
end;
suppose
j is odd;
then consider s be Nat such that
A10: j = 2*s+1 by ABIAN:9;
(diff(cos,Z).(i+1)).x = (diff(cos,Z).(2*j) `| Z).x by A8,
TAYLOR_1:def 5
.=((-1) |^ (2*s+1) (#) cos | Z`| Z).x by A10,TAYLOR_2:19
.=(((-1) |^ (2*s)*(-1)) (#) cos | Z`| Z).x by NEWTON:6
.=((1|^ (2*s)*(-1)) (#) cos | Z`| Z).x by WSIERP_1:2
.=((1*(-1)) (#) cos | Z`| Z).x
.=((-cos)| Z`| Z).x by RFUNCT_1:49
.=(((-1) (#) cos)`| Z).x by A5,FDIFF_2:16
.=(-1)*diff(cos,x) by A1,A3,A4,FDIFF_1:20
.=(-1)*(-sin.x) by SIN_COS:63
.=sin.(x+(2*PI*s)) by SIN_COS2:10
.=sin.(x+((i/2-1)*PI)+2*PI) by A8,A10,SIN_COS:78
.=cos.(PI/2-(x+(i/2+1)*PI)) by SIN_COS:78
.=cos.(-(PI/2-(x+(i/2+1)*PI))) by SIN_COS:30
.=cos.(x+n*PI/2);
hence thesis;
end;
end;
suppose
i is odd;
then consider j be Nat such that
A11: i = 2*j +1 by ABIAN:9;
per cases;
suppose
j is even;
then consider m be Nat such that
A12: j = 2*m by ABIAN:def 2;
(diff(cos,Z).(i+1)).x = (diff(cos,Z).(2*j+1) `| Z).x by A11,
TAYLOR_1:def 5
.=((-1) |^ (2*m+1) (#) sin | Z`| Z).x by A12,TAYLOR_2:19
.=(((-1) |^ (2*m)*(-1)) (#) sin | Z`| Z).x by NEWTON:6
.=((1|^ (2*m)*(-1)) (#) sin | Z`| Z).x by WSIERP_1:2
.=((1*(-1)) (#) sin | Z`| Z).x
.=((-sin)| Z`| Z).x by RFUNCT_1:49
.=(((-1) (#) sin)`| Z).x by A7,FDIFF_2:16
.=(-1)*diff(sin,x) by A1,A2,A6,FDIFF_1:20
.=(-1)*(cos.x) by SIN_COS:64
.=-cos.x
.=cos.(x+PI) by SIN_COS:78
.=cos.(x+PI+2*PI*m) by SIN_COS2:11
.=cos.(x + (i+1)*PI/2) by A11,A12
.=cos.(x+n*PI/2);
hence thesis;
end;
suppose
j is odd;
then consider s be Nat such that
A13: j = 2*s+1 by ABIAN:9;
(diff(cos,Z).(i+1)).x = (diff(cos,Z).(2*j+1) `| Z).x by A11,
TAYLOR_1:def 5
.=((-1) |^ (j+1) (#) sin | Z`| Z).x by TAYLOR_2:19
.=(1|^ (2*(s+1)) (#) sin |Z`| Z).x by A13,WSIERP_1:2
.=(1 (#) sin | Z`| Z).x
.=( sin | Z`| Z).x by RFUNCT_1:21
.=(sin`|Z).x by A6,FDIFF_2:16
.=diff(sin,x) by A1,A6,FDIFF_1:def 7
.=cos.x by SIN_COS:64
.=cos.(x+(2*PI*s)) by SIN_COS2:11
.=cos.(x+(((i-1)/2-1)*PI)+2*PI) by A11,A13,SIN_COS:78
.=cos.(x+n*PI/2);
hence thesis;
end;
end;
end;
hence thesis;
end;
suppose
A14: n=0;
then (diff(cos,Z).n).x =(cos|Z).x by TAYLOR_1:def 5
.=cos.(x+n*PI/2) by A1,A14,FUNCT_1:49;
hence thesis;
end;
end;
theorem Th15:
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
implies diff(f1+f2,Z).n = diff(f1,Z).n + diff(f2,Z).n
proof
defpred P[Nat] means f1 is_differentiable_on $1,Z & f2 is_differentiable_on
$1,Z implies diff(f1+f2,Z).$1 = diff(f1,Z).$1 + diff(f2,Z).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
assume
A3: f1 is_differentiable_on (k+1),Z & f2 is_differentiable_on (k+1),Z;
A4: diff(f1,Z).k is_differentiable_on Z & diff(f2,Z).k
is_differentiable_on Z by A3;
k<k+1 by NAT_1:19;
then diff(f1+f2,Z).(k+1) = ((diff(f1,Z).k)+(diff(f2,Z).k))`|Z by A2,A3,
TAYLOR_1:23,def 5
.= (diff(f1,Z).k)`|Z + (diff(f2,Z).k)`|Z by A4,FDIFF_2:17
.= diff(f1,Z).(k+1) + (diff(f2,Z).k)`|Z by TAYLOR_1:def 5
.= diff(f1,Z).(k+1) + diff(f2,Z).(k+1) by TAYLOR_1:def 5;
hence thesis;
end;
A5: P[0]
proof
assume that
f1 is_differentiable_on 0,Z and
f2 is_differentiable_on 0,Z;
diff(f1+f2,Z).0 = (f1+f2)|Z by TAYLOR_1:def 5
.=f1|Z + f2|Z by RFUNCT_1:44
.=diff(f1,Z).0 + f2|Z by TAYLOR_1:def 5
.=diff(f1,Z).0 + diff(f2,Z).0 by TAYLOR_1:def 5;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th16:
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z
implies diff(f1-f2,Z).n = diff(f1,Z).n - diff(f2,Z).n
proof
defpred P[Nat] means
f1 is_differentiable_on $1,Z & f2
is_differentiable_on $1,Z implies diff(f1-f2,Z).$1 = diff(f1,Z).$1 - diff(f2,Z)
.$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat such that
A2: P[k];
assume
A3: f1 is_differentiable_on (k+1),Z & f2 is_differentiable_on (k+1),Z;
A4: diff(f1,Z).k is_differentiable_on Z & diff(f2,Z).k
is_differentiable_on Z by A3;
k<k+1 by NAT_1:19;
then diff(f1-f2,Z).(k+1) = ((diff(f1,Z).k)-(diff(f2,Z).k))`|Z by A2,A3,
TAYLOR_1:23,def 5
.= (diff(f1,Z).k)`|Z - (diff(f2,Z).k)`|Z by A4,FDIFF_2:18
.= diff(f1,Z).(k+1) - (diff(f2,Z).k)`|Z by TAYLOR_1:def 5
.= diff(f1,Z).(k+1) - diff(f2,Z).(k+1) by TAYLOR_1:def 5;
hence thesis;
end;
A5: P[0]
proof
assume that
f1 is_differentiable_on 0,Z and
f2 is_differentiable_on 0,Z;
diff(f1-f2,Z).0 = (f1-f2)|Z by TAYLOR_1:def 5
.=f1|Z - f2|Z by RFUNCT_1:47
.=diff(f1,Z).0 - f2|Z by TAYLOR_1:def 5
.=diff(f1,Z).0 - diff(f2,Z).0 by TAYLOR_1:def 5;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th17:
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n
implies diff(f1+f2,Z).i = diff(f1,Z).i + diff(f2,Z).i
proof
assume
A1: f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z;
assume i<=n;
then f1 is_differentiable_on i, Z & f2 is_differentiable_on i, Z by A1,
TAYLOR_1:23;
hence thesis by Th15;
end;
theorem Th18:
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i<=n
implies diff(f1-f2,Z).i = diff(f1,Z).i - diff(f2,Z).i
proof
assume
A1: f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z;
assume i<=n;
then f1 is_differentiable_on i, Z & f2 is_differentiable_on i, Z by A1,
TAYLOR_1:23;
hence thesis by Th16;
end;
theorem
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1+
f2 is_differentiable_on n,Z
proof
assume that
A1: f1 is_differentiable_on n,Z and
A2: f2 is_differentiable_on n,Z;
now
let i be Nat such that
A3: i <= n-1;
A4: i in NAT by ORDINAL1:def 12;
A5: diff(f2,Z).i is_differentiable_on Z by A2,A3;
then
A6: Z c= dom (diff(f2,Z).i) by FDIFF_1:def 6;
i <= n by A3,WSIERP_1:18;
then
A7: diff(f1+f2,Z).i = diff(f1,Z).i + diff(f2,Z).i by A1,A2,Th17,A4;
A8: diff(f1,Z).i is_differentiable_on Z by A1,A3;
then Z c= dom (diff(f1,Z).i) by FDIFF_1:def 6;
then Z c= dom (diff(f1,Z).i) /\ dom (diff(f2,Z).i) by A6,XBOOLE_1:19;
then Z c= dom(diff(f1,Z).i + diff(f2,Z).i) by VALUED_1:def 1;
hence diff(f1+f2,Z).i is_differentiable_on Z by A8,A5,A7,FDIFF_1:18;
end;
hence thesis;
end;
theorem
f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1-
f2 is_differentiable_on n,Z
proof
assume that
A1: f1 is_differentiable_on n,Z and
A2: f2 is_differentiable_on n,Z;
now
let i be Nat such that
A3: i <= n-1;
A4: i in NAT by ORDINAL1:def 12;
A5: diff(f2,Z).i is_differentiable_on Z by A2,A3;
then
A6: Z c= dom (diff(f2,Z).i) by FDIFF_1:def 6;
i <= n by A3,WSIERP_1:18;
then
A7: diff(f1-f2,Z).i = diff(f1,Z).i - diff(f2,Z).i by A1,A2,Th18,A4;
A8: diff(f1,Z).i is_differentiable_on Z by A1,A3;
then Z c= dom (diff(f1,Z).i) by FDIFF_1:def 6;
then Z c= dom (diff(f1,Z).i) /\ dom (diff(f2,Z).i) by A6,XBOOLE_1:19;
then Z c= dom(diff(f1,Z).i - diff(f2,Z).i) by VALUED_1:12;
hence diff(f1-f2,Z).i is_differentiable_on Z by A8,A5,A7,FDIFF_1:19;
end;
hence thesis;
end;
theorem Th21:
f is_differentiable_on n,Z implies diff(r(#)f,Z).n = r(#)diff(f, Z).n
proof
defpred P[Nat] means
f is_differentiable_on $1,Z implies diff(r
(#)f,Z).$1 = r(#)diff(f,Z).$1;
A1: for k be Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
assume
A3: f is_differentiable_on (k+1),Z;
A4: diff(f,Z).k is_differentiable_on Z by A3;
k<k+1 by NAT_1:19;
then diff(r(#)f,Z).(k+1) = (r(#)diff(f,Z).k) `| Z by A2,A3,TAYLOR_1:23
,def 5
.= r (#) (diff(f,Z).k `| Z) by A4,FDIFF_2:19
.= r(#) diff(f,Z).(k+1) by TAYLOR_1:def 5;
hence thesis;
end;
A5: P[0]
proof
assume f is_differentiable_on 0,Z;
diff(r(#)f,Z).0 = (r(#)f)|Z by TAYLOR_1:def 5
.=r(#)f|Z by RFUNCT_1:49
.=r(#)diff(f,Z).0 by TAYLOR_1:def 5;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A5,A1);
hence thesis;
end;
theorem Th22:
f is_differentiable_on n,Z implies r(#)f is_differentiable_on n, Z
proof
assume
A1: f is_differentiable_on n,Z;
now
let i be Nat such that
A2: i <= n-1;
A3: i in NAT by ORDINAL1:def 12;
diff(f,Z).i is_differentiable_on Z by A1,A2;
then
A4: r(#) diff(f,Z).i is_differentiable_on Z by FDIFF_2:19;
i <= n by A2,WSIERP_1:18;
hence diff(r(#)f,Z).i is_differentiable_on Z by A1,A4,Th21,TAYLOR_1:23,A3;
end;
hence thesis;
end;
theorem
f is_differentiable_on Z implies diff(f,Z).1 = f`|Z
proof
assume
A1: f is_differentiable_on Z;
then
A2: dom(f`|Z) = Z by FDIFF_1:def 7;
A3: for x being Element of REAL st x in Z holds (diff(f,Z).1).x = (f`|Z).x
proof
let x be Element of REAL;
assume x in Z;
(diff(f,Z).1).x =(diff(f,Z).(1+0)).x
.=((diff(f,Z).0)`|Z).x by TAYLOR_1:def 5
.=(f|Z`|Z).x by TAYLOR_1:def 5
.=(f`|Z).x by A1,FDIFF_2:16;
hence thesis;
end;
dom(diff(f,Z).1) = dom(diff(f,Z).(1+0))
.= dom((diff(f,Z).0)`|Z) by TAYLOR_1:def 5
.= dom(f|Z`|Z) by TAYLOR_1:def 5
.= dom(f`|Z) by A1,FDIFF_2:16
.= Z by A1,FDIFF_1:def 7;
hence thesis by A2,A3,PARTFUN1:5;
end;
theorem
n>=1 & f1 is_differentiable_on n,Z implies diff(f1,Z).1=f1`|Z
proof
assume n>=1 & f1 is_differentiable_on n,Z;
then
A1: f1 is_differentiable_on Z by Th7;
diff(f1,Z).1 = diff(f1,Z).(1+0) .=diff(f1,Z).0`|Z by TAYLOR_1:def 5
.=f1|Z`|Z by TAYLOR_1:def 5
.=f1`|Z by A1,FDIFF_2:16;
hence thesis;
end;
theorem
x in Z implies (diff(r(#)sin,Z).n).x = r*sin.(x + n*PI/2)
proof
assume
A1: x in Z;
A2: sin is_differentiable_on n, Z by TAYLOR_2:21;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
A3: diff(sin,Z ).i is_differentiable_on Z by A2;
dom (diff(sin,Z ).n) = dom (diff(sin,Z ).(i+1))
.= dom((diff(sin,Z ).i)`|Z ) by TAYLOR_1:def 5
.= Z by A3,FDIFF_1:def 7;
then
A4: x in dom (r (#) diff(sin,Z).n) by A1,VALUED_1:def 5;
(diff(r(#)sin,Z ).n).x = (r (#) diff(sin,Z ).n).x by A2,Th21
.= r* (diff(sin,Z ).n).x by A4,VALUED_1:def 5
.= r* (sin.(x + n*PI/2)) by A1,Th11;
hence thesis;
end;
suppose
A5: n=0;
A6: dom(r(#) (sin|Z )) = dom(sin|Z) by VALUED_1:def 5
.= Z by Th1;
(diff(r(#)sin,Z ).n).x = (r (#) diff(sin,Z ).0).x by A2,A5,Th21
.=(r (#) (sin|Z)).x by TAYLOR_1:def 5
.=r*(sin|Z).x by A1,A6,VALUED_1:def 5
.=r* (sin.(x + n*PI/2)) by A1,A5,FUNCT_1:49;
hence thesis;
end;
end;
theorem
x in Z implies (diff(r(#)cos,Z).n).x = r*cos.(x + n*PI/2)
proof
assume
A1: x in Z;
A2: cos is_differentiable_on n, Z by TAYLOR_2:21;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
A3: diff(cos,Z ).i is_differentiable_on Z by A2;
dom (diff(cos,Z ).n) = dom(diff(cos,Z ).(i+1))
.= dom((diff(cos,Z ).i)`|Z ) by TAYLOR_1:def 5
.= Z by A3,FDIFF_1:def 7;
then
A4: x in dom (r (#) diff(cos,Z).n) by A1,VALUED_1:def 5;
(diff(r(#)cos,Z ).n).x = (r (#) diff(cos,Z).n).x by A2,Th21
.= r* (diff(cos,Z).n).x by A4,VALUED_1:def 5
.= r* (cos.(x + n*PI/2)) by A1,Th14;
hence thesis;
end;
suppose
A5: n=0;
A6: dom(r(#) (cos|Z )) = dom(cos|Z) by VALUED_1:def 5
.= Z by Th1;
(diff(r(#)cos,Z ).n).x=(r (#) diff(cos,Z ).0).x by A2,A5,Th21
.=(r (#) (cos|Z)).x by TAYLOR_1:def 5
.=r*(cos|Z).x by A1,A6,VALUED_1:def 5
.=r* (cos.(x + n*PI/2)) by A1,A5,FUNCT_1:49;
hence thesis;
end;
end;
theorem
x in Z implies (diff(r(#)exp_R,Z).n).x = r*exp_R.x
proof
assume
A1: x in Z;
A2: exp_R is_differentiable_on n,Z by TAYLOR_2:10;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
A3: diff(exp_R,Z).i is_differentiable_on Z by A2;
dom (diff(exp_R,Z).n) = dom (diff(exp_R,Z).(i+1))
.= dom((diff(exp_R,Z).i)`|Z) by TAYLOR_1:def 5
.= Z by A3,FDIFF_1:def 7;
then
A4: x in dom (r (#) diff(exp_R,Z).n) by A1,VALUED_1:def 5;
(diff(r(#)exp_R,Z).n).x = (r (#) diff(exp_R,Z).n).x by Th21,TAYLOR_2:10
.= r*(diff(exp_R,Z).n).x by A4,VALUED_1:def 5
.= r*exp_R.x by A1,TAYLOR_2:7;
hence thesis;
end;
suppose
A5: n=0;
A6: dom(r(#) (exp_R|Z )) = dom(exp_R|Z ) by VALUED_1:def 5
.= Z by Th1;
(diff(r(#)exp_R,Z).n).x = (r (#) diff(exp_R,Z).0).x by A5,Th21,TAYLOR_2:10
.= (r (#) exp_R|Z).x by TAYLOR_1:def 5
.= r* ( exp_R|Z).x by A1,A6,VALUED_1:def 5
.= r*exp_R.x by A1,FUNCT_1:49;
hence thesis;
end;
end;
theorem Th28:
#Z n `| Z = (n(#) #Z (n-1)) | Z
proof
dom (n (#) #Z (n-1) ) = dom ( #Z (n-1) ) by VALUED_1:def 5;
then
A1: dom (n (#) #Z (n-1) ) = REAL by FUNCT_2:def 1;
then n (#) #Z (n-1) is Function of REAL, REAL by FUNCT_2:67;
then
A2: dom ((n (#) #Z (n-1)) | Z) = Z by Th1;
A3: #Z n is_differentiable_on Z by Th8,FDIFF_1:26;
A4: for x be Element of REAL st x in Z
holds (( #Z n ) `| Z ).x = ((n (#) #Z (n-1) )| Z
).x
proof
let x be Element of REAL such that
A5: x in Z;
(( #Z n ) `| Z).x = diff(( #Z n),x) by A3,A5,FDIFF_1:def 7
.= n * x #Z (n-1) by TAYLOR_1:2
.=n*( #Z (n-1) ).x by TAYLOR_1:def 1
.=(n (#) #Z (n-1)).x by A1,VALUED_1:def 5
.=((n (#) #Z (n-1)) | Z).x by A2,A5,FUNCT_1:47;
hence thesis;
end;
dom (( #Z n )`| Z) = Z by A3,FDIFF_1:def 7;
hence thesis by A2,A4,PARTFUN1:5;
end;
theorem Th29:
x <> 0 implies ( #Z n)^ is_differentiable_in x & diff(( #Z n)^,x
) = -(n * x #Z (n-1))/(x #Z n)^2
proof
A1: ( #Z n).x = x #Z n & x #Z n = x|^n by PREPOWER:36,TAYLOR_1:def 1;
assume x<>0;
then
A2: ( #Z n).x <>0 by A1,PREPOWER:5;
A3: #Z n is_differentiable_in x by TAYLOR_1:2;
then diff(( #Z n)^,x) = - diff( #Z n,x)/(( #Z n).x)^2 by A2,FDIFF_2:15
.= -(n * x #Z (n-1))/( #Z n.x)^2 by TAYLOR_1:2
.= -(n * x #Z (n-1))/(x #Z n)^2 by TAYLOR_1:def 1;
hence thesis by A2,A3,FDIFF_2:15;
end;
theorem Th30:
n>=1 implies diff( #Z n,Z).2 = (n*(n-1)(#) #Z (n-2))|Z
proof
assume n>=1;
then reconsider m = n-1 as Element of NAT by INT_1:5;
A1: #Z n is_differentiable_on Z by Th8,FDIFF_1:26;
A2: #Z m is_differentiable_on Z by Th8,FDIFF_1:26;
then
A3: (m+1)(#) #Z m is_differentiable_on Z by FDIFF_2:19;
diff( #Z n,Z).2 = diff( #Z n, Z).(1+1)
.= (diff( #Z n, Z ).(1+0))`|Z by TAYLOR_1:def 5
.= (diff( #Z n, Z ).0 `|Z)`|Z by TAYLOR_1:def 5
.= (( #Z n |Z) `|Z)`|Z by TAYLOR_1:def 5
.= ( #Z n `|Z)`|Z by A1,FDIFF_2:16
.= (((m+1)(#) #Z ((m+1)-1))| Z)`|Z by Th28
.= ((m+1)(#) #Z m )`|Z by A3,FDIFF_2:16
.=(m+1) (#) ( #Z m`|Z) by A2,FDIFF_2:19
.=(m+1) (#) ((m (#) #Z (m-1))|Z) by Th28
.=((m+1)(#)(m (#) #Z (m-1) )) |Z by RFUNCT_1:49
.=(n*(n-1)(#) #Z (n-2))|Z by RFUNCT_1:17;
hence thesis;
end;
theorem
n>=2 implies diff( #Z n,Z).3 = (n*(n-1)*(n-2)(#) #Z (n-3))|Z
proof
assume
A1: 2<=n;
then
A2: 2+(-1)<=n+0 by XREAL_1:7;
reconsider m = n-2 as Element of NAT by A1,INT_1:5;
A3: #Z m is_differentiable_on Z by Th8,FDIFF_1:26;
then
A4: (m+2)*(m+1)(#) #Z m is_differentiable_on Z by FDIFF_2:19;
diff( #Z n,Z).3 = diff( #Z n,Z).(2+1)
.= diff( #Z n,Z).2 `|Z by TAYLOR_1:def 5
.= ((n*(n-1)(#) #Z (n-2))|Z) `|Z by A2,Th30
.= ((m+2)*(m+1)(#) #Z m) `|Z by A4,FDIFF_2:16
.= (m+2)*(m+1)(#)( #Z m`|Z ) by A3,FDIFF_2:19
.= (m+2)*(m+1)(#)(( m(#) #Z(m-1))|Z) by Th28
.=(n*(n-1)(#)((n-2)(#) #Z (n-3))) |Z by RFUNCT_1:49
.=(n*(n-1)*(n-2)(#) #Z (n-3)) |Z by RFUNCT_1:17;
hence thesis;
end;
Lm1: n>1 implies (m!)/(n!)*n = (m!)/((n-'1)!)
proof
assume
A1: n>1;
then n-1=n-'1 by XREAL_1:233;
then n=n-'1+1;
then (m!)/(n!)*n = (m!)/((n-'1)!*n)*n by NEWTON:15
.= (m!)/((n-'1)!) by A1,XCMPLX_1:92;
hence thesis;
end;
theorem Th32:
n>m implies diff( #Z n,Z).m = ((n choose m)*(m!)(#) #Z (n-m)) |Z
proof
defpred P[Nat] means n>$1 implies diff( #Z n,Z).$1 = (((n choose $1)*($1!))
(#) #Z (n-$1)) | Z;
A1: for k st P[k] holds P[k+1]
proof
let k such that
A2: P[k];
assume
A3: n>(k+1);
then
A4: n-k>(k+1)-k by XREAL_1:9;
A5: (k+1)+(-1)<=n+0 by A3,XREAL_1:7;
then reconsider l=n-k as Element of NAT by INT_1:5;
l>=(k+1)-k by A3,XREAL_1:9;
then
A6: ((k+1)!)>0 & l-'1=n-k-1 by XREAL_1:233;
reconsider s=n-(k+1) as Element of NAT by A3,INT_1:5;
A7: #Z (l) is_differentiable_on Z by Th8,FDIFF_1:26;
then
A8: (n choose k)*(k!)(#) #Z (l) is_differentiable_on Z by FDIFF_2:19;
0+k<1+k by XREAL_1:6;
then
diff( #Z n,Z).(k+1) =((((n choose k)*(k!))(#) #Z (l)) | Z) `| Z by A2,A3,
TAYLOR_1:def 5,XXREAL_0:2
.=(((n choose k)*(k!))(#) #Z (l))`| Z by A8,FDIFF_2:16
.=(n choose k)*(k!)(#) ( #Z (l) `| Z) by A7,FDIFF_2:19
.=((n choose k)*(k!))(#) (((l)(#) #Z ((l)-1)) | Z) by Th28
.=(((n choose k)*(k!))(#) ((l)(#) #Z (l-1)))| Z by RFUNCT_1:49
.=(((n choose k)*(k!)*(l))(#) #Z (l-1))| Z by RFUNCT_1:17
.=(((n!)/((k!) * (l!))*(k!)*(n-k))(#) #Z (l-1))| Z by A5,NEWTON:def 3
.=(((n!)/ (l!)*l)(#) #Z (l-1))| Z by XCMPLX_1:92
.=(((n!)/ ((l-'1)!))(#) #Z (l-1))| Z by A4,Lm1
.=(((n!)/ (((s)!)*((k+1)!)))*((k+1)!)(#) #Z (n-k-1))| Z by A6,XCMPLX_1:92
.=((n choose (k+1))*((k+1)!)(#) #Z (n-(k+1)))| Z by A3,NEWTON:def 3;
hence thesis;
end;
A9: P[0]
proof
assume n>0;
diff( #Z n,Z).0 = #Z n | Z by TAYLOR_1:def 5
.=((1*1)(#) #Z n )| Z by RFUNCT_1:21
.=(((n choose 0)*(0!))(#) #Z (n-0))| Z by NEWTON:12,19;
hence thesis;
end;
for k holds P[k] from NAT_1:sch 2 (A9,A1);
hence thesis;
end;
theorem
f is_differentiable_on n,Z implies diff(-f,Z).n = -diff(f,Z).n & -f
is_differentiable_on n,Z
by Th21,Th22;
theorem
x0 in Z implies Taylor(sin,Z,x0,x).n = sin.(x0+n*PI/2)*(x-x0)|^ n / (n
!) & Taylor(cos,Z,x0,x).n = cos.(x0+n*PI/2)*(x-x0)|^ n / (n!)
proof
assume
A1: x0 in Z;
A2: Taylor(cos,Z,x0,x).n =(diff(cos,Z).n).x0 *(x-x0)|^ n / (n!) by
TAYLOR_1:def 7
.=cos.(x0+n*PI/2)*(x-x0)|^ n / (n!) by A1,Th14;
Taylor(sin,Z,x0,x).n =(diff(sin,Z).n).x0 *(x-x0)|^ n / (n!) by TAYLOR_1:def 7
.=sin.(x0+n*PI/2)*(x-x0)|^ n / (n!) by A1,Th11;
hence thesis by A2;
end;
theorem
r>0 implies Maclaurin(sin,].-r,r.[,x).n = sin.(n*PI/2)*x|^ n / (n!) &
Maclaurin(cos,].-r,r.[,x).n = cos.(n*PI/2)*x|^ n / (n!)
proof
A1: |.0-0.|=0 by ABSVALUE:2;
assume r>0;
then
A2: 0 in ].0-r,0+r.[ by A1,RCOMP_1:1;
A3: Maclaurin(cos,].-r,r.[,x).n =Taylor(cos,].-r,r.[,0,x).n by TAYLOR_2:def 1
.=(diff(cos,].-r,r.[).n).0 *(x-0)|^ n / (n!) by TAYLOR_1:def 7
.=cos.(0+n*PI/2)*x|^ n / (n!) by A2,Th14;
Maclaurin(sin,].-r,r.[,x).n =Taylor(sin,].-r,r.[,0,x).n by TAYLOR_2:def 1
.=(diff(sin,].-r,r.[).n).0 *(x-0)|^ n / (n!) by TAYLOR_1:def 7
.=sin.(0+n*PI/2)*x|^ n / (n!) by A2,Th11;
hence thesis by A3;
end;
theorem Th36:
n>m & x in Z implies (diff( #Z n,Z).m).x = (n choose m)*(m!)*x #Z (n-m)
proof
assume that
A1: n>m and
A2: x in Z;
dom( #Z (n-m))=REAL by FUNCT_2:def 1;
then
A3: dom((n choose m)*(m!)(#) #Z (n-m))= REAL by VALUED_1:def 5;
then
A4: dom(((n choose m)*(m!)(#) #Z (n-m))|Z) = REAL /\ Z by RELAT_1:61
.= Z by XBOOLE_1:28;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
(diff( #Z n,Z).m).x =(((n choose m)*(m!)(#) #Z (n-m))| Z).x by A1,Th32
.= ((n choose m)*(m!)(#) #Z (n-m)).x by A2,A4,FUNCT_1:47
.=(n choose m)*(m!)*( #Z (n-m)).xx by A3,VALUED_1:def 5
.=(n choose m)*(m!)*x #Z (n-m) by TAYLOR_1:def 1;
hence thesis;
end;
theorem Th37:
x in Z implies (diff( #Z m,Z).m).x = m!
proof
assume
A1: x in Z;
per cases;
suppose
m>0;
then 0<0+m;
then 1<=m by NAT_1:19;
then reconsider n=m-1 as Element of NAT by INT_1:5;
A2: 0+n<n+1 by XREAL_1:6;
A3: #Z 1 is_differentiable_on Z by Th8,FDIFF_1:26;
then
A4: ((n+1)!)(#) #Z 1 is_differentiable_on Z by FDIFF_2:19;
Z c= dom( #Z 1) by A3,FDIFF_1:def 6;
then
A5: Z c= dom (((n+1)!)(#) #Z 1) by VALUED_1:def 5;
(diff( #Z m,Z).m).x =(diff( #Z (n+1),Z).n`| Z).x by TAYLOR_1:def 5
.=(((((n+1) choose n)*(n!)(#) #Z ((n+1)-n)) | Z )`| Z).x by A2,Th32
.=((((((n+1)!)/((n!)*1))*(n!)(#) #Z ((n+1)-n))|Z )`|Z).x by A2,NEWTON:13
,def 3
.=(((((n+1)!)/1(#) #Z 1 )|Z )`| Z).x by XCMPLX_1:92
.=((((n+1)!)(#) #Z 1)`| Z).x by A4,FDIFF_2:16
.=((n+1)!)*diff( #Z 1,x) by A1,A3,A5,FDIFF_1:20
.=((n+1)!)*(1*x #Z (1-1)) by TAYLOR_1:2
.=((n+1)!)*1 by PREPOWER:34
.=m!;
hence thesis;
end;
suppose
A6: m=0;
then (diff( #Z m,Z).m).x = ( #Z 0|Z).x by TAYLOR_1:def 5
.= ( #Z 0).x by A1,FUNCT_1:49
.=x #Z 0 by TAYLOR_1:def 1
.=m! by A6,NEWTON:12,PREPOWER:34;
hence thesis;
end;
end;
theorem Th38:
#Z n is_differentiable_on n,Z
proof
let i be Nat;
assume
A1: i <= n-1;
reconsider i as Element of NAT by ORDINAL1:def 12;
-1+n<0+n by XREAL_1:6;
then
A2: i<n by A1,XXREAL_0:2;
A3: for x be Real
st x in Z holds diff( #Z n,Z).i | Z is_differentiable_in x
proof
i+0 <= (n-1)+1 by A1,XREAL_1:8;
then reconsider m = n-i as Element of NAT by INT_1:5;
A4: #Z m is_differentiable_on Z by Th8,FDIFF_1:26;
let x be Real;
assume x in Z;
then
A5: #Z m | Z is_differentiable_in x by A4,FDIFF_1:def 6;
diff( #Z n,Z).i | Z =(((n choose i)*(i!))(#) #Z m) | Z | Z by A2,Th32
.=(((n choose i)*(i!))(#) #Z m) |Z by FUNCT_1:51
.=((n choose i)*(i!))(#) #Z m | Z by RFUNCT_1:49;
hence thesis by A5,FDIFF_1:15;
end;
dom( #Z (n-i))=REAL by FUNCT_2:def 1;
then
A6: dom((n choose i)*(i!)(#) #Z (n-i))= REAL by VALUED_1:def 5;
dom(diff( #Z n,Z).i) = dom(((n choose i)*(i!)(#) #Z (n-i)) | Z) by A2,Th32
.= REAL /\ Z by A6,RELAT_1:61
.= Z by XBOOLE_1:28;
hence thesis by A3,FDIFF_1:def 6;
end;
theorem
x in Z & n>m implies (diff(a(#) #Z n,Z).m).x = a*(n choose m)*(m!)*x #Z (n-m)
proof
assume that
A1: x in Z and
A2: n>m;
dom( #Z (n-m))=REAL by FUNCT_2:def 1;
then
A3: dom((n choose m)*(m!)(#) #Z (n-m))= REAL by VALUED_1:def 5;
A4: dom(diff( #Z n,Z).m) = dom(((n choose m)*(m!)(#) #Z (n-m)) | Z) by A2,Th32
.= REAL /\ Z by A3,RELAT_1:61
.= Z by XBOOLE_1:28;
A5: dom(a(#)diff( #Z n,Z).m) = dom(diff( #Z n,Z).m) by VALUED_1:def 5;
#Z n is_differentiable_on m, Z by A2,Th38,TAYLOR_1:23;
then (diff(a(#) #Z n,Z).m).x = (a(#)diff( #Z n,Z).m).x by Th21
.= a*(diff( #Z n,Z).m).x by A1,A4,A5,VALUED_1:def 5
.= a*((n choose m)*(m!)*x #Z (n-m)) by A1,A2,Th36;
hence thesis;
end;
theorem
x in Z implies (diff(a(#) #Z n,Z).n).x = a*(n!)
proof
assume
A1: x in Z;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
per cases;
suppose
n>0;
then 0<0+n;
then 1<=n by NAT_1:19;
then reconsider m=n-1 as Element of NAT by INT_1:5;
A2: dom(a(#)diff( #Z n,Z).n) = dom(diff( #Z n,Z).n) by VALUED_1:def 5;
#Z n is_differentiable_on n, Z by Th38;
then
A3: (diff( #Z n,Z).m) is_differentiable_on Z;
A4: dom(diff( #Z n,Z).n) = dom(diff( #Z n,Z).(m+1))
.= dom( (diff( #Z n,Z).m)`| Z) by TAYLOR_1:def 5
.=Z by A3,FDIFF_1:def 7;
(diff(a(#) #Z n,Z).n).x = (a(#)diff( #Z n,Z).n).x by Th21,Th38
.=a*(diff( #Z n,Z).n).x by A1,A4,A2,VALUED_1:def 5
.=a*(n!) by A1,Th37;
hence thesis;
end;
suppose
A5: n=0;
dom( #Z 0)=REAL by FUNCT_2:def 1;
then
A6: dom(a(#) #Z 0)=REAL by VALUED_1:def 5;
(diff(a(#) #Z n,Z).n).x =(a(#)diff( #Z 0,Z).0).x by A5,Th21,Th38
.=(a(#) #Z 0|Z).x by TAYLOR_1:def 5
.=((a(#) #Z 0)|Z).x by RFUNCT_1:49
.=(a(#) #Z 0).x by A1,FUNCT_1:49
.=a*( #Z 0).xx by A6,VALUED_1:def 5
.=a*x #Z 0 by TAYLOR_1:def 1
.=a*(n!) by A5,NEWTON:12,PREPOWER:34;
hence thesis;
end;
end;
theorem Th41:
x0 in Z & n>m implies Taylor( #Z n,Z,x0,x).m = (n choose m)*x0
#Z (n-m) *(x-x0)|^ m & Taylor( #Z n,Z,x0,x).n = (x-x0)|^ n
proof
assume that
A1: x0 in Z and
A2: n>m;
A3: Taylor( #Z n,Z,x0,x).n =(diff( #Z n,Z).n).x0*(x-x0)|^ n / (n!) by
TAYLOR_1:def 7
.=(x-x0)|^ n*(n!)/ (n!) by A1,Th37
.=(x-x0)|^ n by XCMPLX_1:89;
Taylor( #Z n,Z,x0,x).m = (diff( #Z n,Z).m).x0*(x-x0)|^ m / (m!) by
TAYLOR_1:def 7
.= (n choose m)*(m!)*x0 #Z (n-m)*(x-x0)|^ m / (m!) by A1,A2,Th36
.=(n choose m)*(x0 #Z (n-m)*(x-x0)|^ m)*(m!)/ (m!)
.= (n choose m)*x0 #Z (n-m)*(x-x0)|^ m by XCMPLX_1:89;
hence thesis by A3;
end;
theorem
for n,m be Element of NAT,r,x be Element of REAL st n>m & r>0
holds Maclaurin( #Z
n,].-r,r.[,x).m = 0 & Maclaurin( #Z n,].-r,r.[,x).n = x|^ n
proof
let n,m be Element of NAT;
let r,x be Element of REAL;
assume that
A1: n>m and
A2: r>0;
|.0-0.|=0 by ABSVALUE:2;
then
A3: 0 in ].0-r,0+r.[ by A2,RCOMP_1:1;
reconsider s = n-m as Element of NAT by A1,INT_1:5;
A4: n-m>m-m by A1,XREAL_1:9;
A5: Maclaurin( #Z n,].-r,r.[,x).n =Taylor( #Z n,].-r,r.[,0,x).n by
TAYLOR_2:def 1
.=(x-0)|^ n by A1,A3,Th41
.=x|^ n;
Maclaurin( #Z n,].-r,r.[,x).m =Taylor( #Z n,].-r,r.[,0,x).m by TAYLOR_2:def 1
.=(n choose m)*0 #Z (n-m)*(x-0)|^ m by A1,A3,Th41
.=(n choose m)*(0|^s)*x|^ m by PREPOWER:36
.=(n choose m)*0*x|^ m by A4,NEWTON:84
.=0;
hence thesis by A5;
end;
theorem Th43:
not 0 in Z implies ( #Z n)^ is_differentiable_on Z
proof
assume
A1: not 0 in Z;
A2: for x0 st x0 in Z holds #Z n.x0 <> 0
proof
let x0;
A3: #Z n.x0 = x0 #Z n by TAYLOR_1:def 1;
assume x0 in Z;
hence thesis by A1,A3,PREPOWER:38;
end;
#Z n is_differentiable_on Z by Th8,FDIFF_1:26;
hence thesis by A2,FDIFF_2:22;
end;
theorem
not 0 in Z & x0 in Z implies ((( #Z n)^)`|Z).x0 =- n/( #Z (n+1)).x0
proof
assume that
A1: not 0 in Z and
A2: x0 in Z;
A3: ( #Z n)^ is_differentiable_on Z by A1,Th43;
per cases;
suppose
n>0;
then 0<0+n;
then n>=1 by NAT_1:19;
then reconsider i=n-1 as Element of NAT by INT_1:5;
x0 #Z i<>0 by A1,A2,PREPOWER:38;
then
A4: x0|^i<>0 by PREPOWER:36;
((( #Z n)^)`|Z).x0 = diff(( #Z n)^,x0) by A2,A3,FDIFF_1:def 7
.=- (n* x0 #Z i) /( x0 #Z n)^2 by A1,A2,Th29
.=- (n* x0 #Z i) /(x0 |^n)^2 by PREPOWER:36
.= - (n* x0|^i) /( x0 |^n)^2 by PREPOWER:36
.=- (n* x0|^i) /(( x0 |^(i+1))*( x0 |^1*x0 |^i)) by NEWTON:8
.=- (n* x0|^i) /(( x0 |^(i+1)* x0 |^1)*x0 |^i)
.=- (n* x0|^i) /( x0 |^(i+1+1)*x0 |^i) by NEWTON:8
.=- n/x0 |^(i+2) by A4,XCMPLX_1:91
.=- n/x0 #Z (i+2) by PREPOWER:36
.=- n/( #Z (n+1)).x0 by TAYLOR_1:def 1;
hence thesis;
end;
suppose
A5: n=0;
((( #Z n)^)`|Z).x0 = diff(( #Z n)^,x0) by A2,A3,FDIFF_1:def 7
.=- (0* x0 #Z (n-1)) /( x0 #Z n)^2 by A1,A2,A5,Th29
.=- n/( #Z (n+1)).x0 by A5;
hence thesis;
end;
end;
Lm2: #Z 1 = id REAL
proof
for x being Element of REAL holds ( #Z 1).x = (id REAL).x
proof
let x be Element of REAL;
( #Z 1).x = x #Z 1 by TAYLOR_1:def 1
.= x by PREPOWER:35
.= (id REAL).x;
hence thesis;
end;
hence thesis by FUNCT_2:63;
end;
theorem Th45: :: FDIFF_4:14
x <> 0 implies (id REAL)^ is_differentiable_in x & diff((id REAL
)^,x) = -1/x^2
proof
set f = id REAL;
assume
A1: x<>0;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
f.x = x #Z 1 & x #Z 1 = x|^1 by Lm2,PREPOWER:36,TAYLOR_1:def 1;
then
A2: f.x <> 0 by A1;
A3: f is_differentiable_in x by Lm2,TAYLOR_1:2;
then diff(f^,x) = - diff(f,x)/(f.x)^2 by A2,FDIFF_2:15
.=-(1 * x #Z (1-1))/(f.xx)^2 by Lm2,TAYLOR_1:2
.=-(1 * x #Z 0)/x^2
.=-1/x^2 by PREPOWER:34;
hence thesis by A2,A3,FDIFF_2:15;
end;
theorem
not 0 in Z implies ((id REAL)^)`|Z = ((-1)(#)(( #Z 2)^))|Z
proof
assume
A1: not 0 in Z;
then (id REAL)^ is_differentiable_on Z by Lm2,Th43;
then
A2: dom(((id REAL)^)`|Z) = Z by FDIFF_1:def 7;
A3: dom (( #Z 2)^) = REAL \ {0} by Th3;
then
A4: Z c= dom (( #Z 2)^) by A1,ZFMISC_1:34;
A5: for x0 being Element of REAL st
x0 in Z holds (((id REAL)^)`|Z).x0 = (((-1)(#)(( #Z 2)^))|Z). x0
proof
A6: dom((-1)(#)(( #Z 2)^))=dom((( #Z (1+1))^)) by VALUED_1:def 5;
let x0 be Element of REAL;
assume
A7: x0 in Z;
(id REAL)^ is_differentiable_on Z by A1,Lm2,Th43;
then (((id REAL)^)`|Z).x0 = diff((id REAL)^,x0) by A7,FDIFF_1:def 7
.=-1/x0^2 by A1,A7,Th45
.=-1/(x0|^(1+1)) by NEWTON:81
.=-1/x0 #Z 2 by PREPOWER:36
.=-1/( #Z 2).x0 by TAYLOR_1:def 1
.=-1*(( #Z 2).x0)" by XCMPLX_0:def 9
.=-1*(( #Z 2)^).x0 by A4,A7,RFUNCT_1:def 2
.=(-1)*(( #Z 2)^).x0
.=((-1)(#)(( #Z 2)^)).x0 by A4,A7,A6,VALUED_1:def 5
.=(((-1)(#)(( #Z 2)^))|Z).x0 by A7,FUNCT_1:49;
hence thesis;
end;
dom(((-1)(#)(( #Z (1+1))^))|Z)=dom(((-1)(#)(( #Z 2)^)))/\Z by RELAT_1:61
.=dom((( #Z 2)^))/\Z by VALUED_1:def 5
.=Z by A1,A3,XBOOLE_1:28,ZFMISC_1:34;
hence thesis by A2,A5,PARTFUN1:5;
end;
theorem Th47:
x <> 0 implies ( #Z 2)^ is_differentiable_in x & diff(( #Z 2)^,x
) = -(2 * x)/(x #Z 2)^2
proof
A1: ( #Z 2).x = x #Z 2 & x #Z 2 = x|^2 by PREPOWER:36,TAYLOR_1:def 1;
assume x<>0;
then
A2: ( #Z 2).x <>0 by A1,PREPOWER:5;
A3: #Z 2 is_differentiable_in x by TAYLOR_1:2;
then diff(( #Z 2)^,x) = - diff( #Z 2,x)/(( #Z 2).x)^2 by A2,FDIFF_2:15
.= -(2 * x #Z (2-1))/(( #Z 2).x)^2 by TAYLOR_1:2
.= -(2 * x #Z 1)/(x #Z 2)^2 by TAYLOR_1:def 1
.= -(2 * x)/(x #Z 2)^2 by PREPOWER:35;
hence thesis by A2,A3,FDIFF_2:15;
end;
theorem
not 0 in Z implies (( #Z 2)^)`|Z = ((-2)(#)(( #Z 3)^))|Z
proof
assume
A1: not 0 in Z;
then ( #Z 2)^ is_differentiable_on Z by Th43;
then
A2: dom((( #Z 2)^)`|Z) = Z by FDIFF_1:def 7;
Z c= REAL \ {0} by A1,ZFMISC_1:34;
then
A3: Z c= dom (( #Z 3)^) by Th3;
A4: for x0 being Element of REAL
st x0 in Z holds ((( #Z 2)^)`|Z).x0 = (((-2)(#)(( #Z 3)^))|Z).x0
proof
reconsider i=2-1 as Element of NAT;
let x0 be Element of REAL;
A5: dom((-2)(#)(( #Z 3)^))=dom((( #Z 3)^)) by VALUED_1:def 5;
assume
A6: x0 in Z;
then x0 #Z i<>0 by A1,PREPOWER:38;
then
A7: x0|^i<>0 by PREPOWER:36;
( #Z 2)^ is_differentiable_on Z by A1,Th43;
then ((( #Z 2)^)`|Z).x0 = diff(( #Z 2)^,x0) by A6,FDIFF_1:def 7
.= - (2* x0)/( x0 #Z 2)^2 by A1,A6,Th47
.= - (2* x0 #Z 1) /( x0 #Z 2)^2 by PREPOWER:35
.=- (2* x0 #Z 1) /(x0 |^2)^2 by PREPOWER:36
.=- (2* x0|^1) /(( x0 |^2)*( x0 |^(1+1))) by PREPOWER:36
.=- (2* x0|^1) /(( x0 |^2)*( x0 |^1*x0 |^1)) by NEWTON:8
.=- (2* x0|^1) /(( x0 |^(2)* x0 |^1)*x0 |^1)
.=- (2* x0|^1) /( x0 |^(2+1)*x0 |^1) by NEWTON:8
.=- 2/x0 |^(1+2) by A7,XCMPLX_1:91
.=- 2/x0 #Z 3 by PREPOWER:36
.=- 2/( #Z 3).x0 by TAYLOR_1:def 1
.=-2*(( #Z 3).x0)" by XCMPLX_0:def 9
.=-2*(( #Z 3)^).x0 by A3,A6,RFUNCT_1:def 2
.=(-2)*(( #Z 3)^).x0
.=((-2)(#)(( #Z 3)^)).x0 by A3,A6,A5,VALUED_1:def 5
.=(((-2)(#)(( #Z 3)^))|Z).x0 by A6,FUNCT_1:49;
hence thesis;
end;
dom(((-2)(#)(( #Z 3)^))|Z) = dom(((-2)(#)(( #Z 3)^)))/\Z by RELAT_1:61
.=dom(( #Z 3)^)/\Z by VALUED_1:def 5
.=Z by A3,XBOOLE_1:28;
hence thesis by A2,A4,PARTFUN1:5;
end;
theorem Th49:
not 0 in Z & n>=1 implies (( #Z n)^)`|Z = ((-n)(#)(( #Z (n+1))^) )|Z
proof
assume that
A1: not 0 in Z and
A2: n>=1;
n+1>=1+0 & Z c= REAL\{0} by A1,XREAL_1:7,ZFMISC_1:34;
then
A3: Z c= dom((( #Z (n+1))^)) by Th3;
A4: for x0 being Element of REAL
st x0 in Z holds ((( #Z n)^)`|Z).x0 = (((-n)(#)(( #Z (n+1))^))|Z).x0
proof
n+1>=1+0 & Z c= REAL\{0} by A1,XREAL_1:7,ZFMISC_1:34;
then
A5: Z c= dom((( #Z (n+1))^)) by Th3;
reconsider i=n-1 as Element of NAT by A2,INT_1:5;
let x0 be Element of REAL;
A6: dom((-n)(#)(( #Z (n+1))^))=dom((( #Z (n+1))^)) by VALUED_1:def 5;
assume
A7: x0 in Z;
then x0 #Z i<>0 by A1,PREPOWER:38;
then
A8: x0|^i<>0 by PREPOWER:36;
( #Z n)^ is_differentiable_on Z by A1,Th43;
then ((( #Z n)^)`|Z).x0 = diff(( #Z n)^,x0) by A7,FDIFF_1:def 7
.= - (n* x0 #Z (n-1)) /( x0 #Z n)^2 by A1,A7,Th29
.=- (n* x0 #Z i) /(x0 |^n)^2 by PREPOWER:36
.= - (n* x0|^i) /( x0 |^n)^2 by PREPOWER:36
.=- (n* x0|^i) /(( x0 |^(i+1))*( x0 |^1*x0 |^i)) by NEWTON:8
.=- (n* x0|^i) /(( x0 |^(i+1)* x0 |^1)*x0 |^i)
.=- (n* x0|^i) /( x0 |^(i+1+1)*x0 |^i) by NEWTON:8
.=- n/x0 |^(i+2) by A8,XCMPLX_1:91
.=- n/x0 #Z (i+2) by PREPOWER:36
.=- n/( #Z (i+2)).x0 by TAYLOR_1:def 1
.=-n*(( #Z (n+1)).x0)" by XCMPLX_0:def 9
.=-n*(( #Z (n+1))^).x0 by A7,A5,RFUNCT_1:def 2
.=(-n)*(( #Z (n+1))^).x0
.=((-n)(#)(( #Z (n+1))^)).x0 by A7,A6,A5,VALUED_1:def 5
.=(((-n)(#)(( #Z (n+1))^))|Z).x0 by A7,FUNCT_1:49;
hence thesis;
end;
( #Z n)^ is_differentiable_on Z by A1,Th43;
then
A9: dom((( #Z n)^)`|Z) = Z by FDIFF_1:def 7;
dom(((-n)(#)(( #Z (n+1))^))|Z) = dom(((-n)(#)(( #Z (n+1))^)))/\Z by
RELAT_1:61
.=dom((( #Z (n+1))^))/\Z by VALUED_1:def 5
.=Z by A3,XBOOLE_1:28;
hence thesis by A9,A4,PARTFUN1:5;
end;
theorem Th50:
f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z
implies diff(f1(#)f2,Z).2 = (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z)) + f1
(#)(diff(f2,Z).2)
proof
assume that
A1: f1 is_differentiable_on 2,Z and
A2: f2 is_differentiable_on 2,Z;
diff(f1,Z).0 is_differentiable_on Z by A1;
then f1|Z is_differentiable_on Z by TAYLOR_1:def 5;
then
A3: f1 is_differentiable_on Z by Th6;
A4: diff(f1,Z).2 = diff(f1,Z).(1+1) .= diff(f1,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(f1,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=((f1|Z)`|Z)`|Z by TAYLOR_1:def 5
.=(f1`|Z)`|Z by A3,FDIFF_2:16;
diff(f2,Z).0 is_differentiable_on Z by A2;
then f2|Z is_differentiable_on Z by TAYLOR_1:def 5;
then
A5: f2 is_differentiable_on Z by Th6;
then
A6: f1(#)f2 is_differentiable_on Z by A3,FDIFF_2:20;
diff(f2,Z).1 = diff(f2,Z).(1+0) .= diff(f2,Z).0`|Z by TAYLOR_1:def 5
.=(f2|Z)`|Z by TAYLOR_1:def 5
.=f2`|Z by A5,FDIFF_2:16;
then
A7: f2`|Z is_differentiable_on Z by A2;
then
A8: f1(#)(f2`|Z) is_differentiable_on Z by A3,FDIFF_2:20;
diff(f1,Z).1 = diff(f1,Z).(1+0) .= diff(f1,Z).0`|Z by TAYLOR_1:def 5
.=(f1|Z)`|Z by TAYLOR_1:def 5
.=f1`|Z by A3,FDIFF_2:16;
then
A9: f1`|Z is_differentiable_on Z by A1;
then
A10: (f1`|Z)(#)f2 is_differentiable_on Z by A5,FDIFF_2:20;
A11: diff(f2,Z).2 = diff(f2,Z).(1+1) .= diff(f2,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(f2,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=((f2|Z)`|Z)`|Z by TAYLOR_1:def 5
.=(f2`|Z)`|Z by A5,FDIFF_2:16;
diff(f1(#)f2,Z).2 =diff(f1(#)f2,Z).(1+1)
.=diff(f1(#)f2,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(f1(#)f2,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=(((f1(#)f2)|Z)`|Z)`|Z by TAYLOR_1:def 5
.=((f1(#)f2)`|Z)`|Z by A6,FDIFF_2:16
.=((f1`|Z)(#)f2 + f1(#)(f2`|Z))`|Z by A3,A5,FDIFF_2:20
.=((f1`|Z)(#)f2)`|Z+(f1(#)(f2`|Z))`|Z by A10,A8,FDIFF_2:17
.=(((f1`|Z)`|Z)(#)f2 + (f1`|Z)(#)(f2`|Z))+(f1(#)(f2`|Z))`|Z by A5,A9,
FDIFF_2:20
.=((diff(f1,Z).2)(#)f2 + (f1`|Z)(#)(f2`|Z))+ ((f1`|Z)(#)(f2`|Z) + f1(#)(
diff(f2,Z).2)) by A3,A7,A4,A11,FDIFF_2:20
.=(((diff(f1,Z).2)(#)f2 + ((f1`|Z)(#)(f2`|Z))+ (f1`|Z)(#)(f2`|Z))) + f1
(#)(diff(f2,Z).2) by RFUNCT_1:8
.=(diff(f1,Z).2)(#)f2 + ((f1`|Z)(#)(f2`|Z)+ (f1`|Z)(#)(f2`|Z)) + f1(#)(
diff(f2,Z).2) by RFUNCT_1:8
.=(diff(f1,Z).2)(#)f2 + (1(#)((f1`|Z)(#)(f2`|Z))+ ((f1`|Z)(#)(f2`|Z))) +
f1(#)(diff(f2,Z).2) by RFUNCT_1:21
.=(diff(f1,Z).2)(#)f2 + (1(#)((f1`|Z)(#)(f2`|Z))+ 1(#)((f1`|Z)(#)(f2`|Z)
)) + f1(#)(diff(f2,Z).2) by RFUNCT_1:21
.=((diff(f1,Z).2)(#)f2 + ((1+1)(#)((f1`|Z)(#)(f2`|Z))) + f1(#)(diff(f2,Z
).2)) by Th5
.=((diff(f1,Z).2)(#)f2 + (2(#)((f1`|Z)(#)(f2`|Z))) + f1(#)(diff(f2,Z).2)
);
hence thesis;
end;
theorem
Z c= dom ln & Z c= dom((id REAL)^) implies ln`| Z = ((id REAL)^)| Z
proof
assume that
A1: Z c= dom ln and
A2: Z c= dom ((id REAL)^);
A3: dom (((id REAL)^)| Z) = dom(((id REAL)^))/\Z by RELAT_1:61
.=Z by A2,XBOOLE_1:28;
A4: for x0 being Element of REAL
st x0 in dom(((id REAL)^)|Z) holds (ln`| Z).x0 = (((id REAL)^)| Z).x0
proof
let x0 be Element of REAL;
assume
A5: x0 in dom(((id REAL)^)|Z);
ln is_differentiable_on Z by A1,FDIFF_1:26,TAYLOR_1:18;
then (ln`| Z).x0 = diff(ln,x0) by A3,A5,FDIFF_1:def 7
.=1/x0 by A1,A3,A5,TAYLOR_1:18
.=1/((id REAL).x0)
.=1*((id REAL).x0)" by XCMPLX_0:def 9
.= 1*((id REAL)^).x0 by A2,A3,A5,RFUNCT_1:def 2
.= (((id REAL)^)|Z).x0 by A3,A5,FUNCT_1:49;
hence thesis;
end;
ln is_differentiable_on Z by A1,FDIFF_1:26,TAYLOR_1:18;
then dom (((id REAL)^)|Z) = dom (ln`| Z) by A3,FDIFF_1:def 7;
hence thesis by A4,PARTFUN1:5;
end;
theorem
n>=1 & x0 in Z & not 0 in Z implies (diff((( #Z n)^),Z).2).x0 = n*(n+1
)*((( #Z (n+2))^).x0)
proof
assume that
A1: n>=1 and
A2: x0 in Z and
A3: not 0 in Z;
A4: Z c= REAL\{0} by A3,ZFMISC_1:34;
n+1+1>=1+0 by XREAL_1:7;
then
A5: Z c=dom((( #Z (n+2))^)) by A4,Th3;
A6: dom((-(n+1))(#)((( #Z (n+2))^)|Z)) =dom((( #Z (n+2))^)|Z) by VALUED_1:def 5
.=dom((( #Z (n+2))^))/\ Z by RELAT_1:61
.=Z by A5,XBOOLE_1:28;
A7: ( #Z n)^ is_differentiable_on Z by A3,Th43;
A8: n+1>=1+0 by XREAL_1:7;
reconsider m =-n as Element of REAL by XREAL_0:def 1;
A9: (( #Z (n+1))^) is_differentiable_on Z by A3,Th43;
then
A10: m(#)(( #Z (n+1))^) is_differentiable_on Z by FDIFF_2:19;
dom((m )(#)(( #Z (n+1))^))=dom((( #Z (n+1))^)) by VALUED_1:def 5;
then
A11: Z c= dom((-n)(#)(( #Z (n+1))^)) by A8,A4,Th3;
(diff((( #Z n)^),Z).2).x0 = (diff((( #Z n)^),Z).(1+1)).x0
.=((diff((( #Z n)^),Z).(1+0))`|Z).x0 by TAYLOR_1:def 5
.=(((diff((( #Z n)^),Z).0)`|Z)`|Z).x0 by TAYLOR_1:def 5
.=(((((( #Z n)^)|Z))`|Z)`|Z).x0 by TAYLOR_1:def 5
.=((((( #Z n)^))`|Z)`|Z).x0 by A7,FDIFF_2:16
.= (((m(#)(( #Z (n+1))^))|Z)`|Z).x0 by A1,A3,Th49
.=((m(#)(( #Z (n+1))^))`|Z).x0 by A10,FDIFF_2:16
.=m*diff((( #Z (n+1))^),x0) by A2,A9,A11,FDIFF_1:20
.=m*((( #Z (n+1))^)`|Z).x0 by A2,A9,FDIFF_1:def 7
.=m*(((-(n+1))(#)(( #Z ((n+1)+1))^))|Z).x0 by A3,A8,Th49
.=m*((-(n+1))(#)(((( #Z (n+2))^))|Z)).x0 by RFUNCT_1:49
.=m*((-(n+1))*(((( #Z (n+2))^)|Z).x0 )) by A2,A6,VALUED_1:def 5
.=n*(n+1)*((( #Z (n+2))^)|Z).x0
.=n*(n+1)*((( #Z (n+2))^).x0) by A2,FUNCT_1:49;
hence thesis;
end;
theorem
diff(sin^2,Z).2 = 2(#)((cos^2)|Z) +(-2)(#)((sin^2)|Z)
proof
sin is_differentiable_on 2,Z by TAYLOR_2:21;
then
diff(sin^2,Z).2 =(diff(sin,Z).(2*1))(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +
sin(#)(diff(sin,Z).(2*1)) by Th50
.=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +sin(#)(diff
(sin,Z).(2*1))by TAYLOR_2:19
.=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +sin(#)((-1)
|^ 1 (#) sin | Z) by TAYLOR_2:19
.=((-1) |^ 1 (#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +sin(#)((-1)
(#) sin | Z)
.=((-1)(#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +sin(#)((-1)(#)
sin | Z)
.=2(#)((sin`|Z)(#)(sin`|Z)) + (sin(#)((-1)(#) sin | Z) +sin(#)((-1)(#)
sin | Z)) by RFUNCT_1:8
.=2(#)((sin`|Z)(#)(sin`|Z)) + (1(#)(sin(#)((-1)(#) sin | Z)) +sin(#)((-1
)(#) sin | Z)) by RFUNCT_1:21
.=2(#)((sin`|Z)(#)(sin`|Z)) + (1(#)(sin(#)((-1)(#) sin | Z)) +1(#)(sin
(#)((-1)(#) sin | Z))) by RFUNCT_1:21
.=2(#)((sin`|Z)(#)(sin`|Z)) +((1+1)(#)(sin(#)((-1)(#) sin | Z))) by Th5
.=2(#)((cos|Z)(#)(sin`|Z))+2(#)(sin(#)((-1)(#) sin | Z)) by TAYLOR_2:17
.=2(#)((cos|Z)(#)(cos|Z)) +2(#)(sin(#)((-1)(#) sin | Z)) by TAYLOR_2:17
.=2(#)((cos(#)cos)|Z) +2(#)(((-1)(#) sin | Z)(#)sin) by RFUNCT_1:45
.=2(#)((cos(#)cos)|Z) +2(#)((-1)(#)(sin | Z(#) sin)) by RFUNCT_1:12
.=2(#)((cos(#)cos)|Z) +2(#)((-1)(#)((sin(#) sin)|Z)) by RFUNCT_1:45
.=2(#)((cos(#)cos)|Z) +(2*(-1))(#)((sin(#) sin)|Z) by RFUNCT_1:17
.=2(#)((cos(#)cos)|Z) +(-2)(#)((sin(#) sin)|Z)
.=2(#)((cos^2)|Z) +(-2)(#)((sin^2)|Z);
hence thesis;
end;
theorem
diff(cos^2,Z).2 = 2(#)((sin^2)|Z) +(-2)(#)((cos^2)|Z)
proof
cos is_differentiable_on 2,Z by TAYLOR_2:21;
then
diff(cos^2,Z).2 =(diff(cos,Z).(2*1))(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +
cos(#)(diff(cos,Z).(2*1)) by Th50
.=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +cos(#)(diff
(cos,Z).(2*1))by TAYLOR_2:19
.=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +cos(#)((-1)
|^ 1 (#) cos | Z) by TAYLOR_2:19
.=((-1) |^ 1 (#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +cos(#)((-1)
(#) cos | Z)
.=((-1)(#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +cos(#)((-1)(#)
cos | Z)
.=2(#)((cos`|Z)(#)(cos`|Z)) + (cos(#)((-1)(#) cos | Z) +cos(#)((-1)(#)
cos | Z)) by RFUNCT_1:8
.=2(#)((cos`|Z)(#)(cos`|Z)) + (1(#)(cos(#)((-1)(#) cos | Z)) +cos(#)((-1
)(#) cos | Z)) by RFUNCT_1:21
.=2(#)((cos`|Z)(#)(cos`|Z)) + (1(#)(cos(#)((-1)(#) cos | Z)) +1(#)(cos
(#)((-1)(#) cos | Z))) by RFUNCT_1:21
.=2(#)((cos`|Z)(#)(cos`|Z)) +(1+1)(#)(cos(#)((-1)(#) cos | Z)) by Th5
.=2(#)(((-sin)|Z)(#)(cos`|Z))+2(#)(cos(#)((-1)(#) cos | Z)) by TAYLOR_2:17
.=2(#)(((-sin)|Z)(#)((-sin)|Z)) + 2(#)(cos(#)((-1)(#) cos | Z)) by
TAYLOR_2:17
.=2(#)(((-sin)(#)(-sin))|Z) +2(#)(((-1)(#)cos|Z)(#)cos) by RFUNCT_1:45
.=2(#)(((-sin)(#)(-sin))|Z) +2(#)((-1)(#)(cos|Z(#)cos)) by RFUNCT_1:12
.=2(#)(((-sin)(#)(-sin))|Z) +(2*(-1))(#)(cos|Z(#)cos) by RFUNCT_1:17
.=2(#)(((-sin)(#)(-sin))|Z) +(-2)(#)((cos(#)cos)|Z) by RFUNCT_1:45
.=2(#)((sin(#)sin)|Z) +(-2)(#)((cos(#)cos)|Z) by Th2;
hence thesis;
end;
theorem
diff(sin(#)cos,Z).2 = 4(#)((-sin)(#)cos)|Z
proof
cos is_differentiable_on 2,Z & sin is_differentiable_on 2,Z by TAYLOR_2:21;
then
diff(sin(#)cos,Z).2 =(diff(sin,Z).(2*1))(#)cos+2(#)((sin`|Z) (#) (cos`|Z
)) + sin(#)(diff(cos,Z).(2*1)) by Th50
.=((-1) |^ 1(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z)) + sin(#)(diff(
cos,Z).(2*1)) by TAYLOR_2:19
.=((-1) |^ 1(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z)) + sin(#)((-1)
|^ 1(#)cos | Z) by TAYLOR_2:19
.=((-1)(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z)) + sin(#)((-1) |^ 1
(#)cos | Z)
.=((-1)(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z)) + sin(#)((-1)(#)cos
| Z)
.=((-1)(#)sin | Z)(#)cos + 2(#)((cos|Z)(#)(cos`|Z)) + sin(#)((-1)(#)cos
| Z) by TAYLOR_2:17
.=((-1)(#)sin | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z)) + sin(#)((-1)(#)
cos | Z) by TAYLOR_2:17
.=(((-1)(#)sin) | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z)) + sin(#)((-1)
(#)cos | Z) by RFUNCT_1:49
.=(((-1)(#)sin) | Z)(#)cos + 2(#)((cos|Z)(#)((-sin) | Z)) + sin(#)(((-1)
(#)cos) | Z) by RFUNCT_1:49
.=((-sin)(#)cos)| Z + 2(#)((cos|Z)(#)((-sin) | Z)) + sin(#)((-cos) | Z)
by RFUNCT_1:45
.=((-sin)(#)cos)| Z + 2(#)((cos|Z)(#)((-sin) | Z)) + (sin(#)(-cos)) | Z
by RFUNCT_1:45
.=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z + (sin(#)(-cos)) | Z by
RFUNCT_1:45
.=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z + ((-1)(#)(sin(#)cos)) | Z by
RFUNCT_1:13
.=((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z + (((-1)(#)sin)(#)cos) | Z by
RFUNCT_1:12
.=1(#)((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z + ((-sin)(#)cos)| Z by
RFUNCT_1:21
.=1(#)((-sin)(#)cos)| Z + 2(#)((-sin)(#)cos)|Z + 1(#)((-sin)(#)cos)| Z
by RFUNCT_1:21
.=(1+2)(#)((-sin)(#)cos)|Z+ 1(#)((-sin)(#)cos)| Z by Th5
.=(3+1)(#)((-sin)(#)cos)|Z by Th5
.=4(#)((-sin)(#)cos)|Z;
hence thesis;
end;
theorem Th56:
Z c= dom tan implies tan is_differentiable_on Z & tan`|Z = ((cos ^)^2)|Z
proof
set f1 = cos^;
assume
A1: Z c= dom tan;
A2: dom sin /\ dom f1 c=dom f1 by XBOOLE_1:17;
A3: dom(tan)=dom(sin(#)f1) by RFUNCT_1:31,SIN_COS:def 26
.=dom sin /\ dom f1 by VALUED_1:def 4;
then
A4: Z c=dom f1 by A1,A2;
A5: dom((cos^)(#)(cos^)) = dom (cos^) /\ dom (cos^) by VALUED_1:def 4
.= dom (cos^);
then
A6: dom(((cos^)(#)(cos^))|Z) = dom (cos^) /\ Z by RELAT_1:61
.=Z by A1,A3,A2,XBOOLE_1:1,28;
A7: for x st x in Z holds tan is_differentiable_in x
proof
let x;
assume x in Z;
then
A8: cos.x <> 0 by A1,FDIFF_8:1;
sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
hence thesis by A8,FDIFF_2:14,SIN_COS:def 26;
end;
then
A9: tan is_differentiable_on Z by A1,FDIFF_1:9;
A10: for x being Element of REAL
st x in dom (tan`|Z) holds ((tan)`|Z).x = (((cos^)(#)(cos^))|Z).x
proof
let x be Element of REAL;
assume x in dom (tan`|Z);
then
A11: x in Z by A9,FDIFF_1:def 7;
then
A12: cos.x <> 0 by A1,FDIFF_8:1;
((tan)`|Z).x=diff(sin/cos, x) by A9,A11,FDIFF_1:def 7,SIN_COS:def 26
.=1/(cos.x)^2 by A12,FDIFF_7:46
.=(1/cos.x)*(1/cos.x) by XCMPLX_1:102
.=1*(cos.x)"*(1/cos.x) by XCMPLX_0:def 9
.=cos^.x*(1/cos.x) by A4,A11,RFUNCT_1:def 2
.=cos^.x*(1*(cos.x)") by XCMPLX_0:def 9
.=cos^.x * f1.x by A4,A11,RFUNCT_1:def 2
.=(cos^(#)f1).x by A4,A5,A11,VALUED_1:def 4
.=((f1(#)f1)|Z).x by A11,FUNCT_1:49;
hence thesis;
end;
dom (tan`|Z)=Z by A9,FDIFF_1:def 7;
hence thesis by A1,A7,A6,A10,FDIFF_1:9,PARTFUN1:5;
end;
theorem Th57:
Z c= dom tan implies cos^ is_differentiable_on Z & (cos^)`|Z = (
(cos^)(#)tan)|Z
proof
A1: dom sin /\ dom (cos^) c=dom (cos^) by XBOOLE_1:17;
assume
A2: Z c= dom tan;
then
A3: for x st x in Z holds cos.x<>0 by FDIFF_8:1;
then cos^ is_differentiable_on Z by FDIFF_4:39;
then
A4: dom((cos^)`|Z)= Z by FDIFF_1:def 7;
dom(tan) = dom(sin(#)(cos^)) by RFUNCT_1:31,SIN_COS:def 26
.=dom sin /\ dom(cos^) by VALUED_1:def 4;
then
A5: Z c=dom (cos^) by A2,A1;
A6: for x being Element of REAL st x in Z
holds ((cos^)`|Z).x=(((cos^)(#)tan)|Z).x
proof
let x be Element of REAL;
A7: dom((cos^)(#)sin) = dom tan by RFUNCT_1:31,SIN_COS:def 26;
then dom(((cos^)(#)sin)(#)(cos^)) =dom(tan)/\dom(cos^) by VALUED_1:def 4;
then
A8: Z c= dom(((cos^)(#)sin)(#)(cos^)) by A2,A5,XBOOLE_1:19;
assume
A9: x in Z;
then ((cos^)`|Z).x =sin.x/(cos.x)^2 by A3,FDIFF_4:39
.=1/(cos.x)*(sin.x/(cos.x)) by XCMPLX_1:103
.=1/cos.x*sin.x*(1/cos.x) by XCMPLX_1:99
.=1/cos.x*sin.x*(1*(cos.x)") by XCMPLX_0:def 9
.=(1*(cos.x)")*sin.x*(1*(cos.x)") by XCMPLX_0:def 9
.=(cos^).x*sin.x*(1*(cos.x)") by A5,A9,RFUNCT_1:def 2
.=(cos^).x*sin.x*(cos^.x) by A5,A9,RFUNCT_1:def 2
.=((cos^) (#)sin).x*(cos^.x) by A2,A9,A7,VALUED_1:def 4
.=(((cos^)(#)sin)(#)(cos^)).x by A9,A8,VALUED_1:def 4
.=((((cos^)(#)sin)(#)(cos^))|Z).x by A9,FUNCT_1:49
.=(((cos^)(#)tan)|Z).x by RFUNCT_1:31,SIN_COS:def 26;
hence thesis;
end;
dom(((cos^)(#)tan)|Z) = dom((cos^)(#)tan)/\Z by RELAT_1:61
.=(dom(cos^)/\dom tan)/\Z by VALUED_1:def 4
.=Z by A2,A5,XBOOLE_1:19,28;
hence thesis by A3,A4,A6,FDIFF_4:39,PARTFUN1:5;
end;
theorem
Z c= dom tan implies diff(tan,Z).2=2(#)((tan(#)(cos^)(#)(cos^))|Z)
proof
assume
A1: Z c= dom tan;
then
A2: tan is_differentiable_on Z by Th56;
A3: cos^ is_differentiable_on Z by A1,Th57;
then
A4: ((cos^)(#)(cos^)) is_differentiable_on Z by FDIFF_2:20;
diff(tan,Z).2 = diff(tan,Z).(1+1) .=diff(tan,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(tan,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=tan|Z`|Z`|Z by TAYLOR_1:def 5
.=tan`|Z`|Z by A2,FDIFF_2:16
.=(((cos^)^2)|Z)`|Z by A1,Th56
.=((cos^)(#)(cos^))`|Z by A4,FDIFF_2:16
.=(((cos^)`|Z)(#)(cos^)) + ((cos^)`|Z)(#)(cos^) by A3,FDIFF_2:20
.=1(#)(((cos^)`|Z)(#)(cos^))+ ((cos^)`|Z)(#)(cos^) by RFUNCT_1:21
.=1(#)(((cos^)`|Z)(#)(cos^)) + 1(#)(((cos^)`|Z)(#)(cos^)) by RFUNCT_1:21
.=(1+1)(#)(((cos^)`|Z)(#)(cos^)) by Th5
.=2(#)((((cos^)(#)tan)|Z)(#)(cos^)) by A1,Th57
.=2(#)((tan(#)(cos^)(#)(cos^))|Z) by RFUNCT_1:45;
hence thesis;
end;
theorem Th59:
Z c= dom cot implies cot is_differentiable_on Z & cot`|Z = ((-1)
(#)((sin^)^2))|Z
proof
A1: dom(cos)/\dom(sin^)c=dom(sin^) by XBOOLE_1:17;
assume
A2: Z c= dom cot;
A3: for x st x in Z holds cot is_differentiable_in x
proof
let x;
assume x in Z;
then
A4: sin.x <> 0 by A2,FDIFF_8:2;
sin is_differentiable_in x & cos is_differentiable_in x by SIN_COS:63,64;
hence thesis by A4,FDIFF_2:14,SIN_COS:def 27;
end;
then
A5: cot is_differentiable_on Z by A2,FDIFF_1:9;
A6: dom(cot) = dom(cos(#)(sin^)) by RFUNCT_1:31,SIN_COS:def 27
.=dom(cos)/\dom(sin^) by VALUED_1:def 4;
then
A7: Z c=dom(sin^) by A2,A1;
A8: for x being Element of REAL
st x in dom (cot`|Z) holds ((cot)`|Z).x =(((-1)(#)((sin^)(#)(sin^)))|Z).x
proof
let x be Element of REAL;
assume x in dom (cot`|Z);
then
A9: x in Z by A5,FDIFF_1:def 7;
then
A10: sin.x<>0 by A2,FDIFF_8:2;
dom((sin^)(#)(sin^)) = (dom(sin^)/\dom(sin^)) by VALUED_1:def 4
.=dom(sin^);
then
A11: Z c= dom((sin^)(#)(sin^)) by A2,A6,A1;
then x in dom((sin^)(#)(sin^)) by A9;
then
A12: x in dom((-1)(#)((sin^)(#)(sin^))) by VALUED_1:def 5;
((cot)`|Z).x =diff(cos/sin, x) by A5,A9,FDIFF_1:def 7,SIN_COS:def 27
.=-1/(sin.x)^2 by A10,FDIFF_7:47
.=(-1)*(1/(sin.x*sin.x))
.=(-1)*((1/sin.x)*(1/sin.x)) by XCMPLX_1:102
.=(-1)*((1*(sin.x)")*(1/sin.x)) by XCMPLX_0:def 9
.=(-1)*((sin^.x)*(1/sin.x)) by A7,A9,RFUNCT_1:def 2
.=(-1)*((sin^.x)*(1*(sin.x)")) by XCMPLX_0:def 9
.=(-1)*((sin^.x)*(sin^.x)) by A7,A9,RFUNCT_1:def 2
.=(-1)*(((sin^)(#)(sin^)).x) by A9,A11,VALUED_1:def 4
.=((-1)(#)((sin^)(#)(sin^))).x by A12,VALUED_1:def 5
.=(((-1)(#)((sin^)(#)(sin^)))|Z).x by A9,FUNCT_1:49;
hence thesis;
end;
A13: dom(((-1)(#)((sin^)(#)(sin^)))|Z) =dom((-1)(#)((sin^)^2)) /\ Z by
RELAT_1:61
.= dom((sin^)^2) /\ Z by VALUED_1:def 5
.=dom(sin^)/\ dom(sin^)/\Z by VALUED_1:def 4
.=Z by A2,A6,A1,XBOOLE_1:1,28;
dom (cot`|Z) = Z by A5,FDIFF_1:def 7;
hence thesis by A2,A3,A13,A8,FDIFF_1:9,PARTFUN1:5;
end;
theorem Th60:
Z c= dom cot implies sin^ is_differentiable_on Z & (sin^)`|Z = (
-(sin^)(#)cot)|Z
proof
A1: dom(cot) = dom(cos(#)(sin^)) by RFUNCT_1:31,SIN_COS:def 27
.=dom(cos)/\dom(sin^) by VALUED_1:def 4;
assume
A2: Z c= dom cot;
dom(cos)/\dom(sin^) c= dom(sin^) by XBOOLE_1:17;
then
A3: Z c=dom(sin^) by A2,A1;
A4: for x st x in Z holds sin.x<>0 by A2,FDIFF_8:2;
then
A5: sin^ is_differentiable_on Z by FDIFF_4:40;
A6: for x being Element of REAL
st x in dom((sin^)`|Z) holds ((sin^)`|Z).x=((-(sin^)(#)cot)|Z).x
proof
let x be Element of REAL;
A7: dom((-1)(#)((sin^)(#)cot)) =dom((sin^)(#)(cos/sin)) by SIN_COS:def 27
,VALUED_1:def 5
.=dom((sin^)(#)(cos(#)(sin^))) by RFUNCT_1:31;
A8: Z c= dom(cos(#)(sin^)) by A2,A1,VALUED_1:def 4;
dom ((sin^)(#)(cos(#)(sin^))) =dom (sin^)/\dom(cos(#)(sin^)) by
VALUED_1:def 4;
then
A9: Z c=dom ((sin^)(#)(cos(#)(sin^))) by A3,A8,XBOOLE_1:19;
assume x in dom((sin^)`|Z);
then
A10: x in Z by A5,FDIFF_1:def 7;
then ((sin^)`|Z).x = -cos.x/(sin.x)^2 by A4,FDIFF_4:40
.= -(1*cos.x)/(sin.x*sin.x)
.= -(1/sin.x)*(cos.x/sin.x) by XCMPLX_1:76
.= -(1/sin.x)*(cos.x*(1/sin.x)) by XCMPLX_1:99
.= -(1*(sin.x)")*(cos.x*(1/sin.x)) by XCMPLX_0:def 9
.= -(sin.x)"*(cos.x*(1*(sin.x)")) by XCMPLX_0:def 9
.= -(sin^.x)*(cos.x*(sin.x)") by A3,A10,RFUNCT_1:def 2
.= -(sin^.x)*(cos.x*(sin^.x)) by A3,A10,RFUNCT_1:def 2
.= -(sin^.x)*(cos(#)(sin^)).x by A10,A8,VALUED_1:def 4
.= -((sin^)(#)(cos(#)(sin^))).x by A10,A9,VALUED_1:def 4
.= -((sin^)(#)cot).x by RFUNCT_1:31,SIN_COS:def 27
.=(-1)*((sin^)(#)cot).x
.=((-1)(#)((sin^)(#)cot)).x by A10,A9,A7,VALUED_1:def 5
.= ((-(sin^)(#)cot)|Z).x by A10,FUNCT_1:49;
hence thesis;
end;
A11: dom((-(sin^)(#)cot)|Z)=dom((-1)(#)((sin^)(#)cot))/\Z by RELAT_1:61
.=dom((sin^)(#)cot)/\Z by VALUED_1:def 5
.=dom(sin^)/\dom cot/\Z by VALUED_1:def 4
.=Z by A2,A3,XBOOLE_1:19,28;
dom((sin^)`|Z)=Z by A5,FDIFF_1:def 7;
hence thesis by A4,A11,A6,FDIFF_4:40,PARTFUN1:5;
end;
theorem
Z c= dom cot implies diff(cot,Z).2=2(#)(cot(#)(sin^)(#)(sin^))|Z
proof
assume
A1: Z c= dom cot;
then
A2: cot is_differentiable_on Z by Th59;
A3: sin^ is_differentiable_on Z by A1,Th60;
then
A4: ((sin^)(#)(sin^)) is_differentiable_on Z by FDIFF_2:20;
then
A5: ((-1)(#)((sin^)(#)(sin^))) is_differentiable_on Z by FDIFF_2:19;
diff(cot,Z).2 =diff(cot,Z).(1+1) .=diff(cot,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(cot,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=cot|Z`|Z`|Z by TAYLOR_1:def 5
.=cot`|Z`|Z by A2,FDIFF_2:16
.=(((-1)(#)((sin^)(#)(sin^)))|Z)`|Z by A1,Th59
.=((-1)(#)((sin^)(#)(sin^)))`|Z by A5,FDIFF_2:16
.=(-1)(#)(((sin^)(#)(sin^))`|Z) by A4,FDIFF_2:19
.=(-1)(#)(((sin^)`|Z)(#)(sin^) + ((sin^)`|Z)(#)(sin^)) by A3,FDIFF_2:20
.=(-1)(#)(1(#)(((sin^)`|Z)(#)(sin^)) + ((sin^)`|Z)(#)(sin^)) by RFUNCT_1:21
.=(-1)(#)(1(#)(((sin^)`|Z)(#)(sin^)) +1(#)(((sin^)`|Z)(#)(sin^))) by
RFUNCT_1:21
.=(-1)(#)((1+1)(#)(((sin^)`|Z)(#)(sin^))) by Th5
.=(-1)(#)(2(#)(((-(sin^)(#)cot)|Z)(#)(sin^))) by A1,Th60
.=((-1)*2)(#)(((-(sin^)(#)cot)|Z)(#)(sin^)) by RFUNCT_1:17
.=((-1)*2)(#)((((-(sin^)(#)cot))(#)(sin^)))|Z by RFUNCT_1:45
.=(((-1)*2)(#)((((-(sin^)(#)cot))(#)(sin^))))|Z by RFUNCT_1:49
.=((-2)(#)(-(sin^)(#)cot)(#)(sin^))|Z by RFUNCT_1:12
.=((((-2)*(-1))(#)((sin^)(#)cot))(#)(sin^))|Z by RFUNCT_1:17
.=(2(#)(((sin^)(#)cot)(#)(sin^)))|Z by RFUNCT_1:12
.=2(#)(cot(#)(sin^)(#)(sin^))|Z by RFUNCT_1:49;
hence thesis;
end;
theorem
diff(exp_R(#)sin,Z).2 = 2(#)((exp_R(#)cos)|Z)
proof
A1: sin is_differentiable_on 2,Z & exp_R is_differentiable_on 2,Z by
TAYLOR_2:10,21;
A2: dom(2(#)((exp_R(#)cos)|Z)) =dom((exp_R(#)cos)|Z) by VALUED_1:def 5
.=dom(exp_R(#)cos)/\Z by RELAT_1:61
.=REAL/\REAL/\Z by SIN_COS:24,47,VALUED_1:def 4
.=Z by XBOOLE_1:28;
A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then cos|Z is_differentiable_on Z by FDIFF_2:16;
then
A4: exp_R(#)(cos|Z) is_differentiable_on Z by A3,FDIFF_2:20;
A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then
A6: exp_R(#)sin is_differentiable_on Z by A3,FDIFF_2:20;
exp_R|Z is_differentiable_on Z by A3,FDIFF_2:16;
then exp_R|Z(#)sin is_differentiable_on Z by A5,FDIFF_2:20;
then
A7: exp_R|Z(#)sin+exp_R(#)(cos|Z) is_differentiable_on Z by A4,FDIFF_2:17;
A8: dom (diff(exp_R(#)sin,Z).2) = dom (diff(exp_R(#)sin,Z).(1+1))
.=dom ((diff(exp_R(#)sin,Z).(1+0))`|Z) by TAYLOR_1:def 5
.=dom (((diff(exp_R(#)sin,Z).0)`|Z)`|Z) by TAYLOR_1:def 5
.=dom ((((exp_R(#)sin)|Z)`|Z)`|Z) by TAYLOR_1:def 5
.=dom (((exp_R(#)sin)`|Z)`|Z) by A6,FDIFF_2:16
.=dom (((exp_R`|Z)(#)sin+exp_R(#)(sin`|Z))`|Z) by A3,A5,FDIFF_2:20
.=dom (((exp_R|Z)(#)sin+exp_R(#)(sin`|Z))`|Z) by TAYLOR_2:5
.=dom (((exp_R|Z)(#)sin+exp_R(#)(cos|Z))`|Z) by TAYLOR_2:17
.=Z by A7,FDIFF_1:def 7;
A9: dom(0(#)((exp_R(#)sin)|Z)) = dom ((exp_R(#)sin)|Z) by VALUED_1:def 5
.=dom(exp_R(#)sin)/\Z by RELAT_1:61
.=REAL/\REAL/\Z by SIN_COS:24,47,VALUED_1:def 4
.=Z by XBOOLE_1:28;
then
A10: dom(0(#)((exp_R(#)sin)|Z)+ 2(#)((exp_R(#)cos)|Z)) =Z/\Z by A2,
VALUED_1:def 1
.=Z;
for x being Element of REAL
st x in dom(diff(exp_R(#)sin,Z).2) holds (diff(exp_R(#)sin,Z).2).
x = (2(#)((exp_R(#)cos)|Z)).x
proof
let x be Element of REAL;
assume
A11: x in dom(diff(exp_R(#)sin,Z).2);
(diff(exp_R(#)sin,Z).2).x =((diff(exp_R,Z).2)(#)sin + 2(#)((exp_R`|Z)
(#)(sin`|Z)) + exp_R(#)(diff(sin,Z).2)).x by A1,Th50
.=(exp_R|Z(#)sin+2(#)((exp_R`|Z)(#)(sin`|Z))+exp_R(#)(diff(sin,Z).2)).
x by TAYLOR_2:6
.=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(sin`|Z))+exp_R(#)(diff(sin,Z).2)).x
by TAYLOR_2:5
.=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z)) +exp_R(#)(diff(sin,Z).(2*1)
)).x by TAYLOR_2:17
.=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)|^1(#)sin|Z)).
x by TAYLOR_2:19
.=(exp_R|Z(#)sin+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)(#)sin|Z)).x
.=((exp_R(#)sin)|Z+2(#)((exp_R|Z)(#)(cos|Z))+exp_R(#)((-1)(#)sin|Z)).x
by RFUNCT_1:45
.=((exp_R(#)sin)|Z+ 2(#)((exp_R(#)cos)|Z)+exp_R(#)((-1)(#)sin|Z)).x by
RFUNCT_1:45
.=(((exp_R(#)sin)|Z+(exp_R(#)((-1)(#)sin|Z))+2(#)((exp_R(#)cos)|Z))).x
by RFUNCT_1:8
.=(((exp_R(#)sin)|Z+((-1)(#)(exp_R(#)sin|Z))+2(#)((exp_R(#)cos)|Z))).x
by RFUNCT_1:13
.=((exp_R(#)sin)|Z+((-1)(#)((exp_R(#)sin)|Z))+2(#)((exp_R(#)cos)|Z)).x
by RFUNCT_1:45
.=(1(#)((exp_R(#)sin)|Z)+(-1)(#)((exp_R(#)sin)|Z) +2(#)((exp_R(#)cos)|
Z)).x by RFUNCT_1:21
.=((1+(-1))(#)((exp_R(#)sin)|Z)+ 2(#)((exp_R(#)cos)|Z)).x by Th5
.=(0(#)((exp_R(#)sin)|Z)).x+ (2(#)((exp_R(#)cos)|Z)).x by A10,A8,A11,
VALUED_1:def 1
.=0*((exp_R(#)sin)|Z).x+ (2(#)((exp_R(#)cos)|Z)).x by A9,A8,A11,
VALUED_1:def 5
.=(2(#)((exp_R(#)cos)|Z)).x;
hence thesis;
end;
hence thesis by A2,A8,PARTFUN1:5;
end;
theorem
diff(exp_R(#)cos,Z).2 = 2(#)((exp_R(#)-sin)|Z)
proof
A1: cos is_differentiable_on 2,Z & exp_R is_differentiable_on 2,Z by
TAYLOR_2:10,21;
A2: dom(2(#)((exp_R(#)-sin)|Z)) =dom((exp_R(#)-sin)|Z) by VALUED_1:def 5
.=dom(exp_R(#)-sin)/\Z by RELAT_1:61
.=dom(exp_R)/\dom(-sin)/\Z by VALUED_1:def 4
.=REAL/\REAL/\Z by SIN_COS:24,47,VALUED_1:def 5
.=Z by XBOOLE_1:28;
A3: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16;
sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68;
then sin|Z is_differentiable_on Z by FDIFF_2:16;
then (-1)(#)(sin|Z) is_differentiable_on Z by FDIFF_2:19;
then
A4: exp_R(#)((-1)(#)(sin|Z)) is_differentiable_on Z by A3,FDIFF_2:20;
A5: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67;
then
A6: exp_R(#)cos is_differentiable_on Z by A3,FDIFF_2:20;
exp_R|Z is_differentiable_on Z by A3,FDIFF_2:16;
then exp_R|Z(#)cos is_differentiable_on Z by A5,FDIFF_2:20;
then
A7: exp_R|Z(#)cos+exp_R(#)((-1)(#)(sin|Z)) is_differentiable_on Z by A4,
FDIFF_2:17;
A8: dom (diff(exp_R(#)cos,Z).2) = dom (diff(exp_R(#)cos,Z).(1+1))
.=dom ((diff(exp_R(#)cos,Z).(1+0))`|Z) by TAYLOR_1:def 5
.=dom (((diff(exp_R(#)cos,Z).0)`|Z)`|Z) by TAYLOR_1:def 5
.=dom ((((exp_R(#)cos)|Z)`|Z)`|Z) by TAYLOR_1:def 5
.=dom (((exp_R(#)cos)`|Z)`|Z) by A6,FDIFF_2:16
.=dom (((exp_R`|Z)(#)cos+exp_R(#)(cos`|Z))`|Z) by A3,A5,FDIFF_2:20
.=dom (((exp_R|Z)(#)cos+exp_R(#)(cos`|Z))`|Z) by TAYLOR_2:5
.=dom (((exp_R|Z)(#)cos+exp_R(#)((-sin)|Z))`|Z) by TAYLOR_2:17
.=dom (((exp_R|Z)(#)cos+exp_R(#)((-1)(#)(sin|Z)))`|Z) by RFUNCT_1:49
.=Z by A7,FDIFF_1:def 7;
A9: dom(0(#)((exp_R(#)cos)|Z)) = dom ((exp_R(#)cos)|Z) by VALUED_1:def 5
.= dom(exp_R(#)cos)/\Z by RELAT_1:61
.= REAL/\REAL/\Z by SIN_COS:24,47,VALUED_1:def 4
.= Z by XBOOLE_1:28;
then
A10: dom(0(#)((exp_R(#)cos)|Z)+ 2(#)((exp_R(#)-sin)|Z)) =Z/\Z by A2,
VALUED_1:def 1
.=Z;
for x being Element of REAL st x in dom ( diff(exp_R(#)cos,Z).2)
holds (diff(exp_R(#)cos,Z).2).x = (2(#)((exp_R(#)-sin)|Z)).x
proof
let x be Element of REAL;
assume
A11: x in dom (diff(exp_R(#)cos,Z).2);
(diff(exp_R(#)cos,Z).2).x =((diff(exp_R,Z).2)(#)cos + 2(#)((exp_R`|Z)
(#)(cos`|Z)) + exp_R(#)(diff(cos,Z).2)).x by A1,Th50
.=(exp_R|Z(#)cos+2(#)((exp_R`|Z)(#)(cos`|Z))+exp_R(#)(diff(cos,Z).2)).
x by TAYLOR_2:6
.=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(cos`|Z))+exp_R(#)(diff(cos,Z).2)).x
by TAYLOR_2:5
.=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)((-sin)|Z))+exp_R(#)(diff(cos,Z).(2*
1))).x by TAYLOR_2:17
.=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)(diff(cos,Z).(2*1)
)).x by RFUNCT_1:46
.=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)|^1(#)cos|Z))
.x by TAYLOR_2:19
.=(exp_R|Z(#)cos+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)(#)cos|Z)).x
.=((exp_R(#)cos)|Z+2(#)((exp_R|Z)(#)(-sin|Z))+exp_R(#)((-1)(#)cos|Z)).
x by RFUNCT_1:45
.=((exp_R(#)cos)|Z+2(#)((exp_R|Z)(#)(-sin)|Z)+exp_R(#)((-1)(#)cos|Z)).
x by RFUNCT_1:46
.=((exp_R(#)cos)|Z+ 2(#)((exp_R(#)(-sin))|Z)+exp_R(#)((-1)(#)cos|Z)).x
by RFUNCT_1:45
.=(((exp_R(#)cos)|Z+(exp_R(#)((-1)(#)cos|Z))+2(#)((exp_R(#)-sin)|Z))).
x by RFUNCT_1:8
.=(((exp_R(#)cos)|Z+((-1)(#)(exp_R(#)cos|Z))+2(#)((exp_R(#)-sin)|Z))).
x by RFUNCT_1:13
.=((exp_R(#)cos)|Z+((-1)(#)((exp_R(#)cos)|Z))+2(#)((exp_R(#)-sin)|Z)).
x by RFUNCT_1:45
.=(1(#)((exp_R(#)cos)|Z)+(-1)(#)((exp_R(#)cos)|Z)+2(#)((exp_R(#)-sin)|
Z)).x by RFUNCT_1:21
.=((1+(-1))(#)((exp_R(#)cos)|Z)+ 2(#)((exp_R(#)-sin)|Z)).x by Th5
.=(0(#)((exp_R(#)cos)|Z)).x+(2(#)((exp_R(#)-sin)|Z)).x by A10,A8,A11,
VALUED_1:def 1
.=0*((exp_R(#)cos)|Z).x+(2(#)((exp_R(#)-sin)|Z)).x by A9,A8,A11,
VALUED_1:def 5
.=(2(#)((exp_R(#)-sin)|Z)).x;
hence thesis;
end;
hence thesis by A2,A8,PARTFUN1:5;
end;
Lm3: f is_differentiable_on Z implies (f`|Z)`|Z=diff(f,Z).2
proof
assume f is_differentiable_on Z;
then (f`|Z)`|Z =(f|Z`|Z)`|Z by FDIFF_2:16
.=(diff(f,Z).0`|Z)`|Z by TAYLOR_1:def 5
.=(diff(f,Z).(0+1))`|Z by TAYLOR_1:def 5
.=diff(f,Z).(1+1) by TAYLOR_1:def 5;
hence thesis;
end;
theorem Th64:
f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z
implies diff(f1(#)f2,Z).3 =(diff(f1,Z).3)(#)f2 + (3(#)(diff(f1,Z).2(#)(f2`|Z))
+3(#)((f1`|Z)(#)diff(f2,Z).2))+ f1(#)(diff(f2,Z).3)
proof
assume that
A1: f1 is_differentiable_on 3,Z and
A2: f2 is_differentiable_on 3,Z;
A3: f2 is_differentiable_on Z by A2,Th7;
set g2=diff(f2,Z).2;
set g1 =diff(f1,Z).2;
diff(f2,Z).1 =diff(f2,Z).(1+0) .= diff(f2,Z).0`|Z by TAYLOR_1:def 5
.=f2|Z`|Z by TAYLOR_1:def 5
.=f2`|Z by A3,FDIFF_2:16;
then
A4: f2`|Z is_differentiable_on Z by A2;
A5: f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z by A1,A2,
TAYLOR_1:23;
A6: f1 is_differentiable_on Z by A1,Th7;
A7: diff(f1,Z).2 is_differentiable_on Z by A1;
then
A8: (diff(f1,Z).2)(#)f2 is_differentiable_on Z by A3,FDIFF_2:20;
diff(f1,Z).1 =diff(f1,Z).(1+0) .= diff(f1,Z).0`|Z by TAYLOR_1:def 5
.=f1|Z`|Z by TAYLOR_1:def 5
.=f1`|Z by A6,FDIFF_2:16;
then
A9: f1`|Z is_differentiable_on Z by A1;
then
A10: (f1`|Z)(#)(f2`|Z) is_differentiable_on Z by A4,FDIFF_2:20;
then
A11: 2(#)((f1`|Z)(#)(f2`|Z)) is_differentiable_on Z by FDIFF_2:19;
then
A12: (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z)) is_differentiable_on Z by
A8,FDIFF_2:17;
A13: diff(f2,Z).2 is_differentiable_on Z by A2;
then
A14: f1(#)(diff(f2,Z).2) is_differentiable_on Z by A6,FDIFF_2:20;
diff(f1(#)f2,Z).3 =diff(f1(#)f2,Z).(2+1)
.=(diff(f1(#)f2,Z).2)`|Z by TAYLOR_1:def 5
.=((diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z))+ f1(#)(diff(f2,Z).2))`|
Z by A5,Th50
.=((diff(f1,Z).2)(#)f2+2(#)((f1`|Z)(#)(f2`|Z)))`|Z+(f1(#)(diff(f2,Z).2))
`|Z by A14,A12,FDIFF_2:17
.=((diff(f1,Z).2)(#)f2)`|Z+(2(#)((f1`|Z)(#)(f2`|Z)))`|Z +(f1(#)(diff(f2,
Z).2))`|Z by A8,A11,FDIFF_2:17
.=((diff(f1,Z).2)(#)f2)`|Z+2(#)((((f1`|Z)(#)(f2`|Z)))`|Z) +(f1(#)(diff(
f2,Z).2))`|Z by A10,FDIFF_2:19
.=((diff(f1,Z).2)`|Z)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)((((f1`|Z)(#)
(f2`|Z)))`|Z)+(f1(#)(diff(f2,Z).2))`|Z by A3,A7,FDIFF_2:20
.=((diff(f1,Z).2)`|Z)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)((((f1`|Z)(#)
(f2`|Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2) + f1(#)((diff(f2,Z).2)`|Z)) by A6,A13,
FDIFF_2:20
.=(diff(f1,Z).(2+1))(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)((((f1`|Z)(#)(
f2`|Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2) + f1(#)((diff(f2,Z).2)`|Z)) by
TAYLOR_1:def 5
.=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)((((f1`|Z)(#)(f2`|
Z)))`|Z)+((f1`|Z)(#)(diff(f2,Z).2) + f1(#)(diff(f2,Z).(2+1))) by TAYLOR_1:def 5
.=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)(((f1`|Z)`|Z)(#)(
f2`|Z) + (f1`|Z)(#)((f2`|Z)`|Z)) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3
)) by A9,A4,FDIFF_2:20
.=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)(diff(f1,Z).2(#)(
f2`|Z) + (f1`|Z)(#)((f2`|Z)`|Z)) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3
)) by A1,Lm3,Th7
.=(diff(f1,Z).3)(#)f2 + (diff(f1,Z).2)(#)(f2`|Z) +2(#)(diff(f1,Z).2(#)(
f2`|Z) + (f1`|Z)(#)diff(f2,Z).2) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,Z).3
)) by A2,Lm3,Th7
.=(diff(f1,Z).3)(#)f2 + 1(#)(diff(f1,Z).2)(#)(f2`|Z) +2(#)(diff(f1,Z).2
(#)(f2`|Z) + (f1`|Z)(#)diff(f2,Z).2) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(diff(f2,
Z).3)) by RFUNCT_1:21
.=(diff(f1,Z).3)(#)f2 + 1(#)(diff(f1,Z).2)(#)(f2`|Z) +(2(#)(diff(f1,Z).2
(#)(f2`|Z)) +2(#)((f1`|Z)(#)diff(f2,Z).2)) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(
diff(f2,Z).3)) by RFUNCT_1:16
.=(diff(f1,Z).3)(#)f2 +(1(#)(diff(f1,Z).2)(#)(f2`|Z) +(2(#)(diff(f1,Z).2
(#)(f2`|Z)) +2(#)((f1`|Z)(#)diff(f2,Z).2))) +((f1`|Z)(#)(diff(f2,Z).2)+ f1(#)(
diff(f2,Z).3)) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + (((1(#)(diff(f1,Z).2)(#)(f2`|Z) +2(#)(diff(f1,Z)
.2(#)(f2`|Z)))) +2(#)((f1`|Z)(#)diff(f2,Z).2)) +((f1`|Z)(#)(diff(f2,Z).2)+ f1
(#)(diff(f2,Z).3)) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + ((((1(#)(g1(#)(f2`|Z))+2(#)(g1(#)(f2`|Z))))) +2
(#)((f1`|Z)(#)g2))+((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3)) by RFUNCT_1:12
.=(diff(f1,Z).3)(#)f2 + (((((1+2)(#)(g1(#)(f2`|Z))))) +2(#)((f1`|Z)(#)g2
))+((f1`|Z)(#)g2+ f1(#)(diff(f2,Z).3)) by Th5
.=(diff(f1,Z).3)(#)f2 + (((3(#)(g1(#)(f2`|Z)))+2(#)((f1`|Z)(#)g2)) +((f1
`|Z)(#)g2+ f1(#)(diff(f2,Z).3))) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+(2(#)((f1`|Z)(#)g2) +((f1
`|Z)(#)g2+ f1(#)(diff(f2,Z).3)))) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+((2(#)((f1`|Z)(#)g2) +(f1
`|Z)(#)g2)+ f1(#)(diff(f2,Z).3))) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + ((3(#)(g1(#)(f2`|Z)))+((2(#)((f1`|Z)(#)g2) +1(#)
((f1`|Z)(#)g2))+ f1(#)(diff(f2,Z).3))) by RFUNCT_1:21
.=(diff(f1,Z).3)(#)f2+((3(#)(g1(#)(f2`|Z)))+(((2+1)(#)((f1`|Z)(#)g2)) +
f1(#)(diff(f2,Z).3))) by Th5
.=(diff(f1,Z).3)(#)f2 + (3(#)(g1(#)(f2`|Z))+3(#)((f1`|Z)(#)g2) + f1(#)(
diff(f2,Z).3)) by RFUNCT_1:8
.=(diff(f1,Z).3)(#)f2 + (3(#)(g1(#)(f2`|Z))+3(#)((f1`|Z)(#)g2)) + f1(#)(
diff(f2,Z).3) by RFUNCT_1:8;
hence thesis;
end;
theorem
diff(sin^2,Z).3=(-8)(#)((cos(#)sin)|Z)
proof
sin is_differentiable_on 3,Z by TAYLOR_2:21;
then
diff(sin(#)sin,Z).3 =(diff(sin,Z).(2*1+1))(#)sin + (3(#)(diff(sin,Z).(2*
1)(#)(sin`|Z)) +3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)(diff(sin,Z).(2*1+1)
) by Th64
.=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)(diff(sin,Z).(2*1)(#)(sin`|Z)) +3
(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)(diff(sin,Z).(2*1+1)) by TAYLOR_2:19
.=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)(diff(sin,Z).(2*1)(#)(sin`|Z)) +3
(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)((-1) |^ 1 (#) cos | Z) by
TAYLOR_2:19
.=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z))
+3(#)((sin`|Z)(#)diff(sin,Z).(2*1)))+ sin(#)((-1) |^ 1 (#) cos | Z) by
TAYLOR_2:19
.=((-1) |^ 1 (#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z))
+3(#)((sin`|Z)(#)((-1) |^ 1 (#) sin | Z)))+ sin(#)((-1) |^ 1 (#) cos | Z) by
TAYLOR_2:19
.=((-1)(#) cos | Z)(#)sin + (3(#)((-1) |^ 1 (#) sin |Z(#)(sin`|Z)) +3(#)
((sin`|Z)(#)((-1)|^1(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z)
.=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin
`|Z)(#)((-1)|^1(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z)
.=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin
`|Z)(#)((-1)(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z)
.=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin
`|Z)(#)((-1)(#) sin|Z)))+ sin(#)((-1)(#) cos | Z)
.=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(cos|Z)) +3(#)((sin`|
Z)(#)((-1)(#) sin|Z)))+ sin(#)((-1)(#)cos|Z) by TAYLOR_2:17
.=((-1)(#) cos | Z)(#)sin + ((3(#)((-1)(#) sin |Z(#)(cos|Z)) +3(#)((cos|
Z)(#)((-1)(#) sin|Z))))+ sin(#)((-1)(#) cos|Z) by TAYLOR_2:17
.=((-1)(#) cos | Z)(#)sin +((3+3)(#)((cos|Z)(#)((-1)(#) sin|Z))) +sin(#)
((-1)(#) cos|Z) by Th5
.=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(((-1)(#) cos | Z)(#)sin +((-1)(#)
cos | Z)(#)sin) by RFUNCT_1:8
.=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(1(#)(((-1)(#) (cos | Z))(#)sin) +(
(-1)(#) cos | Z)(#)sin) by RFUNCT_1:21
.=(6(#)((cos|Z)(#)((-1)(#) sin|Z))) +(1(#)(((-1)(#) (cos | Z))(#)sin) +1
(#)(((-1)(#) cos | Z)(#)sin)) by RFUNCT_1:21
.=(6(#)((cos|Z)(#)((-1)(#)sin|Z)))+((1+1)(#)(((-1)(#)(cos|Z))(#)sin)) by
Th5
.=(6(#)((-1)(#)((cos|Z)(#)sin|Z)))+(2(#)(((-1)(#)(cos|Z))(#)sin)) by
RFUNCT_1:13
.=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)(((-1)(#)(cos|Z))(#)sin) by RFUNCT_1:45
.=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)((-1)(#)((cos|Z)(#)sin)) by RFUNCT_1:12
.=6(#)((-1)(#)((cos(#)sin)|Z))+2(#)((-1)(#)((cos(#)sin)|Z)) by RFUNCT_1:45
.=(6+2)(#)((-1)(#)((cos(#)sin)|Z)) by Th5
.=(8*(-1))(#)((cos(#)sin)|Z) by RFUNCT_1:17
.=(-8)(#)((cos(#)sin)|Z);
hence thesis;
end;
theorem
f is_differentiable_on 2,Z implies diff(f^2,Z).2=2(#)(f(#)(diff(f,Z).2
))+2(#)((f`|Z)^2)
proof
assume f is_differentiable_on 2,Z;
then
diff(f^2,Z).2 =(diff(f,Z).2)(#)f+(2(#)((f`|Z)(#)(f`|Z))+f(#)(diff(f,Z).2
)) by Th50
.=((diff(f,Z).2)(#)f+ f(#)(diff(f,Z).2)) + 2(#)((f`|Z)(#)(f`|Z)) by
RFUNCT_1:8
.=1(#)(f(#)(diff(f,Z).2))+ f(#)(diff(f,Z).2) + 2(#)((f`|Z)(#)(f`|Z)) by
RFUNCT_1:21
.=1(#)(f(#)(diff(f,Z).2))+1(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z))
by RFUNCT_1:21
.=(1+1)(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z)) by Th5
.=2(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)(#)(f`|Z))
.=2(#)(f(#)(diff(f,Z).2))+2(#)((f`|Z)^2);
hence thesis;
end;
Lm4: f / f = (dom f \ f"{0}) --> 1
proof
A1: dom (f/f) = dom f /\ (dom f \ f"{0}) by RFUNCT_1:def 1
.= (dom f \ f"{0}) by XBOOLE_1:28,36;
for c being object st c in dom (f/f) holds (f/f).c = 1
proof
let c be object;
reconsider cc = c as set by TARSKI:1;
assume
A2: c in dom (f/f);
then c in dom f & not c in f"{0} by A1,XBOOLE_0:def 5;
then not f.c in {0} by FUNCT_1:def 7;
then
A3: f.c <> 0 by TARSKI:def 1;
(f/f).c = f.cc * (f.cc)" by A2,RFUNCT_1:def 1;
hence thesis by A3,XCMPLX_0:def 7;
end;
hence thesis by A1,FUNCOP_1:11;
end;
Lm5: (f (#) (f (#) f))"{0} = f"{0}
proof
thus (f (#) (f (#) f))"{0} c= f"{0}
proof
let x be object;
assume
A1: x in (f (#) (f (#) f))"{0};
then (f (#) (f (#) f)).x in {0} by FUNCT_1:def 7;
then (f (#) (f (#) f)).x = 0 by TARSKI:def 1;
then (f.x) * ((f (#) f).x) = 0 by VALUED_1:5;
then (f.x) * (f.x) * (f.x) = 0 by VALUED_1:5;
then f.x = 0 or (f.x) * (f.x) = 0 by XCMPLX_1:6;
then f.x = 0 or f.x = 0 or f.x = 0 by XCMPLX_1:6;
then
A2: f.x in {0} by TARSKI:def 1;
x in dom (f (#) (f (#) f)) by A1,FUNCT_1:def 7;
then x in dom f /\ dom (f (#) f) by VALUED_1:def 4;
then x in dom f by XBOOLE_0:def 4;
hence thesis by A2,FUNCT_1:def 7;
end;
let x be object;
assume
A3: x in f"{0};
then f.x in {0} by FUNCT_1:def 7;
then
A4: f.x = 0 by TARSKI:def 1;
x in dom f /\ dom f by A3,FUNCT_1:def 7;
then x in dom (f (#) f) /\ dom f by VALUED_1:def 4;
then
A5: x in dom (f (#) (f (#) f)) by VALUED_1:def 4;
(f (#) (f (#) f)).x = (f.x) * ((f (#) f).x) by VALUED_1:5
.= (f.x) * (f.x) by A4
.= 0 by A4;
then (f (#) (f (#) f)).x in {0} by TARSKI:def 1;
hence thesis by A5,FUNCT_1:def 7;
end;
theorem
f is_differentiable_on 2,Z & (for x0 st x0 in Z holds f.x0 <> 0)
implies diff(f^,Z).2=((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) /(f(#)(f(#)f)))
proof
assume that
A1: f is_differentiable_on 2,Z and
A2: for x0 st x0 in Z holds f.x0 <> 0;
A3: f is_differentiable_on Z by A1,Th7;
then
A4: f^ is_differentiable_on Z by A2,FDIFF_2:22;
A5: Z c= dom f by A3,FDIFF_1:def 6;
A6: for x0 st x0 in Z holds (f(#)f).x0 <> 0
proof
let x0;
assume
A7: x0 in Z;
then
A8: f.x0 <>0 by A2;
dom(f(#)f) = dom f/\dom f by VALUED_1:def 4
.= dom f;
then (f(#)f).x0 =f.x0*f.x0 by A5,A7,VALUED_1:def 4;
hence thesis by A8,XCMPLX_1:6;
end;
diff(f,Z).1 = diff(f,Z).(1+0) .=diff(f,Z).0`|Z by TAYLOR_1:def 5
.=f|Z`|Z by TAYLOR_1:def 5
.=f`|Z by A3,FDIFF_2:16;
then
A9: f`|Z is_differentiable_on Z by A1;
then (f|Z) `| Z is_differentiable_on Z by A3,FDIFF_2:16;
then
A10: (diff(f,Z).0) `| Z is_differentiable_on Z by TAYLOR_1:def 5;
A11: f(#)f is_differentiable_on Z by A3,FDIFF_2:20;
then
A12: (f`|Z) / (f (#) f) is_differentiable_on Z by A9,A6,FDIFF_2:21;
diff(f^,Z).2 = diff(f^,Z).(1+1) .=diff(f^,Z).(1+0)`|Z by TAYLOR_1:def 5
.=(diff(f^,Z).0)`|Z`|Z by TAYLOR_1:def 5
.=f^|Z`|Z`|Z by TAYLOR_1:def 5
.=f^`|Z`|Z by A4,FDIFF_2:16
.=(- (f`|Z)/ (f (#) f))`|Z by A2,A3,FDIFF_2:22
.=(-1)(#)(((f`|Z)/ (f (#) f))`|Z) by A12,FDIFF_2:19
.=(-1)(#)((((f`|Z)`|Z)(#)(f(#)f)-(f(#)f)`|Z(#)(f`|Z))/((f(#)f)(#)(f(#)f)
)) by A9,A11,A6,FDIFF_2:21
.=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)- ((f(#)f)`|Z)(#)(f`|Z))/((f(#)f)(#)(f
(#)f))) by A1,Lm3,Th7
.=(-1)(#)(((diff(f,Z).2)(#)(f(#)f)-((f`|Z)(#)f + f(#)(f`|Z))(#)(f`|Z)) /
((f(#)f)(#)(f(#)f))) by A3,FDIFF_2:20
.=(-1)(#)(((diff(f,Z).2)(#)(f^2)-(f(#)((f`|Z)+(f`|Z)))(#)(f`|Z)) /((f(#)
f)(#)(f(#)f))) by RFUNCT_1:11
.=(-1)(#)(((diff(f,Z).2)(#)(f^2)-(f(#)(1(#)(f`|Z)+(f`|Z)))(#)(f`|Z)) /((
f(#)f)(#)(f(#)f))) by RFUNCT_1:21
.=(-1)(#)(((diff(f,Z).2)(#)(f^2)-(f(#)(1(#)(f`|Z)+1(#)(f`|Z)))(#)(f`|Z))
/((f(#)f)(#)(f(#)f))) by RFUNCT_1:21
.=(-1)(#)(((diff(f,Z).2)(#)(f^2)-(f(#)((1+1)(#)(f`|Z)))(#)(f`|Z)) /((f
(#)f)(#)(f(#)f))) by Th5
.=(-1)(#)((f(#)((diff(f,Z).2)(#)f)-(f(#)((2(#)(f`|Z)))(#)(f`|Z))) /((f
(#)f)(#)(f(#)f))) by RFUNCT_1:9
.=((-1)(#)((f(#)((diff(f,Z).2)(#)f)-(f(#)((2(#)(f`|Z)))(#)(f`|Z)))) /((f
(#)f)(#)(f(#)f))) by RFUNCT_1:32
.=((((f(#)((2(#)(f`|Z)))(#)(f`|Z))-(f(#)((diff(f,Z).2)(#)f)))) /((f(#)f)
(#)(f(#)f))) by RFUNCT_1:19
.=((f(#)((2(#)(f`|Z))(#)(f`|Z)))-(f(#)((diff(f,Z).2)(#)f))) /((f(#)f)(#)
(f(#)f)) by RFUNCT_1:9
.=(f(#)(((2(#)(f`|Z))(#)(f`|Z))-((diff(f,Z).2)(#)f))) /(f(#)f(#)(f(#)f))
by RFUNCT_1:15
.=(f(#)(((2(#)(f`|Z))(#)(f`|Z))-((diff(f,Z).2)(#)f))) /(f(#)(f(#)(f(#)f)
)) by RFUNCT_1:9
.=(f/f)(#)((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) /(f(#)(f(#)f))) by
RFUNCT_1:34;
then
A13: diff(f^,Z).2 = (f/f)(#)((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) /(f(#)(f
(#)f)))
.= ((dom f \ f"{0}) --> 1) (#) ((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) /(
f(#)(f(#)f))) by Lm4;
A14: dom (diff(f,Z).(1+1)) = dom ((diff(f,Z).(0+1)) `| Z) by TAYLOR_1:def 5
.= dom ((diff(f,Z).0) `| Z `| Z) by TAYLOR_1:def 5
.= Z by A10,FDIFF_1:def 7;
A15: dom (diff(f,Z).2(#)f) = dom (diff(f,Z).2) /\ dom f by VALUED_1:def 4
.= Z /\ dom f by A14;
A16: dom (2(#)(f`|Z)(#)(f`|Z)) = dom (2(#)((f`|Z)(#)(f`|Z))) by RFUNCT_1:13
.= dom ((f`|Z) (#) (f`|Z)) by VALUED_1:def 5
.= dom (f`|Z) /\ dom (f`|Z) by VALUED_1:def 4
.= dom (f`|Z)
.= Z by A3,FDIFF_1:def 7;
set g1 = ((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) / (f(#)(f(#)f)));
set g2 = (f/f) (#) ((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f) / (f(#)(f(#)f)));
A17: dom (f(#)(f(#)f)) = (dom f) /\ dom (f (#) f) by VALUED_1:def 4
.= (dom f) /\ ((dom f) /\ dom f) by VALUED_1:def 4
.= (dom f) /\ dom f
.= dom f;
A18: f / f = (dom f \ f"{0}) --> 1 by Lm4;
then
A19: dom (f/f) = dom f \ f"{0} by FUNCOP_1:13;
A20: dom g2 = dom (f/f) /\ dom g1 by VALUED_1:def 4;
then
A21: dom g2 c= dom (f/f) by XBOOLE_1:17;
A22: for x being Element of REAL st x in dom g2 holds g2.x = g1.x
proof
let x be Element of REAL;
assume
A23: x in dom g2;
g2.x = ((f/f) (#) g1).x .= ((f/f).x) * (g1.x) by A23,VALUED_1:def 4
.= 1 * (g1.x) by A18,A19,A21,A23,FUNCOP_1:7
.= g1.x;
hence thesis;
end;
dom (((2(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f)/(f(#)(f(#)f)))) = dom (((2
(#)(f`|Z)(#)(f`|Z)-diff(f,Z).2(#)f))) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"{
0}) by RFUNCT_1:def 1
.= (dom (2(#)(f`|Z)(#)(f`|Z)) /\ dom (diff(f,Z).2(#)f)) /\ ((dom (f(#)(f
(#)f))) \ (f(#)(f(#)f))"{0}) by VALUED_1:12
.= (Z /\ dom (diff(f,Z).2(#)f)) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"
{0}) by A16
.= (Z /\ (Z /\ dom f)) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"{0}) by A15
.= (Z /\ Z /\ dom f) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"{0}) by
XBOOLE_1:16
.= (Z /\ dom f) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"{0})
.= (Z /\ dom f) /\ ((dom f) \ (f(#)(f(#)f))"{0}) by A17
.= (Z /\ dom f /\ (dom f)) \ (f(#)(f(#)f))"{0} by XBOOLE_1:49
.= (Z /\ (dom f /\ (dom f))) \ (f(#)(f(#)f))"{0} by XBOOLE_1:16
.= (Z /\ dom f) \ (f(#)(f(#)f))"{0}
.= Z \ (f(#)(f(#)f))"{0} by A5,XBOOLE_1:28
.= Z \ f"{0} by Lm5;
then dom g2 = dom g1 by A5,A19,A20,XBOOLE_1:28,33;
hence thesis by A18,A13,A22,PARTFUN1:5;
end;
theorem
diff(exp_R(#)sin,Z).3=(2(#)(exp_R(#)((-sin)+cos)))|Z
proof
sin is_differentiable_on 3,Z & exp_R is_differentiable_on 3,Z by TAYLOR_2:10
,21;
then diff(exp_R(#)sin,Z).3 =(diff(exp_R,Z).3)(#)sin + (3(#)(diff(exp_R,Z).2
(#)(sin`|Z)) +3(#)((exp_R`|Z)(#)diff(sin,Z).2))+ exp_R(#)(diff(sin,Z).3) by
Th64
.=(exp_R|Z)(#)sin + (3(#)(diff(exp_R,Z).2(#)(sin`|Z)) +3(#)((exp_R`|Z)
(#)diff(sin,Z).2))+ exp_R(#)(diff(sin,Z).3) by TAYLOR_2:6
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(sin`|Z)) +3(#)((exp_R`|Z)(#)diff(
sin,Z).2))+exp_R(#)(diff(sin,Z).3) by TAYLOR_2:6
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(sin`|Z)) +3(#)((exp_R|Z)(#)diff(sin
,Z).2))+exp_R(#)(diff(sin,Z).3) by TAYLOR_2:5
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)diff(sin,
Z).(2*1)))+ exp_R(#)(diff(sin,Z).(2*1+1)) by TAYLOR_2:17
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)|^1
(#)sin|Z)))+ exp_R(#)(diff(sin,Z).(2*1+1)) by TAYLOR_2:19
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)|^1
(#)sin|Z)))+ exp_R(#)((-1) |^ 1(#)cos |Z ) by TAYLOR_2:19
.=(exp_R|Z)(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)(#)
sin|Z)))+exp_R(#)((-1)|^1(#)cos |Z)
.=exp_R|Z(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)(#)sin
|Z)))+exp_R(#)((-1)(#)cos|Z)
.=(exp_R(#)sin)|Z+(3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)(#)sin
|Z)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:45
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +3(#)((exp_R|Z)(#)((-1)(#)sin|Z
)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:45
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +3(#)((-1)(#)((exp_R|Z)(#)sin|Z
)))+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:13
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +(3*(-1))(#)((exp_R|Z)(#)sin|Z)
)+exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:17
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +(-3)(#)((exp_R(#)sin)|Z))+
exp_R(#)((-1)(#)cos|Z) by RFUNCT_1:45
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +(-3)(#)((exp_R(#)sin)|Z))+(-1)
(#)(exp_R(#)cos|Z) by RFUNCT_1:13
.=(exp_R(#)sin)|Z+(3(#)((exp_R(#)cos)|Z) +(-3)(#)((exp_R(#)sin)|Z))+(-1)
(#)((exp_R(#)cos)|Z) by RFUNCT_1:45
.=(exp_R(#)sin)|Z+3(#)((exp_R(#)cos)|Z) +(-3)(#)((exp_R(#)sin)|Z)+(-1)
(#)((exp_R(#)cos)|Z) by RFUNCT_1:8
.=3(#)((exp_R(#)cos)|Z)+1(#)((exp_R(#)sin)|Z) +(-3)(#)((exp_R(#)sin)|Z)+
(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:21
.=3(#)((exp_R(#)cos)|Z)+(1(#)((exp_R(#)sin)|Z) +(-3)(#)((exp_R(#)sin)|Z)
)+(-1)(#)((exp_R(#)cos)|Z) by RFUNCT_1:8
.=3(#)((exp_R(#)cos)|Z)+((1+(-3))(#)((exp_R(#)sin)|Z)) +(-1)(#)((exp_R
(#)cos)|Z) by Th5
.=((-2)(#)((exp_R(#)sin)|Z))+(3(#)((exp_R(#)cos)|Z) +(-1)(#)((exp_R(#)
cos)|Z)) by RFUNCT_1:8
.=((-2)(#)((exp_R(#)sin)|Z))+((3+(-1))(#)((exp_R(#)cos)|Z)) by Th5
.=((-2)(#)(exp_R(#)sin))|Z+2(#)((exp_R(#)cos)|Z) by RFUNCT_1:49
.=((-2)(#)(exp_R(#)sin))|Z+(2(#)(exp_R(#)cos))|Z by RFUNCT_1:49
.=((2*(-1))(#)(exp_R(#)sin)+2(#)(exp_R(#)cos))|Z by RFUNCT_1:44
.=(2(#)((-1)(#)(exp_R(#)sin))+2(#)(exp_R(#)cos))|Z by RFUNCT_1:17
.=(2(#)(((-1)(#)(exp_R(#)sin))+(exp_R(#)cos)))|Z by RFUNCT_1:16
.=(2(#)((exp_R(#)((-1)(#)sin))+(exp_R(#)cos)))|Z by RFUNCT_1:13
.=(2(#)(exp_R(#)((-sin)+cos)))|Z by RFUNCT_1:11;
hence thesis;
end;