:: FDIFF_4 semantic presentation begin theorem Th1: :: FDIFF_4:1 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) implies ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) ) assume that A1: Z c= dom (ln * f) and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ; ::_thesis: ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; A4: for x being Real st x in Z holds f . x = (1 * x) + a by A2; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds ln * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * f is_differentiable_in x ) assume x in Z ; ::_thesis: ln * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A5, FDIFF_1:9; hence ln * f is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A7: ln * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) proof let x be Real; ::_thesis: ( x in Z implies ((ln * f) `| Z) . x = 1 / (a + x) ) assume A8: x in Z ; ::_thesis: ((ln * f) `| Z) . x = 1 / (a + x) then A9: f . x = a + x by A2; ( f is_differentiable_in x & f . x > 0 ) by A2, A5, A8, FDIFF_1:9; then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20 .= ((f `| Z) . x) / (f . x) by A5, A8, FDIFF_1:def_7 .= 1 / (a + x) by A3, A4, A8, A9, FDIFF_1:23 ; hence ((ln * f) `| Z) . x = 1 / (a + x) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (a + x) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem Th2: :: FDIFF_4:2 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ) holds ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * f) & ( for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ) implies ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) ) assume that A1: Z c= dom (ln * f) and A2: for x being Real st x in Z holds ( f . x = x - a & f . x > 0 ) ; ::_thesis: ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) A3: for x being Real st x in Z holds f . x = (1 * x) + (- a) proof let x be Real; ::_thesis: ( x in Z implies f . x = (1 * x) + (- a) ) A4: (1 * x) + (- a) = (1 * x) - a ; assume x in Z ; ::_thesis: f . x = (1 * x) + (- a) hence f . x = (1 * x) + (- a) by A2, A4; ::_thesis: verum end; for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A5: Z c= dom f by TARSKI:def_3; then A6: f is_differentiable_on Z by A3, FDIFF_1:23; A7: for x being Real st x in Z holds ln * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * f is_differentiable_in x ) assume x in Z ; ::_thesis: ln * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence ln * f is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A8: ln * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) proof let x be Real; ::_thesis: ( x in Z implies ((ln * f) `| Z) . x = 1 / (x - a) ) assume A9: x in Z ; ::_thesis: ((ln * f) `| Z) . x = 1 / (x - a) then A10: f . x = x - a by A2; ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A9, FDIFF_1:9; then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20 .= ((f `| Z) . x) / (f . x) by A6, A9, FDIFF_1:def_7 .= 1 / (x - a) by A5, A3, A9, A10, FDIFF_1:23 ; hence ((ln * f) `| Z) . x = 1 / (x - a) by A8, A9, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * f is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * f) `| Z) . x = 1 / (x - a) ) ) by A1, A7, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:3 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (- (ln * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) implies ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) ) assume that A1: Z c= dom (- (ln * f)) and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ; ::_thesis: ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) now__::_thesis:_for_y_being_set_st_y_in_Z_holds_ y_in_dom_(ln_*_f) let y be set ; ::_thesis: ( y in Z implies y in dom (ln * f) ) assume y in Z ; ::_thesis: y in dom (ln * f) then y in dom ((- 1) (#) (ln * f)) by A1; hence y in dom (ln * f) by VALUED_1:def_5; ::_thesis: verum end; then A3: Z c= dom (ln * f) by TARSKI:def_3; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = ((- 1) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f . x = ((- 1) * x) + a ) assume x in Z ; ::_thesis: f . x = ((- 1) * x) + a then f . x = a - x by A2; hence f . x = ((- 1) * x) + a ; ::_thesis: verum end; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ln_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies ln * f is_differentiable_in x ) assume x in Z ; ::_thesis: ln * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence ln * f is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A7: ln * f is_differentiable_on Z by A3, FDIFF_1:9; A8: for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) proof let x be Real; ::_thesis: ( x in Z implies ((- (ln * f)) `| Z) . x = 1 / (a - x) ) assume A9: x in Z ; ::_thesis: ((- (ln * f)) `| Z) . x = 1 / (a - x) then A10: f . x = a - x by A2; ( f . x > 0 & f is_differentiable_in x ) by A2, A6, A9, FDIFF_1:9; then diff ((ln * f),x) = (diff (f,x)) / (f . x) by TAYLOR_1:20 .= ((f `| Z) . x) / (f . x) by A6, A9, FDIFF_1:def_7 .= (- 1) / (a - x) by A4, A5, A9, A10, FDIFF_1:23 ; then (((- 1) (#) (ln * f)) `| Z) . x = (- 1) * ((- 1) / (a - x)) by A1, A7, A9, FDIFF_1:20 .= ((- 1) * (- 1)) / (a - x) by XCMPLX_1:74 .= 1 / (a - x) ; hence ((- (ln * f)) `| Z) . x = 1 / (a - x) ; ::_thesis: verum end; Z c= dom ((- 1) (#) (ln * f)) by A1; hence ( - (ln * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * f)) `| Z) . x = 1 / (a - x) ) ) by A7, A8, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:4 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) - (a (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) implies ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) ) assume that A1: Z c= dom ((id Z) - (a (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ; ::_thesis: ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) A4: Z c= (dom (id Z)) /\ (dom (a (#) f)) by A1, VALUED_1:12; then A5: Z c= dom (a (#) f) by XBOOLE_1:18; then A6: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A7: f is_differentiable_on Z by A2, A3, Th1; then A8: a (#) f is_differentiable_on Z by A5, FDIFF_1:20; A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A4, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds ((a (#) f) `| Z) . x = a / (a + x) proof let x be Real; ::_thesis: ( x in Z implies ((a (#) f) `| Z) . x = a / (a + x) ) assume A13: x in Z ; ::_thesis: ((a (#) f) `| Z) . x = a / (a + x) hence ((a (#) f) `| Z) . x = a * (diff (f,x)) by A5, A7, FDIFF_1:20 .= a * ((f `| Z) . x) by A7, A13, FDIFF_1:def_7 .= a * (1 / (a + x)) by A2, A3, A6, A13, Th1 .= a / (a + x) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) assume A14: x in Z ; ::_thesis: (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) then A15: ( f1 . x = a + x & f1 . x > 0 ) by A3; (((id Z) - (a (#) f)) `| Z) . x = (diff ((id Z),x)) - (diff ((a (#) f),x)) by A1, A11, A8, A14, FDIFF_1:19 .= (((id Z) `| Z) . x) - (diff ((a (#) f),x)) by A11, A14, FDIFF_1:def_7 .= (((id Z) `| Z) . x) - (((a (#) f) `| Z) . x) by A8, A14, FDIFF_1:def_7 .= 1 - (((a (#) f) `| Z) . x) by A10, A9, A14, FDIFF_1:23 .= 1 - (a / (a + x)) by A12, A14 .= ((1 * (a + x)) - a) / (a + x) by A15, XCMPLX_1:127 .= x / (a + x) ; hence (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ; ::_thesis: verum end; hence ( (id Z) - (a (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - (a (#) f)) `| Z) . x = x / (a + x) ) ) by A1, A11, A8, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:5 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) holds ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (((2 * a) (#) f) - (id Z)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ) implies ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) ) assume that A1: Z c= dom (((2 * a) (#) f) - (id Z)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) ; ::_thesis: ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) A4: Z c= (dom ((2 * a) (#) f)) /\ (dom (id Z)) by A1, VALUED_1:12; then A5: Z c= dom ((2 * a) (#) f) by XBOOLE_1:18; then A6: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A7: f is_differentiable_on Z by A2, A3, Th1; then A8: (2 * a) (#) f is_differentiable_on Z by A5, FDIFF_1:20; A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A4, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds (((2 * a) (#) f) `| Z) . x = (2 * a) / (a + x) proof let x be Real; ::_thesis: ( x in Z implies (((2 * a) (#) f) `| Z) . x = (2 * a) / (a + x) ) assume A13: x in Z ; ::_thesis: (((2 * a) (#) f) `| Z) . x = (2 * a) / (a + x) hence (((2 * a) (#) f) `| Z) . x = (2 * a) * (diff (f,x)) by A5, A7, FDIFF_1:20 .= (2 * a) * ((f `| Z) . x) by A7, A13, FDIFF_1:def_7 .= (2 * a) * (1 / (a + x)) by A2, A3, A6, A13, Th1 .= (2 * a) / (a + x) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) proof let x be Real; ::_thesis: ( x in Z implies ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) assume A14: x in Z ; ::_thesis: ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) then A15: ( f1 . x = a + x & f1 . x > 0 ) by A3; ((((2 * a) (#) f) - (id Z)) `| Z) . x = (diff (((2 * a) (#) f),x)) - (diff ((id Z),x)) by A1, A11, A8, A14, FDIFF_1:19 .= (diff (((2 * a) (#) f),x)) - (((id Z) `| Z) . x) by A11, A14, FDIFF_1:def_7 .= ((((2 * a) (#) f) `| Z) . x) - (((id Z) `| Z) . x) by A8, A14, FDIFF_1:def_7 .= ((((2 * a) (#) f) `| Z) . x) - 1 by A10, A9, A14, FDIFF_1:23 .= ((2 * a) / (a + x)) - 1 by A12, A14 .= ((2 * a) - (1 * (a + x))) / (a + x) by A15, XCMPLX_1:126 .= (a - x) / (a + x) ; hence ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ; ::_thesis: verum end; hence ( ((2 * a) (#) f) - (id Z) is_differentiable_on Z & ( for x being Real st x in Z holds ((((2 * a) (#) f) - (id Z)) `| Z) . x = (a - x) / (a + x) ) ) by A1, A11, A8, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:6 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) holds ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) holds ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) holds ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) - ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ) implies ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) ) assume that A1: Z c= dom ((id Z) - ((2 * a) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x + a & f1 . x > 0 ) ; ::_thesis: ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) A4: for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 ) by A3; A5: Z c= (dom (id Z)) /\ (dom ((2 * a) (#) f)) by A1, VALUED_1:12; then A6: Z c= dom ((2 * a) (#) f) by XBOOLE_1:18; then A7: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A8: f is_differentiable_on Z by A2, A4, Th1; then A9: (2 * a) (#) f is_differentiable_on Z by A6, FDIFF_1:20; A10: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A11: Z c= dom (id Z) by A5, XBOOLE_1:18; then A12: id Z is_differentiable_on Z by A10, FDIFF_1:23; A13: for x being Real st x in Z holds (((2 * a) (#) f) `| Z) . x = (2 * a) / (x + a) proof let x be Real; ::_thesis: ( x in Z implies (((2 * a) (#) f) `| Z) . x = (2 * a) / (x + a) ) assume A14: x in Z ; ::_thesis: (((2 * a) (#) f) `| Z) . x = (2 * a) / (x + a) hence (((2 * a) (#) f) `| Z) . x = (2 * a) * (diff (f,x)) by A6, A8, FDIFF_1:20 .= (2 * a) * ((f `| Z) . x) by A8, A14, FDIFF_1:def_7 .= (2 * a) * (1 / (x + a)) by A2, A7, A4, A14, Th1 .= (2 * a) / (x + a) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) assume A15: x in Z ; ::_thesis: (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) then A16: ( f1 . x = x + a & f1 . x > 0 ) by A3; (((id Z) - ((2 * a) (#) f)) `| Z) . x = (diff ((id Z),x)) - (diff (((2 * a) (#) f),x)) by A1, A12, A9, A15, FDIFF_1:19 .= (((id Z) `| Z) . x) - (diff (((2 * a) (#) f),x)) by A12, A15, FDIFF_1:def_7 .= (((id Z) `| Z) . x) - ((((2 * a) (#) f) `| Z) . x) by A9, A15, FDIFF_1:def_7 .= 1 - ((((2 * a) (#) f) `| Z) . x) by A11, A10, A15, FDIFF_1:23 .= 1 - ((2 * a) / (x + a)) by A13, A15 .= ((1 * (x + a)) - (2 * a)) / (x + a) by A16, XCMPLX_1:127 .= (x - a) / (x + a) ; hence (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ; ::_thesis: verum end; hence ( (id Z) - ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((2 * a) (#) f)) `| Z) . x = (x - a) / (x + a) ) ) by A1, A12, A9, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:7 for a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) holds ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) holds ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) holds ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) + ((2 * a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ) implies ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) ) assume that A1: Z c= dom ((id Z) + ((2 * a) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 ) ; ::_thesis: ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) A4: Z c= (dom (id Z)) /\ (dom ((2 * a) (#) f)) by A1, VALUED_1:def_1; then A5: Z c= dom ((2 * a) (#) f) by XBOOLE_1:18; then A6: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A7: f is_differentiable_on Z by A2, A3, Th2; then A8: (2 * a) (#) f is_differentiable_on Z by A5, FDIFF_1:20; A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A4, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds (((2 * a) (#) f) `| Z) . x = (2 * a) / (x - a) proof let x be Real; ::_thesis: ( x in Z implies (((2 * a) (#) f) `| Z) . x = (2 * a) / (x - a) ) assume A13: x in Z ; ::_thesis: (((2 * a) (#) f) `| Z) . x = (2 * a) / (x - a) hence (((2 * a) (#) f) `| Z) . x = (2 * a) * (diff (f,x)) by A5, A7, FDIFF_1:20 .= (2 * a) * ((f `| Z) . x) by A7, A13, FDIFF_1:def_7 .= (2 * a) * (1 / (x - a)) by A2, A3, A6, A13, Th2 .= (2 * a) / (x - a) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) assume A14: x in Z ; ::_thesis: (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) then A15: ( f1 . x = x - a & f1 . x > 0 ) by A3; (((id Z) + ((2 * a) (#) f)) `| Z) . x = (diff ((id Z),x)) + (diff (((2 * a) (#) f),x)) by A1, A11, A8, A14, FDIFF_1:18 .= (((id Z) `| Z) . x) + (diff (((2 * a) (#) f),x)) by A11, A14, FDIFF_1:def_7 .= (((id Z) `| Z) . x) + ((((2 * a) (#) f) `| Z) . x) by A8, A14, FDIFF_1:def_7 .= 1 + ((((2 * a) (#) f) `| Z) . x) by A10, A9, A14, FDIFF_1:23 .= 1 + ((2 * a) / (x - a)) by A12, A14 .= ((1 * (x - a)) + (2 * a)) / (x - a) by A15, XCMPLX_1:113 .= (x + a) / (x - a) ; hence (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ; ::_thesis: verum end; hence ( (id Z) + ((2 * a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((2 * a) (#) f)) `| Z) . x = (x + a) / (x - a) ) ) by A1, A11, A8, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:8 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) + ((a - b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) implies ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) ) assume that A1: Z c= dom ((id Z) + ((a - b) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ; ::_thesis: ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) A4: for x being Real st x in Z holds ( f1 . x = b + x & f1 . x > 0 ) by A3; A5: Z c= (dom (id Z)) /\ (dom ((a - b) (#) f)) by A1, VALUED_1:def_1; then A6: Z c= dom ((a - b) (#) f) by XBOOLE_1:18; then A7: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A8: f is_differentiable_on Z by A2, A4, Th1; then A9: (a - b) (#) f is_differentiable_on Z by A6, FDIFF_1:20; A10: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A11: Z c= dom (id Z) by A5, XBOOLE_1:18; then A12: id Z is_differentiable_on Z by A10, FDIFF_1:23; A13: for x being Real st x in Z holds (((a - b) (#) f) `| Z) . x = (a - b) / (x + b) proof let x be Real; ::_thesis: ( x in Z implies (((a - b) (#) f) `| Z) . x = (a - b) / (x + b) ) assume A14: x in Z ; ::_thesis: (((a - b) (#) f) `| Z) . x = (a - b) / (x + b) hence (((a - b) (#) f) `| Z) . x = (a - b) * (diff (f,x)) by A6, A8, FDIFF_1:20 .= (a - b) * ((f `| Z) . x) by A8, A14, FDIFF_1:def_7 .= (a - b) * (1 / (x + b)) by A2, A7, A4, A14, Th1 .= (a - b) / (x + b) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) assume A15: x in Z ; ::_thesis: (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) then A16: ( f1 . x = x + b & f1 . x > 0 ) by A3; (((id Z) + ((a - b) (#) f)) `| Z) . x = (diff ((id Z),x)) + (diff (((a - b) (#) f),x)) by A1, A12, A9, A15, FDIFF_1:18 .= (((id Z) `| Z) . x) + (diff (((a - b) (#) f),x)) by A12, A15, FDIFF_1:def_7 .= (((id Z) `| Z) . x) + ((((a - b) (#) f) `| Z) . x) by A9, A15, FDIFF_1:def_7 .= 1 + ((((a - b) (#) f) `| Z) . x) by A11, A10, A15, FDIFF_1:23 .= 1 + ((a - b) / (x + b)) by A13, A15 .= ((1 * (x + b)) + (a - b)) / (x + b) by A16, XCMPLX_1:113 .= (x + a) / (x + b) ; hence (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ; ::_thesis: verum end; hence ( (id Z) + ((a - b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a - b) (#) f)) `| Z) . x = (x + a) / (x + b) ) ) by A1, A12, A9, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:9 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) + ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) implies ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) ) assume that A1: Z c= dom ((id Z) + ((a + b) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ; ::_thesis: ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) A4: Z c= (dom (id Z)) /\ (dom ((a + b) (#) f)) by A1, VALUED_1:def_1; then A5: Z c= dom ((a + b) (#) f) by XBOOLE_1:18; then A6: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A7: f is_differentiable_on Z by A2, A3, Th2; then A8: (a + b) (#) f is_differentiable_on Z by A5, FDIFF_1:20; A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A4, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds (((a + b) (#) f) `| Z) . x = (a + b) / (x - b) proof let x be Real; ::_thesis: ( x in Z implies (((a + b) (#) f) `| Z) . x = (a + b) / (x - b) ) assume A13: x in Z ; ::_thesis: (((a + b) (#) f) `| Z) . x = (a + b) / (x - b) hence (((a + b) (#) f) `| Z) . x = (a + b) * (diff (f,x)) by A5, A7, FDIFF_1:20 .= (a + b) * ((f `| Z) . x) by A7, A13, FDIFF_1:def_7 .= (a + b) * (1 / (x - b)) by A2, A3, A6, A13, Th2 .= (a + b) / (x - b) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) assume A14: x in Z ; ::_thesis: (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) then A15: ( f1 . x = x - b & f1 . x > 0 ) by A3; (((id Z) + ((a + b) (#) f)) `| Z) . x = (diff ((id Z),x)) + (diff (((a + b) (#) f),x)) by A1, A11, A8, A14, FDIFF_1:18 .= (((id Z) `| Z) . x) + (diff (((a + b) (#) f),x)) by A11, A14, FDIFF_1:def_7 .= (((id Z) `| Z) . x) + ((((a + b) (#) f) `| Z) . x) by A8, A14, FDIFF_1:def_7 .= 1 + ((((a + b) (#) f) `| Z) . x) by A10, A9, A14, FDIFF_1:23 .= 1 + ((a + b) / (x - b)) by A12, A14 .= ((1 * (x - b)) + (a + b)) / (x - b) by A15, XCMPLX_1:113 .= (x + a) / (x - b) ; hence (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ; ::_thesis: verum end; hence ( (id Z) + ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((a + b) (#) f)) `| Z) . x = (x + a) / (x - b) ) ) by A1, A11, A8, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:10 for a, b being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) holds ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) - ((a + b) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ) implies ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) ) assume that A1: Z c= dom ((id Z) - ((a + b) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x + b & f1 . x > 0 ) ; ::_thesis: ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) A4: for x being Real st x in Z holds ( f1 . x = b + x & f1 . x > 0 ) by A3; A5: Z c= (dom (id Z)) /\ (dom ((a + b) (#) f)) by A1, VALUED_1:12; then A6: Z c= dom ((a + b) (#) f) by XBOOLE_1:18; then A7: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A8: f is_differentiable_on Z by A2, A4, Th1; then A9: (a + b) (#) f is_differentiable_on Z by A6, FDIFF_1:20; A10: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A11: Z c= dom (id Z) by A5, XBOOLE_1:18; then A12: id Z is_differentiable_on Z by A10, FDIFF_1:23; A13: for x being Real st x in Z holds (((a + b) (#) f) `| Z) . x = (a + b) / (x + b) proof let x be Real; ::_thesis: ( x in Z implies (((a + b) (#) f) `| Z) . x = (a + b) / (x + b) ) assume A14: x in Z ; ::_thesis: (((a + b) (#) f) `| Z) . x = (a + b) / (x + b) hence (((a + b) (#) f) `| Z) . x = (a + b) * (diff (f,x)) by A6, A8, FDIFF_1:20 .= (a + b) * ((f `| Z) . x) by A8, A14, FDIFF_1:def_7 .= (a + b) * (1 / (x + b)) by A2, A7, A4, A14, Th1 .= (a + b) / (x + b) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) assume A15: x in Z ; ::_thesis: (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) then A16: ( f1 . x = x + b & f1 . x > 0 ) by A3; (((id Z) - ((a + b) (#) f)) `| Z) . x = (diff ((id Z),x)) - (diff (((a + b) (#) f),x)) by A1, A12, A9, A15, FDIFF_1:19 .= (((id Z) `| Z) . x) - (diff (((a + b) (#) f),x)) by A12, A15, FDIFF_1:def_7 .= (((id Z) `| Z) . x) - ((((a + b) (#) f) `| Z) . x) by A9, A15, FDIFF_1:def_7 .= 1 - ((((a + b) (#) f) `| Z) . x) by A11, A10, A15, FDIFF_1:23 .= 1 - ((a + b) / (x + b)) by A13, A15 .= ((1 * (x + b)) - (a + b)) / (x + b) by A16, XCMPLX_1:127 .= (x - a) / (x + b) ; hence (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ; ::_thesis: verum end; hence ( (id Z) - ((a + b) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) - ((a + b) (#) f)) `| Z) . x = (x - a) / (x + b) ) ) by A1, A12, A9, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:11 for b, a being Real for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) proof let b, a be Real; ::_thesis: for Z being open Subset of REAL for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1 being PartFunc of REAL,REAL st Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) holds ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) let f, f1 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((id Z) + ((b - a) (#) f)) & f = ln * f1 & ( for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ) implies ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) ) assume that A1: Z c= dom ((id Z) + ((b - a) (#) f)) and A2: f = ln * f1 and A3: for x being Real st x in Z holds ( f1 . x = x - b & f1 . x > 0 ) ; ::_thesis: ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) A4: Z c= (dom (id Z)) /\ (dom ((b - a) (#) f)) by A1, VALUED_1:def_1; then A5: Z c= dom ((b - a) (#) f) by XBOOLE_1:18; then A6: Z c= dom (ln * f1) by A2, VALUED_1:def_5; then A7: f is_differentiable_on Z by A2, A3, Th2; then A8: (b - a) (#) f is_differentiable_on Z by A5, FDIFF_1:20; A9: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A10: Z c= dom (id Z) by A4, XBOOLE_1:18; then A11: id Z is_differentiable_on Z by A9, FDIFF_1:23; A12: for x being Real st x in Z holds (((b - a) (#) f) `| Z) . x = (b - a) / (x - b) proof let x be Real; ::_thesis: ( x in Z implies (((b - a) (#) f) `| Z) . x = (b - a) / (x - b) ) assume A13: x in Z ; ::_thesis: (((b - a) (#) f) `| Z) . x = (b - a) / (x - b) hence (((b - a) (#) f) `| Z) . x = (b - a) * (diff (f,x)) by A5, A7, FDIFF_1:20 .= (b - a) * ((f `| Z) . x) by A7, A13, FDIFF_1:def_7 .= (b - a) * (1 / (x - b)) by A2, A3, A6, A13, Th2 .= (b - a) / (x - b) by XCMPLX_1:99 ; ::_thesis: verum end; for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) assume A14: x in Z ; ::_thesis: (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) then A15: ( f1 . x = x - b & f1 . x > 0 ) by A3; (((id Z) + ((b - a) (#) f)) `| Z) . x = (diff ((id Z),x)) + (diff (((b - a) (#) f),x)) by A1, A11, A8, A14, FDIFF_1:18 .= (((id Z) `| Z) . x) + (diff (((b - a) (#) f),x)) by A11, A14, FDIFF_1:def_7 .= (((id Z) `| Z) . x) + ((((b - a) (#) f) `| Z) . x) by A8, A14, FDIFF_1:def_7 .= 1 + ((((b - a) (#) f) `| Z) . x) by A10, A9, A14, FDIFF_1:23 .= 1 + ((b - a) / (x - b)) by A12, A14 .= ((1 * (x - b)) + (b - a)) / (x - b) by A15, XCMPLX_1:113 .= (x - a) / (x - b) ; hence (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ; ::_thesis: verum end; hence ( (id Z) + ((b - a) (#) f) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) + ((b - a) (#) f)) `| Z) . x = (x - a) / (x - b) ) ) by A1, A11, A8, FDIFF_1:18; ::_thesis: verum end; theorem Th12: :: FDIFF_4:12 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) & f2 = #Z 2 holds ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) proof let c, a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) & f2 = #Z 2 holds ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) & f2 = #Z 2 holds ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 + (c (#) f2)) & ( for x being Real st x in Z holds f1 . x = a + (b * x) ) & f2 = #Z 2 implies ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) ) assume that A1: Z c= dom (f1 + (c (#) f2)) and A2: for x being Real st x in Z holds f1 . x = a + (b * x) and A3: f2 = #Z 2 ; ::_thesis: ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) A4: for x being Real st x in Z holds f2 is_differentiable_in x by A3, TAYLOR_1:2; A5: Z c= (dom f1) /\ (dom (c (#) f2)) by A1, VALUED_1:def_1; then A6: Z c= dom f1 by XBOOLE_1:18; A7: for x being Real st x in Z holds f1 . x = (b * x) + a by A2; then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23; A9: Z c= dom (c (#) f2) by A5, XBOOLE_1:18; then Z c= dom f2 by VALUED_1:def_5; then A10: f2 is_differentiable_on Z by A4, FDIFF_1:9; then A11: c (#) f2 is_differentiable_on Z by A9, FDIFF_1:20; A12: for x being Real st x in Z holds (f2 `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * x ) 2 * (x #Z (2 - 1)) = 2 * x by PREPOWER:35; then A13: diff (f2,x) = 2 * x by A3, TAYLOR_1:2; assume x in Z ; ::_thesis: (f2 `| Z) . x = 2 * x hence (f2 `| Z) . x = 2 * x by A10, A13, FDIFF_1:def_7; ::_thesis: verum end; A14: for x being Real st x in Z holds ((c (#) f2) `| Z) . x = (2 * c) * x proof let x be Real; ::_thesis: ( x in Z implies ((c (#) f2) `| Z) . x = (2 * c) * x ) assume A15: x in Z ; ::_thesis: ((c (#) f2) `| Z) . x = (2 * c) * x hence ((c (#) f2) `| Z) . x = c * (diff (f2,x)) by A9, A10, FDIFF_1:20 .= c * ((f2 `| Z) . x) by A10, A15, FDIFF_1:def_7 .= c * (2 * x) by A12, A15 .= (2 * c) * x ; ::_thesis: verum end; for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) proof let x be Real; ::_thesis: ( x in Z implies ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) assume A16: x in Z ; ::_thesis: ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) then ((f1 + (c (#) f2)) `| Z) . x = (diff (f1,x)) + (diff ((c (#) f2),x)) by A1, A8, A11, FDIFF_1:18 .= ((f1 `| Z) . x) + (diff ((c (#) f2),x)) by A8, A16, FDIFF_1:def_7 .= ((f1 `| Z) . x) + (((c (#) f2) `| Z) . x) by A11, A16, FDIFF_1:def_7 .= b + (((c (#) f2) `| Z) . x) by A6, A7, A16, FDIFF_1:23 .= b + ((2 * c) * x) by A14, A16 ; hence ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ; ::_thesis: verum end; hence ( f1 + (c (#) f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + (c (#) f2)) `| Z) . x = b + ((2 * c) * x) ) ) by A1, A8, A11, FDIFF_1:18; ::_thesis: verum end; theorem Th13: :: FDIFF_4:13 for c, a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) proof let c, a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) holds ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 + (c (#) f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ) implies ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) ) assume that A1: Z c= dom (ln * (f1 + (c (#) f2))) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds ( f1 . x = a + (b * x) & (f1 + (c (#) f2)) . x > 0 ) ; ::_thesis: ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) for y being set st y in Z holds y in dom (f1 + (c (#) f2)) by A1, FUNCT_1:11; then A4: Z c= dom (f1 + (c (#) f2)) by TARSKI:def_3; then Z c= (dom f1) /\ (dom (c (#) f2)) by VALUED_1:def_1; then A5: Z c= dom (c (#) f2) by XBOOLE_1:18; A6: for x being Real st x in Z holds f1 . x = a + (b * x) by A3; then A7: f1 + (c (#) f2) is_differentiable_on Z by A2, A4, Th12; A8: for x being Real st x in Z holds ln * (f1 + (c (#) f2)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 + (c (#) f2)) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 + (c (#) f2)) is_differentiable_in x then ( f1 + (c (#) f2) is_differentiable_in x & (f1 + (c (#) f2)) . x > 0 ) by A3, A7, FDIFF_1:9; hence ln * (f1 + (c (#) f2)) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A9: ln * (f1 + (c (#) f2)) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) assume A10: x in Z ; ::_thesis: ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) then x in dom (f1 + (c (#) f2)) by A1, FUNCT_1:11; then A11: (f1 + (c (#) f2)) . x = (f1 . x) + ((c (#) f2) . x) by VALUED_1:def_1 .= (f1 . x) + (c * (f2 . x)) by A5, A10, VALUED_1:def_5 .= (a + (b * x)) + (c * (f2 . x)) by A3, A10 .= (a + (b * x)) + (c * (x #Z 2)) by A2, TAYLOR_1:def_1 .= (a + (b * x)) + (c * (x |^ 2)) by PREPOWER:36 ; ( f1 + (c (#) f2) is_differentiable_in x & (f1 + (c (#) f2)) . x > 0 ) by A3, A7, A10, FDIFF_1:9; then diff ((ln * (f1 + (c (#) f2))),x) = (diff ((f1 + (c (#) f2)),x)) / ((f1 + (c (#) f2)) . x) by TAYLOR_1:20 .= (((f1 + (c (#) f2)) `| Z) . x) / ((f1 + (c (#) f2)) . x) by A7, A10, FDIFF_1:def_7 .= (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) by A2, A4, A6, A10, A11, Th12 ; hence ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 + (c (#) f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + (c (#) f2))) `| Z) . x = (b + ((2 * c) * x)) / ((a + (b * x)) + (c * (x |^ 2))) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem Th14: :: FDIFF_4:14 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) implies ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) ) assume that A1: Z c= dom f and A2: for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ; ::_thesis: ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) A3: for x being Real st x in Z holds f . x = (1 * x) + a by A2; then A4: f is_differentiable_on Z by A1, FDIFF_1:23; A5: for x being Real st x in Z holds f . x <> 0 by A2; then A6: f ^ is_differentiable_on Z by A4, FDIFF_2:22; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((f_^)_`|_Z)_._x_=_-_(1_/_((a_+_x)_^2)) let x be Real; ::_thesis: ( x in Z implies ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) assume A7: x in Z ; ::_thesis: ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) then A8: ( f . x <> 0 & f is_differentiable_in x ) by A2, A4, FDIFF_1:9; ((f ^) `| Z) . x = diff ((f ^),x) by A6, A7, FDIFF_1:def_7 .= - ((diff (f,x)) / ((f . x) ^2)) by A8, FDIFF_2:15 .= - (((f `| Z) . x) / ((f . x) ^2)) by A4, A7, FDIFF_1:def_7 .= - (1 / ((f . x) ^2)) by A1, A3, A7, FDIFF_1:23 .= - (1 / ((a + x) ^2)) by A2, A7 ; hence ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ; ::_thesis: verum end; hence ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = - (1 / ((a + x) ^2)) ) ) by A4, A5, FDIFF_2:22; ::_thesis: verum end; theorem :: FDIFF_4:15 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) holds ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((- 1) (#) (f ^)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ) implies ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) ) assume that A1: Z c= dom ((- 1) (#) (f ^)) and A2: for x being Real st x in Z holds ( f . x = a + x & f . x <> 0 ) ; ::_thesis: ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) A3: dom (f ^) c= dom f by RFUNCT_1:1; Z c= dom (f ^) by A1, VALUED_1:def_5; then A4: Z c= dom f by A3, XBOOLE_1:1; then A5: f ^ is_differentiable_on Z by A2, Th14; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((-_1)_(#)_(f_^))_`|_Z)_._x_=_1_/_((a_+_x)_^2) let x be Real; ::_thesis: ( x in Z implies (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) assume A6: x in Z ; ::_thesis: (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) hence (((- 1) (#) (f ^)) `| Z) . x = (- 1) * (diff ((f ^),x)) by A1, A5, FDIFF_1:20 .= (- 1) * (((f ^) `| Z) . x) by A5, A6, FDIFF_1:def_7 .= (- 1) * (- (1 / ((a + x) ^2))) by A2, A4, A6, Th14 .= 1 / ((a + x) ^2) ; ::_thesis: verum end; hence ( (- 1) (#) (f ^) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 1) (#) (f ^)) `| Z) . x = 1 / ((a + x) ^2) ) ) by A1, A5, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:16 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom f & ( for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ) holds ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom f & ( for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ) implies ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) ) assume that A1: Z c= dom f and A2: for x being Real st x in Z holds ( f . x = a - x & f . x <> 0 ) ; ::_thesis: ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) A3: for x being Real st x in Z holds f . x = ((- 1) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f . x = ((- 1) * x) + a ) assume x in Z ; ::_thesis: f . x = ((- 1) * x) + a then f . x = a - x by A2; hence f . x = ((- 1) * x) + a ; ::_thesis: verum end; then A4: f is_differentiable_on Z by A1, FDIFF_1:23; A5: for x being Real st x in Z holds f . x <> 0 by A2; then A6: f ^ is_differentiable_on Z by A4, FDIFF_2:22; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((f_^)_`|_Z)_._x_=_1_/_((a_-_x)_^2) let x be Real; ::_thesis: ( x in Z implies ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) assume A7: x in Z ; ::_thesis: ((f ^) `| Z) . x = 1 / ((a - x) ^2) then A8: ( f . x <> 0 & f is_differentiable_in x ) by A2, A4, FDIFF_1:9; ((f ^) `| Z) . x = diff ((f ^),x) by A6, A7, FDIFF_1:def_7 .= - ((diff (f,x)) / ((f . x) ^2)) by A8, FDIFF_2:15 .= - (((f `| Z) . x) / ((f . x) ^2)) by A4, A7, FDIFF_1:def_7 .= - ((- 1) / ((f . x) ^2)) by A1, A3, A7, FDIFF_1:23 .= - (- (1 / ((f . x) ^2))) by XCMPLX_1:187 .= 1 / ((a - x) ^2) by A2, A7 ; hence ((f ^) `| Z) . x = 1 / ((a - x) ^2) ; ::_thesis: verum end; hence ( f ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((f ^) `| Z) . x = 1 / ((a - x) ^2) ) ) by A4, A5, FDIFF_2:22; ::_thesis: verum end; theorem Th17: :: FDIFF_4:17 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ^2 ) & f2 = #Z 2 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ^2 ) & f2 = #Z 2 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ^2 ) & f2 = #Z 2 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ^2 ) & f2 = #Z 2 implies ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) ) assume that A1: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ^2 ) ) and A2: f2 = #Z 2 ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) A3: ( Z c= dom (f1 + (1 (#) f2)) & ( for x being Real st x in Z holds f1 . x = (a ^2) + (0 * x) ) ) by A1, RFUNCT_1:21; A4: for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = 2 * x ) assume A5: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = 2 * x ((f1 + f2) `| Z) . x = ((f1 + (1 (#) f2)) `| Z) . x by RFUNCT_1:21 .= 0 + ((2 * 1) * x) by A2, A3, A5, Th12 .= 2 * x ; hence ((f1 + f2) `| Z) . x = 2 * x ; ::_thesis: verum end; f1 + (1 (#) f2) is_differentiable_on Z by A2, A3, Th12; hence ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) by A4, RFUNCT_1:21; ::_thesis: verum end; theorem :: FDIFF_4:18 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 + f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ) implies ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) ) assume that A1: Z c= dom (ln * (f1 + f2)) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 + f2) . x > 0 ) ; ::_thesis: ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) f2 = 1 (#) f2 by RFUNCT_1:21; then A4: for x being Real st x in Z holds ( f1 . x = (a ^2) + (0 * x) & (f1 + (1 (#) f2)) . x > 0 ) by A3; A5: Z c= dom (ln * (f1 + (1 (#) f2))) by A1, RFUNCT_1:21; A6: for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) assume A7: x in Z ; ::_thesis: ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ((ln * (f1 + f2)) `| Z) . x = ((ln * (f1 + (1 (#) f2))) `| Z) . x by RFUNCT_1:21 .= (0 + ((2 * 1) * x)) / (((a ^2) + (0 * x)) + (1 * (x |^ 2))) by A2, A5, A4, A7, Th13 .= (2 * x) / ((a ^2) + (x |^ 2)) ; hence ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ; ::_thesis: verum end; ln * (f1 + (1 (#) f2)) is_differentiable_on Z by A2, A5, A4, Th13; hence ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (2 * x) / ((a ^2) + (x |^ 2)) ) ) by A6, RFUNCT_1:21; ::_thesis: verum end; theorem :: FDIFF_4:19 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (- (ln * (f1 - f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (- (ln * (f1 - f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (- (ln * (f1 - f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) holds ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (- (ln * (f1 - f2))) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ) implies ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) ) assume that A1: Z c= dom (- (ln * (f1 - f2))) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds ( f1 . x = a ^2 & (f1 - f2) . x > 0 ) ; ::_thesis: ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) A4: ( Z c= dom (ln * (f1 + ((- 1) (#) f2))) & ( for x being Real st x in Z holds ( f1 . x = (a ^2) + (0 * x) & (f1 + ((- 1) (#) f2)) . x > 0 ) ) ) by A1, A3, VALUED_1:8; then A5: ln * (f1 + ((- 1) (#) f2)) is_differentiable_on Z by A2, Th13; for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) proof let x be Real; ::_thesis: ( x in Z implies ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) assume A6: x in Z ; ::_thesis: ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) then ((- (ln * (f1 - f2))) `| Z) . x = (- 1) * (diff ((ln * (f1 + ((- 1) (#) f2))),x)) by A1, A5, FDIFF_1:20 .= (- 1) * (((ln * (f1 + ((- 1) (#) f2))) `| Z) . x) by A5, A6, FDIFF_1:def_7 .= (- 1) * ((0 + ((2 * (- 1)) * x)) / (((a ^2) + (0 * x)) + ((- 1) * (x |^ 2)))) by A2, A4, A6, Th13 .= ((- 1) * ((2 * (- 1)) * x)) / ((a ^2) + ((- 1) * (x |^ 2))) by XCMPLX_1:74 .= (2 * x) / ((a ^2) - (x |^ 2)) ; hence ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ; ::_thesis: verum end; hence ( - (ln * (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((- (ln * (f1 - f2))) `| Z) . x = (2 * x) / ((a ^2) - (x |^ 2)) ) ) by A1, A5, FDIFF_1:20; ::_thesis: verum end; theorem Th20: :: FDIFF_4:20 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 3 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 3 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 3 holds ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (f1 + f2) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 3 implies ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) ) assume that A1: Z c= dom (f1 + f2) and A2: for x being Real st x in Z holds f1 . x = a and A3: f2 = #Z 3 ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) A4: for x being Real st x in Z holds f2 is_differentiable_in x by A3, TAYLOR_1:2; A5: Z c= (dom f1) /\ (dom f2) by A1, VALUED_1:def_1; then A6: Z c= dom f1 by XBOOLE_1:18; A7: for x being Real st x in Z holds f1 . x = (0 * x) + a by A2; then A8: f1 is_differentiable_on Z by A6, FDIFF_1:23; Z c= dom f2 by A5, XBOOLE_1:18; then A9: f2 is_differentiable_on Z by A4, FDIFF_1:9; A10: for x being Real st x in Z holds (f2 `| Z) . x = 3 * (x #Z (3 - 1)) proof let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 3 * (x #Z (3 - 1)) ) assume A11: x in Z ; ::_thesis: (f2 `| Z) . x = 3 * (x #Z (3 - 1)) diff (f2,x) = 3 * (x #Z (3 - 1)) by A3, TAYLOR_1:2; hence (f2 `| Z) . x = 3 * (x #Z (3 - 1)) by A9, A11, FDIFF_1:def_7; ::_thesis: verum end; for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) proof let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) assume A12: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = 3 * (x |^ 2) then ((f1 + f2) `| Z) . x = (diff (f1,x)) + (diff (f2,x)) by A1, A8, A9, FDIFF_1:18; hence ((f1 + f2) `| Z) . x = ((f1 `| Z) . x) + (diff (f2,x)) by A8, A12, FDIFF_1:def_7 .= ((f1 `| Z) . x) + ((f2 `| Z) . x) by A9, A12, FDIFF_1:def_7 .= 0 + ((f2 `| Z) . x) by A6, A7, A12, FDIFF_1:23 .= 3 * (x #Z (3 - 1)) by A10, A12 .= 3 * (x |^ 2) by PREPOWER:36 ; ::_thesis: verum end; hence ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 3 * (x |^ 2) ) ) by A1, A8, A9, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:21 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ) holds ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 + f2)) & f2 = #Z 3 & ( for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ) implies ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) ) assume that A1: Z c= dom (ln * (f1 + f2)) and A2: f2 = #Z 3 and A3: for x being Real st x in Z holds ( f1 . x = a & (f1 + f2) . x > 0 ) ; ::_thesis: ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) for y being set st y in Z holds y in dom (f1 + f2) by A1, FUNCT_1:11; then A4: Z c= dom (f1 + f2) by TARSKI:def_3; A5: for x being Real st x in Z holds f1 . x = a by A3; then A6: f1 + f2 is_differentiable_on Z by A2, A4, Th20; A7: for x being Real st x in Z holds ln * (f1 + f2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 + f2) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 + f2) is_differentiable_in x then ( f1 + f2 is_differentiable_in x & (f1 + f2) . x > 0 ) by A3, A6, FDIFF_1:9; hence ln * (f1 + f2) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A8: ln * (f1 + f2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) assume A9: x in Z ; ::_thesis: ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) then A10: x in dom (f1 + f2) by A1, FUNCT_1:11; ( f1 + f2 is_differentiable_in x & (f1 + f2) . x > 0 ) by A3, A6, A9, FDIFF_1:9; then diff ((ln * (f1 + f2)),x) = (diff ((f1 + f2),x)) / ((f1 + f2) . x) by TAYLOR_1:20 .= (((f1 + f2) `| Z) . x) / ((f1 + f2) . x) by A6, A9, FDIFF_1:def_7 .= (3 * (x |^ 2)) / ((f1 + f2) . x) by A2, A4, A5, A9, Th20 .= (3 * (x |^ 2)) / ((f1 . x) + (f2 . x)) by A10, VALUED_1:def_1 .= (3 * (x |^ 2)) / (a + (f2 . x)) by A3, A9 .= (3 * (x |^ 2)) / (a + (x #Z 3)) by A2, TAYLOR_1:def_1 .= (3 * (x |^ 2)) / (a + (x |^ 3)) by PREPOWER:36 ; hence ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) by A8, A9, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 + f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 + f2)) `| Z) . x = (3 * (x |^ 2)) / (a + (x |^ 3)) ) ) by A1, A7, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:22 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) ) assume that A1: Z c= dom (ln * (f1 / f2)) and A2: for x being Real st x in Z holds ( f1 . x = a + x & f1 . x > 0 & f2 . x = a - x & f2 . x > 0 ) ; ::_thesis: ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) for y being set st y in Z holds y in dom (f1 / f2) by A1, FUNCT_1:11; then Z c= dom (f1 / f2) by TARSKI:def_3; then A3: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def_1; then A4: Z c= dom f1 by XBOOLE_1:18; A5: for x being Real st x in Z holds f1 . x = (1 * x) + a by A2; then A6: f1 is_differentiable_on Z by A4, FDIFF_1:23; A7: for x being Real st x in Z holds f2 . x = ((- 1) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f2 . x = ((- 1) * x) + a ) assume x in Z ; ::_thesis: f2 . x = ((- 1) * x) + a then f2 . x = a - x by A2; hence f2 . x = ((- 1) * x) + a ; ::_thesis: verum end; A8: Z c= dom f2 by A3, XBOOLE_1:1; then A9: f2 is_differentiable_on Z by A7, FDIFF_1:23; for x being Real st x in Z holds f2 . x <> 0 by A2; then A10: f1 / f2 is_differentiable_on Z by A6, A9, FDIFF_2:21; A11: for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) assume A12: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) then A13: f2 . x <> 0 by A2; A14: ( f1 . x = a + x & f2 . x = a - x ) by A2, A12; ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A6, A9, A12, FDIFF_1:9; then diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A13, FDIFF_2:14 .= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A6, A12, FDIFF_1:def_7 .= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A9, A12, FDIFF_1:def_7 .= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A4, A5, A12, FDIFF_1:23 .= ((1 * (f2 . x)) - ((- 1) * (f1 . x))) / ((f2 . x) ^2) by A8, A7, A12, FDIFF_1:23 .= (2 * a) / ((a - x) ^2) by A14 ; hence ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) by A10, A12, FDIFF_1:def_7; ::_thesis: verum end; A15: for x being Real st x in Z holds (f1 / f2) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (f1 / f2) . x > 0 ) assume A16: x in Z ; ::_thesis: (f1 / f2) . x > 0 then x in dom (f1 / f2) by A1, FUNCT_1:11; then A17: (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by RFUNCT_1:def_1 .= (f1 . x) / (f2 . x) by XCMPLX_0:def_9 ; ( f1 . x > 0 & f2 . x > 0 ) by A2, A16; hence (f1 / f2) . x > 0 by A17, XREAL_1:139; ::_thesis: verum end; A18: for x being Real st x in Z holds ln * (f1 / f2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 / f2) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 / f2) is_differentiable_in x then ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A10, A15, FDIFF_1:9; hence ln * (f1 / f2) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A19: ln * (f1 / f2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) assume A20: x in Z ; ::_thesis: ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) then A21: ( f2 . x = a - x & f2 . x > 0 ) by A2; A22: ( f1 . x = a + x & f2 . x = a - x ) by A2, A20; A23: x in dom (f1 / f2) by A1, A20, FUNCT_1:11; ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A10, A15, A20, FDIFF_1:9; then diff ((ln * (f1 / f2)),x) = (diff ((f1 / f2),x)) / ((f1 / f2) . x) by TAYLOR_1:20 .= (((f1 / f2) `| Z) . x) / ((f1 / f2) . x) by A10, A20, FDIFF_1:def_7 .= ((2 * a) / ((a - x) ^2)) / ((f1 / f2) . x) by A11, A20 .= ((2 * a) / ((a - x) ^2)) / ((f1 . x) * ((f2 . x) ")) by A23, RFUNCT_1:def_1 .= ((2 * a) / ((a - x) * (a - x))) / ((a + x) / (a - x)) by A22, XCMPLX_0:def_9 .= (((2 * a) / (a - x)) / (a - x)) / ((a + x) / (a - x)) by XCMPLX_1:78 .= (((2 * a) / (a - x)) / ((a + x) / (a - x))) / (a - x) by XCMPLX_1:48 .= ((2 * a) / (a + x)) / (a - x) by A21, XCMPLX_1:55 .= (2 * a) / ((a + x) * (a - x)) by XCMPLX_1:78 .= (2 * a) / ((a ^2) - (x ^2)) ; hence ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) by A19, A20, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((a ^2) - (x ^2)) ) ) by A1, A18, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:23 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) ) assume that A1: Z c= dom (ln * (f1 / f2)) and A2: for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x + a & f2 . x > 0 ) ; ::_thesis: ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) A3: for x being Real st x in Z holds f2 . x = (1 * x) + a by A2; for y being set st y in Z holds y in dom (f1 / f2) by A1, FUNCT_1:11; then Z c= dom (f1 / f2) by TARSKI:def_3; then A4: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def_1; then A5: Z c= dom f1 by XBOOLE_1:18; A6: Z c= dom f2 by A4, XBOOLE_1:1; then A7: f2 is_differentiable_on Z by A3, FDIFF_1:23; A8: for x being Real st x in Z holds f1 . x = (1 * x) + (- a) proof let x be Real; ::_thesis: ( x in Z implies f1 . x = (1 * x) + (- a) ) A9: (1 * x) + (- a) = (1 * x) - a ; assume x in Z ; ::_thesis: f1 . x = (1 * x) + (- a) hence f1 . x = (1 * x) + (- a) by A2, A9; ::_thesis: verum end; then A10: f1 is_differentiable_on Z by A5, FDIFF_1:23; for x being Real st x in Z holds f2 . x <> 0 by A2; then A11: f1 / f2 is_differentiable_on Z by A10, A7, FDIFF_2:21; A12: for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) assume A13: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) then A14: f2 . x <> 0 by A2; A15: ( f1 . x = x - a & f2 . x = x + a ) by A2, A13; ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A10, A7, A13, FDIFF_1:9; then diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A14, FDIFF_2:14 .= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A10, A13, FDIFF_1:def_7 .= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A7, A13, FDIFF_1:def_7 .= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A5, A8, A13, FDIFF_1:23 .= ((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2) by A6, A3, A13, FDIFF_1:23 .= (2 * a) / ((x + a) ^2) by A15 ; hence ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) by A11, A13, FDIFF_1:def_7; ::_thesis: verum end; A16: for x being Real st x in Z holds (f1 / f2) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (f1 / f2) . x > 0 ) assume A17: x in Z ; ::_thesis: (f1 / f2) . x > 0 then x in dom (f1 / f2) by A1, FUNCT_1:11; then A18: (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by RFUNCT_1:def_1 .= (f1 . x) / (f2 . x) by XCMPLX_0:def_9 ; ( f1 . x > 0 & f2 . x > 0 ) by A2, A17; hence (f1 / f2) . x > 0 by A18, XREAL_1:139; ::_thesis: verum end; A19: for x being Real st x in Z holds ln * (f1 / f2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 / f2) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 / f2) is_differentiable_in x then ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A11, A16, FDIFF_1:9; hence ln * (f1 / f2) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A20: ln * (f1 / f2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) assume A21: x in Z ; ::_thesis: ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) then A22: ( f2 . x = x + a & f2 . x > 0 ) by A2; A23: ( f1 . x = x - a & f2 . x = x + a ) by A2, A21; A24: x in dom (f1 / f2) by A1, A21, FUNCT_1:11; ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A11, A16, A21, FDIFF_1:9; then diff ((ln * (f1 / f2)),x) = (diff ((f1 / f2),x)) / ((f1 / f2) . x) by TAYLOR_1:20 .= (((f1 / f2) `| Z) . x) / ((f1 / f2) . x) by A11, A21, FDIFF_1:def_7 .= ((2 * a) / ((x + a) ^2)) / ((f1 / f2) . x) by A12, A21 .= ((2 * a) / ((x + a) ^2)) / ((f1 . x) * ((f2 . x) ")) by A24, RFUNCT_1:def_1 .= ((2 * a) / ((x + a) * (x + a))) / ((x - a) / (x + a)) by A23, XCMPLX_0:def_9 .= (((2 * a) / (x + a)) / (x + a)) / ((x - a) / (x + a)) by XCMPLX_1:78 .= (((2 * a) / (x + a)) / ((x - a) / (x + a))) / (x + a) by XCMPLX_1:48 .= ((2 * a) / (x - a)) / (x + a) by A22, XCMPLX_1:55 .= (2 * a) / ((x - a) * (x + a)) by XCMPLX_1:78 .= (2 * a) / ((x ^2) - (a ^2)) ; hence ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) by A20, A21, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (2 * a) / ((x ^2) - (a ^2)) ) ) by A1, A19, FDIFF_1:9; ::_thesis: verum end; theorem Th24: :: FDIFF_4:24 for a, b being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 / f2)) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) ) assume that A1: Z c= dom (ln * (f1 / f2)) and A2: for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ; ::_thesis: ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) A3: for x being Real st x in Z holds ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) proof let x be Real; ::_thesis: ( x in Z implies ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) ) A4: ( (1 * x) + (- a) = (1 * x) - a & (1 * x) + (- b) = (1 * x) - b ) ; assume x in Z ; ::_thesis: ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) hence ( f1 . x = (1 * x) + (- a) & f2 . x = (1 * x) + (- b) ) by A2, A4; ::_thesis: verum end; then A5: for x being Real st x in Z holds f1 . x = (1 * x) + (- a) ; for y being set st y in Z holds y in dom (f1 / f2) by A1, FUNCT_1:11; then Z c= dom (f1 / f2) by TARSKI:def_3; then A6: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def_1; then A7: Z c= dom f1 by XBOOLE_1:18; then A8: f1 is_differentiable_on Z by A5, FDIFF_1:23; A9: for x being Real st x in Z holds f2 . x = (1 * x) + (- b) by A3; A10: Z c= dom f2 by A6, XBOOLE_1:1; then A11: f2 is_differentiable_on Z by A9, FDIFF_1:23; for x being Real st x in Z holds f2 . x <> 0 by A2; then A12: f1 / f2 is_differentiable_on Z by A8, A11, FDIFF_2:21; A13: for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) assume A14: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) then A15: f2 . x <> 0 by A2; A16: ( f1 . x = x - a & f2 . x = x - b ) by A2, A14; ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A8, A11, A14, FDIFF_1:9; then diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A15, FDIFF_2:14 .= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A8, A14, FDIFF_1:def_7 .= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A11, A14, FDIFF_1:def_7 .= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A7, A5, A14, FDIFF_1:23 .= ((1 * (f2 . x)) - (1 * (f1 . x))) / ((f2 . x) ^2) by A10, A9, A14, FDIFF_1:23 .= (a - b) / ((x - b) ^2) by A16 ; hence ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) by A12, A14, FDIFF_1:def_7; ::_thesis: verum end; A17: for x being Real st x in Z holds (f1 / f2) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (f1 / f2) . x > 0 ) assume A18: x in Z ; ::_thesis: (f1 / f2) . x > 0 then x in dom (f1 / f2) by A1, FUNCT_1:11; then A19: (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by RFUNCT_1:def_1 .= (f1 . x) / (f2 . x) by XCMPLX_0:def_9 ; ( f1 . x > 0 & f2 . x > 0 ) by A2, A18; hence (f1 / f2) . x > 0 by A19, XREAL_1:139; ::_thesis: verum end; A20: for x being Real st x in Z holds ln * (f1 / f2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 / f2) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 / f2) is_differentiable_in x then ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A12, A17, FDIFF_1:9; hence ln * (f1 / f2) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A21: ln * (f1 / f2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) assume A22: x in Z ; ::_thesis: ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) then A23: ( f2 . x = x - b & f2 . x > 0 ) by A2; A24: ( f1 . x = x - a & f2 . x = x - b ) by A2, A22; A25: x in dom (f1 / f2) by A1, A22, FUNCT_1:11; ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A12, A17, A22, FDIFF_1:9; then diff ((ln * (f1 / f2)),x) = (diff ((f1 / f2),x)) / ((f1 / f2) . x) by TAYLOR_1:20 .= (((f1 / f2) `| Z) . x) / ((f1 / f2) . x) by A12, A22, FDIFF_1:def_7 .= ((a - b) / ((x - b) ^2)) / ((f1 / f2) . x) by A13, A22 .= ((a - b) / ((x - b) ^2)) / ((f1 . x) * ((f2 . x) ")) by A25, RFUNCT_1:def_1 .= ((a - b) / ((x - b) * (x - b))) / ((x - a) / (x - b)) by A24, XCMPLX_0:def_9 .= (((a - b) / (x - b)) / (x - b)) / ((x - a) / (x - b)) by XCMPLX_1:78 .= (((a - b) / (x - b)) / ((x - a) / (x - b))) / (x - b) by XCMPLX_1:48 .= ((a - b) / (x - a)) / (x - b) by A23, XCMPLX_1:55 .= (a - b) / ((x - a) * (x - b)) by XCMPLX_1:78 ; hence ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) by A21, A22, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = (a - b) / ((x - a) * (x - b)) ) ) by A1, A20, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:25 for a, b being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) holds ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((1 / (a - b)) (#) f) & f = ln * (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ) implies ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) ) assume that A1: Z c= dom ((1 / (a - b)) (#) f) and A2: f = ln * (f1 / f2) and A3: for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 & a - b <> 0 ) ; ::_thesis: ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) A4: ( ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x = x - b & f2 . x > 0 ) ) & Z c= dom f ) by A1, A3, VALUED_1:def_5; then A5: f is_differentiable_on Z by A2, Th24; for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) proof let x be Real; ::_thesis: ( x in Z implies (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) assume A6: x in Z ; ::_thesis: (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) then A7: a - b <> 0 by A3; (((1 / (a - b)) (#) f) `| Z) . x = (1 / (a - b)) * (diff (f,x)) by A1, A5, A6, FDIFF_1:20 .= (1 / (a - b)) * ((f `| Z) . x) by A5, A6, FDIFF_1:def_7 .= (1 / (a - b)) * ((a - b) / ((x - a) * (x - b))) by A2, A4, A6, Th24 .= ((1 / (a - b)) * (a - b)) / ((x - a) * (x - b)) by XCMPLX_1:74 .= 1 / ((x - a) * (x - b)) by A7, XCMPLX_1:106 ; hence (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ; ::_thesis: verum end; hence ( (1 / (a - b)) (#) f is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / (a - b)) (#) f) `| Z) . x = 1 / ((x - a) * (x - b)) ) ) by A1, A5, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:26 for a being Real for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) holds ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (f1 / f2)) & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ) implies ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) ) assume that A1: Z c= dom (ln * (f1 / f2)) and A2: f2 = #Z 2 and A3: for x being Real st x in Z holds ( f1 . x = x - a & f1 . x > 0 & f2 . x > 0 & x <> 0 ) ; ::_thesis: ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) A4: for x being Real st x in Z holds f2 is_differentiable_in x by A2, TAYLOR_1:2; for y being set st y in Z holds y in dom (f1 / f2) by A1, FUNCT_1:11; then Z c= dom (f1 / f2) by TARSKI:def_3; then A5: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by RFUNCT_1:def_1; then A6: Z c= dom f1 by XBOOLE_1:18; A7: for x being Real st x in Z holds f1 . x = (1 * x) + (- a) proof let x be Real; ::_thesis: ( x in Z implies f1 . x = (1 * x) + (- a) ) A8: (1 * x) + (- a) = (1 * x) - a ; assume x in Z ; ::_thesis: f1 . x = (1 * x) + (- a) hence f1 . x = (1 * x) + (- a) by A3, A8; ::_thesis: verum end; then A9: f1 is_differentiable_on Z by A6, FDIFF_1:23; A10: Z c= dom f2 by A5, XBOOLE_1:1; then A11: f2 is_differentiable_on Z by A4, FDIFF_1:9; for x being Real st x in Z holds f2 . x <> 0 by A3; then A12: f1 / f2 is_differentiable_on Z by A9, A11, FDIFF_2:21; A13: f2 is_differentiable_on Z by A10, A4, FDIFF_1:9; A14: for x being Real st x in Z holds (f2 `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * x ) 2 * (x #Z (2 - 1)) = 2 * x by PREPOWER:35; then A15: diff (f2,x) = 2 * x by A2, TAYLOR_1:2; assume x in Z ; ::_thesis: (f2 `| Z) . x = 2 * x hence (f2 `| Z) . x = 2 * x by A13, A15, FDIFF_1:def_7; ::_thesis: verum end; A16: for x being Real st x in Z holds ((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3) proof let x be Real; ::_thesis: ( x in Z implies ((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3) ) A17: f2 is_differentiable_in x by A2, TAYLOR_1:2; A18: f2 . x = x #Z 2 by A2, TAYLOR_1:def_1 .= x |^ 2 by PREPOWER:36 ; assume A19: x in Z ; ::_thesis: ((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3) then A20: x <> 0 by A3; ( f1 is_differentiable_in x & f2 . x <> 0 ) by A3, A9, A19, FDIFF_1:9; then diff ((f1 / f2),x) = (((diff (f1,x)) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A17, FDIFF_2:14 .= ((((f1 `| Z) . x) * (f2 . x)) - ((diff (f2,x)) * (f1 . x))) / ((f2 . x) ^2) by A9, A19, FDIFF_1:def_7 .= ((((f1 `| Z) . x) * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A11, A19, FDIFF_1:def_7 .= ((1 * (f2 . x)) - (((f2 `| Z) . x) * (f1 . x))) / ((f2 . x) ^2) by A6, A7, A19, FDIFF_1:23 .= ((1 * (f2 . x)) - ((2 * x) * (f1 . x))) / ((f2 . x) ^2) by A14, A19 .= ((x |^ (1 + 1)) - ((2 * x) * (x - a))) / ((x |^ 2) ^2) by A3, A19, A18 .= (((x |^ 1) * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2) by NEWTON:6 .= ((x * x) - ((2 * x) * (x - a))) / ((x |^ 2) ^2) by NEWTON:5 .= (x * ((2 * a) - x)) / (x |^ (2 + 2)) by NEWTON:8 .= (x * ((2 * a) - x)) / (x |^ (3 + 1)) .= (x * ((2 * a) - x)) / ((x |^ 3) * x) by NEWTON:6 .= ((2 * a) - x) / (x |^ 3) by A20, XCMPLX_1:91 ; hence ((f1 / f2) `| Z) . x = ((2 * a) - x) / (x |^ 3) by A12, A19, FDIFF_1:def_7; ::_thesis: verum end; A21: for x being Real st x in Z holds (f1 / f2) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (f1 / f2) . x > 0 ) assume A22: x in Z ; ::_thesis: (f1 / f2) . x > 0 then x in dom (f1 / f2) by A1, FUNCT_1:11; then A23: (f1 / f2) . x = (f1 . x) * ((f2 . x) ") by RFUNCT_1:def_1 .= (f1 . x) / (f2 . x) by XCMPLX_0:def_9 ; ( f1 . x > 0 & f2 . x > 0 ) by A3, A22; hence (f1 / f2) . x > 0 by A23, XREAL_1:139; ::_thesis: verum end; A24: for x being Real st x in Z holds ln * (f1 / f2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (f1 / f2) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (f1 / f2) is_differentiable_in x then ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A12, A21, FDIFF_1:9; hence ln * (f1 / f2) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A25: ln * (f1 / f2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) assume A26: x in Z ; ::_thesis: ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) then A27: x in dom (f1 / f2) by A1, FUNCT_1:11; A28: f2 . x = x #Z 2 by A2, TAYLOR_1:def_1 .= x |^ 2 by PREPOWER:36 ; then A29: x |^ 2 > 0 by A3, A26; A30: f1 . x = x - a by A3, A26; ( f1 / f2 is_differentiable_in x & (f1 / f2) . x > 0 ) by A12, A21, A26, FDIFF_1:9; then diff ((ln * (f1 / f2)),x) = (diff ((f1 / f2),x)) / ((f1 / f2) . x) by TAYLOR_1:20 .= (((f1 / f2) `| Z) . x) / ((f1 / f2) . x) by A12, A26, FDIFF_1:def_7 .= (((2 * a) - x) / (x |^ 3)) / ((f1 / f2) . x) by A16, A26 .= (((2 * a) - x) / (x |^ 3)) / ((f1 . x) * ((f2 . x) ")) by A27, RFUNCT_1:def_1 .= (((2 * a) - x) / (x |^ (2 + 1))) / ((x - a) / (x |^ 2)) by A28, A30, XCMPLX_0:def_9 .= (((2 * a) - x) / ((x |^ 2) * x)) / ((x - a) / (x |^ 2)) by NEWTON:6 .= ((((2 * a) - x) / (x |^ 2)) / x) / ((x - a) / (x |^ 2)) by XCMPLX_1:78 .= ((((2 * a) - x) / (x |^ 2)) / ((x - a) / (x |^ 2))) / x by XCMPLX_1:48 .= (((2 * a) - x) / (x - a)) / x by A29, XCMPLX_1:55 .= ((2 * a) - x) / (x * (x - a)) by XCMPLX_1:78 ; hence ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) by A25, A26, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (f1 / f2) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (f1 / f2)) `| Z) . x = ((2 * a) - x) / (x * (x - a)) ) ) by A1, A24, FDIFF_1:9; ::_thesis: verum end; theorem Th27: :: FDIFF_4:27 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((#R (3 / 2)) * f) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) implies ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) ) assume that A1: Z c= dom ((#R (3 / 2)) * f) and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ; ::_thesis: ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; A4: for x being Real st x in Z holds f . x = (1 * x) + a by A2; then A5: f is_differentiable_on Z by A3, FDIFF_1:23; A6: for x being Real st x in Z holds (#R (3 / 2)) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#R (3 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (3 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A5, FDIFF_1:9; hence (#R (3 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (3 / 2)) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) proof let x be Real; ::_thesis: ( x in Z implies (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) assume A8: x in Z ; ::_thesis: (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) then A9: f . x = a + x by A2; ( f is_differentiable_in x & f . x > 0 ) by A2, A5, A8, FDIFF_1:9; then diff (((#R (3 / 2)) * f),x) = ((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * (diff (f,x)) by TAYLOR_1:22 .= ((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x) by A5, A8, FDIFF_1:def_7 .= ((3 / 2) * ((a + x) #R ((3 / 2) - 1))) * 1 by A3, A4, A8, A9, FDIFF_1:23 .= (3 / 2) * ((a + x) #R (1 / 2)) ; hence (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) by A7, A8, FDIFF_1:def_7; ::_thesis: verum end; hence ( (#R (3 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (3 / 2)) * f) `| Z) . x = (3 / 2) * ((a + x) #R (1 / 2)) ) ) by A1, A6, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:28 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) implies ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) ) assume that A1: Z c= dom ((2 / 3) (#) ((#R (3 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ; ::_thesis: ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) A3: Z c= dom ((#R (3 / 2)) * f) by A1, VALUED_1:def_5; then A4: (#R (3 / 2)) * f is_differentiable_on Z by A2, Th27; for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) proof let x be Real; ::_thesis: ( x in Z implies (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) assume A5: x in Z ; ::_thesis: (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) hence (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (2 / 3) * (diff (((#R (3 / 2)) * f),x)) by A1, A4, FDIFF_1:20 .= (2 / 3) * ((((#R (3 / 2)) * f) `| Z) . x) by A4, A5, FDIFF_1:def_7 .= (2 / 3) * ((3 / 2) * ((a + x) #R (1 / 2))) by A2, A3, A5, Th27 .= (a + x) #R (1 / 2) ; ::_thesis: verum end; hence ( (2 / 3) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / 3) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + x) #R (1 / 2) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:29 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) implies ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) ) assume that A1: Z c= dom ((- (2 / 3)) (#) ((#R (3 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ; ::_thesis: ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) A3: Z c= dom ((#R (3 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = ((- 1) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f . x = ((- 1) * x) + a ) assume x in Z ; ::_thesis: f . x = ((- 1) * x) + a then f . x = a - x by A2; hence f . x = ((- 1) * x) + a ; ::_thesis: verum end; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(3_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (3 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (3 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence (#R (3 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (3 / 2)) * f is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) proof let x be Real; ::_thesis: ( x in Z implies (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) assume A8: x in Z ; ::_thesis: (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) then A9: f . x = a - x by A2; A10: ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A8, FDIFF_1:9; (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (- (2 / 3)) * (diff (((#R (3 / 2)) * f),x)) by A1, A7, A8, FDIFF_1:20 .= (- (2 / 3)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * (diff (f,x))) by A10, TAYLOR_1:22 .= (- (2 / 3)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= (- (2 / 3)) * (((3 / 2) * ((a - x) #R ((3 / 2) - 1))) * (- 1)) by A4, A5, A8, A9, FDIFF_1:23 .= (a - x) #R (1 / 2) ; hence (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ; ::_thesis: verum end; hence ( (- (2 / 3)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / 3)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - x) #R (1 / 2) ) ) by A1, A7, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:30 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (2 (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ) implies ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) ) assume that A1: Z c= dom (2 (#) ((#R (1 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a + x & f . x > 0 ) ; ::_thesis: ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) A3: Z c= dom ((#R (1 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = (1 * x) + a by A2; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(1_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (1 / 2)) * f is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) proof let x be Real; ::_thesis: ( x in Z implies ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) assume A8: x in Z ; ::_thesis: ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) then A9: f . x = a + x by A2; A10: ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A8, FDIFF_1:9; ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = 2 * (diff (((#R (1 / 2)) * f),x)) by A1, A7, A8, FDIFF_1:20 .= 2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x))) by A10, TAYLOR_1:22 .= 2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= 2 * (((1 / 2) * ((a + x) #R ((1 / 2) - 1))) * 1) by A4, A5, A8, A9, FDIFF_1:23 .= (a + x) #R (- (1 / 2)) ; hence ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ; ::_thesis: verum end; hence ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = (a + x) #R (- (1 / 2)) ) ) by A1, A7, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:31 for a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) holds ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ) implies ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) ) assume that A1: Z c= dom ((- 2) (#) ((#R (1 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a - x & f . x > 0 ) ; ::_thesis: ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) A3: Z c= dom ((#R (1 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = ((- 1) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f . x = ((- 1) * x) + a ) assume x in Z ; ::_thesis: f . x = ((- 1) * x) + a then f . x = a - x by A2; hence f . x = ((- 1) * x) + a ; ::_thesis: verum end; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(1_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (1 / 2)) * f is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) proof let x be Real; ::_thesis: ( x in Z implies (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) assume A8: x in Z ; ::_thesis: (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) then A9: f . x = a - x by A2; A10: ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A8, FDIFF_1:9; (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (- 2) * (diff (((#R (1 / 2)) * f),x)) by A1, A7, A8, FDIFF_1:20 .= (- 2) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x))) by A10, TAYLOR_1:22 .= (- 2) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= (- 2) * (((1 / 2) * ((a - x) #R ((1 / 2) - 1))) * (- 1)) by A4, A5, A8, A9, FDIFF_1:23 .= (a - x) #R (- (1 / 2)) ; hence (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ; ::_thesis: verum end; hence ( (- 2) (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- 2) (#) ((#R (1 / 2)) * f)) `| Z) . x = (a - x) #R (- (1 / 2)) ) ) by A1, A7, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:32 for b, a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) holds ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) proof let b, a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) holds ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) holds ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ) implies ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) ) assume that A1: Z c= dom ((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a + (b * x) & b <> 0 & f . x > 0 ) ; ::_thesis: ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) A3: Z c= dom ((#R (3 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = (b * x) + a by A2; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(3_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (3 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (3 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence (#R (3 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (3 / 2)) * f is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) proof let x be Real; ::_thesis: ( x in Z implies (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) assume A8: x in Z ; ::_thesis: (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) then A9: 3 * b <> 0 by A2; A10: f . x = a + (b * x) by A2, A8; A11: ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A8, FDIFF_1:9; (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (2 / (3 * b)) * (diff (((#R (3 / 2)) * f),x)) by A1, A7, A8, FDIFF_1:20 .= (2 / (3 * b)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * (diff (f,x))) by A11, TAYLOR_1:22 .= (2 / (3 * b)) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= (2 / (3 * b)) * (((3 / 2) * ((a + (b * x)) #R ((3 / 2) - 1))) * b) by A4, A5, A8, A10, FDIFF_1:23 .= ((2 / (3 * b)) * ((3 * b) / 2)) * ((a + (b * x)) #R ((3 / 2) - 1)) .= 1 * ((a + (b * x)) #R ((3 / 2) - 1)) by A9, XCMPLX_1:112 .= (a + (b * x)) #R (1 / 2) ; hence (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ; ::_thesis: verum end; hence ( (2 / (3 * b)) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((2 / (3 * b)) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a + (b * x)) #R (1 / 2) ) ) by A1, A7, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:33 for b, a being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) holds ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) proof let b, a be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) holds ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) holds ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) & ( for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ) implies ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) ) assume that A1: Z c= dom ((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) and A2: for x being Real st x in Z holds ( f . x = a - (b * x) & b <> 0 & f . x > 0 ) ; ::_thesis: ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) A3: Z c= dom ((#R (3 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A4: Z c= dom f by TARSKI:def_3; A5: for x being Real st x in Z holds f . x = ((- b) * x) + a proof let x be Real; ::_thesis: ( x in Z implies f . x = ((- b) * x) + a ) assume x in Z ; ::_thesis: f . x = ((- b) * x) + a then f . x = a - (b * x) by A2; hence f . x = ((- b) * x) + a ; ::_thesis: verum end; then A6: f is_differentiable_on Z by A4, FDIFF_1:23; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(3_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (3 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (3 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A6, FDIFF_1:9; hence (#R (3 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A7: (#R (3 / 2)) * f is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) proof let x be Real; ::_thesis: ( x in Z implies (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) assume A8: x in Z ; ::_thesis: (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) then A9: 3 * b <> 0 by A2; A10: f . x = a - (b * x) by A2, A8; A11: ( f is_differentiable_in x & f . x > 0 ) by A2, A6, A8, FDIFF_1:9; (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (- (2 / (3 * b))) * (diff (((#R (3 / 2)) * f),x)) by A1, A7, A8, FDIFF_1:20 .= (- (2 / (3 * b))) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * (diff (f,x))) by A11, TAYLOR_1:22 .= (- (2 / (3 * b))) * (((3 / 2) * ((f . x) #R ((3 / 2) - 1))) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= (- (2 / (3 * b))) * (((3 / 2) * ((a - (b * x)) #R ((3 / 2) - 1))) * (- b)) by A4, A5, A8, A10, FDIFF_1:23 .= ((2 / (3 * b)) * ((3 * b) / 2)) * ((a - (b * x)) #R ((3 / 2) - 1)) .= 1 * ((a - (b * x)) #R ((3 / 2) - 1)) by A9, XCMPLX_1:112 .= (a - (b * x)) #R (1 / 2) ; hence (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ; ::_thesis: verum end; hence ( (- (2 / (3 * b))) (#) ((#R (3 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds (((- (2 / (3 * b))) (#) ((#R (3 / 2)) * f)) `| Z) . x = (a - (b * x)) #R (1 / 2) ) ) by A1, A7, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:34 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((#R (1 / 2)) * f) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) implies ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) ) assume that A1: Z c= dom ((#R (1 / 2)) * f) and A2: f = f1 + f2 and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ; ::_thesis: ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A5: Z c= dom (f1 + f2) by A2, TARSKI:def_3; A6: for x being Real st x in Z holds f1 . x = a ^2 by A4; then A7: f is_differentiable_on Z by A2, A3, A5, Th17; A8: for x being Real st x in Z holds (#R (1 / 2)) * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A4, A7, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A9: (#R (1 / 2)) * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) proof let x be Real; ::_thesis: ( x in Z implies (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) assume A10: x in Z ; ::_thesis: (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) then x in dom (f1 + f2) by A1, A2, FUNCT_1:11; then A11: (f1 + f2) . x = (f1 . x) + (f2 . x) by VALUED_1:def_1 .= (a ^2) + (f2 . x) by A4, A10 .= (a ^2) + (x #Z 2) by A3, TAYLOR_1:def_1 .= (a ^2) + (x |^ 2) by PREPOWER:36 ; ( f is_differentiable_in x & f . x > 0 ) by A4, A7, A10, FDIFF_1:9; then diff (((#R (1 / 2)) * f),x) = ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x)) by TAYLOR_1:22 .= ((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x) by A7, A10, FDIFF_1:def_7 .= ((1 / 2) * (((a ^2) + (x |^ 2)) #R ((1 / 2) - 1))) * (2 * x) by A2, A3, A5, A6, A10, A11, Th17 .= x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ; hence (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) by A9, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( (#R (1 / 2)) * f is_differentiable_on Z & ( for x being Real st x in Z holds (((#R (1 / 2)) * f) `| Z) . x = x * (((a ^2) + (x |^ 2)) #R (- (1 / 2))) ) ) by A1, A8, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:35 for a being Real for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) proof let a be Real; ::_thesis: for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) holds ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (- ((#R (1 / 2)) * f)) & f = f1 - f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ) implies ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) ) assume that A1: Z c= dom (- ((#R (1 / 2)) * f)) and A2: f = f1 - f2 and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds ( f1 . x = a ^2 & f . x > 0 ) ; ::_thesis: ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) A5: for x being Real st x in Z holds f1 . x = (a ^2) + (0 * x) by A4; A6: Z c= dom ((#R (1 / 2)) * f) by A1, VALUED_1:8; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A7: Z c= dom (f1 + ((- 1) (#) f2)) by A2, TARSKI:def_3; then A8: f is_differentiable_on Z by A2, A3, A5, Th12; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(1_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A4, A8, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A9: (#R (1 / 2)) * f is_differentiable_on Z by A6, FDIFF_1:9; for x being Real st x in Z holds (((- 1) (#) ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) proof let x be Real; ::_thesis: ( x in Z implies (((- 1) (#) ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) assume A10: x in Z ; ::_thesis: (((- 1) (#) ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) then A11: ( f is_differentiable_in x & f . x > 0 ) by A4, A8, FDIFF_1:9; x in dom (f1 - f2) by A2, A6, A10, FUNCT_1:11; then A12: (f1 - f2) . x = (f1 . x) - (f2 . x) by VALUED_1:13 .= (a ^2) - (f2 . x) by A4, A10 .= (a ^2) - (x #Z 2) by A3, TAYLOR_1:def_1 .= (a ^2) - (x |^ 2) by PREPOWER:36 ; (((- 1) (#) ((#R (1 / 2)) * f)) `| Z) . x = (- 1) * (diff (((#R (1 / 2)) * f),x)) by A1, A9, A10, FDIFF_1:20 .= (- 1) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x))) by A11, TAYLOR_1:22 .= (- 1) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A8, A10, FDIFF_1:def_7 .= (- 1) * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (0 + ((2 * (- 1)) * x))) by A2, A3, A7, A5, A10, Th12 .= x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) by A2, A12 ; hence (((- 1) (#) ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ; ::_thesis: verum end; hence ( - ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((- ((#R (1 / 2)) * f)) `| Z) . x = x * (((a ^2) - (x |^ 2)) #R (- (1 / 2))) ) ) by A1, A9, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:36 for Z being open Subset of REAL for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) proof let Z be open Subset of REAL; ::_thesis: for f, f1, f2 being PartFunc of REAL,REAL st Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x & f . x > 0 ) ) holds ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) let f, f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (2 (#) ((#R (1 / 2)) * f)) & f = f1 + f2 & f2 = #Z 2 & ( for x being Real st x in Z holds ( f1 . x = x & f . x > 0 ) ) implies ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) ) assume that A1: Z c= dom (2 (#) ((#R (1 / 2)) * f)) and A2: f = f1 + f2 and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds ( f1 . x = x & f . x > 0 ) ; ::_thesis: ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) A5: for x being Real st x in Z holds f1 . x = 0 + (1 * x) by A4; A6: f2 = 1 (#) f2 by RFUNCT_1:21; A7: Z c= dom ((#R (1 / 2)) * f) by A1, VALUED_1:def_5; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A8: Z c= dom (f1 + (1 (#) f2)) by A2, A6, TARSKI:def_3; then A9: f1 + f2 is_differentiable_on Z by A3, A6, A5, Th12; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(1_/_2))_*_f_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * f is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * f is_differentiable_in x then ( f is_differentiable_in x & f . x > 0 ) by A2, A4, A9, FDIFF_1:9; hence (#R (1 / 2)) * f is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; then A10: (#R (1 / 2)) * f is_differentiable_on Z by A7, FDIFF_1:9; A11: for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 1 + ((2 * 1) * x) by A3, A6, A8, A5, Th12; for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) proof let x be Real; ::_thesis: ( x in Z implies ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) assume A12: x in Z ; ::_thesis: ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) then A13: ( f is_differentiable_in x & f . x > 0 ) by A2, A4, A9, FDIFF_1:9; x in dom (f1 + f2) by A2, A7, A12, FUNCT_1:11; then A14: (f1 + f2) . x = (f1 . x) + (f2 . x) by VALUED_1:def_1 .= x + (f2 . x) by A4, A12 .= x + (x #Z 2) by A3, TAYLOR_1:def_1 .= x + (x |^ 2) by PREPOWER:36 ; ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = 2 * (diff (((#R (1 / 2)) * f),x)) by A1, A10, A12, FDIFF_1:20 .= 2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * (diff (f,x))) by A13, TAYLOR_1:22 .= 2 * (((1 / 2) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x)) by A2, A9, A12, FDIFF_1:def_7 .= ((2 * (1 / 2)) * ((f . x) #R ((1 / 2) - 1))) * ((f `| Z) . x) .= ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) by A2, A11, A12, A14 ; hence ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ; ::_thesis: verum end; hence ( 2 (#) ((#R (1 / 2)) * f) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * f)) `| Z) . x = ((2 * x) + 1) * (((x |^ 2) + x) #R (- (1 / 2))) ) ) by A1, A10, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:37 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (sin * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (sin * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) ) assume that A1: Z c= dom (sin * f) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; then A4: f is_differentiable_on Z by A2, FDIFF_1:23; A5: for x being Real st x in Z holds sin * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * f is_differentiable_in x ) assume x in Z ; ::_thesis: sin * f is_differentiable_in x then A6: f is_differentiable_in x by A4, FDIFF_1:9; sin is_differentiable_in f . x by SIN_COS:64; hence sin * f is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: sin * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) A8: sin is_differentiable_in f . x by SIN_COS:64; assume A9: x in Z ; ::_thesis: ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) then f is_differentiable_in x by A4, FDIFF_1:9; then diff ((sin * f),x) = (diff (sin,(f . x))) * (diff (f,x)) by A8, FDIFF_2:13 .= (cos . (f . x)) * (diff (f,x)) by SIN_COS:64 .= (cos . ((a * x) + b)) * (diff (f,x)) by A2, A9 .= (cos . ((a * x) + b)) * ((f `| Z) . x) by A4, A9, FDIFF_1:def_7 .= a * (cos . ((a * x) + b)) by A2, A3, A9, FDIFF_1:23 ; hence ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) by A7, A9, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * f is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * f) `| Z) . x = a * (cos . ((a * x) + b)) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:38 for a, b being Real for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) proof let a, b be Real; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (cos * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) holds ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (cos * f) & ( for x being Real st x in Z holds f . x = (a * x) + b ) implies ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) ) assume that A1: Z c= dom (cos * f) and A2: for x being Real st x in Z holds f . x = (a * x) + b ; ::_thesis: ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) for y being set st y in Z holds y in dom f by A1, FUNCT_1:11; then A3: Z c= dom f by TARSKI:def_3; then A4: f is_differentiable_on Z by A2, FDIFF_1:23; A5: for x being Real st x in Z holds cos * f is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * f is_differentiable_in x ) assume x in Z ; ::_thesis: cos * f is_differentiable_in x then A6: f is_differentiable_in x by A4, FDIFF_1:9; cos is_differentiable_in f . x by SIN_COS:63; hence cos * f is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: cos * f is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) A8: diff (cos,(f . x)) = - (sin . (f . x)) by SIN_COS:63; A9: cos is_differentiable_in f . x by SIN_COS:63; assume A10: x in Z ; ::_thesis: ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) then f is_differentiable_in x by A4, FDIFF_1:9; then diff ((cos * f),x) = (diff (cos,(f . x))) * (diff (f,x)) by A9, FDIFF_2:13 .= - ((sin . (f . x)) * (diff (f,x))) by A8 .= - ((sin . ((a * x) + b)) * (diff (f,x))) by A2, A10 .= - ((sin . ((a * x) + b)) * ((f `| Z) . x)) by A4, A10, FDIFF_1:def_7 .= - (a * (sin . ((a * x) + b))) by A2, A3, A10, FDIFF_1:23 ; hence ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) by A7, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * f is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * f) `| Z) . x = - (a * (sin . ((a * x) + b))) ) ) by A1, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:39 for Z being open Subset of REAL st ( for x being Real st x in Z holds cos . x <> 0 ) holds ( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) proof let Z be open Subset of REAL; ::_thesis: ( ( for x being Real st x in Z holds cos . x <> 0 ) implies ( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) ) assume A1: for x being Real st x in Z holds cos . x <> 0 ; ::_thesis: ( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) A2: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; then A3: cos ^ is_differentiable_on Z by A1, FDIFF_2:22; for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) A4: cos is_differentiable_in x by SIN_COS:63; assume A5: x in Z ; ::_thesis: ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) then A6: cos . x <> 0 by A1; ((cos ^) `| Z) . x = diff ((cos ^),x) by A3, A5, FDIFF_1:def_7 .= - ((diff (cos,x)) / ((cos . x) ^2)) by A6, A4, FDIFF_2:15 .= - ((- (sin . x)) / ((cos . x) ^2)) by SIN_COS:63 .= - (- ((sin . x) / ((cos . x) ^2))) by XCMPLX_1:187 .= (sin . x) / ((cos . x) ^2) ; hence ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ; ::_thesis: verum end; hence ( cos ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((cos ^) `| Z) . x = (sin . x) / ((cos . x) ^2) ) ) by A1, A2, FDIFF_2:22; ::_thesis: verum end; theorem :: FDIFF_4:40 for Z being open Subset of REAL st ( for x being Real st x in Z holds sin . x <> 0 ) holds ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( ( for x being Real st x in Z holds sin . x <> 0 ) implies ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) ) A1: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; assume A2: for x being Real st x in Z holds sin . x <> 0 ; ::_thesis: ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) then A3: sin ^ is_differentiable_on Z by A1, FDIFF_2:22; for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) proof let x be Real; ::_thesis: ( x in Z implies ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) assume A4: x in Z ; ::_thesis: ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) then A5: ( sin . x <> 0 & sin is_differentiable_in x ) by A2, A1, FDIFF_1:9; ((sin ^) `| Z) . x = diff ((sin ^),x) by A3, A4, FDIFF_1:def_7 .= - ((diff (sin,x)) / ((sin . x) ^2)) by A5, FDIFF_2:15 .= - ((cos . x) / ((sin . x) ^2)) by SIN_COS:64 ; hence ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ; ::_thesis: verum end; hence ( sin ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((sin ^) `| Z) . x = - ((cos . x) / ((sin . x) ^2)) ) ) by A2, A1, FDIFF_2:22; ::_thesis: verum end; theorem :: FDIFF_4:41 for Z being open Subset of REAL st Z c= dom (sin (#) cos) holds ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = cos (2 * x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin (#) cos) implies ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = cos (2 * x) ) ) ) A1: ( sin is_differentiable_on Z & cos is_differentiable_on Z ) by FDIFF_1:26, SIN_COS:67, SIN_COS:68; assume A2: Z c= dom (sin (#) cos) ; ::_thesis: ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = cos (2 * x) ) ) now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_(#)_cos)_`|_Z)_._x_=_cos_(2_*_x) let x be Real; ::_thesis: ( x in Z implies ((sin (#) cos) `| Z) . x = cos (2 * x) ) assume x in Z ; ::_thesis: ((sin (#) cos) `| Z) . x = cos (2 * x) hence ((sin (#) cos) `| Z) . x = ((cos . x) * (diff (sin,x))) + ((sin . x) * (diff (cos,x))) by A2, A1, FDIFF_1:21 .= ((cos . x) * (cos . x)) + ((sin . x) * (diff (cos,x))) by SIN_COS:64 .= ((cos . x) * (cos . x)) + ((sin . x) * (- (sin . x))) by SIN_COS:63 .= ((cos . x) ^2) - ((sin . x) * (sin . x)) .= ((cos x) ^2) - ((sin . x) ^2) by SIN_COS:def_19 .= ((cos x) ^2) - ((sin x) ^2) by SIN_COS:def_17 .= cos (2 * x) by SIN_COS5:7 ; ::_thesis: verum end; hence ( sin (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds ((sin (#) cos) `| Z) . x = cos (2 * x) ) ) by A2, A1, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_4:42 for Z being open Subset of REAL st Z c= dom (ln * cos) & ( for x being Real st x in Z holds cos . x > 0 ) holds ( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * cos) & ( for x being Real st x in Z holds cos . x > 0 ) implies ( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) ) ) ) assume that A1: Z c= dom (ln * cos) and A2: for x being Real st x in Z holds cos . x > 0 ; ::_thesis: ( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) ) ) A3: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; A4: for x being Real st x in Z holds ln * cos is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * cos is_differentiable_in x ) assume x in Z ; ::_thesis: ln * cos is_differentiable_in x then ( cos is_differentiable_in x & cos . x > 0 ) by A2, A3, FDIFF_1:9; hence ln * cos is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A5: ln * cos is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) proof let x be Real; ::_thesis: ( x in Z implies ((ln * cos) `| Z) . x = - (tan x) ) assume A6: x in Z ; ::_thesis: ((ln * cos) `| Z) . x = - (tan x) then ( cos is_differentiable_in x & cos . x > 0 ) by A2, A3, FDIFF_1:9; then diff ((ln * cos),x) = (diff (cos,x)) / (cos . x) by TAYLOR_1:20 .= (- (sin . x)) / (cos . x) by SIN_COS:63 .= - ((sin . x) / (cos . x)) by XCMPLX_1:187 .= - ((sin x) / (cos . x)) by SIN_COS:def_17 .= - ((sin x) / (cos x)) by SIN_COS:def_19 .= - (tan x) by SIN_COS4:def_1 ; hence ((ln * cos) `| Z) . x = - (tan x) by A5, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * cos is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * cos) `| Z) . x = - (tan x) ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:43 for Z being open Subset of REAL st Z c= dom (ln * sin) & ( for x being Real st x in Z holds sin . x > 0 ) holds ( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln * sin) & ( for x being Real st x in Z holds sin . x > 0 ) implies ( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x ) ) ) assume that A1: Z c= dom (ln * sin) and A2: for x being Real st x in Z holds sin . x > 0 ; ::_thesis: ( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x ) ) A3: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; A4: for x being Real st x in Z holds ln * sin is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * sin is_differentiable_in x ) assume x in Z ; ::_thesis: ln * sin is_differentiable_in x then ( sin is_differentiable_in x & sin . x > 0 ) by A2, A3, FDIFF_1:9; hence ln * sin is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A5: ln * sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x proof let x be Real; ::_thesis: ( x in Z implies ((ln * sin) `| Z) . x = cot x ) assume A6: x in Z ; ::_thesis: ((ln * sin) `| Z) . x = cot x then ( sin is_differentiable_in x & sin . x > 0 ) by A2, A3, FDIFF_1:9; then diff ((ln * sin),x) = (diff (sin,x)) / (sin . x) by TAYLOR_1:20 .= (cos . x) / (sin . x) by SIN_COS:64 .= (cos x) / (sin . x) by SIN_COS:def_19 .= (cos x) / (sin x) by SIN_COS:def_17 .= cot x by SIN_COS4:def_2 ; hence ((ln * sin) `| Z) . x = cot x by A5, A6, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * sin is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * sin) `| Z) . x = cot x ) ) by A1, A4, FDIFF_1:9; ::_thesis: verum end; theorem Th44: :: FDIFF_4:44 for Z being open Subset of REAL st Z c= dom ((- (id Z)) (#) cos) holds ( (- (id Z)) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- (id Z)) (#) cos) implies ( (- (id Z)) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) ) ) A1: for x being Real st x in Z holds (- (id Z)) . x = ((- 1) * x) + 0 proof let x be Real; ::_thesis: ( x in Z implies (- (id Z)) . x = ((- 1) * x) + 0 ) assume A2: x in Z ; ::_thesis: (- (id Z)) . x = ((- 1) * x) + 0 (- (id Z)) . x = - ((id Z) . x) by VALUED_1:8 .= - x by A2, FUNCT_1:18 .= ((- 1) * x) + 0 ; hence (- (id Z)) . x = ((- 1) * x) + 0 ; ::_thesis: verum end; assume A3: Z c= dom ((- (id Z)) (#) cos) ; ::_thesis: ( (- (id Z)) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) ) then Z c= (dom (- (id Z))) /\ (dom cos) by VALUED_1:def_4; then A4: Z c= dom (- (id Z)) by XBOOLE_1:18; then A5: - (id Z) is_differentiable_on Z by A1, FDIFF_1:23; A6: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((-_(id_Z))_(#)_cos)_`|_Z)_._x_=_(-_(cos_._x))_+_(x_*_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) assume A7: x in Z ; ::_thesis: (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) hence (((- (id Z)) (#) cos) `| Z) . x = ((cos . x) * (diff ((- (id Z)),x))) + (((- (id Z)) . x) * (diff (cos,x))) by A3, A5, A6, FDIFF_1:21 .= ((cos . x) * (((- (id Z)) `| Z) . x)) + (((- (id Z)) . x) * (diff (cos,x))) by A5, A7, FDIFF_1:def_7 .= ((cos . x) * (- 1)) + (((- (id Z)) . x) * (diff (cos,x))) by A4, A1, A7, FDIFF_1:23 .= ((cos . x) * (- 1)) + (((- (id Z)) . x) * (- (sin . x))) by SIN_COS:63 .= (- (cos . x)) + ((((- 1) * x) + 0) * (- (sin . x))) by A1, A7 .= (- (cos . x)) + (x * (sin . x)) ; ::_thesis: verum end; hence ( (- (id Z)) (#) cos is_differentiable_on Z & ( for x being Real st x in Z holds (((- (id Z)) (#) cos) `| Z) . x = (- (cos . x)) + (x * (sin . x)) ) ) by A3, A5, A6, FDIFF_1:21; ::_thesis: verum end; theorem Th45: :: FDIFF_4:45 for Z being open Subset of REAL st Z c= dom ((id Z) (#) sin) holds ( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) sin) implies ( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) ) ) ) A1: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; assume A2: Z c= dom ((id Z) (#) sin) ; ::_thesis: ( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) ) ) then Z c= (dom (id Z)) /\ (dom sin) by VALUED_1:def_4; then A3: Z c= dom (id Z) by XBOOLE_1:18; then A4: id Z is_differentiable_on Z by A1, FDIFF_1:23; A5: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((id_Z)_(#)_sin)_`|_Z)_._x_=_(sin_._x)_+_(x_*_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) ) assume A6: x in Z ; ::_thesis: (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) hence (((id Z) (#) sin) `| Z) . x = ((sin . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff (sin,x))) by A2, A4, A5, FDIFF_1:21 .= ((sin . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff (sin,x))) by A4, A6, FDIFF_1:def_7 .= ((sin . x) * 1) + (((id Z) . x) * (diff (sin,x))) by A3, A1, A6, FDIFF_1:23 .= ((sin . x) * 1) + (((id Z) . x) * (cos . x)) by SIN_COS:64 .= (sin . x) + (x * (cos . x)) by A6, FUNCT_1:18 ; ::_thesis: verum end; hence ( (id Z) (#) sin is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) sin) `| Z) . x = (sin . x) + (x * (cos . x)) ) ) by A2, A4, A5, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_4:46 for Z being open Subset of REAL st Z c= dom (((- (id Z)) (#) cos) + sin) holds ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((- (id Z)) (#) cos) + sin) implies ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) ) assume A1: Z c= dom (((- (id Z)) (#) cos) + sin) ; ::_thesis: ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) then Z c= (dom ((- (id Z)) (#) cos)) /\ (dom sin) by VALUED_1:def_1; then A2: Z c= dom ((- (id Z)) (#) cos) by XBOOLE_1:18; then A3: (- (id Z)) (#) cos is_differentiable_on Z by Th44; A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((-_(id_Z))_(#)_cos)_+_sin)_`|_Z)_._x_=_x_*_(sin_._x) let x be Real; ::_thesis: ( x in Z implies ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) assume A5: x in Z ; ::_thesis: ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) hence ((((- (id Z)) (#) cos) + sin) `| Z) . x = (diff (((- (id Z)) (#) cos),x)) + (diff (sin,x)) by A1, A3, A4, FDIFF_1:18 .= ((((- (id Z)) (#) cos) `| Z) . x) + (diff (sin,x)) by A3, A5, FDIFF_1:def_7 .= ((- (cos . x)) + (x * (sin . x))) + (diff (sin,x)) by A2, A5, Th44 .= ((- (cos . x)) + (x * (sin . x))) + (cos . x) by SIN_COS:64 .= x * (sin . x) ; ::_thesis: verum end; hence ( ((- (id Z)) (#) cos) + sin is_differentiable_on Z & ( for x being Real st x in Z holds ((((- (id Z)) (#) cos) + sin) `| Z) . x = x * (sin . x) ) ) by A1, A3, A4, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:47 for Z being open Subset of REAL st Z c= dom (((id Z) (#) sin) + cos) holds ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) (#) sin) + cos) implies ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) ) assume A1: Z c= dom (((id Z) (#) sin) + cos) ; ::_thesis: ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) then Z c= (dom ((id Z) (#) sin)) /\ (dom cos) by VALUED_1:def_1; then A2: Z c= dom ((id Z) (#) sin) by XBOOLE_1:18; then A3: (id Z) (#) sin is_differentiable_on Z by Th45; A4: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((id_Z)_(#)_sin)_+_cos)_`|_Z)_._x_=_x_*_(cos_._x) let x be Real; ::_thesis: ( x in Z implies ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) assume A5: x in Z ; ::_thesis: ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) hence ((((id Z) (#) sin) + cos) `| Z) . x = (diff (((id Z) (#) sin),x)) + (diff (cos,x)) by A1, A3, A4, FDIFF_1:18 .= ((((id Z) (#) sin) `| Z) . x) + (diff (cos,x)) by A3, A5, FDIFF_1:def_7 .= ((sin . x) + (x * (cos . x))) + (diff (cos,x)) by A2, A5, Th45 .= ((sin . x) + (x * (cos . x))) + (- (sin . x)) by SIN_COS:63 .= x * (cos . x) ; ::_thesis: verum end; hence ( ((id Z) (#) sin) + cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) (#) sin) + cos) `| Z) . x = x * (cos . x) ) ) by A1, A3, A4, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:48 for Z being open Subset of REAL st Z c= dom (2 (#) ((#R (1 / 2)) * sin)) & ( for x being Real st x in Z holds sin . x > 0 ) holds ( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (2 (#) ((#R (1 / 2)) * sin)) & ( for x being Real st x in Z holds sin . x > 0 ) implies ( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) ) ) assume that A1: Z c= dom (2 (#) ((#R (1 / 2)) * sin)) and A2: for x being Real st x in Z holds sin . x > 0 ; ::_thesis: ( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) ) A3: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#R_(1_/_2))_*_sin_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#R (1 / 2)) * sin is_differentiable_in x ) assume x in Z ; ::_thesis: (#R (1 / 2)) * sin is_differentiable_in x then ( sin is_differentiable_in x & sin . x > 0 ) by A2, SIN_COS:64; hence (#R (1 / 2)) * sin is_differentiable_in x by TAYLOR_1:22; ::_thesis: verum end; Z c= dom ((#R (1 / 2)) * sin) by A1, VALUED_1:def_5; then A4: (#R (1 / 2)) * sin is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) proof let x be Real; ::_thesis: ( x in Z implies ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) assume A5: x in Z ; ::_thesis: ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) then A6: ( sin is_differentiable_in x & sin . x > 0 ) by A2, SIN_COS:64; ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = 2 * (diff (((#R (1 / 2)) * sin),x)) by A1, A4, A5, FDIFF_1:20 .= 2 * (((1 / 2) * ((sin . x) #R ((1 / 2) - 1))) * (diff (sin,x))) by A6, TAYLOR_1:22 .= 2 * (((1 / 2) * ((sin . x) #R ((1 / 2) - 1))) * (cos . x)) by SIN_COS:64 .= (cos . x) * ((sin . x) #R (- (1 / 2))) ; hence ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ; ::_thesis: verum end; hence ( 2 (#) ((#R (1 / 2)) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds ((2 (#) ((#R (1 / 2)) * sin)) `| Z) . x = (cos . x) * ((sin . x) #R (- (1 / 2))) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem Th49: :: FDIFF_4:49 for Z being open Subset of REAL st Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) holds ( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) implies ( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) ) ) A1: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_2)_*_sin_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z 2) * sin is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z 2) * sin is_differentiable_in x sin is_differentiable_in x by SIN_COS:64; hence (#Z 2) * sin is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; assume A2: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) ; ::_thesis: ( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) ) then Z c= dom ((#Z 2) * sin) by VALUED_1:def_5; then A3: (#Z 2) * sin is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) A4: sin is_differentiable_in x by SIN_COS:64; assume x in Z ; ::_thesis: (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) then (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (1 / 2) * (diff (((#Z 2) * sin),x)) by A2, A3, FDIFF_1:20 .= (1 / 2) * ((2 * ((sin . x) #Z (2 - 1))) * (diff (sin,x))) by A4, TAYLOR_1:3 .= (1 / 2) * ((2 * ((sin . x) #Z (2 - 1))) * (cos . x)) by SIN_COS:64 .= ((sin . x) #Z (2 - 1)) * (cos . x) .= (sin . x) * (cos . x) by PREPOWER:35 ; hence (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ; ::_thesis: verum end; hence ( (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x = (sin . x) * (cos . x) ) ) by A2, A3, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:50 for Z being open Subset of REAL st Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x < 1 ) ) holds ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x < 1 ) ) implies ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) ) assume that A1: Z c= dom (sin + ((1 / 2) (#) ((#Z 2) * sin))) and A2: for x being Real st x in Z holds ( sin . x > 0 & sin . x < 1 ) ; ::_thesis: ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom sin) by A1, VALUED_1:def_1; then A3: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) by XBOOLE_1:18; then A4: (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z by Th49; A5: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_+_((1_/_2)_(#)_((#Z_2)_*_sin)))_`|_Z)_._x_=_((cos_._x)_|^_3)_/_(1_-_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) assume A6: x in Z ; ::_thesis: ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) then sin . x < 1 by A2; then A7: 1 - (sin . x) > 0 by XREAL_1:50; ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = (diff (sin,x)) + (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A1, A4, A5, A6, FDIFF_1:18 .= (cos . x) + (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by SIN_COS:64 .= (cos . x) + ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) by A4, A6, FDIFF_1:def_7 .= (cos . x) + ((sin . x) * (cos . x)) by A3, A6, Th49 .= (((cos . x) * (1 + (sin . x))) * (1 - (sin . x))) / (1 - (sin . x)) by A7, XCMPLX_1:89 .= ((cos . x) * (1 - ((sin . x) ^2))) / (1 - (sin . x)) .= ((cos . x) * (1 - ((sin x) ^2))) / (1 - (sin . x)) by SIN_COS:def_17 .= ((cos . x) * ((cos x) * (cos x))) / (1 - (sin . x)) by SIN_COS4:5 .= ((cos . x) * ((cos x) |^ 2)) / (1 - (sin . x)) by WSIERP_1:1 .= ((cos . x) * ((cos . x) |^ 2)) / (1 - (sin . x)) by SIN_COS:def_19 .= ((cos . x) |^ (2 + 1)) / (1 - (sin . x)) by NEWTON:6 .= ((cos . x) |^ 3) / (1 - (sin . x)) ; hence ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ; ::_thesis: verum end; hence ( sin + ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 - (sin . x)) ) ) by A1, A4, A5, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_4:51 for Z being open Subset of REAL st Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x < 1 ) ) holds ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x < 1 ) ) implies ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) ) assume that A1: Z c= dom (((1 / 2) (#) ((#Z 2) * sin)) - cos) and A2: for x being Real st x in Z holds ( sin . x > 0 & cos . x < 1 ) ; ::_thesis: ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom cos) by A1, VALUED_1:12; then A3: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) by XBOOLE_1:18; then A4: (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z by Th49; A5: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((1_/_2)_(#)_((#Z_2)_*_sin))_-_cos)_`|_Z)_._x_=_((sin_._x)_|^_3)_/_(1_-_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) assume A6: x in Z ; ::_thesis: ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) then A7: 1 - (cos . x) > 0 by A2, XREAL_1:50; ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) - (diff (cos,x)) by A1, A4, A5, A6, FDIFF_1:19 .= (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) - (- (sin . x)) by SIN_COS:63 .= ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) - (- (sin . x)) by A4, A6, FDIFF_1:def_7 .= ((sin . x) * (cos . x)) - (- (sin . x)) by A3, A6, Th49 .= (((sin . x) * (1 + (cos . x))) * (1 - (cos . x))) / (1 - (cos . x)) by A7, XCMPLX_1:89 .= ((sin . x) * (1 - ((cos . x) ^2))) / (1 - (cos . x)) .= ((sin . x) * (1 - ((cos x) ^2))) / (1 - (cos . x)) by SIN_COS:def_19 .= ((sin . x) * ((sin x) * (sin x))) / (1 - (cos . x)) by SIN_COS4:4 .= ((sin . x) * ((sin x) |^ 2)) / (1 - (cos . x)) by WSIERP_1:1 .= ((sin . x) * ((sin . x) |^ 2)) / (1 - (cos . x)) by SIN_COS:def_17 .= ((sin . x) |^ (2 + 1)) / (1 - (cos . x)) by NEWTON:6 .= ((sin . x) |^ 3) / (1 - (cos . x)) ; hence ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ; ::_thesis: verum end; hence ( ((1 / 2) (#) ((#Z 2) * sin)) - cos is_differentiable_on Z & ( for x being Real st x in Z holds ((((1 / 2) (#) ((#Z 2) * sin)) - cos) `| Z) . x = ((sin . x) |^ 3) / (1 - (cos . x)) ) ) by A1, A4, A5, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:52 for Z being open Subset of REAL st Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x > - 1 ) ) holds ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & sin . x > - 1 ) ) implies ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) ) assume that A1: Z c= dom (sin - ((1 / 2) (#) ((#Z 2) * sin))) and A2: for x being Real st x in Z holds ( sin . x > 0 & sin . x > - 1 ) ; ::_thesis: ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom sin) by A1, VALUED_1:12; then A3: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) by XBOOLE_1:18; then A4: (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z by Th49; A5: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_-_((1_/_2)_(#)_((#Z_2)_*_sin)))_`|_Z)_._x_=_((cos_._x)_|^_3)_/_(1_+_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) assume A6: x in Z ; ::_thesis: ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) then sin . x > - 1 by A2; then A7: (sin . x) - (- 1) > 0 by XREAL_1:50; ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = (diff (sin,x)) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A1, A4, A5, A6, FDIFF_1:19 .= (cos . x) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by SIN_COS:64 .= (cos . x) - ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) by A4, A6, FDIFF_1:def_7 .= (cos . x) - ((sin . x) * (cos . x)) by A3, A6, Th49 .= (((cos . x) * (1 - (sin . x))) * (1 + (sin . x))) / (1 + (sin . x)) by A7, XCMPLX_1:89 .= ((cos . x) * (1 - ((sin . x) ^2))) / (1 + (sin . x)) .= ((cos . x) * (1 - ((sin x) ^2))) / (1 + (sin . x)) by SIN_COS:def_17 .= ((cos . x) * ((cos x) * (cos x))) / (1 + (sin . x)) by SIN_COS4:5 .= ((cos . x) * ((cos x) |^ 2)) / (1 + (sin . x)) by WSIERP_1:1 .= ((cos . x) * ((cos . x) |^ 2)) / (1 + (sin . x)) by SIN_COS:def_19 .= ((cos . x) |^ (2 + 1)) / (1 + (sin . x)) by NEWTON:6 .= ((cos . x) |^ 3) / (1 + (sin . x)) ; hence ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ; ::_thesis: verum end; hence ( sin - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((cos . x) |^ 3) / (1 + (sin . x)) ) ) by A1, A4, A5, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:53 for Z being open Subset of REAL st Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x > - 1 ) ) holds ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) & ( for x being Real st x in Z holds ( sin . x > 0 & cos . x > - 1 ) ) implies ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) ) assume that A1: Z c= dom ((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) and A2: for x being Real st x in Z holds ( sin . x > 0 & cos . x > - 1 ) ; ::_thesis: ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) A3: Z c= (dom ((1 / 2) (#) ((#Z 2) * sin))) /\ (dom (- cos)) by A1, VALUED_1:12; then A4: Z c= dom (- cos) by XBOOLE_1:18; A5: Z c= dom ((1 / 2) (#) ((#Z 2) * sin)) by A3, XBOOLE_1:18; then A6: (1 / 2) (#) ((#Z 2) * sin) is_differentiable_on Z by Th49; A7: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; (- 1) (#) cos = - cos ; then A8: - cos is_differentiable_on Z by A4, A7, FDIFF_1:20; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((-_cos)_-_((1_/_2)_(#)_((#Z_2)_*_sin)))_`|_Z)_._x_=_((sin_._x)_|^_3)_/_(1_+_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) assume A9: x in Z ; ::_thesis: (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) then A10: (cos . x) - (- 1) > 0 by A2, XREAL_1:50; (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = (diff ((- cos),x)) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A1, A6, A8, A9, FDIFF_1:19 .= (((- cos) `| Z) . x) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A8, A9, FDIFF_1:def_7 .= ((- 1) * (diff (cos,x))) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by A4, A7, A9, FDIFF_1:20 .= ((- 1) * (- (sin . x))) - (diff (((1 / 2) (#) ((#Z 2) * sin)),x)) by SIN_COS:63 .= (sin . x) - ((((1 / 2) (#) ((#Z 2) * sin)) `| Z) . x) by A6, A9, FDIFF_1:def_7 .= (sin . x) - ((sin . x) * (cos . x)) by A5, A9, Th49 .= (((sin . x) * (1 - (cos . x))) * (1 + (cos . x))) / (1 + (cos . x)) by A10, XCMPLX_1:89 .= ((sin . x) * (1 - ((cos . x) ^2))) / (1 + (cos . x)) .= ((sin . x) * (1 - ((cos x) ^2))) / (1 + (cos . x)) by SIN_COS:def_19 .= ((sin . x) * ((sin x) * (sin x))) / (1 + (cos . x)) by SIN_COS4:4 .= ((sin . x) * ((sin x) |^ 2)) / (1 + (cos . x)) by WSIERP_1:1 .= ((sin . x) * ((sin . x) |^ 2)) / (1 + (cos . x)) by SIN_COS:def_17 .= ((sin . x) |^ (2 + 1)) / (1 + (cos . x)) by NEWTON:6 .= ((sin . x) |^ 3) / (1 + (cos . x)) ; hence (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ; ::_thesis: verum end; hence ( (- cos) - ((1 / 2) (#) ((#Z 2) * sin)) is_differentiable_on Z & ( for x being Real st x in Z holds (((- cos) - ((1 / 2) (#) ((#Z 2) * sin))) `| Z) . x = ((sin . x) |^ 3) / (1 + (cos . x)) ) ) by A1, A6, A8, FDIFF_1:19; ::_thesis: verum end; theorem :: FDIFF_4:54 for n being Element of NAT for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * sin)) & n > 0 holds ( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL st Z c= dom ((1 / n) (#) ((#Z n) * sin)) & n > 0 holds ( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) ) let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((1 / n) (#) ((#Z n) * sin)) & n > 0 implies ( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) ) ) assume that A1: Z c= dom ((1 / n) (#) ((#Z n) * sin)) and A2: n > 0 ; ::_thesis: ( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) ) A3: now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_n)_*_sin_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z n) * sin is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * sin is_differentiable_in x sin is_differentiable_in x by SIN_COS:64; hence (#Z n) * sin is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; Z c= dom ((#Z n) * sin) by A1, VALUED_1:def_5; then A4: (#Z n) * sin is_differentiable_on Z by A3, FDIFF_1:9; for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) A5: sin is_differentiable_in x by SIN_COS:64; assume x in Z ; ::_thesis: (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) then (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = (1 / n) * (diff (((#Z n) * sin),x)) by A1, A4, FDIFF_1:20 .= (1 / n) * ((n * ((sin . x) #Z (n - 1))) * (diff (sin,x))) by A5, TAYLOR_1:3 .= (1 / n) * ((n * ((sin . x) #Z (n - 1))) * (cos . x)) by SIN_COS:64 .= (((1 / n) * n) * ((sin . x) #Z (n - 1))) * (cos . x) .= (((n ") * n) * ((sin . x) #Z (n - 1))) * (cos . x) by XCMPLX_1:215 .= (1 * ((sin . x) #Z (n - 1))) * (cos . x) by A2, XCMPLX_0:def_7 .= ((sin . x) #Z (n - 1)) * (cos . x) ; hence (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ; ::_thesis: verum end; hence ( (1 / n) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((1 / n) (#) ((#Z n) * sin)) `| Z) . x = ((sin . x) #Z (n - 1)) * (cos . x) ) ) by A1, A4, FDIFF_1:20; ::_thesis: verum end; theorem :: FDIFF_4:55 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds f . x = x - 1 ) holds ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds f . x = x - 1 ) holds ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (exp_R (#) f) & ( for x being Real st x in Z holds f . x = x - 1 ) implies ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) ) assume that A1: Z c= dom (exp_R (#) f) and A2: for x being Real st x in Z holds f . x = x - 1 ; ::_thesis: ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) A3: for x being Real st x in Z holds f . x = (1 * x) + (- 1) proof let x be Real; ::_thesis: ( x in Z implies f . x = (1 * x) + (- 1) ) A4: (1 * x) + (- 1) = (1 * x) - 1 ; assume x in Z ; ::_thesis: f . x = (1 * x) + (- 1) hence f . x = (1 * x) + (- 1) by A2, A4; ::_thesis: verum end; Z c= (dom f) /\ (dom exp_R) by A1, VALUED_1:def_4; then A5: Z c= dom f by XBOOLE_1:18; then A6: f is_differentiable_on Z by A3, FDIFF_1:23; A7: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((exp_R_(#)_f)_`|_Z)_._x_=_x_*_(exp_R_._x) let x be Real; ::_thesis: ( x in Z implies ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) assume A8: x in Z ; ::_thesis: ((exp_R (#) f) `| Z) . x = x * (exp_R . x) hence ((exp_R (#) f) `| Z) . x = ((f . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff (f,x))) by A1, A6, A7, FDIFF_1:21 .= ((x - 1) * (diff (exp_R,x))) + ((exp_R . x) * (diff (f,x))) by A2, A8 .= ((x - 1) * (exp_R . x)) + ((exp_R . x) * (diff (f,x))) by TAYLOR_1:16 .= ((x - 1) * (exp_R . x)) + ((exp_R . x) * ((f `| Z) . x)) by A6, A8, FDIFF_1:def_7 .= ((x - 1) * (exp_R . x)) + ((exp_R . x) * 1) by A5, A3, A8, FDIFF_1:23 .= x * (exp_R . x) ; ::_thesis: verum end; hence ( exp_R (#) f is_differentiable_on Z & ( for x being Real st x in Z holds ((exp_R (#) f) `| Z) . x = x * (exp_R . x) ) ) by A1, A6, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_4:56 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R / (exp_R + f))) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (ln * (exp_R / (exp_R + f))) & ( for x being Real st x in Z holds f . x = 1 ) holds ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * (exp_R / (exp_R + f))) & ( for x being Real st x in Z holds f . x = 1 ) implies ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) ) assume that A1: Z c= dom (ln * (exp_R / (exp_R + f))) and A2: for x being Real st x in Z holds f . x = 1 ; ::_thesis: ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) A3: for x being Real st x in Z holds f . x = (0 * x) + 1 by A2; for y being set st y in Z holds y in dom (exp_R / (exp_R + f)) by A1, FUNCT_1:11; then Z c= dom (exp_R / (exp_R + f)) by TARSKI:def_3; then Z c= (dom exp_R) /\ ((dom (exp_R + f)) \ ((exp_R + f) " {0})) by RFUNCT_1:def_1; then A4: Z c= dom (exp_R + f) by XBOOLE_1:1; then Z c= (dom exp_R) /\ (dom f) by VALUED_1:def_1; then A5: Z c= dom f by XBOOLE_1:18; then A6: f is_differentiable_on Z by A3, FDIFF_1:23; A7: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; then A8: exp_R + f is_differentiable_on Z by A4, A6, FDIFF_1:18; A9: for x being Real st x in Z holds (exp_R + f) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (exp_R + f) . x > 0 ) assume A10: x in Z ; ::_thesis: (exp_R + f) . x > 0 then (exp_R + f) . x = (exp_R . x) + (f . x) by A4, VALUED_1:def_1 .= (exp_R . x) + 1 by A2, A10 ; hence (exp_R + f) . x > 0 by SIN_COS:54, XREAL_1:34; ::_thesis: verum end; then for x being Real st x in Z holds (exp_R + f) . x <> 0 ; then A11: exp_R / (exp_R + f) is_differentiable_on Z by A7, A8, FDIFF_2:21; A12: for x being Real st x in Z holds ((exp_R + f) `| Z) . x = exp_R . x proof let x be Real; ::_thesis: ( x in Z implies ((exp_R + f) `| Z) . x = exp_R . x ) assume A13: x in Z ; ::_thesis: ((exp_R + f) `| Z) . x = exp_R . x hence ((exp_R + f) `| Z) . x = (diff (exp_R,x)) + (diff (f,x)) by A4, A6, A7, FDIFF_1:18 .= (exp_R . x) + (diff (f,x)) by SIN_COS:65 .= (exp_R . x) + ((f `| Z) . x) by A6, A13, FDIFF_1:def_7 .= (exp_R . x) + 0 by A5, A3, A13, FDIFF_1:23 .= exp_R . x ; ::_thesis: verum end; A14: for x being Real st x in Z holds ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2) proof let x be Real; ::_thesis: ( x in Z implies ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2) ) A15: exp_R is_differentiable_in x by SIN_COS:65; assume A16: x in Z ; ::_thesis: ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2) then A17: (exp_R + f) . x = (exp_R . x) + (f . x) by A4, VALUED_1:def_1 .= (exp_R . x) + 1 by A2, A16 ; ( exp_R + f is_differentiable_in x & (exp_R + f) . x <> 0 ) by A8, A9, A16, FDIFF_1:9; then diff ((exp_R / (exp_R + f)),x) = (((diff (exp_R,x)) * ((exp_R + f) . x)) - ((diff ((exp_R + f),x)) * (exp_R . x))) / (((exp_R + f) . x) ^2) by A15, FDIFF_2:14 .= (((exp_R . x) * ((exp_R + f) . x)) - ((diff ((exp_R + f),x)) * (exp_R . x))) / (((exp_R + f) . x) ^2) by SIN_COS:65 .= (((exp_R . x) * ((exp_R . x) + 1)) - ((((exp_R + f) `| Z) . x) * (exp_R . x))) / (((exp_R . x) + 1) ^2) by A8, A16, A17, FDIFF_1:def_7 .= (((exp_R . x) * ((exp_R . x) + 1)) - ((exp_R . x) * (exp_R . x))) / (((exp_R . x) + 1) ^2) by A12, A16 .= (exp_R . x) / (((exp_R . x) + 1) ^2) ; hence ((exp_R / (exp_R + f)) `| Z) . x = (exp_R . x) / (((exp_R . x) + 1) ^2) by A11, A16, FDIFF_1:def_7; ::_thesis: verum end; A18: for x being Real st x in Z holds (exp_R / (exp_R + f)) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies (exp_R / (exp_R + f)) . x > 0 ) A19: exp_R . x > 0 by SIN_COS:54; assume A20: x in Z ; ::_thesis: (exp_R / (exp_R + f)) . x > 0 then x in dom (exp_R / (exp_R + f)) by A1, FUNCT_1:11; then A21: (exp_R / (exp_R + f)) . x = (exp_R . x) * (((exp_R + f) . x) ") by RFUNCT_1:def_1 .= (exp_R . x) * (1 / ((exp_R + f) . x)) by XCMPLX_1:215 .= (exp_R . x) / ((exp_R + f) . x) by XCMPLX_1:99 ; (exp_R + f) . x > 0 by A9, A20; hence (exp_R / (exp_R + f)) . x > 0 by A21, A19, XREAL_1:139; ::_thesis: verum end; A22: for x being Real st x in Z holds ln * (exp_R / (exp_R + f)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * (exp_R / (exp_R + f)) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * (exp_R / (exp_R + f)) is_differentiable_in x then ( exp_R / (exp_R + f) is_differentiable_in x & (exp_R / (exp_R + f)) . x > 0 ) by A11, A18, FDIFF_1:9; hence ln * (exp_R / (exp_R + f)) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A23: ln * (exp_R / (exp_R + f)) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) proof let x be Real; ::_thesis: ( x in Z implies ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) assume A24: x in Z ; ::_thesis: ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) then x in dom (exp_R / (exp_R + f)) by A1, FUNCT_1:11; then A25: (exp_R / (exp_R + f)) . x = (exp_R . x) * (((exp_R + f) . x) ") by RFUNCT_1:def_1 .= (exp_R . x) * (1 / ((exp_R + f) . x)) by XCMPLX_1:215 .= (exp_R . x) / ((exp_R + f) . x) by XCMPLX_1:99 .= (exp_R . x) / ((exp_R . x) + (f . x)) by A4, A24, VALUED_1:def_1 .= (exp_R . x) / ((exp_R . x) + 1) by A2, A24 ; then A26: (exp_R . x) / ((exp_R . x) + 1) > 0 by A18, A24; ( exp_R / (exp_R + f) is_differentiable_in x & (exp_R / (exp_R + f)) . x > 0 ) by A11, A18, A24, FDIFF_1:9; then diff ((ln * (exp_R / (exp_R + f))),x) = (diff ((exp_R / (exp_R + f)),x)) / ((exp_R / (exp_R + f)) . x) by TAYLOR_1:20 .= (((exp_R / (exp_R + f)) `| Z) . x) / ((exp_R / (exp_R + f)) . x) by A11, A24, FDIFF_1:def_7 .= ((exp_R . x) / (((exp_R . x) + 1) ^2)) / ((exp_R . x) / ((exp_R . x) + 1)) by A14, A24, A25 .= (((exp_R . x) / ((exp_R . x) + 1)) / ((exp_R . x) + 1)) / ((exp_R . x) / ((exp_R . x) + 1)) by XCMPLX_1:78 .= (((exp_R . x) / ((exp_R . x) + 1)) / ((exp_R . x) / ((exp_R . x) + 1))) / ((exp_R . x) + 1) by XCMPLX_1:48 .= 1 / ((exp_R . x) + 1) by A26, XCMPLX_1:60 ; hence ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) by A23, A24, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * (exp_R / (exp_R + f)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * (exp_R / (exp_R + f))) `| Z) . x = 1 / ((exp_R . x) + 1) ) ) by A1, A22, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_4:57 for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom (ln * ((exp_R - f) / exp_R)) & ( for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ) holds ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) proof let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom (ln * ((exp_R - f) / exp_R)) & ( for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ) holds ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * ((exp_R - f) / exp_R)) & ( for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ) implies ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) ) assume that A1: Z c= dom (ln * ((exp_R - f) / exp_R)) and A2: for x being Real st x in Z holds ( f . x = 1 & (exp_R - f) . x > 0 ) ; ::_thesis: ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) A3: for x being Real st x in Z holds f . x = (0 * x) + 1 by A2; for y being set st y in Z holds y in dom ((exp_R - f) / exp_R) by A1, FUNCT_1:11; then Z c= dom ((exp_R - f) / exp_R) by TARSKI:def_3; then Z c= (dom (exp_R - f)) /\ ((dom exp_R) \ (exp_R " {0})) by RFUNCT_1:def_1; then A4: Z c= dom (exp_R - f) by XBOOLE_1:18; then Z c= (dom exp_R) /\ (dom f) by VALUED_1:12; then A5: Z c= dom f by XBOOLE_1:18; then A6: f is_differentiable_on Z by A3, FDIFF_1:23; A7: exp_R is_differentiable_on Z by FDIFF_1:26, TAYLOR_1:16; then A8: exp_R - f is_differentiable_on Z by A4, A6, FDIFF_1:19; for x being Real st x in Z holds exp_R . x <> 0 by SIN_COS:54; then A9: (exp_R - f) / exp_R is_differentiable_on Z by A7, A8, FDIFF_2:21; A10: for x being Real st x in Z holds ((exp_R - f) `| Z) . x = exp_R . x proof let x be Real; ::_thesis: ( x in Z implies ((exp_R - f) `| Z) . x = exp_R . x ) assume A11: x in Z ; ::_thesis: ((exp_R - f) `| Z) . x = exp_R . x hence ((exp_R - f) `| Z) . x = (diff (exp_R,x)) - (diff (f,x)) by A4, A6, A7, FDIFF_1:19 .= (exp_R . x) - (diff (f,x)) by SIN_COS:65 .= (exp_R . x) - ((f `| Z) . x) by A6, A11, FDIFF_1:def_7 .= (exp_R . x) - 0 by A5, A3, A11, FDIFF_1:23 .= exp_R . x ; ::_thesis: verum end; A12: for x being Real st x in Z holds (((exp_R - f) / exp_R) `| Z) . x = 1 / (exp_R . x) proof let x be Real; ::_thesis: ( x in Z implies (((exp_R - f) / exp_R) `| Z) . x = 1 / (exp_R . x) ) A13: exp_R . x <> 0 by SIN_COS:54; assume A14: x in Z ; ::_thesis: (((exp_R - f) / exp_R) `| Z) . x = 1 / (exp_R . x) then A15: (exp_R - f) . x = (exp_R . x) - (f . x) by A4, VALUED_1:13 .= (exp_R . x) - 1 by A2, A14 ; ( exp_R is_differentiable_in x & exp_R - f is_differentiable_in x ) by A8, A14, FDIFF_1:9, SIN_COS:65; then diff (((exp_R - f) / exp_R),x) = (((diff ((exp_R - f),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((exp_R - f) . x))) / ((exp_R . x) ^2) by A13, FDIFF_2:14 .= (((((exp_R - f) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((exp_R - f) . x))) / ((exp_R . x) ^2) by A8, A14, FDIFF_1:def_7 .= (((exp_R . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((exp_R - f) . x))) / ((exp_R . x) ^2) by A10, A14 .= (((exp_R . x) * (exp_R . x)) - ((exp_R . x) * ((exp_R . x) - 1))) / ((exp_R . x) ^2) by A15, SIN_COS:65 .= ((exp_R . x) / (exp_R . x)) / (exp_R . x) by XCMPLX_1:78 .= 1 / (exp_R . x) by A13, XCMPLX_1:60 ; hence (((exp_R - f) / exp_R) `| Z) . x = 1 / (exp_R . x) by A9, A14, FDIFF_1:def_7; ::_thesis: verum end; A16: for x being Real st x in Z holds ((exp_R - f) / exp_R) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies ((exp_R - f) / exp_R) . x > 0 ) A17: exp_R . x > 0 by SIN_COS:54; assume A18: x in Z ; ::_thesis: ((exp_R - f) / exp_R) . x > 0 then x in dom ((exp_R - f) / exp_R) by A1, FUNCT_1:11; then A19: ((exp_R - f) / exp_R) . x = ((exp_R - f) . x) * ((exp_R . x) ") by RFUNCT_1:def_1 .= ((exp_R - f) . x) * (1 / (exp_R . x)) by XCMPLX_1:215 .= ((exp_R - f) . x) / (exp_R . x) by XCMPLX_1:99 ; (exp_R - f) . x > 0 by A2, A18; hence ((exp_R - f) / exp_R) . x > 0 by A19, A17, XREAL_1:139; ::_thesis: verum end; A20: for x being Real st x in Z holds ln * ((exp_R - f) / exp_R) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * ((exp_R - f) / exp_R) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * ((exp_R - f) / exp_R) is_differentiable_in x then ( (exp_R - f) / exp_R is_differentiable_in x & ((exp_R - f) / exp_R) . x > 0 ) by A9, A16, FDIFF_1:9; hence ln * ((exp_R - f) / exp_R) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A21: ln * ((exp_R - f) / exp_R) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) proof let x be Real; ::_thesis: ( x in Z implies ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) A22: exp_R . x > 0 by SIN_COS:54; assume A23: x in Z ; ::_thesis: ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) then x in dom ((exp_R - f) / exp_R) by A1, FUNCT_1:11; then A24: ((exp_R - f) / exp_R) . x = ((exp_R - f) . x) * ((exp_R . x) ") by RFUNCT_1:def_1 .= ((exp_R - f) . x) * (1 / (exp_R . x)) by XCMPLX_1:215 .= ((exp_R - f) . x) / (exp_R . x) by XCMPLX_1:99 .= ((exp_R . x) - (f . x)) / (exp_R . x) by A4, A23, VALUED_1:13 .= ((exp_R . x) - 1) / (exp_R . x) by A2, A23 ; ( (exp_R - f) / exp_R is_differentiable_in x & ((exp_R - f) / exp_R) . x > 0 ) by A9, A16, A23, FDIFF_1:9; then diff ((ln * ((exp_R - f) / exp_R)),x) = (diff (((exp_R - f) / exp_R),x)) / (((exp_R - f) / exp_R) . x) by TAYLOR_1:20 .= ((((exp_R - f) / exp_R) `| Z) . x) / (((exp_R - f) / exp_R) . x) by A9, A23, FDIFF_1:def_7 .= (1 / (exp_R . x)) / (((exp_R . x) - 1) / (exp_R . x)) by A12, A23, A24 .= 1 / ((exp_R . x) - 1) by A22, XCMPLX_1:55 ; hence ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) by A21, A23, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * ((exp_R - f) / exp_R) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((exp_R - f) / exp_R)) `| Z) . x = 1 / ((exp_R . x) - 1) ) ) by A1, A20, FDIFF_1:9; ::_thesis: verum end;