:: Several Higher Differentiation Formulas of Special Functions :: by Junjie Zhao , Xiquan Liang and Li Yan :: :: Received March 18, 2008 :: Copyright (c) 2008-2012 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; notations SUBSET_1, PARTFUN1, RCOMP_1, XXREAL_0, NUMBERS, COMPLEX1, FUNCT_2, FUNCOP_1, REAL_1, ORDINAL1, NAT_1, NAT_D, VALUED_1, SEQ_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, SEQ_1, VALUED_1, BINOP_2, NAT_D, SEQFUNC, RELSET_1, NEWTON; registrations RELSET_1, NUMBERS, XXREAL_0, NAT_1, MEMBERED, VALUED_0, RCOMP_1, FUNCT_1, INT_1, ORDINAL1, FUNCT_2; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; definitions TAYLOR_1, VALUED_1, FDIFF_1, TARSKI, SQUARE_1, XBOOLE_0; 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; 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 st x in dom(f1(#)f2) holds ((-f1)(#)(-f2)).x=(f1(#)f2).x proof let x; 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 set; 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 set; A4: 0 in {0} by TARSKI:def 1; assume x in {0}; then A5: x = 0 by TARSKI:def 1; {0} 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 set; 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 Element of REAL holds n(#)f1+m(#)f1=(n+m)(#)f1 proof let n,m be Element of 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 st x in dom f1 holds (n(#)f1+m(#)f1).x=((n+m)(#)f1).x proof let x; 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,XBOOLE_1:1; 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,TAYLOR_1:def 6; 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 be Real st x in REAL holds ( #Z n)|REAL is_differentiable_in x proof let x be Real; 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 by NEWTON:5 .=((-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 Element of NAT such that A8: i = 2*j by ABIAN:def 2; per cases; suppose j is even; then consider m be Element of 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 by NEWTON:10 .=(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 Element of 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 by NEWTON:10 .=((-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 Element of NAT such that A11: i = 2*j +1 by ABIAN:9; per cases; suppose j is even; then consider m be Element of 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 by NEWTON:10 .=(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 Element of 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 by NEWTON:10 .=((-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 by WSIERP_1:1 .=((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 Element of NAT such that A8: i = 2*j by ABIAN:def 2; per cases; suppose j is even; then consider m be Element of 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 by NEWTON:10 .=(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 Element of 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 by NEWTON:10 .=((-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 Element of NAT such that A11: i = 2*j +1 by ABIAN:9; per cases; suppose j is even; then consider m be Element of 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 by NEWTON:10 .=((-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 Element of 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 by NEWTON:10 .=( 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 Element of NAT st P[k] holds P[k+1] proof let k be Element of NAT such that A2: P[k]; assume A3: f1 is_differentiable_on (k+1),Z & f2 is_differentiable_on (k+1),Z; k<= (k+1)-1; then A4: diff(f1,Z).k is_differentiable_on Z & diff(f2,Z).k is_differentiable_on Z by A3,TAYLOR_1:def 6; k=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,TAYLOR_1:def 6; 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,TAYLOR_1:def 6; 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,TAYLOR_1:def 6; 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 Real st x in Z holds (( #Z n ) `| Z ).x = ((n (#) #Z (n-1) )| Z ).x proof let x be 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]; A3: (k!)>0 by NEWTON:17; assume A4: n>(k+1); then A5: n-k>(k+1)-k by XREAL_1:9; A6: (k+1)+(-1)<=n+0 by A4,XREAL_1:7; then reconsider l=n-k as Element of NAT by INT_1:5; l>=(k+1)-k by A4,XREAL_1:9; then A7: ((k+1)!)>0 & l-'1=n-k-1 by NEWTON:17,XREAL_1:233; reconsider s=n-(k+1) as Element of NAT by A4,INT_1:5; A8: #Z (l) is_differentiable_on Z by Th8,FDIFF_1:26; then A9: (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,A4, TAYLOR_1:def 5,XXREAL_0:2 .=(((n choose k)*(k!))(#) #Z (l))`| Z by A9,FDIFF_2:16 .=(n choose k)*(k!)(#) ( #Z (l) `| Z) by A8,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 A6,NEWTON:def 3 .=(((n!)/ (l!)*l)(#) #Z (l-1))| Z by A3,XCMPLX_1:92 .=(((n!)/ ((l-'1)!))(#) #Z (l-1))| Z by A5,Lm1 .=(((n!)/ (((s)!)*((k+1)!)))*((k+1)!)(#) #Z (n-k-1))| Z by A7,XCMPLX_1:92 .=((n choose (k+1))*((k+1)!)(#) #Z (n-(k+1)))| Z by A4,NEWTON:def 3; hence thesis; end; A10: 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 (A10,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 proof A1: -f = (-1)(#)f; assume A2: f is_differentiable_on n,Z; then diff(-f,Z).n = (-1)(#) diff(f,Z).n by Th21 .= -diff(f,Z).n; hence thesis by A2,A1,Th22; end; 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: abs(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; (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)).x 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+n0 by NEWTON:17; A4: #Z 1 is_differentiable_on Z by Th8,FDIFF_1:26; then A5: ((n+1)!)(#) #Z 1 is_differentiable_on Z by FDIFF_2:19; Z c= dom( #Z 1) by A4,FDIFF_1:def 6; then A6: 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 A3,XCMPLX_1:92 .=((((n+1)!)(#) #Z 1)`| Z).x by A5,FDIFF_2:16 .=((n+1)!)*diff( #Z 1,x) by A1,A4,A6,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 A7: 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 A7,NEWTON:12,PREPOWER:34; hence thesis; end; end; theorem Th38: #Z n is_differentiable_on n,Z proof let i be Element of NAT; assume A1: i <= n-1; reconsider i as Element of NAT; -1+n<0+n by XREAL_1:6; then A2: im 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; 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 by TAYLOR_1:def 6; 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).x 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: n!<>0 by NEWTON:17; A4: 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 A3,XCMPLX_1:89; A5: m!<>0 by NEWTON:17; 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 A5,XCMPLX_1:89; hence thesis by A4; end; theorem for n,m be Element of NAT,r,x be 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 Real; assume that A1: n>m and A2: r>0; abs(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 by FUNCT_1:18; 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; 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,PREPOWER:5; 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.x)^2 by Lm2,TAYLOR_1:2 .=-(1 * x #Z 0)/x^2 by FUNCT_1:18 .=-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 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; 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 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; 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 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; 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; A3: 0<= 2-1; then diff(f1,Z).0 is_differentiable_on Z by A1,TAYLOR_1:def 6; then f1|Z is_differentiable_on Z by TAYLOR_1:def 5; then A4: f1 is_differentiable_on Z by Th6; A5: 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 A4,FDIFF_2:16; A6: 1<=2-1; diff(f2,Z).0 is_differentiable_on Z by A2,A3,TAYLOR_1:def 6; then f2|Z is_differentiable_on Z by TAYLOR_1:def 5; then A7: f2 is_differentiable_on Z by Th6; then A8: f1(#)f2 is_differentiable_on Z by A4,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 A7,FDIFF_2:16; then A9: f2`|Z is_differentiable_on Z by A2,A6,TAYLOR_1:def 6; then A10: f1(#)(f2`|Z) is_differentiable_on Z by A4,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 A4,FDIFF_2:16; then A11: f1`|Z is_differentiable_on Z by A1,A6,TAYLOR_1:def 6; then A12: (f1`|Z)(#)f2 is_differentiable_on Z by A7,FDIFF_2:20; A13: 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 A7,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 A8,FDIFF_2:16 .=((f1`|Z)(#)f2 + f1(#)(f2`|Z))`|Z by A4,A7,FDIFF_2:20 .=((f1`|Z)(#)f2)`|Z+(f1(#)(f2`|Z))`|Z by A12,A10,FDIFF_2:17 .=(((f1`|Z)`|Z)(#)f2 + (f1`|Z)(#)(f2`|Z))+(f1(#)(f2`|Z))`|Z by A7,A11, FDIFF_2:20 .=((diff(f1,Z).2)(#)f2 + (f1`|Z)(#)(f2`|Z))+ ((f1`|Z)(#)(f2`|Z) + f1(#)( diff(f2,Z).2)) by A4,A9,A5,A13,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 st x0 in dom(((id REAL)^)|Z) holds (ln`| Z).x0 = (((id REAL)^)| Z ).x0 proof let x0; 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) by FUNCT_1:18 .=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; 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)by NEWTON:5 .=((-1)(#) sin | Z)(#)sin + 2(#)((sin`|Z)(#)(sin`|Z)) +sin(#)((-1)(#) sin | Z) by NEWTON:5 .=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)by NEWTON:5 .=((-1)(#) cos | Z)(#)cos + 2(#)((cos`|Z)(#)(cos`|Z)) +cos(#)((-1)(#) cos | Z) by NEWTON:5 .=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) by NEWTON:5 .=((-1)(#)sin | Z)(#)cos + 2(#)((sin`|Z)(#)(cos`|Z)) + sin(#)((-1)(#)cos | Z) by NEWTON:5 .=((-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,XBOOLE_1:1; 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 st x in dom (tan`|Z) holds ((tan)`|Z).x = (((cos^)(#)(cos^))|Z).x proof let x; 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,XBOOLE_1:1; A6: for x st x in Z holds ((cos^)`|Z).x=(((cos^)(#)tan)|Z).x proof let x; 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,XBOOLE_1:1; A8: for x st x in dom (cot`|Z) holds ((cot)`|Z).x =(((-1)(#)((sin^)(#)(sin^ )))|Z).x proof let x; 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,XBOOLE_1:1; 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,XBOOLE_1:1; 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 st x in dom((sin^)`|Z) holds ((sin^)`|Z).x=((-(sin^)(#)cot)|Z).x proof let x; 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 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; 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 by NEWTON:5 .=((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 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; 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 by NEWTON:5 .=((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; A4: 1<= 3-1; 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 A5: f2`|Z is_differentiable_on Z by A2,A4,TAYLOR_1:def 6; A6: f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z by A1,A2, TAYLOR_1:23; A7: f1 is_differentiable_on Z by A1,Th7; A8: 2 <=3-1; then A9: diff(f1,Z).2 is_differentiable_on Z by A1,TAYLOR_1:def 6; then A10: (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 A7,FDIFF_2:16; then A11: f1`|Z is_differentiable_on Z by A1,A4,TAYLOR_1:def 6; then A12: (f1`|Z)(#)(f2`|Z) is_differentiable_on Z by A5,FDIFF_2:20; then A13: 2(#)((f1`|Z)(#)(f2`|Z)) is_differentiable_on Z by FDIFF_2:19; then A14: (diff(f1,Z).2)(#)f2 + 2(#)((f1`|Z)(#)(f2`|Z)) is_differentiable_on Z by A10,FDIFF_2:17; A15: diff(f2,Z).2 is_differentiable_on Z by A2,A8,TAYLOR_1:def 6; then A16: f1(#)(diff(f2,Z).2) is_differentiable_on Z by A7,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 A6,Th50 .=((diff(f1,Z).2)(#)f2+2(#)((f1`|Z)(#)(f2`|Z)))`|Z+(f1(#)(diff(f2,Z).2)) `|Z by A16,A14,FDIFF_2:17 .=((diff(f1,Z).2)(#)f2)`|Z+(2(#)((f1`|Z)(#)(f2`|Z)))`|Z +(f1(#)(diff(f2, Z).2))`|Z by A10,A13,FDIFF_2:17 .=((diff(f1,Z).2)(#)f2)`|Z+2(#)((((f1`|Z)(#)(f2`|Z)))`|Z) +(f1(#)(diff( f2,Z).2))`|Z by A12,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,A9,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 A7,A15, 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 A11,A5,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) by NEWTON:5 .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin `|Z)(#)((-1)|^1(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z) by NEWTON:5 .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin `|Z)(#)((-1)(#)sin|Z)))+sin(#)((-1)|^1(#)cos|Z) by NEWTON:5 .=((-1)(#) cos | Z)(#)sin + (3(#)((-1)(#) sin |Z(#)(sin`|Z)) +3(#)((sin `|Z)(#)((-1)(#) sin|Z)))+ sin(#)((-1)(#) cos | Z) by NEWTON:5 .=((-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 set st c in dom (f/f) holds (f/f).c = 1 proof let c be set; 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.c * (f.c)" 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 set; 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 set; 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; A9: 1<=2-1; 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 A10: f`|Z is_differentiable_on Z by A1,A9,TAYLOR_1:def 6; then (f|Z) `| Z is_differentiable_on Z by A3,FDIFF_2:16; then A11: (diff(f,Z).0) `| Z is_differentiable_on Z by TAYLOR_1:def 5; A12: f(#)f is_differentiable_on Z by A3,FDIFF_2:20; then A13: (f`|Z) / (f (#) f) is_differentiable_on Z by A10,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 A13,FDIFF_2:19 .=(-1)(#)((((f`|Z)`|Z)(#)(f(#)f)-(f(#)f)`|Z(#)(f`|Z))/((f(#)f)(#)(f(#)f) )) by A10,A12,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 A14: 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; A15: 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 A11,FDIFF_1:def 7; A16: dom (diff(f,Z).2(#)f) = dom (diff(f,Z).2) /\ dom f by VALUED_1:def 4 .= Z /\ dom f by A15; A17: 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))); A18: 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; A19: f / f = (dom f \ f"{0}) --> 1 by Lm4; then A20: dom (f/f) = dom f \ f"{0} by FUNCOP_1:13; A21: dom g2 = dom (f/f) /\ dom g1 by VALUED_1:def 4; then A22: dom g2 c= dom (f/f) by XBOOLE_1:17; A23: for x being Element of REAL st x in dom g2 holds g2.x = g1.x proof let x be Element of REAL; assume A24: x in dom g2; g2.x = ((f/f) (#) g1).x .= ((f/f).x) * (g1.x) by A24,VALUED_1:def 4 .= 1 * (g1.x) by A19,A20,A22,A24,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 A17 .= (Z /\ (Z /\ dom f)) /\ ((dom (f(#)(f(#)f))) \ (f(#)(f(#)f))"{0}) by A16 .= (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 A18 .= (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,A20,A21,XBOOLE_1:28,33; hence thesis by A19,A14,A23,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) by NEWTON:5 .=exp_R|Z(#)sin + (3(#)(exp_R|Z(#)(cos|Z)) +3(#)((exp_R|Z)(#)((-1)(#)sin |Z)))+exp_R(#)((-1)(#)cos|Z) by NEWTON:5 .=(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;