:: FDIFF_5 semantic presentation begin Lm1: 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 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 ) & 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 ) & 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 ) & 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) and A2: for x being Real st x in Z holds f1 . x = a and A3: 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 ) ) 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 = 2 * (x #Z (2 - 1)) proof let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * (x #Z (2 - 1)) ) assume A11: x in Z ; ::_thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1)) diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2; hence (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def_7; ::_thesis: verum end; 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 A12: x in Z ; ::_thesis: ((f1 + f2) `| Z) . x = 2 * x 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 .= 2 * (x #Z (2 - 1)) by A10, A12 .= 2 * (x |^ 1) by PREPOWER:36 .= 2 * x by NEWTON:5 ; ::_thesis: verum end; hence ( f1 + f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 + f2) `| Z) . x = 2 * x ) ) by A1, A8, A9, FDIFF_1:18; ::_thesis: verum end; Lm2: 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 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 ) & 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 ) & 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 ) & 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) and A2: for x being Real st x in Z holds f1 . x = a and A3: 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) ) ) 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:12; 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 = 2 * (x #Z (2 - 1)) proof let x be Real; ::_thesis: ( x in Z implies (f2 `| Z) . x = 2 * (x #Z (2 - 1)) ) assume A11: x in Z ; ::_thesis: (f2 `| Z) . x = 2 * (x #Z (2 - 1)) diff (f2,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2; hence (f2 `| Z) . x = 2 * (x #Z (2 - 1)) by A9, A11, FDIFF_1:def_7; ::_thesis: verum end; 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 A12: x in Z ; ::_thesis: ((f1 - f2) `| Z) . x = - (2 * x) then ((f1 - f2) `| Z) . x = (diff (f1,x)) - (diff (f2,x)) by A1, A8, A9, FDIFF_1:19; 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 .= 0 - (2 * (x #Z (2 - 1))) by A10, A12 .= 0 - (2 * (x |^ 1)) by PREPOWER:36 .= - (2 * (x |^ 1)) .= - (2 * x) by NEWTON:5 ; ::_thesis: verum end; hence ( f1 - f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 - f2) `| Z) . x = - (2 * x) ) ) by A1, A8, A9, FDIFF_1:19; ::_thesis: verum end; Lm3: for Z being open Subset of REAL st Z c= dom (#R (1 / 2)) holds ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (#R (1 / 2)) implies ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) ) assume A1: Z c= dom (#R (1 / 2)) ; ::_thesis: ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) A2: for x being Real st x in Z holds #R (1 / 2) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies #R (1 / 2) is_differentiable_in x ) assume x in Z ; ::_thesis: #R (1 / 2) is_differentiable_in x then x in dom (#R (1 / 2)) by A1; then x in right_open_halfline 0 by TAYLOR_1:def_4; then x > 0 by XXREAL_1:4; hence #R (1 / 2) is_differentiable_in x by TAYLOR_1:21; ::_thesis: verum end; then A3: #R (1 / 2) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) proof let x be Real; ::_thesis: ( x in Z implies ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) assume A4: x in Z ; ::_thesis: ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) then x in dom (#R (1 / 2)) by A1; then x in right_open_halfline 0 by TAYLOR_1:def_4; then x > 0 by XXREAL_1:4; then diff ((#R (1 / 2)),x) = (1 / 2) * (x #R ((1 / 2) - 1)) by TAYLOR_1:21 .= (1 / 2) * (x #R (- (1 / 2))) ; hence ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( #R (1 / 2) is_differentiable_on Z & ( for x being Real st x in Z holds ((#R (1 / 2)) `| Z) . x = (1 / 2) * (x #R (- (1 / 2))) ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_5:1 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 + x & f2 . x = a - x & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - 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 + x & f2 . x = a - x & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - 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 + x & f2 . x = a - x & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - 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 + x & f2 . x = a - x & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) ) assume that A1: Z c= dom (f1 / f2) and A2: for x being Real st x in Z holds ( f1 . x = a + x & f2 . x = a - x & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) A3: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, 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; A10: for x being Real st x in Z holds f2 . x <> 0 by A2; then A11: f1 / f2 is_differentiable_on Z by A6, A9, FDIFF_2:21; 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 A11, A12, FDIFF_1:def_7; ::_thesis: verum end; hence ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((a - x) ^2) ) ) by A6, A9, A10, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_5:2 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 = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + 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 (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^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 = x - a & f2 . x = x + a & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^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 = x - a & f2 . x = x + a & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) ) assume that A1: Z c= dom (f1 / f2) and A2: for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x + a & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) A3: for x being Real st x in Z holds f2 . x = (1 * x) + a by A2; A4: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, 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; A11: for x being Real st x in Z holds f2 . x <> 0 by A2; then A12: f1 / f2 is_differentiable_on Z by A10, A7, FDIFF_2:21; 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 A12, A13, FDIFF_1:def_7; ::_thesis: verum end; hence ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (2 * a) / ((x + a) ^2) ) ) by A10, A7, A11, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_5:3 for a, b 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 = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) 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 (f1 / f2) & ( for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^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 = x - a & f2 . x = x - b & f2 . x <> 0 ) ) holds ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^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 = x - a & f2 . x = x - b & f2 . x <> 0 ) ) implies ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) ) assume that A1: Z c= dom (f1 / f2) and A2: for x being Real st x in Z holds ( f1 . x = x - a & f2 . x = x - b & f2 . x <> 0 ) ; ::_thesis: ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) 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) ; A6: Z c= (dom f1) /\ ((dom f2) \ (f2 " {0})) by A1, 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; A12: for x being Real st x in Z holds f2 . x <> 0 by A2; then A13: f1 / f2 is_differentiable_on Z by A8, A11, FDIFF_2:21; 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 A13, A14, FDIFF_1:def_7; ::_thesis: verum end; hence ( f1 / f2 is_differentiable_on Z & ( for x being Real st x in Z holds ((f1 / f2) `| Z) . x = (a - b) / ((x - b) ^2) ) ) by A8, A11, A12, FDIFF_2:21; ::_thesis: verum end; theorem Th4: :: FDIFF_5:4 for Z being open Subset of REAL st not 0 in Z holds ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) ) set f = id Z; A1: ( Z c= dom (id Z) & ( for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 ) ) by FUNCT_1:17; then A2: id Z is_differentiable_on Z by FDIFF_1:23; assume A3: not 0 in Z ; ::_thesis: ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) then A4: for x being Real st x in Z holds (id Z) . x <> 0 by FUNCT_1:18; then A5: (id Z) ^ is_differentiable_on Z by A2, FDIFF_2:22; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((id_Z)_^)_`|_Z)_._x_=_-_(1_/_(x_^2)) let x be Real; ::_thesis: ( x in Z implies (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) assume A6: x in Z ; ::_thesis: (((id Z) ^) `| Z) . x = - (1 / (x ^2)) then A7: ( (id Z) . x <> 0 & id Z is_differentiable_in x ) by A3, A2, FDIFF_1:9, FUNCT_1:18; (((id Z) ^) `| Z) . x = diff (((id Z) ^),x) by A5, A6, FDIFF_1:def_7 .= - ((diff ((id Z),x)) / (((id Z) . x) ^2)) by A7, FDIFF_2:15 .= - ((((id Z) `| Z) . x) / (((id Z) . x) ^2)) by A2, A6, FDIFF_1:def_7 .= - (1 / (((id Z) . x) ^2)) by A1, A6, FDIFF_1:23 .= - (1 / (x ^2)) by A6, FUNCT_1:18 ; hence (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ; ::_thesis: verum end; hence ( (id Z) ^ is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) ^) `| Z) . x = - (1 / (x ^2)) ) ) by A2, A4, FDIFF_2:22; ::_thesis: verum end; Lm4: for Z being open Subset of REAL st not 0 in Z holds dom (sin * ((id Z) ^)) = Z proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies dom (sin * ((id Z) ^)) = Z ) A1: rng ((id Z) ^) c= REAL by RELAT_1:def_19; assume A2: not 0 in Z ; ::_thesis: dom (sin * ((id Z) ^)) = Z (id Z) " {0} c= {} proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (id Z) " {0} or x in {} ) assume A3: x in (id Z) " {0} ; ::_thesis: x in {} then x in dom (id Z) by FUNCT_1:def_7; then A4: x in Z by FUNCT_1:17; (id Z) . x in {0} by A3, FUNCT_1:def_7; then x in {0} by A4, FUNCT_1:18; hence x in {} by A2, A4, TARSKI:def_1; ::_thesis: verum end; then A5: (id Z) " {0} = {} by XBOOLE_1:3; dom ((id Z) ^) = (dom (id Z)) \ ((id Z) " {0}) by RFUNCT_1:def_2 .= Z by A5, FUNCT_1:17 ; hence dom (sin * ((id Z) ^)) = Z by A1, RELAT_1:27, SIN_COS:24; ::_thesis: verum end; theorem Th5: :: FDIFF_5:5 for Z being open Subset of REAL st not 0 in Z holds ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z implies ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) ) set f = id Z; assume A1: not 0 in Z ; ::_thesis: ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) then A2: Z c= dom (sin * ((id Z) ^)) by Lm4; then for y being set st y in Z holds y in dom ((id Z) ^) by FUNCT_1:11; then A3: Z c= dom ((id Z) ^) by TARSKI:def_3; A4: (id Z) ^ is_differentiable_on Z by A1, Th4; A5: for x being Real st x in Z holds sin * ((id Z) ^) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies sin * ((id Z) ^) is_differentiable_in x ) assume x in Z ; ::_thesis: sin * ((id Z) ^) is_differentiable_in x then A6: (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9; sin is_differentiable_in ((id Z) ^) . x by SIN_COS:64; hence sin * ((id Z) ^) is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: sin * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9; for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) proof let x be Real; ::_thesis: ( x in Z implies ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) A8: sin is_differentiable_in ((id Z) ^) . x by SIN_COS:64; assume A9: x in Z ; ::_thesis: ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) then (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9; then diff ((sin * ((id Z) ^)),x) = (diff (sin,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A8, FDIFF_2:13 .= (cos . (((id Z) ^) . x)) * (diff (((id Z) ^),x)) by SIN_COS:64 .= (cos . (((id Z) . x) ")) * (diff (((id Z) ^),x)) by A3, A9, RFUNCT_1:def_2 .= (cos . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x) by A4, A9, FDIFF_1:def_7 .= (cos . (((id Z) . x) ")) * (- (1 / (x ^2))) by A1, A9, Th4 .= (cos . (1 * (x "))) * (- (1 / (x ^2))) by A9, FUNCT_1:18 .= (cos . (1 / x)) * (- (1 / (x ^2))) by XCMPLX_0:def_9 ; hence ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) by A7, A9, FDIFF_1:def_7; ::_thesis: verum end; hence ( sin * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin * ((id Z) ^)) `| Z) . x = - ((1 / (x ^2)) * (cos . (1 / x))) ) ) by A2, A5, FDIFF_1:9; ::_thesis: verum end; theorem Th6: :: FDIFF_5:6 for Z being open Subset of REAL st not 0 in Z & Z c= dom (cos * ((id Z) ^)) holds ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & Z c= dom (cos * ((id Z) ^)) implies ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (cos * ((id Z) ^)) ; ::_thesis: ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) for y being set st y in Z holds y in dom ((id Z) ^) by A2, FUNCT_1:11; then A3: Z c= dom ((id Z) ^) by TARSKI:def_3; A4: (id Z) ^ is_differentiable_on Z by A1, Th4; A5: for x being Real st x in Z holds cos * ((id Z) ^) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies cos * ((id Z) ^) is_differentiable_in x ) assume x in Z ; ::_thesis: cos * ((id Z) ^) is_differentiable_in x then A6: (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9; cos is_differentiable_in ((id Z) ^) . x by SIN_COS:63; hence cos * ((id Z) ^) is_differentiable_in x by A6, FDIFF_2:13; ::_thesis: verum end; then A7: cos * ((id Z) ^) is_differentiable_on Z by A2, FDIFF_1:9; for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) proof let x be Real; ::_thesis: ( x in Z implies ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) A8: diff (cos,(((id Z) ^) . x)) = - (sin . (((id Z) ^) . x)) by SIN_COS:63; A9: cos is_differentiable_in ((id Z) ^) . x by SIN_COS:63; assume A10: x in Z ; ::_thesis: ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) then (id Z) ^ is_differentiable_in x by A4, FDIFF_1:9; then diff ((cos * ((id Z) ^)),x) = (diff (cos,(((id Z) ^) . x))) * (diff (((id Z) ^),x)) by A9, FDIFF_2:13 .= - ((sin . (((id Z) ^) . x)) * (diff (((id Z) ^),x))) by A8 .= - ((sin . (((id Z) . x) ")) * (diff (((id Z) ^),x))) by A3, A10, RFUNCT_1:def_2 .= - ((sin . (((id Z) . x) ")) * ((((id Z) ^) `| Z) . x)) by A4, A10, FDIFF_1:def_7 .= - ((sin . (((id Z) . x) ")) * (- (1 / (x ^2)))) by A1, A10, Th4 .= - ((sin . (1 * (x "))) * (- (1 / (x ^2)))) by A10, FUNCT_1:18 .= - ((sin . (1 / x)) * (- (1 / (x ^2)))) by XCMPLX_0:def_9 .= (sin . (1 / x)) * (1 / (x ^2)) ; hence ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) by A7, A10, FDIFF_1:def_7; ::_thesis: verum end; hence ( cos * ((id Z) ^) is_differentiable_on Z & ( for x being Real st x in Z holds ((cos * ((id Z) ^)) `| Z) . x = (1 / (x ^2)) * (sin . (1 / x)) ) ) by A2, A5, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_5:7 for Z being open Subset of REAL st Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z holds ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) (sin * ((id Z) ^))) & not 0 in Z implies ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) ) set f = id Z; assume that A1: Z c= dom ((id Z) (#) (sin * ((id Z) ^))) and A2: not 0 in Z ; ::_thesis: ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) A3: sin * ((id Z) ^) is_differentiable_on Z by A2, Th5; A4: Z c= (dom (id Z)) /\ (dom (sin * ((id Z) ^))) by A1, VALUED_1:def_4; then A5: Z c= dom (id Z) by XBOOLE_1:18; A6: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; then A7: id Z is_differentiable_on Z by A5, FDIFF_1:23; A8: Z c= dom (sin * ((id Z) ^)) by A4, XBOOLE_1:18; then for y being set st y in Z holds y in dom ((id Z) ^) by FUNCT_1:11; then A9: Z c= dom ((id Z) ^) by TARSKI:def_3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((id_Z)_(#)_(sin_*_((id_Z)_^)))_`|_Z)_._x_=_(sin_._(1_/_x))_-_((1_/_x)_*_(cos_._(1_/_x))) let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) assume A10: x in Z ; ::_thesis: (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) then (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (((sin * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A1, A3, A7, FDIFF_1:21 .= (((sin * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A7, A10, FDIFF_1:def_7 .= (((sin * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((sin * ((id Z) ^)),x))) by A5, A6, A10, FDIFF_1:23 .= ((sin * ((id Z) ^)) . x) + (x * (diff ((sin * ((id Z) ^)),x))) by A10, FUNCT_1:18 .= ((sin * ((id Z) ^)) . x) + (x * (((sin * ((id Z) ^)) `| Z) . x)) by A3, A10, FDIFF_1:def_7 .= ((sin * ((id Z) ^)) . x) + (x * (- ((1 / (x ^2)) * (cos . (1 / x))))) by A2, A10, Th5 .= ((sin * ((id Z) ^)) . x) - ((x * (1 / (x * x))) * (cos . (1 / x))) .= ((sin * ((id Z) ^)) . x) - ((x * ((1 / x) * (1 / x))) * (cos . (1 / x))) by XCMPLX_1:102 .= ((sin * ((id Z) ^)) . x) - (((x * (1 / x)) * (1 / x)) * (cos . (1 / x))) .= ((sin * ((id Z) ^)) . x) - ((1 * (1 / x)) * (cos . (1 / x))) by A2, A10, XCMPLX_1:106 .= (sin . (((id Z) ^) . x)) - ((1 / x) * (cos . (1 / x))) by A8, A10, FUNCT_1:12 .= (sin . (((id Z) . x) ")) - ((1 / x) * (cos . (1 / x))) by A9, A10, RFUNCT_1:def_2 .= (sin . (1 * (x "))) - ((1 / x) * (cos . (1 / x))) by A10, FUNCT_1:18 .= (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) by XCMPLX_0:def_9 ; hence (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ; ::_thesis: verum end; hence ( (id Z) (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (sin * ((id Z) ^))) `| Z) . x = (sin . (1 / x)) - ((1 / x) * (cos . (1 / x))) ) ) by A1, A3, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:8 for Z being open Subset of REAL st Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z holds ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) (cos * ((id Z) ^))) & not 0 in Z implies ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) ) set f = id Z; assume that A1: Z c= dom ((id Z) (#) (cos * ((id Z) ^))) and A2: not 0 in Z ; ::_thesis: ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) A3: Z c= (dom (id Z)) /\ (dom (cos * ((id Z) ^))) by A1, VALUED_1:def_4; then A4: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18; then A5: cos * ((id Z) ^) is_differentiable_on Z by A2, Th6; A6: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; A7: Z c= dom (id Z) by A3, XBOOLE_1:18; then A8: id Z is_differentiable_on Z by A6, FDIFF_1:23; for y being set st y in Z holds y in dom ((id Z) ^) by A4, FUNCT_1:11; then A9: Z c= dom ((id Z) ^) by TARSKI:def_3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((id_Z)_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_(cos_._(1_/_x))_+_((1_/_x)_*_(sin_._(1_/_x))) let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) assume A10: x in Z ; ::_thesis: (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) then (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff ((id Z),x))) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A1, A5, A8, FDIFF_1:21 .= (((cos * ((id Z) ^)) . x) * (((id Z) `| Z) . x)) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A8, A10, FDIFF_1:def_7 .= (((cos * ((id Z) ^)) . x) * 1) + (((id Z) . x) * (diff ((cos * ((id Z) ^)),x))) by A7, A6, A10, FDIFF_1:23 .= ((cos * ((id Z) ^)) . x) + (x * (diff ((cos * ((id Z) ^)),x))) by A10, FUNCT_1:18 .= ((cos * ((id Z) ^)) . x) + (x * (((cos * ((id Z) ^)) `| Z) . x)) by A5, A10, FDIFF_1:def_7 .= ((cos * ((id Z) ^)) . x) + (x * ((1 / (x ^2)) * (sin . (1 / x)))) by A2, A4, A10, Th6 .= ((cos * ((id Z) ^)) . x) + ((x * (1 / (x * x))) * (sin . (1 / x))) .= ((cos * ((id Z) ^)) . x) + ((x * ((1 / x) * (1 / x))) * (sin . (1 / x))) by XCMPLX_1:102 .= ((cos * ((id Z) ^)) . x) + (((x * (1 / x)) * (1 / x)) * (sin . (1 / x))) .= ((cos * ((id Z) ^)) . x) + ((1 * (1 / x)) * (sin . (1 / x))) by A2, A10, XCMPLX_1:106 .= (cos . (((id Z) ^) . x)) + ((1 / x) * (sin . (1 / x))) by A4, A10, FUNCT_1:12 .= (cos . (((id Z) . x) ")) + ((1 / x) * (sin . (1 / x))) by A9, A10, RFUNCT_1:def_2 .= (cos . (1 * (x "))) + ((1 / x) * (sin . (1 / x))) by A10, FUNCT_1:18 .= (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) by XCMPLX_0:def_9 ; hence (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ; ::_thesis: verum end; hence ( (id Z) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) (cos * ((id Z) ^))) `| Z) . x = (cos . (1 / x)) + ((1 / x) * (sin . (1 / x))) ) ) by A1, A5, A8, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:9 for Z being open Subset of REAL st Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z holds ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) & not 0 in Z implies ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) ) set f = id Z; assume that A1: Z c= dom ((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) and A2: not 0 in Z ; ::_thesis: ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) A3: sin * ((id Z) ^) is_differentiable_on Z by A2, Th5; A4: Z c= (dom (sin * ((id Z) ^))) /\ (dom (cos * ((id Z) ^))) by A1, VALUED_1:def_4; then A5: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18; then A6: cos * ((id Z) ^) is_differentiable_on Z by A2, Th6; A7: Z c= dom (sin * ((id Z) ^)) by A4, XBOOLE_1:18; then for y being set st y in Z holds y in dom ((id Z) ^) by FUNCT_1:11; then A8: Z c= dom ((id Z) ^) by TARSKI:def_3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((sin_*_((id_Z)_^))_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_(1_/_(x_^2))_*_(((sin_._(1_/_x))_^2)_-_((cos_._(1_/_x))_^2)) let x be Real; ::_thesis: ( x in Z implies (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) assume A9: x in Z ; ::_thesis: (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) then (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff ((sin * ((id Z) ^)),x))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A1, A6, A3, FDIFF_1:21 .= (((cos * ((id Z) ^)) . x) * (((sin * ((id Z) ^)) `| Z) . x)) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A3, A9, FDIFF_1:def_7 .= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (diff ((cos * ((id Z) ^)),x))) by A2, A9, Th5 .= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * (((cos * ((id Z) ^)) `| Z) . x)) by A6, A9, FDIFF_1:def_7 .= (((cos * ((id Z) ^)) . x) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A2, A5, A9, Th6 .= ((cos . (((id Z) ^) . x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A5, A9, FUNCT_1:12 .= ((cos . (((id Z) . x) ")) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def_2 .= ((cos . (1 * (x "))) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by A9, FUNCT_1:18 .= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + (((sin * ((id Z) ^)) . x) * ((1 / (x ^2)) * (sin . (1 / x)))) by XCMPLX_0:def_9 .= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (((id Z) ^) . x)) * ((1 / (x ^2)) * (sin . (1 / x)))) by A7, A9, FUNCT_1:12 .= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (((id Z) . x) ")) * ((1 / (x ^2)) * (sin . (1 / x)))) by A8, A9, RFUNCT_1:def_2 .= ((cos . (1 / x)) * (- ((1 / (x ^2)) * (cos . (1 / x))))) + ((sin . (1 * (x "))) * ((1 / (x ^2)) * (sin . (1 / x)))) by A9, FUNCT_1:18 .= (- (((cos . (1 / x)) * (1 / (x ^2))) * (cos . (1 / x)))) + ((sin . (1 / x)) * ((1 / (x ^2)) * (sin . (1 / x)))) by XCMPLX_0:def_9 .= (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ; hence (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ; ::_thesis: verum end; hence ( (sin * ((id Z) ^)) (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * ((id Z) ^)) (#) (cos * ((id Z) ^))) `| Z) . x = (1 / (x ^2)) * (((sin . (1 / x)) ^2) - ((cos . (1 / x)) ^2)) ) ) by A1, A6, A3, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:10 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((sin * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) ) assume that A1: Z c= dom ((sin * f) (#) ((#Z n) * sin)) and A2: n >= 1 and A3: for x being Real st x in Z holds f . x = n * x ; ::_thesis: ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) A4: for x being Real st x in Z holds f . x = (n * x) + 0 by A3; A5: Z c= (dom (sin * f)) /\ (dom ((#Z n) * sin)) by A1, VALUED_1:def_4; then A6: Z c= dom (sin * f) by XBOOLE_1:18; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A7: Z c= dom f by TARSKI:def_3; then A8: f is_differentiable_on Z by A4, FDIFF_1:23; 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 A9: f is_differentiable_in x by A8, FDIFF_1:9; sin is_differentiable_in f . x by SIN_COS:64; hence sin * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum end; then A10: sin * f is_differentiable_on Z by A6, FDIFF_1:9; A11: for x being Real st x in Z holds ((sin * f) `| Z) . x = n * (cos . (n * x)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) ) A12: sin is_differentiable_in f . x by SIN_COS:64; assume A13: x in Z ; ::_thesis: ((sin * f) `| Z) . x = n * (cos . (n * x)) then f is_differentiable_in x by A8, FDIFF_1:9; then diff ((sin * f),x) = (diff (sin,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13 .= (cos . (f . x)) * (diff (f,x)) by SIN_COS:64 .= (cos . (n * x)) * (diff (f,x)) by A3, A13 .= (cos . (n * x)) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7 .= n * (cos . (n * x)) by A7, A4, A13, FDIFF_1:23 ; hence ((sin * f) `| Z) . x = n * (cos . (n * x)) by A10, A13, FDIFF_1:def_7; ::_thesis: verum end; A14: Z c= dom ((#Z n) * sin) by A5, XBOOLE_1:18; 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; then A15: (#Z n) * sin is_differentiable_on Z by A14, FDIFF_1:9; A16: for x being Real st x in Z holds (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) ) sin is_differentiable_in x by SIN_COS:64; then A17: diff (((#Z n) * sin),x) = (n * ((sin . x) #Z (n - 1))) * (diff (sin,x)) by TAYLOR_1:3 .= (n * ((sin . x) #Z (n - 1))) * (cos . x) by SIN_COS:64 ; assume x in Z ; ::_thesis: (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) hence (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) by A15, A17, FDIFF_1:def_7; ::_thesis: verum end; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((sin_*_f)_(#)_((#Z_n)_*_sin))_`|_Z)_._x_=_(n_*_((sin_._x)_#Z_(n_-_1)))_*_(sin_._((n_+_1)_*_x)) let x be Real; ::_thesis: ( x in Z implies (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) A18: n - 1 is Element of NAT by A2, NAT_1:21; assume A19: x in Z ; ::_thesis: (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) then (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = ((((#Z n) * sin) . x) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A1, A10, A15, FDIFF_1:21 .= (((#Z n) . (sin . x)) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A14, A19, FUNCT_1:12 .= (((sin . x) #Z n) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by TAYLOR_1:def_1 .= (((sin . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A10, A19, FDIFF_1:def_7 .= (((sin . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff (((#Z n) * sin),x))) by A11, A19 .= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff (((#Z n) * sin),x))) by A6, A19, FUNCT_1:12 .= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff (((#Z n) * sin),x))) by A3, A19 .= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * sin) `| Z) . x)) by A15, A19, FDIFF_1:def_7 .= (((sin . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((n * ((sin . x) #Z (n - 1))) * (cos . x))) by A16, A19 .= (((sin . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) .= ((((sin . x) #Z (n - 1)) * ((sin . x) #Z 1)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by A18, TAYLOR_1:1 .= ((((sin . x) #Z (n - 1)) * (sin . x)) * (n * (cos . (n * x)))) + ((((sin . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by PREPOWER:35 .= (n * ((sin . x) #Z (n - 1))) * (((sin . x) * (cos . (n * x))) + ((cos . x) * (sin . (n * x)))) .= (n * ((sin . x) #Z (n - 1))) * (sin . (x + (n * x))) by SIN_COS:74 .= (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ; hence (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ; ::_thesis: verum end; hence ( (sin * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (sin . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:11 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((cos * f) (#) ((#Z n) * sin)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) implies ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) ) assume that A1: Z c= dom ((cos * f) (#) ((#Z n) * sin)) and A2: n >= 1 and A3: for x being Real st x in Z holds f . x = n * x ; ::_thesis: ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) A4: for x being Real st x in Z holds f . x = (n * x) + 0 by A3; A5: Z c= (dom (cos * f)) /\ (dom ((#Z n) * sin)) by A1, VALUED_1:def_4; then A6: Z c= dom (cos * f) by XBOOLE_1:18; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A7: Z c= dom f by TARSKI:def_3; then A8: f is_differentiable_on Z by A4, FDIFF_1:23; 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 A9: f is_differentiable_in x by A8, FDIFF_1:9; cos is_differentiable_in f . x by SIN_COS:63; hence cos * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum end; then A10: cos * f is_differentiable_on Z by A6, FDIFF_1:9; A11: for x being Real st x in Z holds ((cos * f) `| Z) . x = - (n * (sin . (n * x))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * f) `| Z) . x = - (n * (sin . (n * x))) ) A12: cos is_differentiable_in f . x by SIN_COS:63; assume A13: x in Z ; ::_thesis: ((cos * f) `| Z) . x = - (n * (sin . (n * x))) then f is_differentiable_in x by A8, FDIFF_1:9; then diff ((cos * f),x) = (diff (cos,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13 .= (- (sin . (f . x))) * (diff (f,x)) by SIN_COS:63 .= (- (sin . (n * x))) * (diff (f,x)) by A3, A13 .= (- (sin . (n * x))) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7 .= (- (sin . (n * x))) * n by A7, A4, A13, FDIFF_1:23 .= - (n * (sin . (n * x))) ; hence ((cos * f) `| Z) . x = - (n * (sin . (n * x))) by A10, A13, FDIFF_1:def_7; ::_thesis: verum end; A14: Z c= dom ((#Z n) * sin) by A5, XBOOLE_1:18; 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; then A15: (#Z n) * sin is_differentiable_on Z by A14, FDIFF_1:9; A16: for x being Real st x in Z holds (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) ) sin is_differentiable_in x by SIN_COS:64; then A17: diff (((#Z n) * sin),x) = (n * ((sin . x) #Z (n - 1))) * (diff (sin,x)) by TAYLOR_1:3 .= (n * ((sin . x) #Z (n - 1))) * (cos . x) by SIN_COS:64 ; assume x in Z ; ::_thesis: (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) hence (((#Z n) * sin) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . x) by A15, A17, FDIFF_1:def_7; ::_thesis: verum end; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((cos_*_f)_(#)_((#Z_n)_*_sin))_`|_Z)_._x_=_(n_*_((sin_._x)_#Z_(n_-_1)))_*_(cos_._((n_+_1)_*_x)) let x be Real; ::_thesis: ( x in Z implies (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) A18: n - 1 is Element of NAT by A2, NAT_1:21; assume A19: x in Z ; ::_thesis: (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) then (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = ((((#Z n) * sin) . x) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A1, A10, A15, FDIFF_1:21 .= (((#Z n) . (sin . x)) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A14, A19, FUNCT_1:12 .= (((sin . x) #Z n) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by TAYLOR_1:def_1 .= (((sin . x) #Z n) * (((cos * f) `| Z) . x)) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A10, A19, FDIFF_1:def_7 .= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + (((cos * f) . x) * (diff (((#Z n) * sin),x))) by A11, A19 .= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (f . x)) * (diff (((#Z n) * sin),x))) by A6, A19, FUNCT_1:12 .= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (diff (((#Z n) * sin),x))) by A3, A19 .= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((((#Z n) * sin) `| Z) . x)) by A15, A19, FDIFF_1:def_7 .= (((sin . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((n * ((sin . x) #Z (n - 1))) * (cos . x))) by A16, A19 .= (((sin . x) #Z ((n - 1) + 1)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) .= ((((sin . x) #Z (n - 1)) * ((sin . x) #Z 1)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by A18, TAYLOR_1:1 .= ((((sin . x) #Z (n - 1)) * (sin . x)) * (- (n * (sin . (n * x))))) + ((((cos . (n * x)) * n) * ((sin . x) #Z (n - 1))) * (cos . x)) by PREPOWER:35 .= (n * ((sin . x) #Z (n - 1))) * (((cos . (n * x)) * (cos . x)) - ((sin . x) * (sin . (n * x)))) .= (n * ((sin . x) #Z (n - 1))) * (cos . (x + (n * x))) by SIN_COS:74 .= (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; hence (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; ::_thesis: verum end; hence ( (cos * f) (#) ((#Z n) * sin) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * sin)) `| Z) . x = (n * ((sin . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:12 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((cos * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) implies ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) ) assume that A1: Z c= dom ((cos * f) (#) ((#Z n) * cos)) and A2: n >= 1 and A3: for x being Real st x in Z holds f . x = n * x ; ::_thesis: ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) A4: for x being Real st x in Z holds f . x = (n * x) + 0 by A3; A5: Z c= (dom (cos * f)) /\ (dom ((#Z n) * cos)) by A1, VALUED_1:def_4; then A6: Z c= dom (cos * f) by XBOOLE_1:18; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A7: Z c= dom f by TARSKI:def_3; then A8: f is_differentiable_on Z by A4, FDIFF_1:23; 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 A9: f is_differentiable_in x by A8, FDIFF_1:9; cos is_differentiable_in f . x by SIN_COS:63; hence cos * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum end; then A10: cos * f is_differentiable_on Z by A6, FDIFF_1:9; A11: for x being Real st x in Z holds ((cos * f) `| Z) . x = - (n * (sin . (n * x))) proof let x be Real; ::_thesis: ( x in Z implies ((cos * f) `| Z) . x = - (n * (sin . (n * x))) ) A12: cos is_differentiable_in f . x by SIN_COS:63; assume A13: x in Z ; ::_thesis: ((cos * f) `| Z) . x = - (n * (sin . (n * x))) then f is_differentiable_in x by A8, FDIFF_1:9; then diff ((cos * f),x) = (diff (cos,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13 .= (- (sin . (f . x))) * (diff (f,x)) by SIN_COS:63 .= - ((sin . (f . x)) * (diff (f,x))) .= - ((sin . (n * x)) * (diff (f,x))) by A3, A13 .= - ((sin . (n * x)) * ((f `| Z) . x)) by A8, A13, FDIFF_1:def_7 .= - (n * (sin . (n * x))) by A7, A4, A13, FDIFF_1:23 ; hence ((cos * f) `| Z) . x = - (n * (sin . (n * x))) by A10, A13, FDIFF_1:def_7; ::_thesis: verum end; A14: Z c= dom ((#Z n) * cos) by A5, XBOOLE_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_n)_*_cos_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z n) * cos is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * cos is_differentiable_in x cos is_differentiable_in x by SIN_COS:63; hence (#Z n) * cos is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A15: (#Z n) * cos is_differentiable_on Z by A14, FDIFF_1:9; A16: for x being Real st x in Z holds (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ) cos is_differentiable_in x by SIN_COS:63; then A17: diff (((#Z n) * cos),x) = (n * ((cos . x) #Z (n - 1))) * (diff (cos,x)) by TAYLOR_1:3 .= (n * ((cos . x) #Z (n - 1))) * (- (sin . x)) by SIN_COS:63 .= - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ; assume x in Z ; ::_thesis: (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) hence (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) by A15, A17, FDIFF_1:def_7; ::_thesis: verum end; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((cos_*_f)_(#)_((#Z_n)_*_cos))_`|_Z)_._x_=_-_((n_*_((cos_._x)_#Z_(n_-_1)))_*_(sin_._((n_+_1)_*_x))) let x be Real; ::_thesis: ( x in Z implies (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) A18: n - 1 is Element of NAT by A2, NAT_1:21; assume A19: x in Z ; ::_thesis: (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) then (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = ((((#Z n) * cos) . x) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A1, A10, A15, FDIFF_1:21 .= (((#Z n) . (cos . x)) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A14, A19, FUNCT_1:12 .= (((cos . x) #Z n) * (diff ((cos * f),x))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by TAYLOR_1:def_1 .= (((cos . x) #Z n) * (((cos * f) `| Z) . x)) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A10, A19, FDIFF_1:def_7 .= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + (((cos * f) . x) * (diff (((#Z n) * cos),x))) by A11, A19 .= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (f . x)) * (diff (((#Z n) * cos),x))) by A6, A19, FUNCT_1:12 .= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (diff (((#Z n) * cos),x))) by A3, A19 .= (((cos . x) #Z n) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * ((((#Z n) * cos) `| Z) . x)) by A15, A19, FDIFF_1:def_7 .= (((cos . x) #Z ((n - 1) + 1)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A16, A19 .= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A18, TAYLOR_1:1 .= ((((cos . x) #Z (n - 1)) * (cos . x)) * (- (n * (sin . (n * x))))) + ((cos . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by PREPOWER:35 .= - ((n * ((cos . x) #Z (n - 1))) * (((sin . (n * x)) * (cos . x)) + ((cos . (n * x)) * (sin . x)))) .= - ((n * ((cos . x) #Z (n - 1))) * (sin . (x + (n * x)))) by SIN_COS:74 .= - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ; hence (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ; ::_thesis: verum end; hence ( (cos * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((cos * f) (#) ((#Z n) * cos)) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . ((n + 1) * x))) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:13 for n being Element of NAT for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) proof let n be Element of NAT ; ::_thesis: for Z being open Subset of REAL for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) let Z be open Subset of REAL; ::_thesis: for f being PartFunc of REAL,REAL st Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) holds ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) let f be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((sin * f) (#) ((#Z n) * cos)) & n >= 1 & ( for x being Real st x in Z holds f . x = n * x ) implies ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) ) assume that A1: Z c= dom ((sin * f) (#) ((#Z n) * cos)) and A2: n >= 1 and A3: for x being Real st x in Z holds f . x = n * x ; ::_thesis: ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) A4: for x being Real st x in Z holds f . x = (n * x) + 0 by A3; A5: Z c= (dom (sin * f)) /\ (dom ((#Z n) * cos)) by A1, VALUED_1:def_4; then A6: Z c= dom (sin * f) by XBOOLE_1:18; then for y being set st y in Z holds y in dom f by FUNCT_1:11; then A7: Z c= dom f by TARSKI:def_3; then A8: f is_differentiable_on Z by A4, FDIFF_1:23; 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 A9: f is_differentiable_in x by A8, FDIFF_1:9; sin is_differentiable_in f . x by SIN_COS:64; hence sin * f is_differentiable_in x by A9, FDIFF_2:13; ::_thesis: verum end; then A10: sin * f is_differentiable_on Z by A6, FDIFF_1:9; A11: for x being Real st x in Z holds ((sin * f) `| Z) . x = n * (cos . (n * x)) proof let x be Real; ::_thesis: ( x in Z implies ((sin * f) `| Z) . x = n * (cos . (n * x)) ) A12: sin is_differentiable_in f . x by SIN_COS:64; assume A13: x in Z ; ::_thesis: ((sin * f) `| Z) . x = n * (cos . (n * x)) then f is_differentiable_in x by A8, FDIFF_1:9; then diff ((sin * f),x) = (diff (sin,(f . x))) * (diff (f,x)) by A12, FDIFF_2:13 .= (cos . (f . x)) * (diff (f,x)) by SIN_COS:64 .= (cos . (n * x)) * (diff (f,x)) by A3, A13 .= (cos . (n * x)) * ((f `| Z) . x) by A8, A13, FDIFF_1:def_7 .= n * (cos . (n * x)) by A7, A4, A13, FDIFF_1:23 ; hence ((sin * f) `| Z) . x = n * (cos . (n * x)) by A10, A13, FDIFF_1:def_7; ::_thesis: verum end; A14: Z c= dom ((#Z n) * cos) by A5, XBOOLE_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (#Z_n)_*_cos_is_differentiable_in_x let x be Real; ::_thesis: ( x in Z implies (#Z n) * cos is_differentiable_in x ) assume x in Z ; ::_thesis: (#Z n) * cos is_differentiable_in x cos is_differentiable_in x by SIN_COS:63; hence (#Z n) * cos is_differentiable_in x by TAYLOR_1:3; ::_thesis: verum end; then A15: (#Z n) * cos is_differentiable_on Z by A14, FDIFF_1:9; A16: for x being Real st x in Z holds (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) proof let x be Real; ::_thesis: ( x in Z implies (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ) cos is_differentiable_in x by SIN_COS:63; then A17: diff (((#Z n) * cos),x) = (n * ((cos . x) #Z (n - 1))) * (diff (cos,x)) by TAYLOR_1:3 .= (n * ((cos . x) #Z (n - 1))) * (- (sin . x)) by SIN_COS:63 .= - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) ; assume x in Z ; ::_thesis: (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) hence (((#Z n) * cos) `| Z) . x = - ((n * ((cos . x) #Z (n - 1))) * (sin . x)) by A15, A17, FDIFF_1:def_7; ::_thesis: verum end; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ (((sin_*_f)_(#)_((#Z_n)_*_cos))_`|_Z)_._x_=_(n_*_((cos_._x)_#Z_(n_-_1)))_*_(cos_._((n_+_1)_*_x)) let x be Real; ::_thesis: ( x in Z implies (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) A18: n - 1 is Element of NAT by A2, NAT_1:21; assume A19: x in Z ; ::_thesis: (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) then (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = ((((#Z n) * cos) . x) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A1, A10, A15, FDIFF_1:21 .= (((#Z n) . (cos . x)) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A14, A19, FUNCT_1:12 .= (((cos . x) #Z n) * (diff ((sin * f),x))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by TAYLOR_1:def_1 .= (((cos . x) #Z n) * (((sin * f) `| Z) . x)) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A10, A19, FDIFF_1:def_7 .= (((cos . x) #Z n) * (n * (cos . (n * x)))) + (((sin * f) . x) * (diff (((#Z n) * cos),x))) by A11, A19 .= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (f . x)) * (diff (((#Z n) * cos),x))) by A6, A19, FUNCT_1:12 .= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (diff (((#Z n) * cos),x))) by A3, A19 .= (((cos . x) #Z n) * (n * (cos . (n * x)))) + ((sin . (n * x)) * ((((#Z n) * cos) `| Z) . x)) by A15, A19, FDIFF_1:def_7 .= (((cos . x) #Z ((n - 1) + 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A16, A19 .= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) + ((sin . (n * x)) * (- ((n * ((cos . x) #Z (n - 1))) * (sin . x)))) by A18, TAYLOR_1:1 .= ((((cos . x) #Z (n - 1)) * ((cos . x) #Z 1)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x)) .= ((((cos . x) #Z (n - 1)) * (cos . x)) * (n * (cos . (n * x)))) - ((((sin . (n * x)) * n) * ((cos . x) #Z (n - 1))) * (sin . x)) by PREPOWER:35 .= (n * ((cos . x) #Z (n - 1))) * (((cos . (n * x)) * (cos . x)) - ((sin . x) * (sin . (n * x)))) .= (n * ((cos . x) #Z (n - 1))) * (cos . (x + (n * x))) by SIN_COS:74 .= (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; hence (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ; ::_thesis: verum end; hence ( (sin * f) (#) ((#Z n) * cos) is_differentiable_on Z & ( for x being Real st x in Z holds (((sin * f) (#) ((#Z n) * cos)) `| Z) . x = (n * ((cos . x) #Z (n - 1))) * (cos . ((n + 1) * x)) ) ) by A1, A10, A15, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:14 for Z being open Subset of REAL st not 0 in Z & 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 = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & 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 = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) ) set f = id Z; assume that A1: not 0 in Z and 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 = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, Th4; A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; Z c= (dom ((id Z) ^)) /\ (dom sin) by A2, VALUED_1:def_4; then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((id_Z)_^)_(#)_sin)_`|_Z)_._x_=_((1_/_x)_*_(cos_._x))_-_((1_/_(x_^2))_*_(sin_._x)) let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) assume A6: x in Z ; ::_thesis: ((((id Z) ^) (#) sin) `| Z) . x = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) hence ((((id Z) ^) (#) sin) `| Z) . x = ((sin . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (sin,x))) by A2, A3, A4, FDIFF_1:21 .= ((sin . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (sin,x))) by A3, A6, FDIFF_1:def_7 .= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (sin,x))) by A1, A6, Th4 .= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (cos . x)) by SIN_COS:64 .= ((sin . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (cos . x)) by A5, A6, RFUNCT_1:def_2 .= ((sin . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (cos . x)) by A6, FUNCT_1:18 .= (- ((1 / (x ^2)) * (sin . x))) + ((1 / x) * (cos . x)) by XCMPLX_0:def_9 .= ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ; ::_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 = ((1 / x) * (cos . x)) - ((1 / (x ^2)) * (sin . x)) ) ) by A2, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:15 for Z being open Subset of REAL st not 0 in Z & 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 = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( not 0 in Z & 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 = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: 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 = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) A3: (id Z) ^ is_differentiable_on Z by A1, Th4; A4: cos is_differentiable_on Z by FDIFF_1:26, SIN_COS:67; Z c= (dom ((id Z) ^)) /\ (dom cos) by A2, VALUED_1:def_4; then A5: Z c= dom ((id Z) ^) by XBOOLE_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((id_Z)_^)_(#)_cos)_`|_Z)_._x_=_(-_((1_/_x)_*_(sin_._x)))_-_((1_/_(x_^2))_*_(cos_._x)) let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) assume A6: x in Z ; ::_thesis: ((((id Z) ^) (#) cos) `| Z) . x = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) hence ((((id Z) ^) (#) cos) `| Z) . x = ((cos . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (cos,x))) by A2, A3, A4, FDIFF_1:21 .= ((cos . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (cos,x))) by A3, A6, FDIFF_1:def_7 .= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (cos,x))) by A1, A6, Th4 .= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (- (sin . x))) by SIN_COS:63 .= ((cos . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (- (sin . x))) by A5, A6, RFUNCT_1:def_2 .= ((cos . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (- (sin . x))) by A6, FUNCT_1:18 .= (- ((1 / (x ^2)) * (cos . x))) + ((1 / x) * (- (sin . x))) by XCMPLX_0:def_9 .= (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . 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 = (- ((1 / x) * (sin . x))) - ((1 / (x ^2)) * (cos . x)) ) ) by A2, A3, A4, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:16 for Z being open Subset of REAL st Z c= dom (sin + (#R (1 / 2))) holds ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (sin + (#R (1 / 2))) implies ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) ) assume A1: Z c= dom (sin + (#R (1 / 2))) ; ::_thesis: ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) then Z c= (dom (#R (1 / 2))) /\ (dom sin) by VALUED_1:def_1; then A2: Z c= dom (#R (1 / 2)) by XBOOLE_1:18; then A3: #R (1 / 2) is_differentiable_on Z by Lm3; A4: sin is_differentiable_on Z by FDIFF_1:26, SIN_COS:68; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((sin_+_(#R_(1_/_2)))_`|_Z)_._x_=_(cos_._x)_+_((1_/_2)_*_(x_#R_(-_(1_/_2)))) let x be Real; ::_thesis: ( x in Z implies ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) assume A5: x in Z ; ::_thesis: ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) then ((sin + (#R (1 / 2))) `| Z) . x = (diff (sin,x)) + (diff ((#R (1 / 2)),x)) by A1, A3, A4, FDIFF_1:18 .= (cos . x) + (diff ((#R (1 / 2)),x)) by SIN_COS:64 .= (cos . x) + (((#R (1 / 2)) `| Z) . x) by A3, A5, FDIFF_1:def_7 .= (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) by A2, A5, Lm3 ; hence ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ; ::_thesis: verum end; hence ( sin + (#R (1 / 2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((sin + (#R (1 / 2))) `| Z) . x = (cos . x) + ((1 / 2) * (x #R (- (1 / 2)))) ) ) by A1, A3, A4, FDIFF_1:18; ::_thesis: verum end; theorem :: FDIFF_5:17 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) proof let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 holds ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) let g be PartFunc of REAL,REAL; ::_thesis: ( not 0 in Z & Z c= dom (g (#) (sin * ((id Z) ^))) & g = #Z 2 implies ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (g (#) (sin * ((id Z) ^))) and A3: g = #Z 2 ; ::_thesis: ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) A4: for x being Real st x in Z holds g is_differentiable_in x by A3, TAYLOR_1:2; A5: Z c= (dom g) /\ (dom (sin * ((id Z) ^))) by A2, VALUED_1:def_4; then Z c= dom g by XBOOLE_1:18; then A6: g is_differentiable_on Z by A4, FDIFF_1:9; A7: for x being Real st x in Z holds (g `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x ) assume A8: x in Z ; ::_thesis: (g `| Z) . x = 2 * x diff (g,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2 .= 2 * x by PREPOWER:35 ; hence (g `| Z) . x = 2 * x by A6, A8, FDIFF_1:def_7; ::_thesis: verum end; A9: sin * ((id Z) ^) is_differentiable_on Z by A1, Th5; A10: Z c= dom (sin * ((id Z) ^)) by A5, XBOOLE_1:18; then for y being set st y in Z holds y in dom ((id Z) ^) by FUNCT_1:11; then A11: Z c= dom ((id Z) ^) by TARSKI:def_3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((g_(#)_(sin_*_((id_Z)_^)))_`|_Z)_._x_=_((2_*_x)_*_(sin_._(1_/_x)))_-_(cos_._(1_/_x)) let x be Real; ::_thesis: ( x in Z implies ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) assume A12: x in Z ; ::_thesis: ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) then ((g (#) (sin * ((id Z) ^))) `| Z) . x = (((sin * ((id Z) ^)) . x) * (diff (g,x))) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A2, A9, A6, FDIFF_1:21 .= (((sin * ((id Z) ^)) . x) * ((g `| Z) . x)) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A6, A12, FDIFF_1:def_7 .= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((g . x) * (diff ((sin * ((id Z) ^)),x))) by A7, A12 .= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (diff ((sin * ((id Z) ^)),x))) by A3, TAYLOR_1:def_1 .= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (((sin * ((id Z) ^)) `| Z) . x)) by A9, A12, FDIFF_1:def_7 .= (((sin * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (- ((1 / (x ^2)) * (cos . (1 / x))))) by A1, A12, Th5 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x #Z (1 + 1)) * ((1 / (x ^2)) * (cos . (1 / x)))) .= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2)) * (cos . (1 / x)))) by TAYLOR_1:1 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * (x #Z 1)) * ((1 / (x ^2)) * (cos . (1 / x)))) by PREPOWER:35 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * x) * (((1 * 1) / (x * x)) * (cos . (1 / x)))) by PREPOWER:35 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((x * x) * (((1 / x) * (1 / x)) * (cos . (1 / x)))) by XCMPLX_1:102 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x * (1 / x)) * (x * (1 / x))) * (cos . (1 / x))) .= (((sin * ((id Z) ^)) . x) * (2 * x)) - (((x * (1 / x)) * 1) * (cos . (1 / x))) by A1, A12, XCMPLX_1:106 .= (((sin * ((id Z) ^)) . x) * (2 * x)) - ((1 * 1) * (cos . (1 / x))) by A1, A12, XCMPLX_1:106 .= ((sin . (((id Z) ^) . x)) * (2 * x)) - (cos . (1 / x)) by A10, A12, FUNCT_1:12 .= ((sin . (((id Z) . x) ")) * (2 * x)) - (cos . (1 / x)) by A11, A12, RFUNCT_1:def_2 .= ((sin . (1 * (x "))) * (2 * x)) - (cos . (1 / x)) by A12, FUNCT_1:18 .= ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) by XCMPLX_0:def_9 ; hence ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ; ::_thesis: verum end; hence ( g (#) (sin * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (sin * ((id Z) ^))) `| Z) . x = ((2 * x) * (sin . (1 / x))) - (cos . (1 / x)) ) ) by A2, A9, A6, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:18 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) proof let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 holds ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) let g be PartFunc of REAL,REAL; ::_thesis: ( not 0 in Z & Z c= dom (g (#) (cos * ((id Z) ^))) & g = #Z 2 implies ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) ) set f = id Z; assume that A1: not 0 in Z and A2: Z c= dom (g (#) (cos * ((id Z) ^))) and A3: g = #Z 2 ; ::_thesis: ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) A4: for x being Real st x in Z holds g is_differentiable_in x by A3, TAYLOR_1:2; A5: Z c= (dom g) /\ (dom (cos * ((id Z) ^))) by A2, VALUED_1:def_4; then A6: Z c= dom (cos * ((id Z) ^)) by XBOOLE_1:18; then A7: cos * ((id Z) ^) is_differentiable_on Z by A1, Th6; Z c= dom g by A5, XBOOLE_1:18; then A8: g is_differentiable_on Z by A4, FDIFF_1:9; A9: for x being Real st x in Z holds (g `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x ) assume A10: x in Z ; ::_thesis: (g `| Z) . x = 2 * x diff (g,x) = 2 * (x #Z (2 - 1)) by A3, TAYLOR_1:2 .= 2 * x by PREPOWER:35 ; hence (g `| Z) . x = 2 * x by A8, A10, FDIFF_1:def_7; ::_thesis: verum end; for y being set st y in Z holds y in dom ((id Z) ^) by A6, FUNCT_1:11; then A11: Z c= dom ((id Z) ^) by TARSKI:def_3; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((g_(#)_(cos_*_((id_Z)_^)))_`|_Z)_._x_=_((2_*_x)_*_(cos_._(1_/_x)))_+_(sin_._(1_/_x)) let x be Real; ::_thesis: ( x in Z implies ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) assume A12: x in Z ; ::_thesis: ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) then ((g (#) (cos * ((id Z) ^))) `| Z) . x = (((cos * ((id Z) ^)) . x) * (diff (g,x))) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A2, A7, A8, FDIFF_1:21 .= (((cos * ((id Z) ^)) . x) * ((g `| Z) . x)) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A8, A12, FDIFF_1:def_7 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((g . x) * (diff ((cos * ((id Z) ^)),x))) by A9, A12 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (diff ((cos * ((id Z) ^)),x))) by A3, TAYLOR_1:def_1 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z 2) * (((cos * ((id Z) ^)) `| Z) . x)) by A7, A12, FDIFF_1:def_7 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x #Z (1 + 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by A1, A6, A12, Th6 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x #Z 1) * (x #Z 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by TAYLOR_1:1 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * (x #Z 1)) * ((1 / (x ^2)) * (sin . (1 / x)))) by PREPOWER:35 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * x) * (((1 * 1) / (x * x)) * (sin . (1 / x)))) by PREPOWER:35 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((x * x) * (((1 / x) * (1 / x)) * (sin . (1 / x)))) by XCMPLX_1:102 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x * (1 / x)) * (x * (1 / x))) * (sin . (1 / x))) .= (((cos * ((id Z) ^)) . x) * (2 * x)) + (((x * (1 / x)) * 1) * (sin . (1 / x))) by A1, A12, XCMPLX_1:106 .= (((cos * ((id Z) ^)) . x) * (2 * x)) + ((1 * 1) * (sin . (1 / x))) by A1, A12, XCMPLX_1:106 .= ((cos . (((id Z) ^) . x)) * (2 * x)) + (sin . (1 / x)) by A6, A12, FUNCT_1:12 .= ((cos . (((id Z) . x) ")) * (2 * x)) + (sin . (1 / x)) by A11, A12, RFUNCT_1:def_2 .= ((cos . (1 * (x "))) * (2 * x)) + (sin . (1 / x)) by A12, FUNCT_1:18 .= ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) by XCMPLX_0:def_9 ; hence ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ; ::_thesis: verum end; hence ( g (#) (cos * ((id Z) ^)) is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) (cos * ((id Z) ^))) `| Z) . x = ((2 * x) * (cos . (1 / x))) + (sin . (1 / x)) ) ) by A2, A7, A8, FDIFF_1:21; ::_thesis: verum end; Lm5: for x being Real st x in dom ln holds x > 0 by TAYLOR_1:18, XXREAL_1:4; theorem Th19: :: FDIFF_5:19 for Z being open Subset of REAL st Z c= dom ln holds ( ln is_differentiable_on Z & ( for x being Real st x in Z holds (ln `| Z) . x = 1 / x ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ln implies ( ln is_differentiable_on Z & ( for x being Real st x in Z holds (ln `| Z) . x = 1 / x ) ) ) assume A1: Z c= dom ln ; ::_thesis: ( ln is_differentiable_on Z & ( for x being Real st x in Z holds (ln `| Z) . x = 1 / x ) ) then A2: for x being Real st x in Z holds ln is_differentiable_in x by Lm5, TAYLOR_1:18; then A3: ln is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds (ln `| Z) . x = 1 / x proof let x be Real; ::_thesis: ( x in Z implies (ln `| Z) . x = 1 / x ) assume A4: x in Z ; ::_thesis: (ln `| Z) . x = 1 / x then diff (ln,x) = 1 / x by A1, TAYLOR_1:18; hence (ln `| Z) . x = 1 / x by A3, A4, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln is_differentiable_on Z & ( for x being Real st x in Z holds (ln `| Z) . x = 1 / x ) ) by A1, A2, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_5:20 for Z being open Subset of REAL st Z c= dom ((id Z) (#) ln) holds ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom ((id Z) (#) ln) implies ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) ) set f = ln ; assume A1: Z c= dom ((id Z) (#) ln) ; ::_thesis: ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) then A2: Z c= (dom (id Z)) /\ (dom ln) by VALUED_1:def_4; then A3: Z c= dom (id Z) by XBOOLE_1:18; A4: for x being Real st x in Z holds (id Z) . x = (1 * x) + 0 by FUNCT_1:18; then A5: id Z is_differentiable_on Z by A3, FDIFF_1:23; A6: Z c= dom ln by A2, XBOOLE_1:18; then A7: ln is_differentiable_on Z by Th19; for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) proof let x be Real; ::_thesis: ( x in Z implies (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) assume A8: x in Z ; ::_thesis: (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) then A9: x <> 0 by A6, TAYLOR_1:18, XXREAL_1:4; (((id Z) (#) ln) `| Z) . x = (((id Z) . x) * (diff (ln,x))) + ((ln . x) * (diff ((id Z),x))) by A1, A5, A7, A8, FDIFF_1:21 .= (((id Z) . x) * ((ln `| Z) . x)) + ((ln . x) * (diff ((id Z),x))) by A7, A8, FDIFF_1:def_7 .= (((id Z) . x) * (1 / x)) + ((ln . x) * (diff ((id Z),x))) by A6, A8, Th19 .= (x * (1 / x)) + ((ln . x) * (diff ((id Z),x))) by A8, FUNCT_1:18 .= (x * (1 / x)) + ((ln . x) * (((id Z) `| Z) . x)) by A5, A8, FDIFF_1:def_7 .= (x * (1 / x)) + ((ln . x) * 1) by A3, A4, A8, FDIFF_1:23 .= 1 + (ln . x) by A9, XCMPLX_1:106 ; hence (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ; ::_thesis: verum end; hence ( (id Z) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds (((id Z) (#) ln) `| Z) . x = 1 + (ln . x) ) ) by A1, A5, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:21 for Z being open Subset of REAL for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds x > 0 ) holds ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: for g being PartFunc of REAL,REAL st Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds x > 0 ) holds ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) let g be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (g (#) ln) & g = #Z 2 & ( for x being Real st x in Z holds x > 0 ) implies ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) ) set f = ln ; assume that A1: Z c= dom (g (#) ln) and A2: g = #Z 2 and A3: for x being Real st x in Z holds x > 0 ; ::_thesis: ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) A4: for x being Real st x in Z holds g is_differentiable_in x by A2, TAYLOR_1:2; A5: Z c= (dom g) /\ (dom ln) by A1, VALUED_1:def_4; then A6: Z c= dom ln by XBOOLE_1:18; then A7: ln is_differentiable_on Z by Th19; Z c= dom g by A5, XBOOLE_1:18; then A8: g is_differentiable_on Z by A4, FDIFF_1:9; A9: for x being Real st x in Z holds (g `| Z) . x = 2 * x proof let x be Real; ::_thesis: ( x in Z implies (g `| Z) . x = 2 * x ) assume A10: x in Z ; ::_thesis: (g `| Z) . x = 2 * x diff (g,x) = 2 * (x #Z (2 - 1)) by A2, TAYLOR_1:2 .= 2 * x by PREPOWER:35 ; hence (g `| Z) . x = 2 * x by A8, A10, FDIFF_1:def_7; ::_thesis: verum end; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((g_(#)_ln)_`|_Z)_._x_=_x_+_((2_*_x)_*_(ln_._x)) let x be Real; ::_thesis: ( x in Z implies ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) assume A11: x in Z ; ::_thesis: ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) then A12: x <> 0 by A3; ((g (#) ln) `| Z) . x = ((g . x) * (diff (ln,x))) + ((ln . x) * (diff (g,x))) by A1, A8, A7, A11, FDIFF_1:21 .= ((g . x) * ((ln `| Z) . x)) + ((ln . x) * (diff (g,x))) by A7, A11, FDIFF_1:def_7 .= ((g . x) * (1 / x)) + ((ln . x) * (diff (g,x))) by A6, A11, Th19 .= ((x #Z 2) * (1 / x)) + ((ln . x) * (diff (g,x))) by A2, TAYLOR_1:def_1 .= ((x #Z 2) * (1 / x)) + ((ln . x) * ((g `| Z) . x)) by A8, A11, FDIFF_1:def_7 .= ((x #Z (1 + 1)) * (1 / x)) + ((2 * x) * (ln . x)) by A9, A11 .= (((x #Z 1) * (x #Z 1)) * (1 / x)) + ((2 * x) * (ln . x)) by TAYLOR_1:1 .= (((x #Z 1) * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35 .= ((x * x) * (1 / x)) + ((2 * x) * (ln . x)) by PREPOWER:35 .= (x * (x * (1 / x))) + ((2 * x) * (ln . x)) .= (x * 1) + ((2 * x) * (ln . x)) by A12, XCMPLX_1:106 .= x + ((2 * x) * (ln . x)) ; hence ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ; ::_thesis: verum end; hence ( g (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((g (#) ln) `| Z) . x = x + ((2 * x) * (ln . x)) ) ) by A1, A8, A7, FDIFF_1:21; ::_thesis: verum end; theorem Th22: :: FDIFF_5:22 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) / (f1 - f2)) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) holds ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 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) / (f1 - f2)) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) holds ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) holds ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom ((f1 + f2) / (f1 - f2)) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) implies ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) ) assume that A1: Z c= dom ((f1 + f2) / (f1 - f2)) and A2: for x being Real st x in Z holds f1 . x = a and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds (f1 - f2) . x > 0 ; ::_thesis: ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) A5: Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0})) by A1, RFUNCT_1:def_1; then A6: Z c= dom (f1 + f2) by XBOOLE_1:18; then A7: f1 + f2 is_differentiable_on Z by A2, A3, Lm1; A8: Z c= dom (f1 - f2) by A5, XBOOLE_1:1; then A9: f1 - f2 is_differentiable_on Z by A2, A3, Lm2; A10: for x being Real st x in Z holds (f1 - f2) . x <> 0 by A4; then A11: (f1 + f2) / (f1 - f2) is_differentiable_on Z by A7, A9, FDIFF_2:21; for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) proof let x be Real; ::_thesis: ( x in Z implies (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) assume A12: x in Z ; ::_thesis: (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) then A13: f1 . x = a by A2; A14: (f1 - f2) . x <> 0 by A4, A12; ( f1 + f2 is_differentiable_in x & f1 - f2 is_differentiable_in x ) by A7, A9, A12, FDIFF_1:9; then diff (((f1 + f2) / (f1 - f2)),x) = (((diff ((f1 + f2),x)) * ((f1 - f2) . x)) - ((diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2) by A14, FDIFF_2:14 .= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 + f2) . x))) / (((f1 - f2) . x) ^2) by A8, A12, VALUED_1:13 .= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 - f2) . x) ^2) by A6, A12, VALUED_1:def_1 .= (((diff ((f1 + f2),x)) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A8, A12, VALUED_1:13 .= (((((f1 + f2) `| Z) . x) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A7, A12, FDIFF_1:def_7 .= (((2 * x) * ((f1 . x) - (f2 . x))) - ((diff ((f1 - f2),x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A2, A3, A6, A12, Lm1 .= (((2 * x) * ((f1 . x) - (f2 . x))) - ((((f1 - f2) `| Z) . x) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A9, A12, FDIFF_1:def_7 .= (((2 * x) * ((f1 . x) - (f2 . x))) - ((- (2 * x)) * ((f1 . x) + (f2 . x)))) / (((f1 . x) - (f2 . x)) ^2) by A2, A3, A8, A12, Lm2 .= ((4 * x) * a) / ((a - (x #Z 2)) ^2) by A3, A13, TAYLOR_1:def_1 .= ((4 * x) * a) / ((a - (x |^ 2)) ^2) by PREPOWER:36 .= ((4 * x) * a) / (((a - (x |^ 2)) |^ 1) * (a - (x |^ 2))) by NEWTON:5 .= ((4 * x) * a) / ((a - (x |^ 2)) |^ (1 + 1)) by NEWTON:6 .= ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ; hence (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) by A11, A12, FDIFF_1:def_7; ::_thesis: verum end; hence ( (f1 + f2) / (f1 - f2) is_differentiable_on Z & ( for x being Real st x in Z holds (((f1 + f2) / (f1 - f2)) `| Z) . x = ((4 * a) * x) / ((a - (x |^ 2)) |^ 2) ) ) by A7, A9, A10, FDIFF_2:21; ::_thesis: verum end; theorem :: FDIFF_5: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) / (f1 - f2))) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds (f1 + f2) . x > 0 ) holds ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) 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) / (f1 - f2))) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds (f1 + f2) . x > 0 ) holds ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) let Z be open Subset of REAL; ::_thesis: for f1, f2 being PartFunc of REAL,REAL st Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds (f1 + f2) . x > 0 ) holds ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) let f1, f2 be PartFunc of REAL,REAL; ::_thesis: ( Z c= dom (ln * ((f1 + f2) / (f1 - f2))) & ( for x being Real st x in Z holds f1 . x = a ) & f2 = #Z 2 & ( for x being Real st x in Z holds (f1 - f2) . x > 0 ) & ( for x being Real st x in Z holds (f1 + f2) . x > 0 ) implies ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) ) assume that A1: Z c= dom (ln * ((f1 + f2) / (f1 - f2))) and A2: for x being Real st x in Z holds f1 . x = a and A3: f2 = #Z 2 and A4: for x being Real st x in Z holds (f1 - f2) . x > 0 and A5: for x being Real st x in Z holds (f1 + f2) . x > 0 ; ::_thesis: ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) for y being set st y in Z holds y in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11; then A6: Z c= dom ((f1 + f2) / (f1 - f2)) by TARSKI:def_3; then A7: (f1 + f2) / (f1 - f2) is_differentiable_on Z by A2, A3, A4, Th22; A8: Z c= (dom (f1 + f2)) /\ ((dom (f1 - f2)) \ ((f1 - f2) " {0})) by A6, RFUNCT_1:def_1; then A9: Z c= dom (f1 + f2) by XBOOLE_1:18; A10: Z c= dom (f1 - f2) by A8, XBOOLE_1:1; A11: for x being Real st x in Z holds ((f1 + f2) / (f1 - f2)) . x > 0 proof let x be Real; ::_thesis: ( x in Z implies ((f1 + f2) / (f1 - f2)) . x > 0 ) assume A12: x in Z ; ::_thesis: ((f1 + f2) / (f1 - f2)) . x > 0 then x in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11; then A13: ((f1 + f2) / (f1 - f2)) . x = ((f1 + f2) . x) * (((f1 - f2) . x) ") by RFUNCT_1:def_1 .= ((f1 + f2) . x) / ((f1 - f2) . x) by XCMPLX_0:def_9 ; ( (f1 + f2) . x > 0 & (f1 - f2) . x > 0 ) by A4, A5, A12; hence ((f1 + f2) / (f1 - f2)) . x > 0 by A13, XREAL_1:139; ::_thesis: verum end; A14: for x being Real st x in Z holds ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x proof let x be Real; ::_thesis: ( x in Z implies ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x ) assume x in Z ; ::_thesis: ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x then ( (f1 + f2) / (f1 - f2) is_differentiable_in x & ((f1 + f2) / (f1 - f2)) . x > 0 ) by A7, A11, FDIFF_1:9; hence ln * ((f1 + f2) / (f1 - f2)) is_differentiable_in x by TAYLOR_1:20; ::_thesis: verum end; then A15: ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z by A1, FDIFF_1:9; for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) proof let x be Real; ::_thesis: ( x in Z implies ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) assume A16: x in Z ; ::_thesis: ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) then A17: x in dom ((f1 + f2) / (f1 - f2)) by A1, FUNCT_1:11; A18: (f1 - f2) . x <> 0 by A4, A16; A19: f1 . x = a by A2, A16; ( (f1 + f2) / (f1 - f2) is_differentiable_in x & ((f1 + f2) / (f1 - f2)) . x > 0 ) by A7, A11, A16, FDIFF_1:9; then diff ((ln * ((f1 + f2) / (f1 - f2))),x) = (diff (((f1 + f2) / (f1 - f2)),x)) / (((f1 + f2) / (f1 - f2)) . x) by TAYLOR_1:20 .= ((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) / (f1 - f2)) . x) by A7, A16, FDIFF_1:def_7 .= ((((f1 + f2) / (f1 - f2)) `| Z) . x) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A17, RFUNCT_1:def_1 .= (((4 * a) * x) / (((f1 . x) - (x |^ 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A2, A3, A4, A6, A16, A19, Th22 .= (((4 * a) * x) / (((f1 . x) - (x #Z 2)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by PREPOWER:36 .= (((4 * a) * x) / (((f1 . x) - (f2 . x)) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A3, TAYLOR_1:def_1 .= (((4 * a) * x) / (((f1 - f2) . x) |^ 2)) / (((f1 + f2) . x) * (((f1 - f2) . x) ")) by A10, A16, VALUED_1:13 .= (((4 * a) * x) / (((f1 - f2) . x) |^ (1 + 1))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by XCMPLX_0:def_9 .= (((4 * a) * x) / ((((f1 - f2) . x) |^ 1) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by NEWTON:6 .= (((4 * a) * x) / (((f1 - f2) . x) * ((f1 - f2) . x))) / (((f1 + f2) . x) / ((f1 - f2) . x)) by NEWTON:5 .= ((((4 * a) * x) / ((f1 - f2) . x)) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x)) by XCMPLX_1:78 .= ((((4 * a) * x) / ((f1 - f2) . x)) / (((f1 + f2) . x) / ((f1 - f2) . x))) / ((f1 - f2) . x) by XCMPLX_1:48 .= (((4 * a) * x) / ((f1 + f2) . x)) / ((f1 - f2) . x) by A18, XCMPLX_1:55 .= ((4 * a) * x) / (((f1 + f2) . x) * ((f1 - f2) . x)) by XCMPLX_1:78 .= ((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 - f2) . x)) by A9, A16, VALUED_1:def_1 .= ((4 * a) * x) / (((f1 . x) + (f2 . x)) * ((f1 . x) - (f2 . x))) by A10, A16, VALUED_1:13 .= ((4 * a) * x) / ((a * a) - ((f2 . x) * (f2 . x))) by A19 .= ((4 * a) * x) / ((a * a) - ((x #Z 2) * (f2 . x))) by A3, TAYLOR_1:def_1 .= ((4 * a) * x) / ((a * a) - ((x #Z 2) * (x #Z 2))) by A3, TAYLOR_1:def_1 .= ((4 * a) * x) / (((a |^ 1) * a) - ((x #Z 2) * (x #Z 2))) by NEWTON:5 .= ((4 * a) * x) / ((a |^ (1 + 1)) - ((x #Z 2) * (x #Z 2))) by NEWTON:6 .= ((4 * a) * x) / ((a |^ (1 + 1)) - ((x |^ 2) * (x #Z 2))) by PREPOWER:36 .= ((4 * a) * x) / ((a |^ 2) - ((x |^ 2) * (x |^ 2))) by PREPOWER:36 .= ((4 * a) * x) / ((a |^ 2) - (x |^ (2 + 2))) by NEWTON:8 .= ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ; hence ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) by A15, A16, FDIFF_1:def_7; ::_thesis: verum end; hence ( ln * ((f1 + f2) / (f1 - f2)) is_differentiable_on Z & ( for x being Real st x in Z holds ((ln * ((f1 + f2) / (f1 - f2))) `| Z) . x = ((4 * a) * x) / ((a |^ 2) - (x |^ 4)) ) ) by A1, A14, FDIFF_1:9; ::_thesis: verum end; theorem :: FDIFF_5:24 for Z being open Subset of REAL st Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds x > 0 ) holds ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (((id Z) ^) (#) ln) & ( for x being Real st x in Z holds x > 0 ) implies ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) ) set f = id Z; set g = ln ; assume that A1: Z c= dom (((id Z) ^) (#) ln) and A2: for x being Real st x in Z holds x > 0 ; ::_thesis: ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) A3: not 0 in Z by A2; then A4: (id Z) ^ is_differentiable_on Z by Th4; A5: Z c= (dom ((id Z) ^)) /\ (dom ln) by A1, VALUED_1:def_4; then A6: Z c= dom ln by XBOOLE_1:18; then A7: ln is_differentiable_on Z by Th19; A8: Z c= dom ((id Z) ^) by A5, XBOOLE_1:18; now__::_thesis:_for_x_being_Real_st_x_in_Z_holds_ ((((id_Z)_^)_(#)_ln)_`|_Z)_._x_=_(1_/_(x_^2))_*_(1_-_(ln_._x)) let x be Real; ::_thesis: ( x in Z implies ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) assume A9: x in Z ; ::_thesis: ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) then ((((id Z) ^) (#) ln) `| Z) . x = ((ln . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff (ln,x))) by A1, A4, A7, FDIFF_1:21 .= ((ln . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff (ln,x))) by A4, A9, FDIFF_1:def_7 .= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff (ln,x))) by A3, A9, Th4 .= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * ((ln `| Z) . x)) by A7, A9, FDIFF_1:def_7 .= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (1 / x)) by A6, A9, Th19 .= ((ln . x) * (- (1 / (x ^2)))) + ((((id Z) . x) ") * (1 / x)) by A8, A9, RFUNCT_1:def_2 .= ((ln . x) * (- (1 / (x ^2)))) + ((1 * (x ")) * (1 / x)) by A9, FUNCT_1:18 .= (- ((1 / (x ^2)) * (ln . x))) + ((1 / x) * (1 / x)) by XCMPLX_0:def_9 .= (- ((1 / (x ^2)) * (ln . x))) + (1 / (x ^2)) by XCMPLX_1:102 .= (1 / (x ^2)) * (1 - (ln . x)) ; hence ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ; ::_thesis: verum end; hence ( ((id Z) ^) (#) ln is_differentiable_on Z & ( for x being Real st x in Z holds ((((id Z) ^) (#) ln) `| Z) . x = (1 / (x ^2)) * (1 - (ln . x)) ) ) by A1, A4, A7, FDIFF_1:21; ::_thesis: verum end; theorem :: FDIFF_5:25 for Z being open Subset of REAL st Z c= dom (ln ^) & ( for x being Real st x in Z holds ln . x <> 0 ) holds ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) proof let Z be open Subset of REAL; ::_thesis: ( Z c= dom (ln ^) & ( for x being Real st x in Z holds ln . x <> 0 ) implies ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) ) set f = ln ; assume that A1: Z c= dom (ln ^) and A2: for x being Real st x in Z holds ln . x <> 0 ; ::_thesis: ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) dom (ln ^) c= dom ln by RFUNCT_1:1; then A3: Z c= dom ln by A1, XBOOLE_1:1; then A4: ln is_differentiable_on Z by Th19; then A5: ln ^ is_differentiable_on Z by A2, FDIFF_2:22; for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) proof let x be Real; ::_thesis: ( x in Z implies ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) assume A6: x in Z ; ::_thesis: ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) then A7: ( ln . x <> 0 & ln is_differentiable_in x ) by A2, A4, FDIFF_1:9; ((ln ^) `| Z) . x = diff ((ln ^),x) by A5, A6, FDIFF_1:def_7 .= - ((diff (ln,x)) / ((ln . x) ^2)) by A7, FDIFF_2:15 .= - (((ln `| Z) . x) / ((ln . x) ^2)) by A4, A6, FDIFF_1:def_7 .= - ((1 / x) / ((ln . x) ^2)) by A3, A6, Th19 .= - (1 / (x * ((ln . x) ^2))) by XCMPLX_1:78 ; hence ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ; ::_thesis: verum end; hence ( ln ^ is_differentiable_on Z & ( for x being Real st x in Z holds ((ln ^) `| Z) . x = - (1 / (x * ((ln . x) ^2))) ) ) by A2, A4, FDIFF_2:22; ::_thesis: verum end;