:: HFDIFF_1 semantic presentation begin theorem Th1: :: HFDIFF_1:1 for Z being open Subset of REAL for f being Function of REAL,REAL holds dom (f | Z) = Z proof let Z be open Subset of REAL; ::_thesis: for f being Function of REAL,REAL holds dom (f | Z) = Z let f be Function of REAL,REAL; ::_thesis: dom (f | Z) = Z 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 ; ::_thesis: verum end; theorem Th2: :: HFDIFF_1:2 for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2 proof let f1, f2 be PartFunc of REAL,REAL; ::_thesis: (- f1) (#) (- f2) = f1 (#) f2 ( 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 being Real st x in dom (f1 (#) f2) holds ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x proof let x be Real; ::_thesis: ( x in dom (f1 (#) f2) implies ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x ) assume A2: x in dom (f1 (#) f2) ; ::_thesis: ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x 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 ((- f1) (#) (- f2)) . x = (f1 (#) f2) . x by A2, VALUED_1:def_4; ::_thesis: verum end; hence (- f1) (#) (- f2) = f1 (#) f2 by A1, PARTFUN1:5; ::_thesis: verum end; theorem Th3: :: HFDIFF_1:3 for n being Element of NAT st n >= 1 holds ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) proof let n be Element of NAT ; ::_thesis: ( n >= 1 implies ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) ) assume A1: n >= 1 ; ::_thesis: ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) A2: (#Z n) " {0} = {0} proof thus (#Z n) " {0} c= {0} :: according to XBOOLE_0:def_10 ::_thesis: {0} c= (#Z n) " {0} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (#Z n) " {0} or x in {0} ) assume A3: x in (#Z n) " {0} ; ::_thesis: x in {0} then reconsider x = 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 x in {0} by TARSKI:def_1; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {0} or x in (#Z n) " {0} ) A4: 0 in {0} by TARSKI:def_1; assume x in {0} ; ::_thesis: x in (#Z n) " {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 x in (#Z n) " {0} by A5, A6, A4, FUNCT_1:def_7; ::_thesis: verum end; then dom ((#Z n) ^) = (dom (#Z n)) \ {0} by RFUNCT_1:def_2 .= REAL \ {0} by FUNCT_2:def_1 ; hence ( dom ((#Z n) ^) = REAL \ {0} & (#Z n) " {0} = {0} ) by A2; ::_thesis: verum end; theorem :: HFDIFF_1:4 for r, p being Real for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^)) proof let r, p be Real; ::_thesis: for n being Element of NAT holds (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^)) let n be Element of NAT ; ::_thesis: (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^)) 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__::_thesis:_for_c_being_set_st_c_in_dom_((r_*_p)_(#)_((#Z_n)_^))_holds_ ((r_*_p)_(#)_((#Z_n)_^))_._c_=_(r_(#)_(p_(#)_((#Z_n)_^)))_._c let c be set ; ::_thesis: ( c in dom ((r * p) (#) ((#Z n) ^)) implies ((r * p) (#) ((#Z n) ^)) . c = (r (#) (p (#) ((#Z n) ^))) . c ) assume A2: c in dom ((r * p) (#) ((#Z n) ^)) ; ::_thesis: ((r * p) (#) ((#Z n) ^)) . c = (r (#) (p (#) ((#Z n) ^))) . c 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 ; ::_thesis: verum end; hence (r * p) (#) ((#Z n) ^) = r (#) (p (#) ((#Z n) ^)) by A1, FUNCT_1:2; ::_thesis: verum end; theorem Th5: :: HFDIFF_1:5 for f1 being PartFunc of REAL,REAL for n, m being Element of REAL holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1 proof let f1 be PartFunc of REAL,REAL; ::_thesis: for n, m being Element of REAL holds (n (#) f1) + (m (#) f1) = (n + m) (#) f1 let n, m be Element of REAL ; ::_thesis: (n (#) f1) + (m (#) f1) = (n + m) (#) f1 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 Real st x in dom f1 holds ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x proof let x be Real; ::_thesis: ( x in dom f1 implies ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x ) assume A3: x in dom f1 ; ::_thesis: ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x 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 ((n (#) f1) + (m (#) f1)) . x = ((n + m) (#) f1) . x by A5; ::_thesis: verum end; dom ((n (#) f1) + (m (#) f1)) = dom ((n + m) (#) f1) by A1, VALUED_1:def_5; hence (n (#) f1) + (m (#) f1) = (n + m) (#) f1 by A1, A2, PARTFUN1:5; ::_thesis: verum end; theorem Th6: :: HFDIFF_1:6 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds f is_differentiable_on Z proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f | Z is_differentiable_on Z holds f is_differentiable_on Z let f be PartFunc of REAL,REAL; ::_thesis: ( f | Z is_differentiable_on Z implies f is_differentiable_on Z ) A1: dom (f | Z) c= dom f by RELAT_1:60; assume A2: f | Z is_differentiable_on Z ; ::_thesis: f is_differentiable_on Z then A3: for x being Real 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 f is_differentiable_on Z by A3, FDIFF_1:def_6; ::_thesis: verum end; theorem Th7: :: HFDIFF_1:7 for n being Element of NAT for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds f1 is_differentiable_on Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds f1 is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds f1 is_differentiable_on Z let f1 be PartFunc of REAL,REAL; ::_thesis: ( n >= 1 & f1 is_differentiable_on n,Z implies f1 is_differentiable_on Z ) assume that A1: n >= 1 and A2: f1 is_differentiable_on n,Z ; ::_thesis: f1 is_differentiable_on 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 f1 is_differentiable_on Z by Th6; ::_thesis: verum end; theorem Th8: :: HFDIFF_1:8 for n being Element of NAT holds #Z n is_differentiable_on REAL proof let n be Element of NAT ; ::_thesis: #Z n is_differentiable_on REAL A1: dom (#Z n) = REAL by FUNCT_2:def_1; for x being Real st x in REAL holds (#Z n) | REAL is_differentiable_in x proof let x be Real; ::_thesis: ( x in REAL implies (#Z n) | REAL is_differentiable_in x ) assume x in REAL ; ::_thesis: (#Z n) | REAL is_differentiable_in x #Z n is_differentiable_in x by TAYLOR_1:2; hence (#Z n) | REAL is_differentiable_in x by A1, RELAT_1:68; ::_thesis: verum end; hence #Z n is_differentiable_on REAL by A1, FDIFF_1:def_6; ::_thesis: verum end; theorem :: HFDIFF_1:9 for x being Real for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . 2) . x = - (sin . x) proof let x be Real; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . 2) . x = - (sin . x) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (sin,Z)) . 2) . x = - (sin . x) ) assume A1: x in Z ; ::_thesis: ((diff (sin,Z)) . 2) . x = - (sin . x) 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 ((diff (sin,Z)) . 2) . x = - (sin . x) ; ::_thesis: verum end; theorem :: HFDIFF_1:10 for x being Real for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . 3) . x = (- cos) . x proof let x be Real; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . 3) . x = (- cos) . x let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (sin,Z)) . 3) . x = (- cos) . x ) assume x in Z ; ::_thesis: ((diff (sin,Z)) . 3) . x = (- cos) . x 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 ((diff (sin,Z)) . 3) . x = (- cos) . x ; ::_thesis: verum end; theorem Th11: :: HFDIFF_1:11 for x being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) proof let x be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ) assume A1: x in Z ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) 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; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) 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__::_thesis:_((diff_(sin,Z))_._n)_._x_=_sin_._(x_+_((n_*_PI)_/_2)) percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider j being Element of NAT such that A8: i = 2 * j by ABIAN:def_2; percases ( j is even or j is odd ) ; suppose j is even ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider m being 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 ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; suppose j is odd ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider s being 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 ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; suppose i is odd ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider j being Element of NAT such that A11: i = (2 * j) + 1 by ABIAN:9; percases ( j is even or j is odd ) ; suppose j is even ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider m being 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 ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; suppose j is odd ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) then consider s being 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 ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; end; end; hence ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; supposeA14: n = 0 ; ::_thesis: ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) 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 ((diff (sin,Z)) . n) . x = sin . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; theorem :: HFDIFF_1:12 for x being Real for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . 2) . x = - (cos . x) proof let x be Real; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . 2) . x = - (cos . x) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (cos,Z)) . 2) . x = - (cos . x) ) assume A1: x in Z ; ::_thesis: ((diff (cos,Z)) . 2) . x = - (cos . x) 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 ((diff (cos,Z)) . 2) . x = - (cos . x) ; ::_thesis: verum end; theorem :: HFDIFF_1:13 for x being Real for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . 3) . x = sin . x proof let x be Real; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . 3) . x = sin . x let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (cos,Z)) . 3) . x = sin . x ) assume x in Z ; ::_thesis: ((diff (cos,Z)) . 3) . x = sin . x 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 ((diff (cos,Z)) . 3) . x = sin . x ; ::_thesis: verum end; theorem Th14: :: HFDIFF_1:14 for x being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) proof let x be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ) assume A1: x in Z ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) 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; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) 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__::_thesis:_((diff_(cos,Z))_._n)_._x_=_cos_._(x_+_((n_*_PI)_/_2)) percases ( i is even or i is odd ) ; suppose i is even ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider j being Element of NAT such that A8: i = 2 * j by ABIAN:def_2; percases ( j is even or j is odd ) ; suppose j is even ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider m being 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 ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; suppose j is odd ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider s being 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 ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; suppose i is odd ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider j being Element of NAT such that A11: i = (2 * j) + 1 by ABIAN:9; percases ( j is even or j is odd ) ; suppose j is even ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider m being 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 ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; suppose j is odd ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) then consider s being 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 ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; end; end; hence ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; supposeA14: n = 0 ; ::_thesis: ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) 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 ((diff (cos,Z)) . n) . x = cos . (x + ((n * PI) / 2)) ; ::_thesis: verum end; end; end; theorem Th15: :: HFDIFF_1:15 for n being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 + f2),Z)) . n = ((diff (f1,Z)) . n) + ((diff (f2,Z)) . n) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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) ) defpred S1[ 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 being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] assume A3: ( f1 is_differentiable_on k + 1,Z & f2 is_differentiable_on k + 1,Z ) ; ::_thesis: (diff ((f1 + f2),Z)) . (k + 1) = ((diff (f1,Z)) . (k + 1)) + ((diff (f2,Z)) . (k + 1)) 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 < 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, TAYLOR_1: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 (diff ((f1 + f2),Z)) . (k + 1) = ((diff (f1,Z)) . (k + 1)) + ((diff (f2,Z)) . (k + 1)) ; ::_thesis: verum end; A5: S1[ 0 ] proof assume that f1 is_differentiable_on 0 ,Z and f2 is_differentiable_on 0 ,Z ; ::_thesis: (diff ((f1 + f2),Z)) . 0 = ((diff (f1,Z)) . 0) + ((diff (f2,Z)) . 0) (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 (diff ((f1 + f2),Z)) . 0 = ((diff (f1,Z)) . 0) + ((diff (f2,Z)) . 0) ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A1); hence ( 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) ) ; ::_thesis: verum end; theorem Th16: :: HFDIFF_1:16 for n being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds (diff ((f1 - f2),Z)) . n = ((diff (f1,Z)) . n) - ((diff (f2,Z)) . n) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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) ) defpred S1[ Element of 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 being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] assume A3: ( f1 is_differentiable_on k + 1,Z & f2 is_differentiable_on k + 1,Z ) ; ::_thesis: (diff ((f1 - f2),Z)) . (k + 1) = ((diff (f1,Z)) . (k + 1)) - ((diff (f2,Z)) . (k + 1)) 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 < 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, TAYLOR_1: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 (diff ((f1 - f2),Z)) . (k + 1) = ((diff (f1,Z)) . (k + 1)) - ((diff (f2,Z)) . (k + 1)) ; ::_thesis: verum end; A5: S1[ 0 ] proof assume that f1 is_differentiable_on 0 ,Z and f2 is_differentiable_on 0 ,Z ; ::_thesis: (diff ((f1 - f2),Z)) . 0 = ((diff (f1,Z)) . 0) - ((diff (f2,Z)) . 0) (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 (diff ((f1 - f2),Z)) . 0 = ((diff (f1,Z)) . 0) - ((diff (f2,Z)) . 0) ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A1); hence ( 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) ) ; ::_thesis: verum end; theorem Th17: :: HFDIFF_1:17 for n, i being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) proof let n, i be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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) ) assume A1: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z ) ; ::_thesis: ( not i <= n or (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) ) assume i <= n ; ::_thesis: (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) then ( f1 is_differentiable_on i,Z & f2 is_differentiable_on i,Z ) by A1, TAYLOR_1:23; hence (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) by Th15; ::_thesis: verum end; theorem Th18: :: HFDIFF_1:18 for n, i being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) proof let n, i be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z & i <= n holds (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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) ) assume A1: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z ) ; ::_thesis: ( not i <= n or (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) ) assume i <= n ; ::_thesis: (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) then ( f1 is_differentiable_on i,Z & f2 is_differentiable_on i,Z ) by A1, TAYLOR_1:23; hence (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) by Th16; ::_thesis: verum end; theorem :: HFDIFF_1:19 for n being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 + f2 is_differentiable_on n,Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 + f2 is_differentiable_on n,Z let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 + f2 is_differentiable_on n,Z let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1 + f2 is_differentiable_on n,Z ) assume that A1: f1 is_differentiable_on n,Z and A2: f2 is_differentiable_on n,Z ; ::_thesis: f1 + f2 is_differentiable_on n,Z now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_n_-_1_holds_ (diff_((f1_+_f2),Z))_._i_is_differentiable_on_Z let i be Element of NAT ; ::_thesis: ( i <= n - 1 implies (diff ((f1 + f2),Z)) . i is_differentiable_on Z ) assume A3: i <= n - 1 ; ::_thesis: (diff ((f1 + f2),Z)) . i is_differentiable_on Z A4: (diff (f2,Z)) . i is_differentiable_on Z by A2, A3, TAYLOR_1:def_6; then A5: Z c= dom ((diff (f2,Z)) . i) by FDIFF_1:def_6; i <= n by A3, WSIERP_1:18; then A6: (diff ((f1 + f2),Z)) . i = ((diff (f1,Z)) . i) + ((diff (f2,Z)) . i) by A1, A2, Th17; A7: (diff (f1,Z)) . i is_differentiable_on Z by A1, A3, TAYLOR_1:def_6; 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 A5, 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 A7, A4, A6, FDIFF_1:18; ::_thesis: verum end; hence f1 + f2 is_differentiable_on n,Z by TAYLOR_1:def_6; ::_thesis: verum end; theorem :: HFDIFF_1:20 for n being Element of NAT for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 - f2 is_differentiable_on n,Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 - f2 is_differentiable_on n,Z let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z holds f1 - f2 is_differentiable_on n,Z let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( f1 is_differentiable_on n,Z & f2 is_differentiable_on n,Z implies f1 - f2 is_differentiable_on n,Z ) assume that A1: f1 is_differentiable_on n,Z and A2: f2 is_differentiable_on n,Z ; ::_thesis: f1 - f2 is_differentiable_on n,Z now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_n_-_1_holds_ (diff_((f1_-_f2),Z))_._i_is_differentiable_on_Z let i be Element of NAT ; ::_thesis: ( i <= n - 1 implies (diff ((f1 - f2),Z)) . i is_differentiable_on Z ) assume A3: i <= n - 1 ; ::_thesis: (diff ((f1 - f2),Z)) . i is_differentiable_on Z A4: (diff (f2,Z)) . i is_differentiable_on Z by A2, A3, TAYLOR_1:def_6; then A5: Z c= dom ((diff (f2,Z)) . i) by FDIFF_1:def_6; i <= n by A3, WSIERP_1:18; then A6: (diff ((f1 - f2),Z)) . i = ((diff (f1,Z)) . i) - ((diff (f2,Z)) . i) by A1, A2, Th18; A7: (diff (f1,Z)) . i is_differentiable_on Z by A1, A3, TAYLOR_1:def_6; 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 A5, 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 A7, A4, A6, FDIFF_1:19; ::_thesis: verum end; hence f1 - f2 is_differentiable_on n,Z by TAYLOR_1:def_6; ::_thesis: verum end; theorem Th21: :: HFDIFF_1:21 for r being Real for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) proof let r be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on n,Z implies (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) ) defpred S1[ Element of NAT ] means ( f is_differentiable_on $1,Z implies (diff ((r (#) f),Z)) . $1 = r (#) ((diff (f,Z)) . $1) ); A1: for k being Element of NAT st S1[k] holds S1[k + 1] proof let k be Element of NAT ; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] assume A3: f is_differentiable_on k + 1,Z ; ::_thesis: (diff ((r (#) f),Z)) . (k + 1) = r (#) ((diff (f,Z)) . (k + 1)) k <= (k + 1) - 1 ; then A4: (diff (f,Z)) . k is_differentiable_on Z by A3, TAYLOR_1:def_6; 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, TAYLOR_1: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 (diff ((r (#) f),Z)) . (k + 1) = r (#) ((diff (f,Z)) . (k + 1)) ; ::_thesis: verum end; A5: S1[ 0 ] proof assume f is_differentiable_on 0 ,Z ; ::_thesis: (diff ((r (#) f),Z)) . 0 = r (#) ((diff (f,Z)) . 0) (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 (diff ((r (#) f),Z)) . 0 = r (#) ((diff (f,Z)) . 0) ; ::_thesis: verum end; for k being Element of NAT holds S1[k] from NAT_1:sch_1(A5, A1); hence ( f is_differentiable_on n,Z implies (diff ((r (#) f),Z)) . n = r (#) ((diff (f,Z)) . n) ) ; ::_thesis: verum end; theorem Th22: :: HFDIFF_1:22 for r being Real for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds r (#) f is_differentiable_on n,Z proof let r be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds r (#) f is_differentiable_on n,Z let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds r (#) f is_differentiable_on n,Z let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds r (#) f is_differentiable_on n,Z let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on n,Z implies r (#) f is_differentiable_on n,Z ) assume A1: f is_differentiable_on n,Z ; ::_thesis: r (#) f is_differentiable_on n,Z now__::_thesis:_for_i_being_Element_of_NAT_st_i_<=_n_-_1_holds_ (diff_((r_(#)_f),Z))_._i_is_differentiable_on_Z let i be Element of NAT ; ::_thesis: ( i <= n - 1 implies (diff ((r (#) f),Z)) . i is_differentiable_on Z ) assume A2: i <= n - 1 ; ::_thesis: (diff ((r (#) f),Z)) . i is_differentiable_on Z (diff (f,Z)) . i is_differentiable_on Z by A1, A2, TAYLOR_1:def_6; then A3: 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, A3, Th21, TAYLOR_1:23; ::_thesis: verum end; hence r (#) f is_differentiable_on n,Z by TAYLOR_1:def_6; ::_thesis: verum end; theorem :: HFDIFF_1:23 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds (diff (f,Z)) . 1 = f `| Z proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds (diff (f,Z)) . 1 = f `| Z let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on Z implies (diff (f,Z)) . 1 = f `| Z ) assume A1: f is_differentiable_on Z ; ::_thesis: (diff (f,Z)) . 1 = f `| Z then A2: dom (f `| Z) = Z by FDIFF_1:def_7; A3: for x being Real st x in Z holds ((diff (f,Z)) . 1) . x = (f `| Z) . x proof let x be Real; ::_thesis: ( x in Z implies ((diff (f,Z)) . 1) . x = (f `| Z) . x ) assume x in Z ; ::_thesis: ((diff (f,Z)) . 1) . x = (f `| Z) . x ((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 ((diff (f,Z)) . 1) . x = (f `| Z) . x ; ::_thesis: verum 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 (diff (f,Z)) . 1 = f `| Z by A2, A3, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:24 for n being Element of NAT for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds (diff (f1,Z)) . 1 = f1 `| Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds (diff (f1,Z)) . 1 = f1 `| Z let Z be open Subset of REAL; ::_thesis: for f1 being PartFunc of REAL,REAL st n >= 1 & f1 is_differentiable_on n,Z holds (diff (f1,Z)) . 1 = f1 `| Z let f1 be PartFunc of REAL,REAL; ::_thesis: ( n >= 1 & f1 is_differentiable_on n,Z implies (diff (f1,Z)) . 1 = f1 `| Z ) assume ( n >= 1 & f1 is_differentiable_on n,Z ) ; ::_thesis: (diff (f1,Z)) . 1 = f1 `| 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 (diff (f1,Z)) . 1 = f1 `| Z ; ::_thesis: verum end; theorem :: HFDIFF_1:25 for x, r being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) proof let x, r be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) ) assume A1: x in Z ; ::_thesis: ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) A2: sin is_differentiable_on n,Z by TAYLOR_2:21; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) 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 ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) ; ::_thesis: verum end; supposeA5: n = 0 ; ::_thesis: ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) 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 ((diff ((r (#) sin),Z)) . n) . x = r * (sin . (x + ((n * PI) / 2))) ; ::_thesis: verum end; end; end; theorem :: HFDIFF_1:26 for x, r being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) proof let x, r be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) ) assume A1: x in Z ; ::_thesis: ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) A2: cos is_differentiable_on n,Z by TAYLOR_2:21; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) 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 ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) ; ::_thesis: verum end; supposeA5: n = 0 ; ::_thesis: ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) 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 ((diff ((r (#) cos),Z)) . n) . x = r * (cos . (x + ((n * PI) / 2))) ; ::_thesis: verum end; end; end; theorem :: HFDIFF_1:27 for x, r being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) proof let x, r be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) ) assume A1: x in Z ; ::_thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) A2: exp_R is_differentiable_on n,Z by TAYLOR_2:10; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) 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 ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) ; ::_thesis: verum end; supposeA5: n = 0 ; ::_thesis: ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) 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 ((diff ((r (#) exp_R),Z)) . n) . x = r * (exp_R . x) ; ::_thesis: verum end; end; end; theorem Th28: :: HFDIFF_1:28 for n being Element of NAT for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z let Z be open Subset of REAL; ::_thesis: (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z 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 being Real st x in Z holds ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x proof let x be Real; ::_thesis: ( x in Z implies ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x ) assume A5: x in Z ; ::_thesis: ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x ((#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 ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x ; ::_thesis: verum end; dom ((#Z n) `| Z) = Z by A3, FDIFF_1:def_7; hence (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z by A2, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th29: :: HFDIFF_1:29 for x being Real for n being Element of NAT st x <> 0 holds ( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) ) proof let x be Real; ::_thesis: for n being Element of NAT st x <> 0 holds ( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) ) let n be Element of NAT ; ::_thesis: ( x <> 0 implies ( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) ) ) A1: ( (#Z n) . x = x #Z n & x #Z n = x |^ n ) by PREPOWER:36, TAYLOR_1:def_1; assume x <> 0 ; ::_thesis: ( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) ) 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 ( (#Z n) ^ is_differentiable_in x & diff (((#Z n) ^),x) = - ((n * (x #Z (n - 1))) / ((x #Z n) ^2)) ) by A2, A3, FDIFF_2:15; ::_thesis: verum end; theorem Th30: :: HFDIFF_1:30 for n being Element of NAT for Z being open Subset of REAL st n >= 1 holds (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st n >= 1 holds (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z let Z be open Subset of REAL; ::_thesis: ( n >= 1 implies (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z ) assume n >= 1 ; ::_thesis: (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z 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 (diff ((#Z n),Z)) . 2 = ((n * (n - 1)) (#) (#Z (n - 2))) | Z ; ::_thesis: verum end; theorem :: HFDIFF_1:31 for n being Element of NAT for Z being open Subset of REAL st n >= 2 holds (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st n >= 2 holds (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z let Z be open Subset of REAL; ::_thesis: ( n >= 2 implies (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z ) assume A1: 2 <= n ; ::_thesis: (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z 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 (diff ((#Z n),Z)) . 3 = (((n * (n - 1)) * (n - 2)) (#) (#Z (n - 3))) | Z ; ::_thesis: verum end; Lm1: for n, m being Element of NAT st n > 1 holds ((m !) / (n !)) * n = (m !) / ((n -' 1) !) proof let n, m be Element of NAT ; ::_thesis: ( n > 1 implies ((m !) / (n !)) * n = (m !) / ((n -' 1) !) ) assume A1: n > 1 ; ::_thesis: ((m !) / (n !)) * n = (m !) / ((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 ((m !) / (n !)) * n = (m !) / ((n -' 1) !) ; ::_thesis: verum end; theorem Th32: :: HFDIFF_1:32 for n, m being Element of NAT for Z being open Subset of REAL st n > m holds (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z proof let n, m be Element of NAT ; ::_thesis: for Z being open Subset of REAL st n > m holds (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z let Z be open Subset of REAL; ::_thesis: ( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z ) defpred S1[ Nat] means ( n > $1 implies (diff ((#Z n),Z)) . $1 = (((n choose $1) * ($1 !)) (#) (#Z (n - $1))) | Z ); A1: for k being Nat st S1[k] holds S1[k + 1] proof let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] ) assume A2: S1[k] ; ::_thesis: S1[k + 1] A3: k ! > 0 by NEWTON:17; assume A4: n > k + 1 ; ::_thesis: (diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z 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 (diff ((#Z n),Z)) . (k + 1) = (((n choose (k + 1)) * ((k + 1) !)) (#) (#Z (n - (k + 1)))) | Z ; ::_thesis: verum end; A10: S1[ 0 ] proof assume n > 0 ; ::_thesis: (diff ((#Z n),Z)) . 0 = (((n choose 0) * (0 !)) (#) (#Z (n - 0))) | Z (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, NEWTON:19 ; hence (diff ((#Z n),Z)) . 0 = (((n choose 0) * (0 !)) (#) (#Z (n - 0))) | Z ; ::_thesis: verum end; for k being Nat holds S1[k] from NAT_1:sch_2(A10, A1); hence ( n > m implies (diff ((#Z n),Z)) . m = (((n choose m) * (m !)) (#) (#Z (n - m))) | Z ) ; ::_thesis: verum end; theorem :: HFDIFF_1:33 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on n,Z holds ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on n,Z implies ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) ) A1: - f = (- 1) (#) f ; assume A2: f is_differentiable_on n,Z ; ::_thesis: ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) then (diff ((- f),Z)) . n = (- 1) (#) ((diff (f,Z)) . n) by Th21 .= - ((diff (f,Z)) . n) ; hence ( (diff ((- f),Z)) . n = - ((diff (f,Z)) . n) & - f is_differentiable_on n,Z ) by A2, A1, Th22; ::_thesis: verum end; theorem :: HFDIFF_1:34 for x0, x being Real for n being Element of NAT for Z being open Subset of REAL st x0 in Z holds ( (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 let x0, x be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x0 in Z holds ( (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 !) ) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x0 in Z holds ( (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 !) ) let Z be open Subset of REAL; ::_thesis: ( 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 !) ) ) assume A1: x0 in Z ; ::_thesis: ( (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 !) ) 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 ( (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 !) ) by A2; ::_thesis: verum end; theorem :: HFDIFF_1:35 for r, x being Real for n being Element of NAT st r > 0 holds ( (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 let r, x be Real; ::_thesis: for n being Element of NAT st r > 0 holds ( (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 !) ) let n be Element of NAT ; ::_thesis: ( 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 !) ) ) A1: abs (0 - 0) = 0 by ABSVALUE:2; assume r > 0 ; ::_thesis: ( (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 !) ) 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 ( (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 !) ) by A3; ::_thesis: verum end; theorem Th36: :: HFDIFF_1:36 for x being Real for n, m being Element of NAT for Z being open Subset of REAL st n > m & x in Z holds ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) proof let x be Real; ::_thesis: for n, m being Element of NAT for Z being open Subset of REAL st n > m & x in Z holds ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) let n, m be Element of NAT ; ::_thesis: for Z being open Subset of REAL st n > m & x in Z holds ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) let Z be open Subset of REAL; ::_thesis: ( n > m & x in Z implies ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) ) assume that A1: n > m and A2: x in Z ; ::_thesis: ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (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; 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 ((diff ((#Z n),Z)) . m) . x = ((n choose m) * (m !)) * (x #Z (n - m)) ; ::_thesis: verum end; theorem Th37: :: HFDIFF_1:37 for x being Real for m being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((#Z m),Z)) . m) . x = m ! proof let x be Real; ::_thesis: for m being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((#Z m),Z)) . m) . x = m ! let m be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff ((#Z m),Z)) . m) . x = m ! let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff ((#Z m),Z)) . m) . x = m ! ) assume A1: x in Z ; ::_thesis: ((diff ((#Z m),Z)) . m) . x = m ! percases ( m > 0 or m = 0 ) ; suppose m > 0 ; ::_thesis: ((diff ((#Z m),Z)) . m) . x = m ! 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: n ! <> 0 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, NEWTON: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 ((diff ((#Z m),Z)) . m) . x = m ! ; ::_thesis: verum end; supposeA7: m = 0 ; ::_thesis: ((diff ((#Z m),Z)) . m) . x = m ! 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 ((diff ((#Z m),Z)) . m) . x = m ! ; ::_thesis: verum end; end; end; theorem Th38: :: HFDIFF_1:38 for n being Element of NAT for Z being open Subset of REAL holds #Z n is_differentiable_on n,Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL holds #Z n is_differentiable_on n,Z let Z be open Subset of REAL; ::_thesis: #Z n is_differentiable_on n,Z let i be Element of NAT ; :: according to TAYLOR_1:def_6 ::_thesis: ( not i <= n - 1 or (diff ((#Z n),Z)) . i is_differentiable_on Z ) assume A1: i <= n - 1 ; ::_thesis: (diff ((#Z n),Z)) . i is_differentiable_on Z reconsider i = i as Element of NAT ; (- 1) + n < 0 + n by XREAL_1:6; then A2: i < n by A1, XXREAL_0:2; A3: for x being 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; ::_thesis: ( x in Z implies ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x ) assume x in Z ; ::_thesis: ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x 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 ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x by A5, FDIFF_1:15; ::_thesis: verum 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 (diff ((#Z n),Z)) . i is_differentiable_on Z by A3, FDIFF_1:def_6; ::_thesis: verum end; theorem :: HFDIFF_1:39 for x, a being Real for n, m being Element of NAT for Z being open Subset of REAL st x in Z & n > m holds ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) proof let x, a be Real; ::_thesis: for n, m being Element of NAT for Z being open Subset of REAL st x in Z & n > m holds ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) let n, m be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z & n > m holds ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) let Z be open Subset of REAL; ::_thesis: ( x in Z & n > m implies ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) ) assume that A1: x in Z and A2: n > m ; ::_thesis: ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (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 ((diff ((a (#) (#Z n)),Z)) . m) . x = ((a * (n choose m)) * (m !)) * (x #Z (n - m)) ; ::_thesis: verum end; theorem :: HFDIFF_1:40 for x, a being Real for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) proof let x, a be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st x in Z holds ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x in Z holds ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) let Z be open Subset of REAL; ::_thesis: ( x in Z implies ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) ) assume A1: x in Z ; ::_thesis: ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) 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 ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) ; ::_thesis: verum end; supposeA5: n = 0 ; ::_thesis: ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) 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 ((diff ((a (#) (#Z n)),Z)) . n) . x = a * (n !) ; ::_thesis: verum end; end; end; theorem Th41: :: HFDIFF_1:41 for x0, x being Real for n, m being Element of NAT for Z being open Subset of REAL st x0 in Z & n > m holds ( (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 let x0, x be Real; ::_thesis: for n, m being Element of NAT for Z being open Subset of REAL st x0 in Z & n > m holds ( (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 ) let n, m be Element of NAT ; ::_thesis: for Z being open Subset of REAL st x0 in Z & n > m holds ( (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 ) let Z be open Subset of REAL; ::_thesis: ( 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 ) ) assume that A1: x0 in Z and A2: n > m ; ::_thesis: ( (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 ) 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 ( (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 ) by A4; ::_thesis: verum end; theorem :: HFDIFF_1:42 for n, m being Element of NAT for r, x being 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 ; ::_thesis: for r, x being Real st n > m & r > 0 holds ( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n ) let r, x be Real; ::_thesis: ( n > m & r > 0 implies ( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n ) ) assume that A1: n > m and A2: r > 0 ; ::_thesis: ( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n ) 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 ( (Maclaurin ((#Z n),].(- r),r.[,x)) . m = 0 & (Maclaurin ((#Z n),].(- r),r.[,x)) . n = x |^ n ) by A5; ::_thesis: verum end; theorem Th43: :: HFDIFF_1:43 for n being Element of NAT for Z being open Subset of REAL st not 0 in Z holds (#Z n) ^ is_differentiable_on Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st not 0 in Z holds (#Z n) ^ is_differentiable_on Z let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies (#Z n) ^ is_differentiable_on Z ) assume A1: not 0 in Z ; ::_thesis: (#Z n) ^ is_differentiable_on Z A2: for x0 being Real st x0 in Z holds (#Z n) . x0 <> 0 proof let x0 be Real; ::_thesis: ( x0 in Z implies (#Z n) . x0 <> 0 ) A3: (#Z n) . x0 = x0 #Z n by TAYLOR_1:def_1; assume x0 in Z ; ::_thesis: (#Z n) . x0 <> 0 hence (#Z n) . x0 <> 0 by A1, A3, PREPOWER:38; ::_thesis: verum end; #Z n is_differentiable_on Z by Th8, FDIFF_1:26; hence (#Z n) ^ is_differentiable_on Z by A2, FDIFF_2:22; ::_thesis: verum end; theorem :: HFDIFF_1:44 for x0 being Real for n being Element of NAT for Z being open Subset of REAL st not 0 in Z & x0 in Z holds (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) proof let x0 be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st not 0 in Z & x0 in Z holds (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st not 0 in Z & x0 in Z holds (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & x0 in Z implies (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) ) assume that A1: not 0 in Z and A2: x0 in Z ; ::_thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) A3: (#Z n) ^ is_differentiable_on Z by A1, Th43; percases ( n > 0 or n = 0 ) ; suppose n > 0 ; ::_thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) 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 (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) ; ::_thesis: verum end; supposeA5: n = 0 ; ::_thesis: (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) (((#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 (((#Z n) ^) `| Z) . x0 = - (n / ((#Z (n + 1)) . x0)) ; ::_thesis: verum end; 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 ; ::_thesis: (#Z 1) . x = (id REAL) . x (#Z 1) . x = x #Z 1 by TAYLOR_1:def_1 .= x by PREPOWER:35 .= (id REAL) . x by FUNCT_1:18 ; hence (#Z 1) . x = (id REAL) . x ; ::_thesis: verum end; hence #Z 1 = id REAL by FUNCT_2:63; ::_thesis: verum end; theorem Th45: :: HFDIFF_1:45 for x being Real st x <> 0 holds ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) ) proof let x be Real; ::_thesis: ( x <> 0 implies ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) ) ) set f = id REAL; assume A1: x <> 0 ; ::_thesis: ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) ) ( (id REAL) . x = x #Z 1 & x #Z 1 = x |^ 1 ) by Lm2, PREPOWER:36, TAYLOR_1:def_1; then A2: (id REAL) . x <> 0 by A1, PREPOWER:5; A3: id REAL is_differentiable_in x by Lm2, TAYLOR_1:2; then diff (((id REAL) ^),x) = - ((diff ((id REAL),x)) / (((id REAL) . x) ^2)) by A2, FDIFF_2:15 .= - ((1 * (x #Z (1 - 1))) / (((id REAL) . x) ^2)) by Lm2, TAYLOR_1:2 .= - ((1 * (x #Z 0)) / (x ^2)) by FUNCT_1:18 .= - (1 / (x ^2)) by PREPOWER:34 ; hence ( (id REAL) ^ is_differentiable_in x & diff (((id REAL) ^),x) = - (1 / (x ^2)) ) by A2, A3, FDIFF_2:15; ::_thesis: verum end; theorem :: HFDIFF_1:46 for Z being open Subset of REAL st not 0 in Z holds ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z ) assume A1: not 0 in Z ; ::_thesis: ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | 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 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 Real; ::_thesis: ( x0 in Z implies (((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0 ) assume A7: x0 in Z ; ::_thesis: (((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0 (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 (((id REAL) ^) `| Z) . x0 = (((- 1) (#) ((#Z 2) ^)) | Z) . x0 ; ::_thesis: verum 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 ((id REAL) ^) `| Z = ((- 1) (#) ((#Z 2) ^)) | Z by A2, A5, PARTFUN1:5; ::_thesis: verum end; theorem Th47: :: HFDIFF_1:47 for x being Real st x <> 0 holds ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) proof let x be Real; ::_thesis: ( x <> 0 implies ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) ) A1: ( (#Z 2) . x = x #Z 2 & x #Z 2 = x |^ 2 ) by PREPOWER:36, TAYLOR_1:def_1; assume x <> 0 ; ::_thesis: ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) 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 ( (#Z 2) ^ is_differentiable_in x & diff (((#Z 2) ^),x) = - ((2 * x) / ((x #Z 2) ^2)) ) by A2, A3, FDIFF_2:15; ::_thesis: verum end; theorem :: HFDIFF_1:48 for Z being open Subset of REAL st not 0 in Z holds ((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | Z proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | Z ) assume A1: not 0 in Z ; ::_thesis: ((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | 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 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 Real; ::_thesis: ( x0 in Z implies (((#Z 2) ^) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^)) | Z) . x0 ) A5: dom ((- 2) (#) ((#Z 3) ^)) = dom ((#Z 3) ^) by VALUED_1:def_5; assume A6: x0 in Z ; ::_thesis: (((#Z 2) ^) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^)) | Z) . x0 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 (((#Z 2) ^) `| Z) . x0 = (((- 2) (#) ((#Z 3) ^)) | Z) . x0 ; ::_thesis: verum 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 ((#Z 2) ^) `| Z = ((- 2) (#) ((#Z 3) ^)) | Z by A2, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th49: :: HFDIFF_1:49 for n being Element of NAT for Z being open Subset of REAL st not 0 in Z & n >= 1 holds ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st not 0 in Z & n >= 1 holds ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & n >= 1 implies ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z ) assume that A1: not 0 in Z and A2: n >= 1 ; ::_thesis: ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z ( 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 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 Real; ::_thesis: ( x0 in Z implies (((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0 ) A6: dom ((- n) (#) ((#Z (n + 1)) ^)) = dom ((#Z (n + 1)) ^) by VALUED_1:def_5; assume A7: x0 in Z ; ::_thesis: (((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0 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 (((#Z n) ^) `| Z) . x0 = (((- n) (#) ((#Z (n + 1)) ^)) | Z) . x0 ; ::_thesis: verum 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 ((#Z n) ^) `| Z = ((- n) (#) ((#Z (n + 1)) ^)) | Z by A9, A4, PARTFUN1:5; ::_thesis: verum end; theorem Th50: :: HFDIFF_1:50 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2)) proof let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 2,Z & f2 is_differentiable_on 2,Z holds (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2)) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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)) ) assume that A1: f1 is_differentiable_on 2,Z and A2: f2 is_differentiable_on 2,Z ; ::_thesis: (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2)) 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 (diff ((f1 (#) f2),Z)) . 2 = ((((diff (f1,Z)) . 2) (#) f2) + (2 (#) ((f1 `| Z) (#) (f2 `| Z)))) + (f1 (#) ((diff (f2,Z)) . 2)) ; ::_thesis: verum end; theorem :: HFDIFF_1:51 for Z being open Subset of REAL st Z c= dom ln & Z c= dom ((id REAL) ^) holds ln `| Z = ((id REAL) ^) | Z proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ln & Z c= dom ((id REAL) ^) implies ln `| Z = ((id REAL) ^) | Z ) assume that A1: Z c= dom ln and A2: Z c= dom ((id REAL) ^) ; ::_thesis: ln `| Z = ((id REAL) ^) | Z A3: dom (((id REAL) ^) | Z) = (dom ((id REAL) ^)) /\ Z by RELAT_1:61 .= Z by A2, XBOOLE_1:28 ; A4: for x0 being Real st x0 in dom (((id REAL) ^) | Z) holds (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 proof let x0 be Real; ::_thesis: ( x0 in dom (((id REAL) ^) | Z) implies (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 ) assume A5: x0 in dom (((id REAL) ^) | Z) ; ::_thesis: (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 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 (ln `| Z) . x0 = (((id REAL) ^) | Z) . x0 ; ::_thesis: verum 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 ln `| Z = ((id REAL) ^) | Z by A4, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:52 for x0 being Real for n being Element of NAT for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) proof let x0 be Real; ::_thesis: for n being Element of NAT for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st n >= 1 & x0 in Z & not 0 in Z holds ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) let Z be open Subset of REAL; ::_thesis: ( n >= 1 & x0 in Z & not 0 in Z implies ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) ) assume that A1: n >= 1 and A2: x0 in Z and A3: not 0 in Z ; ::_thesis: ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) 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 ((diff (((#Z n) ^),Z)) . 2) . x0 = (n * (n + 1)) * (((#Z (n + 2)) ^) . x0) ; ::_thesis: verum end; theorem :: HFDIFF_1:53 for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 2 = (2 (#) ((cos ^2) | Z)) + ((- 2) (#) ((sin ^2) | Z)) proof let Z be open Subset of REAL; ::_thesis: (diff ((sin ^2),Z)) . 2 = (2 (#) ((cos ^2) | Z)) + ((- 2) (#) ((sin ^2) | Z)) 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 (diff ((sin ^2),Z)) . 2 = (2 (#) ((cos ^2) | Z)) + ((- 2) (#) ((sin ^2) | Z)) ; ::_thesis: verum end; theorem :: HFDIFF_1:54 for Z being open Subset of REAL holds (diff ((cos ^2),Z)) . 2 = (2 (#) ((sin ^2) | Z)) + ((- 2) (#) ((cos ^2) | Z)) proof let Z be open Subset of REAL; ::_thesis: (diff ((cos ^2),Z)) . 2 = (2 (#) ((sin ^2) | Z)) + ((- 2) (#) ((cos ^2) | Z)) 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 (diff ((cos ^2),Z)) . 2 = (2 (#) ((sin ^2) | Z)) + ((- 2) (#) ((cos ^2) | Z)) ; ::_thesis: verum end; theorem :: HFDIFF_1:55 for Z being open Subset of REAL holds (diff ((sin (#) cos),Z)) . 2 = 4 (#) (((- sin) (#) cos) | Z) proof let Z be open Subset of REAL; ::_thesis: (diff ((sin (#) cos),Z)) . 2 = 4 (#) (((- sin) (#) cos) | Z) ( 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 (diff ((sin (#) cos),Z)) . 2 = 4 (#) (((- sin) (#) cos) | Z) ; ::_thesis: verum end; theorem Th56: :: HFDIFF_1:56 for Z being open Subset of REAL st Z c= dom tan holds ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom tan implies ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) ) set f1 = cos ^ ; assume A1: Z c= dom tan ; ::_thesis: ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) A2: (dom sin) /\ (dom (cos ^)) c= dom (cos ^) by XBOOLE_1:17; A3: dom tan = dom (sin (#) (cos ^)) by RFUNCT_1:31, SIN_COS:def_26 .= (dom sin) /\ (dom (cos ^)) by VALUED_1:def_4 ; then A4: Z c= dom (cos ^) 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, XBOOLE_1:28 ; A7: for x being Real st x in Z holds tan is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies tan is_differentiable_in x ) assume x in Z ; ::_thesis: tan is_differentiable_in x then A8: cos . x <> 0 by A1, FDIFF_8:1; ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; hence tan is_differentiable_in x by A8, FDIFF_2:14, SIN_COS:def_26; ::_thesis: verum end; then A9: tan is_differentiable_on Z by A1, FDIFF_1:9; A10: for x being Real st x in dom (tan `| Z) holds (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x proof let x be Real; ::_thesis: ( x in dom (tan `| Z) implies (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x ) assume x in dom (tan `| Z) ; ::_thesis: (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x 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) * ((cos ^) . x) by A4, A11, RFUNCT_1:def_2 .= ((cos ^) (#) (cos ^)) . x by A4, A5, A11, VALUED_1:def_4 .= (((cos ^) (#) (cos ^)) | Z) . x by A11, FUNCT_1:49 ; hence (tan `| Z) . x = (((cos ^) (#) (cos ^)) | Z) . x ; ::_thesis: verum end; dom (tan `| Z) = Z by A9, FDIFF_1:def_7; hence ( tan is_differentiable_on Z & tan `| Z = ((cos ^) ^2) | Z ) by A1, A7, A6, A10, FDIFF_1:9, PARTFUN1:5; ::_thesis: verum end; theorem Th57: :: HFDIFF_1:57 for Z being open Subset of REAL st Z c= dom tan holds ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom tan implies ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z ) ) A1: (dom sin) /\ (dom (cos ^)) c= dom (cos ^) by XBOOLE_1:17; assume A2: Z c= dom tan ; ::_thesis: ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z ) then A3: for x being Real 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 being Real st x in Z holds ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x proof let x be Real; ::_thesis: ( x in Z implies ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . 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 ; ::_thesis: ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x 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 ((cos ^) `| Z) . x = (((cos ^) (#) tan) | Z) . x ; ::_thesis: verum 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, XBOOLE_1:28 ; hence ( cos ^ is_differentiable_on Z & (cos ^) `| Z = ((cos ^) (#) tan) | Z ) by A3, A4, A6, FDIFF_4:39, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:58 for Z being open Subset of REAL st Z c= dom tan holds (diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom tan implies (diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) ) assume A1: Z c= dom tan ; ::_thesis: (diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) 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 (diff (tan,Z)) . 2 = 2 (#) (((tan (#) (cos ^)) (#) (cos ^)) | Z) ; ::_thesis: verum end; theorem Th59: :: HFDIFF_1:59 for Z being open Subset of REAL st Z c= dom cot holds ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom cot implies ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z ) ) A1: (dom cos) /\ (dom (sin ^)) c= dom (sin ^) by XBOOLE_1:17; assume A2: Z c= dom cot ; ::_thesis: ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z ) A3: for x being Real st x in Z holds cot is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cot is_differentiable_in x ) assume x in Z ; ::_thesis: cot is_differentiable_in x then A4: sin . x <> 0 by A2, FDIFF_8:2; ( sin is_differentiable_in x & cos is_differentiable_in x ) by SIN_COS:63, SIN_COS:64; hence cot is_differentiable_in x by A4, FDIFF_2:14, SIN_COS:def_27; ::_thesis: verum 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 being Real st x in dom (cot `| Z) holds (cot `| Z) . x = (((- 1) (#) ((sin ^) (#) (sin ^))) | Z) . x proof let x be Real; ::_thesis: ( x in dom (cot `| Z) implies (cot `| Z) . x = (((- 1) (#) ((sin ^) (#) (sin ^))) | Z) . x ) assume x in dom (cot `| Z) ; ::_thesis: (cot `| Z) . x = (((- 1) (#) ((sin ^) (#) (sin ^))) | Z) . x 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 (cot `| Z) . x = (((- 1) (#) ((sin ^) (#) (sin ^))) | Z) . x ; ::_thesis: verum 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, XBOOLE_1:28 ; dom (cot `| Z) = Z by A5, FDIFF_1:def_7; hence ( cot is_differentiable_on Z & cot `| Z = ((- 1) (#) ((sin ^) ^2)) | Z ) by A2, A3, A13, A8, FDIFF_1:9, PARTFUN1:5; ::_thesis: verum end; theorem Th60: :: HFDIFF_1:60 for Z being open Subset of REAL st Z c= dom cot holds ( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom cot implies ( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z ) ) 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 ; ::_thesis: ( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z ) (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 being Real 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 Real st x in dom ((sin ^) `| Z) holds ((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . x proof let x be Real; ::_thesis: ( x in dom ((sin ^) `| Z) implies ((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . 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) ; ::_thesis: ((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . x 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 ((sin ^) `| Z) . x = ((- ((sin ^) (#) cot)) | Z) . x ; ::_thesis: verum 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, XBOOLE_1:28 ; dom ((sin ^) `| Z) = Z by A5, FDIFF_1:def_7; hence ( sin ^ is_differentiable_on Z & (sin ^) `| Z = (- ((sin ^) (#) cot)) | Z ) by A4, A11, A6, FDIFF_4:40, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:61 for Z being open Subset of REAL st Z c= dom cot holds (diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom cot implies (diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z) ) assume A1: Z c= dom cot ; ::_thesis: (diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z) 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 (diff (cot,Z)) . 2 = 2 (#) (((cot (#) (sin ^)) (#) (sin ^)) | Z) ; ::_thesis: verum end; theorem :: HFDIFF_1:62 for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z) proof let Z be open Subset of REAL; ::_thesis: (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z) A1: ( sin is_differentiable_on 2,Z & exp_R is_differentiable_on 2,Z ) by TAYLOR_2:10, TAYLOR_2: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, SIN_COS: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, SIN_COS: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 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 Real; ::_thesis: ( x in dom ((diff ((exp_R (#) sin),Z)) . 2) implies ((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x ) assume A11: x in dom ((diff ((exp_R (#) sin),Z)) . 2) ; ::_thesis: ((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x ((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 ((diff ((exp_R (#) sin),Z)) . 2) . x = (2 (#) ((exp_R (#) cos) | Z)) . x ; ::_thesis: verum end; hence (diff ((exp_R (#) sin),Z)) . 2 = 2 (#) ((exp_R (#) cos) | Z) by A2, A8, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:63 for Z being open Subset of REAL holds (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z) proof let Z be open Subset of REAL; ::_thesis: (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z) A1: ( cos is_differentiable_on 2,Z & exp_R is_differentiable_on 2,Z ) by TAYLOR_2:10, TAYLOR_2: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, SIN_COS: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, SIN_COS: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 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 Real; ::_thesis: ( x in dom ((diff ((exp_R (#) cos),Z)) . 2) implies ((diff ((exp_R (#) cos),Z)) . 2) . x = (2 (#) ((exp_R (#) (- sin)) | Z)) . x ) assume A11: x in dom ((diff ((exp_R (#) cos),Z)) . 2) ; ::_thesis: ((diff ((exp_R (#) cos),Z)) . 2) . x = (2 (#) ((exp_R (#) (- sin)) | Z)) . x ((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 ((diff ((exp_R (#) cos),Z)) . 2) . x = (2 (#) ((exp_R (#) (- sin)) | Z)) . x ; ::_thesis: verum end; hence (diff ((exp_R (#) cos),Z)) . 2 = 2 (#) ((exp_R (#) (- sin)) | Z) by A2, A8, PARTFUN1:5; ::_thesis: verum end; Lm3: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds (f `| Z) `| Z = (diff (f,Z)) . 2 proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds (f `| Z) `| Z = (diff (f,Z)) . 2 let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on Z implies (f `| Z) `| Z = (diff (f,Z)) . 2 ) assume f is_differentiable_on Z ; ::_thesis: (f `| Z) `| Z = (diff (f,Z)) . 2 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 (f `| Z) `| Z = (diff (f,Z)) . 2 ; ::_thesis: verum end; theorem Th64: :: HFDIFF_1:64 for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z holds (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 let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st f1 is_differentiable_on 3,Z & f2 is_differentiable_on 3,Z holds (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)) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( 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)) ) assume that A1: f1 is_differentiable_on 3,Z and A2: f2 is_differentiable_on 3,Z ; ::_thesis: (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)) 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 (#) (((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:12 .= ((((diff (f1,Z)) . 3) (#) f2) + (((1 + 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 Th5 .= (((diff (f1,Z)) . 3) (#) f2) + (((3 (#) (((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) + ((3 (#) (((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) + ((3 (#) (((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) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (((2 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (1 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))) + (f1 (#) ((diff (f2,Z)) . 3)))) by RFUNCT_1:21 .= (((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (((2 + 1) (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))) + (f1 (#) ((diff (f2,Z)) . 3)))) by Th5 .= (((diff (f1,Z)) . 3) (#) f2) + (((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2)))) + (f1 (#) ((diff (f2,Z)) . 3))) by RFUNCT_1:8 .= ((((diff (f1,Z)) . 3) (#) f2) + ((3 (#) (((diff (f1,Z)) . 2) (#) (f2 `| Z))) + (3 (#) ((f1 `| Z) (#) ((diff (f2,Z)) . 2))))) + (f1 (#) ((diff (f2,Z)) . 3)) by RFUNCT_1:8 ; hence (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)) ; ::_thesis: verum end; theorem :: HFDIFF_1:65 for Z being open Subset of REAL holds (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z) proof let Z be open Subset of REAL; ::_thesis: (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z) 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 (diff ((sin ^2),Z)) . 3 = (- 8) (#) ((cos (#) sin) | Z) ; ::_thesis: verum end; theorem :: HFDIFF_1:66 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z holds (diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2)) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z holds (diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2)) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on 2,Z implies (diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2)) ) assume f is_differentiable_on 2,Z ; ::_thesis: (diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2)) 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 (diff ((f ^2),Z)) . 2 = (2 (#) (f (#) ((diff (f,Z)) . 2))) + (2 (#) ((f `| Z) ^2)) ; ::_thesis: verum end; Lm4: for f being PartFunc of REAL,REAL holds f / f = ((dom f) \ (f " {0})) --> 1 proof let f be PartFunc of REAL,REAL; ::_thesis: f / f = ((dom f) \ (f " {0})) --> 1 A1: dom (f / f) = (dom f) /\ ((dom f) \ (f " {0})) by RFUNCT_1:def_1 .= (dom f) \ (f " {0}) by XBOOLE_1:28, XBOOLE_1:36 ; for c being set st c in dom (f / f) holds (f / f) . c = 1 proof let c be set ; ::_thesis: ( c in dom (f / f) implies (f / f) . c = 1 ) assume A2: c in dom (f / f) ; ::_thesis: (f / f) . c = 1 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 (f / f) . c = 1 by A3, XCMPLX_0:def_7; ::_thesis: verum end; hence f / f = ((dom f) \ (f " {0})) --> 1 by A1, FUNCOP_1:11; ::_thesis: verum end; Lm5: for f being PartFunc of REAL,REAL holds (f (#) (f (#) f)) " {0} = f " {0} proof let f be PartFunc of REAL,REAL; ::_thesis: (f (#) (f (#) f)) " {0} = f " {0} thus (f (#) (f (#) f)) " {0} c= f " {0} :: according to XBOOLE_0:def_10 ::_thesis: f " {0} c= (f (#) (f (#) f)) " {0} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (f (#) (f (#) f)) " {0} or x in f " {0} ) assume A1: x in (f (#) (f (#) f)) " {0} ; ::_thesis: x in 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 x in f " {0} by A2, FUNCT_1:def_7; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in f " {0} or x in (f (#) (f (#) f)) " {0} ) assume A3: x in f " {0} ; ::_thesis: x in (f (#) (f (#) 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 x in (f (#) (f (#) f)) " {0} by A5, FUNCT_1:def_7; ::_thesis: verum end; theorem :: HFDIFF_1:67 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds f . x0 <> 0 ) holds (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st f is_differentiable_on 2,Z & ( for x0 being Real st x0 in Z holds f . x0 <> 0 ) holds (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) let f be PartFunc of REAL,REAL; ::_thesis: ( f is_differentiable_on 2,Z & ( for x0 being Real 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)) ) assume that A1: f is_differentiable_on 2,Z and A2: for x0 being Real st x0 in Z holds f . x0 <> 0 ; ::_thesis: (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) 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 being Real st x0 in Z holds (f (#) f) . x0 <> 0 proof let x0 be Real; ::_thesis: ( x0 in Z implies (f (#) f) . x0 <> 0 ) assume A7: x0 in Z ; ::_thesis: (f (#) f) . x0 <> 0 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 (f (#) f) . x0 <> 0 by A8, XCMPLX_1:6; ::_thesis: verum 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 ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = (dom (f / f)) /\ (dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) by VALUED_1:def_4; then A22: dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) c= dom (f / f) by XBOOLE_1:17; A23: for x being Element of REAL st x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) holds ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x proof let x be Element of REAL ; ::_thesis: ( x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) implies ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ) assume A24: x in dom ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) ; ::_thesis: ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x .= ((f / f) . x) * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x) by A24, VALUED_1:def_4 .= 1 * (((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x) by A19, A20, A22, A24, FUNCOP_1:7 .= ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ; hence ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) . x = ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) . x ; ::_thesis: verum 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 ((f / f) (#) ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)))) = dom ((((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f))) by A5, A20, A21, XBOOLE_1:28, XBOOLE_1:33; hence (diff ((f ^),Z)) . 2 = (((2 (#) (f `| Z)) (#) (f `| Z)) - (((diff (f,Z)) . 2) (#) f)) / (f (#) (f (#) f)) by A19, A14, A23, PARTFUN1:5; ::_thesis: verum end; theorem :: HFDIFF_1:68 for Z being open Subset of REAL holds (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z proof let Z be open Subset of REAL; ::_thesis: (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z ( sin is_differentiable_on 3,Z & exp_R is_differentiable_on 3,Z ) by TAYLOR_2:10, TAYLOR_2: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 (diff ((exp_R (#) sin),Z)) . 3 = (2 (#) (exp_R (#) ((- sin) + cos))) | Z ; ::_thesis: verum end;